Created
April 18, 2025 20:37
-
-
Save kory33/6c6d697fd54dff2fca4041859b48bf82 to your computer and use it in GitHub Desktop.
E.Rijke Introduction to Homotopy Type Theory, Ex4.3 in Scala
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| scalaVersion := "3.6.1" | |
| libraryDependencies ++= Seq() | |
| scalacOptions ++= Seq( | |
| "-deprecation", | |
| "-encoding", | |
| "UTF-8", | |
| "-feature", | |
| "-unchecked", | |
| "-Ypartial-unification", | |
| "-Ykind-projector:underscores" | |
| ) |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| type Not[A] = A => Nothing | |
| type ~[A] = Not[A] | |
| infix type ×[A, B] = (A, B) | |
| infix type +[A, B] = Either[A, B] | |
| infix type ↔[A, B] = (A => B) × (B => A) | |
| def a_i[P]: ~[P × ~[P]] = p_np => { | |
| val (p, np) = p_np | |
| np(p) | |
| } | |
| def a_ii[P]: ~[P ↔ ~[P]] = { impls => | |
| val (forward, backward) = impls | |
| val np: ~[P] = p => forward(p)(p) | |
| val p: P = backward(np) | |
| np(p) // = forward(p)(p)(backward(np)) | |
| } | |
| def b_i[P]: P => ~[~[P]] = p => np => np(p) | |
| def b_ii[P, Q]: (P => Q) => (~[~[P]] => ~[~[Q]]) = { f => notnotp => notq => | |
| val notp: ~[P] = p => notq(f(p)) | |
| notnotp(notp) // = notnotp(p => notq(f(p))) | |
| } | |
| def b_iii[P, Q]: (P => ~[~[Q]]) => (~[~[P]] => ~[~[Q]]) = { | |
| f => notnotp => notq => | |
| val notp: ~[P] = p => f(p)(notq) | |
| notnotp(notp) // = notnotp(p => f(p)(notq)) | |
| } | |
| type DN[P] = ~[~[P]] | |
| def dn_pure[P]: P => DN[P] = b_i | |
| def dn_map[P, Q]: DN[P] => (P => Q) => DN[Q] = dnp => ptoq => b_ii(ptoq)(dnp) | |
| def dn_flatMap[P, Q]: DN[P] => (P => DN[Q]) => DN[Q] = dnp => f => b_iii(f)(dnp) | |
| def dn_flatten[P]: DN[DN[P]] => DN[P] = dn_flatMap[DN[P], P](_)(dnp => dnp) | |
| def dn_ap[P, Q]: DN[P] => DN[P => Q] => DN[Q] = { dnp => dnpq => | |
| dn_flatMap(dnp)(p => dn_map(dnpq)(pq => pq(p))) | |
| } | |
| // some intuitive lemmas | |
| def not_bot: ~[Nothing] = n => n | |
| def notnotnot_bot: ~[~[~[Nothing]]] = dn_pure(not_bot) | |
| def contrapose[P, Q]: (P => Q) => (~[Q] => ~[P]) = { ptoq => notq => p => | |
| notq(ptoq(p)) | |
| } | |
| def c_i[P]: DN[DN[P] => P] = { not_dnptop => | |
| not_dnptop(dnp => dnp(p => not_dnptop(_ => p))) | |
| } | |
| def c_ii[P, Q]: DN[((P => Q) => P) => P] = { not_peirce_law => | |
| not_peirce_law { ptoq_top => | |
| ptoq_top { p => | |
| not_peirce_law(_ => p) | |
| } | |
| } | |
| } | |
| def c_iii[P, Q]: DN[(P => Q) + (Q => P)] = { not_dummett => | |
| not_dummett(Left(p => not_dummett(Right(_ => p)))) | |
| } | |
| def c_iv[P]: DN[P + ~[P]] = dn_flatMap(c_iii[P, ~[P]]) { | |
| case Left(ptonotp) => dn_map(dn_pure((p: P) => ptonotp(p)(p)))(Right(_)) | |
| case Right(notptop) => dn_map((notp: ~[P]) => notp(notptop(notp)))(Left(_)) | |
| } | |
| def dn_lem[P]: DN[P + ~[P]] = c_iv[P] | |
| def d_i[P]: (P + ~[P]) => (DN[P] => P) = { lem => notnotp => | |
| lem match { | |
| case Left(p) => p | |
| case Right(np) => notnotp(np) | |
| } | |
| } | |
| def d_ii[P, Q]: DN[Q => P] ↔ ((P + ~[P]) => (Q => P)) = | |
| ( | |
| { notnot_qtop => lem => q => | |
| lem match { | |
| case Left(p) => p | |
| case Right(np) => notnot_qtop { qtop => np(qtop(q)) } // "impossible" | |
| } | |
| }, | |
| { lem_to_qtop => not_qtop => | |
| notnotnot_bot { | |
| dn_flatMap(c_iv[P]) { lem => | |
| not_qtop(lem_to_qtop(lem)) | |
| } | |
| } | |
| } | |
| ) | |
| def e_i[P]: ~[DN[P]] => ~[P] = contrapose(dn_pure) | |
| def e_ii[P, Q]: DN[P => DN[Q]] => (P => DN[Q]) = { dn_ptodnq => p => | |
| dn_flatMap(dn_ptodnq) { ptodnq => ptodnq(p) } | |
| } | |
| def e_iii[P, Q]: DN[DN[P] × DN[Q]] => (DN[P] × DN[Q]) = { dn_dnpdnq => | |
| ( | |
| dn_flatMap(dn_dnpdnq)((dnp, _) => dnp), | |
| dn_flatMap(dn_dnpdnq)((_, dnq) => dnq) | |
| ) | |
| } | |
| def f_i[P, Q]: DN[P × Q] ↔ (DN[P] × DN[Q]) = ( | |
| dnpq => e_iii(dn_map(dnpq)((p, q) => (dn_pure(p), dn_pure(q)))), | |
| (dnp, dnq) => | |
| dn_flatMap(dnp) { p => | |
| dn_map(dnq) { q => | |
| (p, q) | |
| } | |
| } | |
| ) | |
| def f_ii[P, Q]: DN[P + Q] ↔ ~[~[P] × ~[Q]] = ( | |
| contrapose { (notp, notq) => porq => | |
| porq match { | |
| case Left(p) => notp(p) | |
| case Right(q) => notq(q) | |
| } | |
| }, | |
| not_notpnotq => { | |
| dn_flatMap(dn_lem[P]) { lem_p => | |
| dn_flatMap(dn_lem[Q]) { lem_q => | |
| (lem_p, lem_q) match { | |
| case (Left(p), _) => dn_pure(Left(p)) | |
| case (_, Left(q)) => dn_pure(Right(q)) | |
| case (Right(notp), Right(notq)) => not_notpnotq(notp, notq) | |
| } | |
| } | |
| } | |
| } | |
| ) | |
| def f_iii[P, Q]: DN[P => Q] ↔ (DN[P] => DN[Q]) = | |
| ( | |
| // ~[~[P => Q]] => (~[~[P]] => ~[~[Q]]) | |
| { dn_ptoq => dnp => | |
| dn_flatMap(dnp)(p => dn_map(dn_ptoq)(ptoq => ptoq(p))) | |
| }, | |
| // (~[~[P]] => ~[~[Q]]) => ~[~[P => Q]] | |
| { dnp_to_dnq => not_ptoq => | |
| not_ptoq { p => | |
| dnp_to_dnq(notp => notp(p))(q => not_ptoq(_ => q)) | |
| } | |
| } | |
| ) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment