Skip to content

Instantly share code, notes, and snippets.

@EduardoRFS

EduardoRFS/torrens.md

Created March 7, 2023 20:35
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save EduardoRFS/a92ea4bf0ac9a7bc440f2537a7b158ed to your computer and use it in GitHub Desktop.
Save EduardoRFS/a92ea4bf0ac9a7bc440f2537a7b158ed to your computer and use it in GitHub Desktop.
Download ZIP
Raw
torrens.md 
((Bool,
  true : Bool,
  false : Bool,
  case : (b : Bool) -> (A : Type) -> A -> A -> A
) => M)(
  (A : Type) -> A -> A -> A,
  A => x => y => x,
  A => x => y => y,
  b => A => x => y => b A x y
)
// isomorphic
((Bool,
  true : Bool,
  false : Bool,
  case : (b : Bool) -> (A : Type) -> A -> A -> A
) => M)(
  (A : Type) -> A -> A -> A,
  A => x => y => y,
  A => x => y => x,
  b => A => x => y => b A y x
)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment