From 8a8567c9bba38184c5a3590226cff7b39fa56bfd Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Sat, 6 Jun 2015 11:15:14 +0200 Subject: [PATCH] Add AIM talk --- examples/aim.ctt | 656 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 656 insertions(+) create mode 100644 examples/aim.ctt diff --git a/examples/aim.ctt b/examples/aim.ctt new file mode 100644 index 0000000..22b1e0e --- /dev/null +++ b/examples/aim.ctt @@ -0,0 +1,656 @@ +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 HoTT/UF, 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 + +Note: At the moment one should use the no_regular branch. + +-} + + ------------------------------------------ + -- 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 + + +{- + Identity 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 + + +IdP is heterogeneous equality: + + + |- P : ID A B |- a : A |- b : B + ----------------------------------------------- + |- IdP P a b Type + +-} + +-- The usual identity can be seen a special case of IdP: +Id (A : U) (a b : A) : U = IdP ( A) a b + +-- "" abstracts the name/color/dimension i: +refl (A : U) (a : A) : Id A a a = a + + +{- + +A proof "p : Id A a b" is thought of as a line between a and b: + + p + a ------> b + + +A proof "sq : Id (Id 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 : Id A a b) : Id A a a = refl A (p @ 0) +face1 (A : U) (a b : A) (p : Id A a b) : Id 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 : Id A a b) : Id 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) -> Id (B x) (f x) (g x)) : Id ((y : A) -> B y) f g = + \(a : A) -> (p a) @ i + +-- To see the definition of funExt makes sense we can compute its faces: +-- +-- funExt @ 0 = \(a : A) -> (p a) @ 0 (faces commute with operations) +-- = \(a : A) -> f a (p a proves Id (B a) (f a) (g a)) +-- = f (by 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 : Id A a b) : Id A b a = p @ -i + +-- This operation is an involution: +symK (A : U) (a b : A) (p : Id A a b) : Id (Id A a b) p p = + refl (Id 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) * Id A a x + +contrSingl (A : U) (a b : A) (p : Id A a b) : + Id (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 : Id A a b) : + Id (Id A a a) (<_> p @ 0) (<_> p @ 0) = + refl (Id 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 : Id A a b) : Id A a a = p @ i /\ -i +testDisj (A : U) (a b : A) (p : Id A a b) : Id A b b = p @ i \/ -i + + +{- + Compositions +------------------------------------------------------------------------ + +Given a cube, we form a new cube by replacing some faces along +equalities. This can be seen a generalization of composition of +relations. + +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 Id is obtained from a composition of this open square: + + + a - - - - - - - - > c + ^ ^ + | | + | | + a | | q + | | + | | + | | + a ----------------> b + p @ i + +The composition computes the dashed line at the top of the square. + +-} +trans (A : U) (a b c : A) (p : Id A a b) (q : Id A b c) : Id A a c = + comp (<_> A) (p @ i) [ (i = 0) -> a, (i = 1) -> q ] + +-- "Kan composition": +kan (A : U) (a b c d : A) (p : Id A a b) + (q : Id A a c) (r : Id A b d) : Id A c d = + comp (<_> A) (p @ i) [ (i = 0) -> q, (i = 1) -> r ] + + +-- The first two nonzero h-levels are propositions and sets: +prop (A : U) : U = (a b : A) -> Id A a b +set (A : U) : U = (a b : A) -> prop (Id 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 : Id 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 : Id A a0 a1) (v : Id A b0 b1) + (r0 : Id A a0 b0) (r1 : Id A a1 b1) : U + = IdP ( (IdP ( A) (u @ i) (v @ i))) r0 r1 + +constSquare (A : U) (a : A) (p : Id 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 ] + + + +-- 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) -> Id nat (add zero a) a = undefined + +addSuc (a : nat) : (b : nat) -> Id 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) -> Id nat (add a b) (add b a) = undefined + +addAssoc (a b : nat) : (c : nat) -> Id 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 : Id U A B -> A -> B + +It can be defined as a composition with an empty cube/system. + +-} + +transport (A B : U) (p : Id U A B) (a : A) : B = comp p a [] + +-- This gives a simple proof of subst: +subst (A : U) (P : A -> U) (a b : A) (p : Id A a b) (e : P a) : P b = + transport (P a) (P b) (cong A U P a b p) e + +-- Combined with the fact that singletons are contractible this gives +-- the J eliminator: +J (A : U) (a : A) (C : (x : A) -> Id A a x -> U) + (d : C a (refl A a)) (x : A) (p : Id 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) : Id 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) -> Id A a x -> U) (d : C a (refl A a)) : +-- Id (C a (refl A a)) (J A a C d a (refl A a)) d = refl (C a (refl A a)) d + +-- 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. + + +{- + Glueing +-------------------------------------------------------------------------- + +The univalence axiom says that equivalent (written as ~) types are +equal: + + (A = B) ~ (A ~ B) + +Glueing is a weaker form of this for producing non-trivial equalities +from isomorphisms. In particular glueing gives a map from Iso(A,B) to +A = B. This weak form of univalence is useful for developing a lot of +examples. + +-} + +isoId (A B : U) (f : A -> B) (g : B -> A) + (s : (y : B) -> Id B (f (g y)) y) + (t : (x : A) -> Id A (g (f x)) x) : Id U A B = + glue A [ (i = 0) -> (A,idfun A,idfun A,refl A,refl A) + , (i = 1) -> (B,g,f,t,s) ] + +-- Note that we have to glue the identity isomorphism to (i = 0), this +-- is because lack of regularity. Compare with trans. + + + --------------------------------------------------------- + -- Example: Non-trivial equality between bool and bool -- + --------------------------------------------------------- + +-- Not is involutive: +notK : (b : bool) -> Id bool (not (not b)) b = split + false -> false + true -> true + +-- This defines a non-trivial equality between bool and bool: +notEq : Id U bool bool = isoId bool bool not not notK notK + +-- We can transport true along this non-trivial equality: +testFalse : bool = transport bool bool 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) -> Id Z (sucZ (predZ x)) x = split + inl u -> inl u + inr v -> lem v + where + lem : (u : nat) -> Id Z (sucZ (predZ (inr u))) (inr u) = split + zero -> inr zero + suc n -> inr (suc n) + +predsucZ : (x : Z) -> Id Z (predZ (sucZ x)) x = split + inl u -> lem u + where + lem : (u : nat) -> Id Z (predZ (sucZ (inl u))) (inl u) = split + zero -> inl zero + suc n -> inl (suc n) + inr v -> inr v + +sucIdZ : Id U Z Z = isoId Z Z sucZ predZ sucpredZ predsucZ + +-- We can transport along the proof forward and backwards: +testOneZ : Z = transport Z Z sucIdZ zeroZ +testNOneZ : Z = transport Z Z ( sucIdZ @ - i) zeroZ + + + ----------------------------------- + -- Example: Equality in pi types -- + ----------------------------------- + +pi (A : U) (P : A -> U) : U = (x : A) -> P x + +-- Equality in pi types: +idPi (A : U) (B : A -> U) (f g : pi A B) : + Id U (Id (pi A B) f g) ((x : A) -> Id (B x) (f x) (g x)) = + isoId (Id (pi A B) f g) ((x : A) -> Id (B x) (f x) (g x)) F G S T + where T0 : U = Id (pi A B) f g + T1 : U = (x : A) -> Id (B x) (f x) (g x) + F (p : T0) : T1 = \(x : A) -> (p @ i) x + G (p : T1) : T0 = \(x : A) -> (p x) @ i + S (p : T1) : Id T1 (F (G p)) p = p + T (p : T0) : Id T0 (G (F p)) p = p + +-- If B is a family of sets then pi A B is a set: +setPi (A : U) (B : A -> U) (h : (x : A) -> set (B x)) : set (pi A B) = + \(f g : pi A B) -> + let T : U = (x : A) -> Id (B x) (f x) (g x) + rem : prop T = + \(p q : T) -> \(x : A) -> h x (f x) (g x) (p x) (q x) @ i + in subst U prop T (Id (pi A B) f g) ( idPi A B f g @ -i) rem + + + +{- + 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 circle as a HIT -- + ---------------------------------- + +data S1 = base + | loop [ (i = 0) -> base, (i = 1) -> base] + +loopS1 : U = Id S1 base base + +-- The loop constructor +loop1 : loopS1 = loop{S1} @ i + +invLoop : loopS1 = sym S1 base base loop1 + +helix : S1 -> U = split + base -> Z + loop @ i -> sucIdZ @ i + +-- The winding number: +winding (p : loopS1) : Z = transport Z Z ( helix (p @ i)) zeroZ + +-- Loop composition: +compS1 : loopS1 -> loopS1 -> loopS1 = trans 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) -> Id 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) + +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 : Id loopS1 ( base) ( loop{S1} @ (i /\ -i)) = + loop{S1} @ j /\ i /\ -i + + + ------------------------------------ + -- 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: +zeroZ : Id 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) -> Id Z (toZ (fromZ a)) a = split + inl n -> inl n + inr n -> inr n + +fromZK : (a : int) -> Id int (fromZ (toZ a)) a = split + pos n -> pos n + neg n -> rem n + where rem : (n : nat) -> Id int (fromZ (toZ (neg n))) (neg n) = split + zero -> zeroZ + suc m -> neg (suc m) + zeroP @ i -> zeroZ @ i /\ j -- A connection makes this proof easy! + +isoIntZ : Id U Z int = isoId Z int fromZ toZ fromZK toZK + +-- This is proved in the library but admitted here: +ZSet : set Z = undefined + +intSet : set int = subst U set Z int isoIntZ ZSet + + +{- + 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 seems to work without regularity (this is work in + progress). + + o Meta-theoretical properties of the system and correctness of the + model. Formalization? + + o Integration of ideas into other proof assistants (eg Agda)? + +-} + + + +{- Solutions: + +addZero : (a : nat) -> Id nat (add zero a) a = split + zero -> zero + suc a' -> suc (addZero a' @ i) + +addCom (a : nat) : (b : nat) -> Id 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 ] +-} -- 2.34.1