From: Anders Mörtberg Date: Thu, 20 Oct 2016 20:33:03 +0000 (-0400) Subject: remove examples/aim.ctt as it is subsumed by examples/demo.ctt X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=749ec9f4e39197540f739e8a0b57ea7a981d9f0e;p=cubicaltt.git remove examples/aim.ctt as it is subsumed by examples/demo.ctt --- diff --git a/examples/aim.ctt b/examples/aim.ctt deleted file mode 100644 index d308cee..0000000 --- a/examples/aim.ctt +++ /dev/null @@ -1,825 +0,0 @@ --- Talk given by Anders Mörtberg at AIMXXI: --- http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.AIMXXI -module aim where - -{- - cubicaltt: Cubical type theory --------------------------------------------------------------------------- - (j.w.w. Cyril Cohen, Thierry Coquand, Simon Huber) - -Experimental implementation of a type theory in which the user can -directly manipulate n-dimensional cubes. It is based on a model of -type theory in cubical sets with connections. The goal is to have a -type theory with well behaved identity types and to give a -computational interpretation of notions from UF/HoTT, in particular -the univalence axiom and higher inductive types. - -The system is based on Mini-TT: "A simple type-theoretic language: -Mini-TT" by Thierry Coquand, Yoshiki Kinoshita, Bengt Nordström and -Makoto Takeya. - -Mini-TT is a variant Martin-Löf type theory with data -types. cubiclaltt extends Mini-TT with: - - o Name abstraction and application - o Compositions - o Isomorphisms can be transformed into equalities - o Some higher inductive types - - -Try it: https://github.com/mortberg/cubicaltt - - --} - - ------------------------------------------ - -- Some examples of programs in Mini-TT -- - ------------------------------------------ - --- The identity function: -idfun (A : U) (a : A) : A = a - --- The booleans: -data bool = false - | true - -not : bool -> bool = split - false -> true - true -> false - -{- - Path types, names and formulas --------------------------------------------------------------------------- - -An element in ID A B is a line in the universe connecting A and B: - - - |- A Type |- B Type - ------------------------------ - |- ID A B Type - - -PathP is heterogeneous equality: - - - |- P : ID A B |- a : A |- b : B - ----------------------------------------------- - |- PathP P a b Type - --} - --- The constant Path type can be seen a special case of PathP: -Path (A : U) (a b : A) : U = PathP ( A) a b - --- "" abstracts the name/color/dimension i: -refl (A : U) (a : A) : Path A a a = a - -{- - -A proof "p : Path A a b" is thought of as a line between a and b: - - p - a ------> b - - -A proof "sq : Path (Path A a b) p q" is thought of as a square between p and q: - - - q - a ------> b - ^ ^ - | sq | - | | - a ------> b - p - - -And so on... - --} - - --- It is possible to take the face of a path to obtain its endpoints: -face0 (A : U) (a b : A) (p : Path A a b) : Path A a a = refl A (p @ 0) -face1 (A : U) (a b : A) (p : Path A a b) : Path A b b = refl A (p @ 1) - - --- By applying a path to a name i, "p @ i", it is seen as a path "in --- dimension i" connecting "p @ 0" to "p @ 1". This way we get a --- simple proof of cong: -cong (A B : U) (f : A -> B) (a b : A) (p : Path A a b) : Path B (f a) (f b) = - f (p @ i) - --- This also gives a short proof of function extensionality: -funExt (A : U) (B : A -> U) (f g : (x : A) -> B x) - (p : (x : A) -> Path (B x) (f x) (g x)) : Path ((y : A) -> B y) f g = - \(x : A) -> (p x) @ i - -{- - -To see that the definition of funExt makes sense we can compute its -faces: - -funExt @ 0 = \(a : A) -> (p a) @ 0 - = \(a : A) -> f a - = f - -The last equality holds because of eta. - --} - - -{- - -Paths can be applied to formulas in the free distributive lattice -generated by names i,j,k... and negated names -i,-j,-k... - -A grammar for formulas is: - -name := i,j,k... - -formula := formula /\ formula - | formula \/ formula - | name - | - name - | 0 - | 1 - -An intuition is that the names range between [0,1] and that i /\ j is -min(i,j), i \/ j is max(i,j) and -i is 1 - i. - --} - --- Applying a path to a negated name inverts it: -sym (A : U) (a b : A) (p : Path A a b) : Path A b a = p @ -i - --- This operation is an involution: -symK (A : U) (a b : A) (p : Path A a b) : Path (Path A a b) p p = - refl (Path A a b) (sym A b a (sym A a b p)) - - -{- Connections: - -Applying a path to a conjunction: - - - p @ i - a ----------------> b - ^ ^ - | | - | | - p @ 0 | p @ i /\ j | p @ j - | | - | | - | | - a ----------------> a - p @ 0 - - - -And a disjunction gives: - - p @ 1 - b ----------------> b - ^ ^ - | | - | | - p @ j | p @ i \/ j | p @ 1 - | | - | | - | | - a ----------------> b - p @ i - --} - - --- This gives a simple proof that singletons are contractible: - -singl (A : U) (a : A) : U = (x : A) * Path A a x - -contrSingl (A : U) (a b : A) (p : Path A a b) : - Path (singl A a) (a,refl A a) (b,p) = - (p @ i, p @ i /\ j) - - -{- - -Note that formulas does not form a boolean algebra, but a de Morgan -algebra. This means that "p @ 0" and "p @ i /\ -i" are different! - -testDeMorganAlgebra (A : U) (a b : A) (p : Path A a b) : - Path (Path A a a) (<_> p @ 0) (<_> p @ 0) = - refl (Path A a a) ( p @ i /\ -i) - -This is clear with the intuition that /\ correspond to min. More about -this later... - --} - -testConj (A : U) (a b : A) (p : Path A a b) : Path A a a = p @ i /\ -i -testDisj (A : U) (a b : A) (p : Path A a b) : Path A b b = p @ i \/ -i - - - -{- - -So far we have: MLTT + Path, , @, i/\j... - -We can prove that singletons are contractible. But, we don't have -transport: - -transportf (A : U) (P : A -> U) (a b : A) (p : Path A a b) : P a -> P b - -Which is what is needed to get J as: - - J = contr. singl. + transport - -In order to get this (and a lot more) we consider compositions. - --} - - - - - - -{- - Compositions ------------------------------------------------------------------------- - -The comp operation takes a line in the universe, a principal side and -a system describing the rest of the shape, and produces the missing -side (opposite of the principal side). - - -Transitivity of Path is obtained from a composition of this open square: - -i : I, j : I |- - - a - - - - - - - - > c - ^ ^ - | | - | | - (<_> a)@j| | q @ j - | | - | | - | | - a ----------------> b - p @ i - -The composition computes the dashed line at the top of the square. - ( (<_>a)@i ) = ( (<_>a)@j) : Path (Path A a a) ( a) ( a) - -p = p @ i - -i : I |- (<_>a) @i -|- (<_> a) @ i -|- <_> a --} - - -pathscomp0 (A : U) (a b c : A) (p : Path A a b) (q : Path A b c) : Path A a c = - comp (<_> A) (p @ i) [ (i = 0) -> <_> a - , (i = 1) -> q ] - - --- The first two nonzero h-levels are propositions and sets: -prop (A : U) : U = (a b : A) -> Path A a b -set (A : U) : U = (a b : A) -> prop (Path A a b) - --- Using compositions we get a short proof that any prop is a set. To --- understand this proof one should draw an open cube with the back --- face being a constant square in a and the sides given by the system --- below. -propSet (A : U) (h : prop A) : set A = - \(a b : A) (p q : Path A a b) -> - comp (<_> A) a [ (j=0) -> h a a - , (j=1) -> h a b - , (i=0) -> h a (p @ j) - , (i=1) -> h a (q @ j)] - --- From this we get a short proof that the type of propositions is a --- proposition. Note that this uses a binary form of funext. -propIsProp (A : U) : prop (prop A) = - \(f g : prop A) -> - \(a b : A) -> (propSet A f a b (f a b) (g a b)) @ i - -{- - -We can also define the type of squares: - - u - a0 -----> a1 - | | - r0 | | r1 - | | - V V - b0 -----> b1 - v - --} -Square (A : U) (a0 a1 b0 b1 : A) (u : Path A a0 a1) (v : Path A b0 b1) - (r0 : Path A a0 b0) (r1 : Path A a1 b1) : U - = PathP ( (PathP ( A) (u @ i) (v @ i))) r0 r1 - -constSquare (A : U) (a : A) (p : Path A a a) : Square A a a a a p p p p = - comp (<_> A) a [ (i = 0) -> p @ j \/ - k - , (i = 1) -> p @ j /\ k - , (j = 0) -> p @ i \/ - k - , (j = 1) -> p @ i /\ k ] - - - --- The first argument to comp is a line in the universe. So far we --- have only considered constant lines.. - --- "Kan composition": -kan (A : U) (a b c d : A) (p : Path A a b) - (q : Path A a c) (r : Path A b d) : Path A c d = - comp (<_> A) (p @ i) [ (i = 0) -> q, (i = 1) -> r ] - --- Generalized Kan composition: -kan' (A B : U) (P : Path U A B) (a b : A) (c d : B) (p : Path A a b) - (q : PathP P a c) (r : PathP P b d) : Path B c d = - comp P (p @ i) [ (i = 0) -> q, (i = 1) -> r ] - -kan'' (A : U) (a b c d : A) (p : Path A a b) - (q : Path A a c) (r : Path A b d) : Path A c d = - kan' A A (<_> A) a b c d p q r - - - - --- Names and compisitions provides a convenient way for reasoning with --- equalities: - -data nat = zero - | suc (n : nat) - -one : nat = suc zero -two : nat = suc one - -add (a : nat) : nat -> nat = split - zero -> a - suc b -> suc (add a b) - --- Exercise (for solution see bottom of the file): -addZero : (a : nat) -> Path nat (add zero a) a = undefined - -addSuc (a : nat) : (b : nat) -> Path nat (add (suc a) b) (suc (add a b)) = split - zero -> suc a - suc b' -> suc (addSuc a b' @ i) - --- Exercise (can be done with a composition): -addCom (a : nat) : (b : nat) -> Path nat (add a b) (add b a) = undefined - -addAssoc (a b : nat) : (c : nat) -> Path nat (add a (add b c)) (add (add a b) c) = split - zero -> add a b - suc c' -> suc (addAssoc a b c' @ i) - - - - -{- - Transport --------------------------------------------------------------------------- - -Transport takes a path in the universe between A and B and produces a -function from A to B: - - transport : Path U A B -> A -> B - --} - --- This gives a simple proof of subst (called transportf above and in --- UniMath): -subst (A : U) (P : A -> U) (a b : A) (p : Path A a b) (e : P a) : P b = - transport (cong A U P a b p) e - - --- Transport is defined in the Haskell code as a composition with an --- empty cube/system. It can also be directly defined as: -trans (A B : U) (p : Path U A B) (a : A) : B = comp p a [] - --- However these are not exactly the same because the lack of implicit --- arguments. - --- subst with the fact that singletons are contractible this gives --- the J eliminator: -J (A : U) (a : A) (C : (x : A) -> Path A a x -> U) - (d : C a (refl A a)) (x : A) (p : Path A a x) : C x p = - subst (singl A a) T (a,refl A a) (x,p) (contrSingl A a x p) d - where T (bp : singl A a) : U = C bp.1 bp.2 - --- Note: Transporting with refl is not the identity function: - --- transRefl (A : U) (a : A) : Path A a a = refl A (transport (refl U A) a) - --- This implies that the elimination rule for J does not hold definitonally: - --- defEqJ (A : U) (a : A) (C : (x : A) -> Path A a x -> U) (d : C a (refl A a)) : --- Path (C a (refl A a)) (J A a C d a (refl A a)) d = refl (C a (refl A a)) d - --- We can get the equality between a and the transport of a by filling: -transFill (A : U) (a : A) : Path A a (transport (<_> A) a) = - fill (<_> A) a [] - - --- This might not be too bad though. Nils-Anders Danielsson has --- verified in Agda that many of the consequences of univalence can be --- developed without defEqJ. - - --- We used to have a system where defEqJ was definitional, however it --- relied on a condition called "regularity" which Dan Licata showed to --- not hold for the universe (at least for the way we define --- composition in the universe). - --- A "strange" term showing what happens without regularity --- strange (A : U) (a b c : A) (p : Path A a b) (q : Path A b c) : --- Path A (comp (<_> A) a []) c = --- comp (<_> A) (p @ i) [ (i = 1) -> q ] - - - --- It seems like we can recover a new Path type with the correct --- definitional equalities using ideas from awfs of Andrew --- Swan... Simon has implemented this in the branch "defeq". - - - - - - - - - -{- - -So far we have: MLTT + Path, , @, i/\j, compositions, transport - -With all of this we get J, but so far without def. eq. - -We also want univalence and HITs. - --} - - - - - - -{- - Glueing --------------------------------------------------------------------------- - -Glueing is what enables us to prove univalence by producing -non-trivial equalities from equivalences. In particular glueing gives -a map from Equiv(A,B) to A = B. - --} - -isContr (A : U) : U = (x : A) * ((y : A) -> Path A x y) - -fiber (A B : U) (f : A -> B) (y : B) : U = - (x : A) * Path B y (f x) - -isEquiv (A B : U) (f : A -> B) : U = - (y : B) -> isContr (fiber A B f y) - -idIsEquiv (A : U) : isEquiv A A (idfun A) = - \(a : A) -> ((a, refl A a) - ,\(z : fiber A A (idfun A) a) -> contrSingl A a z.1 z.2) - --- Using the grad lemma we can transform isomorphisms into equalities. -lemIso (A B : U) (f : A -> B) (g : B -> A) - (s : (y : B) -> Path B (f (g y)) y) - (t : (x : A) -> Path A (g (f x)) x) - (y : B) (x0 x1 : A) (p0 : Path B y (f x0)) (p1 : Path B y (f x1)) : - Path (fiber A B f y) (x0,p0) (x1,p1) = (p @ i,sq1 @ i) - where - rem0 : Path A (g y) x0 = - comp (<_> A) (g (p0 @ i)) [ (i = 1) -> t x0, (i = 0) -> <_> g y ] - - rem1 : Path A (g y) x1 = - comp (<_> A) (g (p1 @ i)) [ (i = 1) -> t x1, (i = 0) -> <_> g y ] - - p : Path A x0 x1 = - comp (<_> A) (g y) [ (i = 0) -> rem0 - , (i = 1) -> rem1 ] - - fill0 : Square A (g y) (g (f x0)) (g y) x0 - ( g (p0 @ i)) rem0 ( g y) (t x0) = - comp (<_> A) (g (p0 @ i)) [ (i = 1) -> t x0 @ j /\ k - , (i = 0) -> <_> g y - , (j = 0) -> <_> g (p0 @ i) ] - - fill1 : Square A (g y) (g (f x1)) (g y) x1 - ( g (p1 @ i)) rem1 ( g y) (t x1) = - comp (<_> A) (g (p1 @ i)) [ (i = 1) -> t x1 @ j /\ k - , (i = 0) -> <_> g y - , (j = 0) -> <_> g (p1 @ i) ] - - fill2 : Square A (g y) (g y) x0 x1 - (<_> g y) p rem0 rem1 = - comp (<_> A) (g y) [ (i = 0) -> rem0 @ j /\ k - , (i = 1) -> rem1 @ j /\ k - , (j = 0) -> <_> g y ] - - sq : Square A (g y) (g y) (g (f x0)) (g (f x1)) - ( g y) ( g (f (p @ i))) - ( g (p0 @ j)) ( g (p1 @ j)) = - comp (<_> A) (fill2 @ i @ j) [ (i = 0) -> fill0 @ j @ -k - , (i = 1) -> fill1 @ j @ -k - , (j = 0) -> <_> g y - , (j = 1) -> t (p @ i) @ -k ] - - sq1 : Square B y y (f x0) (f x1) - (<_>y) ( f (p @ i)) p0 p1 = - comp (<_> B) (f (sq @ i @j)) [ (i = 0) -> s (p0 @ j) - , (i = 1) -> s (p1 @ j) - , (j = 1) -> s (f (p @ i)) - , (j = 0) -> s y ] - -gradLemma (A B : U) (f : A -> B) (g : B -> A) - (s : (y : B) -> Path B (f (g y)) y) - (t : (x : A) -> Path A (g (f x)) x) : isEquiv A B f = - \ (y:B) -> ((g y,s y@-i),\ (z:fiber A B f y) -> lemIso A B f g s t y (g y) z.1 (s y@-i) z.2) - - - -isoPath (A B : U) (f : A -> B) (g : B -> A) - (s : (y : B) -> Path B (f (g y)) y) - (t : (x : A) -> Path A (g (f x)) x) : Path U A B = - Glue B [ (i = 0) -> (A,f,gradLemma A B f g s t) - , (i = 1) -> (B,idfun B,idIsEquiv B) ] - - - - - - - --------------------------------------------------------- - -- Example: Non-trivial equality between bool and bool -- - --------------------------------------------------------- - --- Not is involutive: -notK : (b : bool) -> Path bool (not (not b)) b = split - false -> false - true -> true - --- This defines a non-trivial equality between bool and bool: -notEq : Path U bool bool = isoPath bool bool not not notK notK - --- We can transport true along this non-trivial equality: -testFalse : bool = transport notEq true - - - - - - - - --------------------------------------------------- - -- Example: Non-trivial equality between Z and Z -- - --------------------------------------------------- - --- Integers: -data or (A B : U) = inl (a : A) - | inr (b : B) - -Z : U = or nat nat - -{- Z represents: - - +2 = inr (suc (suc zero)) - +1 = inr (suc zero) - 0 = inr zero - -1 = inl zero - -2 = inl (suc zero) - --} - -zeroZ : Z = inr zero - -sucZ : Z -> Z = split - inl u -> auxsucZ u - where - auxsucZ : nat -> Z = split - zero -> zeroZ - suc n -> inl n - inr v -> inr (suc v) - -predZ : Z -> Z = split - inl u -> inl (suc u) - inr v -> auxpredZ v - where - auxpredZ : nat -> Z = split - zero -> inl zero - suc n -> inr n - -sucpredZ : (x : Z) -> Path Z (sucZ (predZ x)) x = split - inl u -> inl u - inr v -> lem v - where - lem : (u : nat) -> Path Z (sucZ (predZ (inr u))) (inr u) = split - zero -> inr zero - suc n -> inr (suc n) - -predsucZ : (x : Z) -> Path Z (predZ (sucZ x)) x = split - inl u -> lem u - where - lem : (u : nat) -> Path Z (predZ (sucZ (inl u))) (inl u) = split - zero -> inl zero - suc n -> inl (suc n) - inr v -> inr v - -sucPathZ : Path U Z Z = isoPath Z Z sucZ predZ sucpredZ predsucZ - --- We can transport along the proof forward and backwards: -testOneZ : Z = transport sucPathZ zeroZ -testNOneZ : Z = transport ( sucPathZ @ - i) zeroZ - - --- transport sucPathZ = sucZ ? - - - - ------------------------------------------------------------------ --- Using Glue we get a proof of univalence, see univalence.ctt -- - - - - - - -{- - Higher-inductive types (HITs) --------------------------------------------------------------------------- - -Another way to obtain non-trivial equalities are HITs. These -generalize normal inductive types by allowing constructors that define -(possibly higher) equalities. - --} - - - ------------------------------------ - -- Example: The integers as a HIT -- - ------------------------------------ - -{- - -There is a minor issue with the definition of Z: the negative numbers -are off by one. - -What we really want is the equality "inl zero = inr zero". - -Solution: Define the integers as a HIT! - --} - -data int = pos (n : nat) - | neg (n : nat) - | zeroP [ (i = 0) -> pos zero - , (i = 1) -> neg zero ] - --- Nice version of the zero constructor: -zeroPath : Path int (pos zero) (neg zero) = zeroP {int} @ i - -sucInt : int -> int = split - pos n -> pos (suc n) - neg n -> sucNat n - where sucNat : nat -> int = split - zero -> pos one - suc n -> neg n - zeroP @ i -> pos one - -toZ : int -> Z = split - pos n -> inr n - neg n -> auxToZ n - where auxToZ : nat -> Z = split - zero -> inr zero - suc n -> inl n - zeroP @ i -> inr zero - -fromZ : Z -> int = split - inl n -> neg (suc n) - inr n -> pos n - -toZK : (a : Z) -> Path Z (toZ (fromZ a)) a = split - inl n -> inl n - inr n -> inr n - -fromZK : (a : int) -> Path int (fromZ (toZ a)) a = split - pos n -> pos n - neg n -> rem n - where rem : (n : nat) -> Path int (fromZ (toZ (neg n))) (neg n) = split - zero -> zeroPath - suc m -> neg (suc m) - zeroP @ i -> zeroPath @ i /\ j -- A connection makes this proof easy! - -isoIntZ : Path U Z int = isoPath Z int fromZ toZ fromZK toZK - - - - ---------------------------------- - -- Example: The circle as a HIT -- - ---------------------------------- - -data S1 = base - | loop [ (i = 0) -> base, (i = 1) -> base] - -loopS1 : U = Path S1 base base - --- The loop constructor -loop1 : loopS1 = loop{S1} @ i - -invLoop : loopS1 = loop1 @ -i - -helix : S1 -> U = split - base -> Z - loop @ i -> sucPathZ @ i - --- The winding number: -winding (p : loopS1) : Z = transport ( helix (p @ i)) zeroZ - --- Loop composition: -compS1 : loopS1 -> loopS1 -> loopS1 = pathscomp0 S1 base base base - --- Some examples of winding numbers: -loopZ1 : Z = winding loop1 -loopZ2 : Z = winding (compS1 loop1 loop1) -loopZ3 : Z = winding (compS1 loop1 (compS1 loop1 loop1)) -loopZN1 : Z = winding invLoop -loopZ0 : Z = winding (compS1 loop1 invLoop) - -mLoop : (x : S1) -> Path S1 x x = split - base -> loop1 - loop @ i -> constSquare S1 base loop1 @ i - --- Multiplication: -mult (x : S1) : S1 -> S1 = split - base -> x - loop @ i -> mLoop x @ i - --- Squaring: -square (x : S1) : S1 = mult x x - -doubleLoop (l : loopS1) : loopS1 = square (l @ i) - -doubleLoop' (l : loopS1) : loopS1 = compS1 l l - -loopZ4 : Z = winding (doubleLoop (compS1 loop1 loop1)) -loopZ8 : Z = winding (doubleLoop (doubleLoop (compS1 loop1 loop1))) - --- A nice example of a homotopy on the circle. The path going halfway --- around the circle and then back is contractible: -hmtpy : Path loopS1 ( base) ( loop{S1} @ (i /\ -i)) = - loop{S1} @ j /\ i /\ -i - - - --------------------------------------------------------------------------- --- For a higher dimensional HIT see, torus.ctt - - - - - - - - - -{- - Issues and Future Work --------------------------------------------------------------------------- - - o Definitional equality for J? Problem pointed out by Dan Licata - with regularity for composition in the universe. However, the - system might still work without regularity (this is what is being - implemented in the no_regular branch). - - o Meta-theoretical properties of the system and correctness of the - model. Formalization? - - o Integration of ideas into other proof assistants (e.g. Agda)? - --} - - - -{- Solutions: - -addZero : (a : nat) -> Path nat (add zero a) a = split - zero -> zero - suc a' -> suc (addZero a' @ i) - -addCom (a : nat) : (b : nat) -> Path nat (add a b) (add b a) = split - zero -> addZero a @ -i - suc b' -> comp (<_> nat) (suc (addCom a b' @ i)) [ (i = 0) -> suc (add a b') - , (i = 1) -> addSuc b' a @ -j ] - --}