invS1 (x:S1) : S1 = invMult x base
-lemInvS1 : Path S1 (invS1 base) base = <i> comp (<_>S1) (comp (<_>S1) base [(i=1) -> refl S1 base]) [(i=1) -> refl S1 base]
+lemInvS1 : Path S1 (invS1 base) base =
+ <i> comp (<_>S1) (comp (<_>S1) base [(i=1) -> refl S1 base]) [(i=1) -> refl S1 base]
loopInvS1 : U = Path S1 (invS1 base) (invS1 base)
+-- Two definitions of injectivity and proof that they can be
+-- identified
module injective where
-import prop
+import equiv
-- First definition of injectivity, informally: if two elements f a0, f a1 are
-- equal in B, then a0, a1 must be equal in A.
Path U (inj0 A B f sA sB) (inj1 A B f sA sB)
= propPath (inj0 A B f sA sB) (inj1 A B f sA sB)
(inj01 A B f sA sB) (inj10 A B f sA sB)
- (prop_inj0 A B f sA sB) (prop_inj1 A B f sA sB)
\ No newline at end of file
+ (prop_inj0 A B f sA sB) (prop_inj1 A B f sA sB)
+-- The integers as nat + nat with proof that suc is an iso giving a\r
+-- non-trivial path from Z to Z\r
module int where\r
\r
import equiv\r
+-- The integers as a HIT (identifying +0 with -0). Proof that this
+-- representation is isomorphic to the one in int.ctt
module integer where
import int
+-- The interval as a HIT. Proof of funtion extensionality from it.
module interval where
-import gradLemma
import equiv
-
-data I = zero | one | seg <i> [(i = 0) -> zero, (i = 1) -> one]
+data I = zero
+ | one
+ | seg <i> [ (i = 0) -> zero
+ , (i = 1) -> one ]
-- Proof of funext from the interval
fext (A B : U) (f g : A -> B) (p : (x : A) -> Path B (f x) (g x)) :
+-- Lists
module list where
import prelude
-data list (A : U) = nil | cons (a : A) (as : list A)
+data list (A : U) = nil
+ | cons (a : A) (as : list A)
append (A : U) : list A -> list A -> list A = split
nil -> idfun (list A)
+-- Natural numbers
module nat where
import bool
+-- Ordinals
module ordinal where
import prelude
+-- Characterization of equality in pi types.
module pi where
import equiv
+-- The prelude. Definition of Path types and basic operations on them
+-- (refl, mapOnPath, funExt...). Definition of prop, set and
+-- groupoid. Some basic data types (empty, unit, or, and).
module prelude where
-- Identity types
+-- Propositional truncation as a HIT. (WARNING: not working correctly)
module propTrunc where
import prelude
+-- Definition of retract and section\r
module retract where\r
\r
import prelude\r
+-- Various results about sigma types.
module sigma where
import equiv
+-- Two definitions of a subset and a proof that they are equal.
module subset where
import injective
-- Show that we can identify the two definitions of subsets with each other
subsetPath (A : U) (sA : set A) : Path U (subset0 A sA) (subset1 A sA)
= isoPath (subset0 A sA) (subset1 A sA) (subset01 A sA) (subset10 A sA)
- (subsetIso1 A sA) (subsetIso0 A sA)
\ No newline at end of file
+ (subsetIso1 A sA) (subsetIso0 A sA)
+-- Suspension. Definition of the circle as the suspension of bool and\r
+-- a proof that this is equal to the standard HIT representation of\r
+-- the circle.\r
module susp where\r
\r
import circle\r
\r
data susp (A : U) = north\r
| south\r
- | merid (a:A) <i> [(i=0) -> north, (i=1) -> south]\r
+ | merid (a : A) <i> [ (i=0) -> north\r
+ , (i=1) -> south ]\r
\r
-- n-spheres\r
sphere : nat -> U = split\r
+-- Torsors. Proof that S1 is equal to BZ, the classifying space of Z.\r
module torsor where\r
-import prelude\r
+\r
import int\r
-import circle\r
import helix\r
-import univalence\r
\r
--\r
\r
-- This file contains two proofs of the univalence axiom. One using
-- unglue (section 7.2) and a direct one (appendix B of the cubicaltt
-- paper). The normal form of the first proof can be computed (and
--- typecheck, see nthmUniv) while the second one uses very much memory
--- and don't terminate in reasonable time.
+-- typechecked) while the second one uses very much memory and don't
+-- terminate in reasonable time.
module univalence where
import retract
module multS1 where
-import circle
-
--- another inverse function
-
--- the multiplication is invertible
-
-lemPropFib (P:S1 -> U) (pP:(x:S1) -> prop (P x)) (bP: P base) : (x:S1) -> P x = split
- base -> bP
- loop @ i -> (lemPropF S1 P pP base base loop1 bP bP) @ i
-
-idL : (x : S1) -> Path S1 (mult base x) x = split
- base -> refl S1 base
- loop @ i -> <j> loop1 @ i
-
-multIsEquiv : (x:S1) -> isEquiv S1 S1 (mult x) = lemPropFib P pP bP
- where P (x:S1) : U = isEquiv S1 S1 (mult x)
- pP (x:S1) : prop (P x) = propIsEquiv S1 S1 (mult x)
- rem : Path (S1 -> S1) (idfun S1) (mult base) = <i>\ (x:S1) -> idL x @ -i
- bP : P base = subst (S1->S1) (isEquiv S1 S1) (idfun S1) (mult base) rem (idIsEquiv S1)
-
--- inverse of multiplication by x
-
-invMult (x y:S1) : S1 = (multIsEquiv x y).1.1
-
-invS1 (x:S1) : S1 = invMult x base
+import helix
pt0 : S1 = mapOnPath S1 S1 invS1 base base loop2@0
test1 : S1 = mapOnPath S1 S1 invS1 base base loop2@1
+-- Experimental implementation of quotient HIT (not finished)
module quotient where
-import prelude
import circle
-- Quotient A by R
projects / cubicaltt.git / commitdiff