From ded3dc64bdb70f454ff2973a9ad9e4b9e926e09d Mon Sep 17 00:00:00 2001 From: Anders Date: Thu, 18 Jun 2015 18:45:17 +0200 Subject: [PATCH] Update README and update demo.ctt --- README.md | 9 +- examples/bool.ctt | 12 ++ examples/circle.ctt | 20 +- examples/demo.ctt | 448 +++++++++++++++++++++++++++++++---------- examples/gradLemma.ctt | 4 - examples/int.ctt | 20 +- examples/integer.ctt | 15 +- examples/pi.ctt | 6 +- 8 files changed, 414 insertions(+), 120 deletions(-) diff --git a/README.md b/README.md index 003d17a..8e983d0 100644 --- a/README.md +++ b/README.md @@ -7,9 +7,10 @@ theory with: * Path abstraction and application * Composition and transport -* Isomorphisms can be transformed into equalities +* Equivalences can be transformed into equalities (and univalence can + be proved, see "examples/univalence.ctt") * Some higher inductive types (see "examples/circle.ctt" and - "examples/susp.ctt") + "examples/integer.ctt") Because of this it is not necessary to have a special file of primitives (like in [cubical](https://github.com/simhu/cubical)), for @@ -21,10 +22,6 @@ funExt (A : U) (B : A -> U) (f g : (x : A) -> B x) Id ((y : A) -> B y) f g = \(a : A) -> (p a) @ i ``` -This proof can be compared with the one in "examples/uafunext1.ctt" -which proves that univalence implies function extensionality (the -normal form of these proofs are almost the same). - For more examples, see "examples/demo.ctt". diff --git a/examples/bool.ctt b/examples/bool.ctt index ff1a722..fea7111 100644 --- a/examples/bool.ctt +++ b/examples/bool.ctt @@ -4,19 +4,31 @@ import gradLemma data bool = false | true + --------------------------------------------------------- + -- Example: Non-trivial equality between bool and bool -- + --------------------------------------------------------- + negBool : bool -> bool = split false -> true true -> false +-- negBool is involutive: negBoolK : (b : bool) -> Id bool (negBool (negBool b)) b = split false -> refl bool false true -> refl bool true +-- This defines a non-trivial equality between bool and bool: negBoolEq : Id U bool bool = isoId bool bool negBool negBool negBoolK negBoolK +-- We can transport true along this non-trivial equality: testFalse : bool = transport negBoolEq true + + + +-- An isomorphic representation to bool: + data F2 = zeroF2 | oneF2 f2ToBool : F2 -> bool = split diff --git a/examples/circle.ctt b/examples/circle.ctt index ea38957..126b319 100644 --- a/examples/circle.ctt +++ b/examples/circle.ctt @@ -3,6 +3,10 @@ module circle where import bool import int + ---------------------------------- + -- Example: The circle as a HIT -- + ---------------------------------- + data S1 = base | loop [(i=0) -> base, (i=1) -> base] @@ -31,6 +35,13 @@ loop2 : loopS1 = compS1 loop1 loop1 loop2' : loopS1 = compId' S1 base base base loop1 loop1 loop2'' : loopS1 = compId'' S1 base base loop1 base loop1 +-- More examples: +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 @@ -44,7 +55,12 @@ square (x : S1) : S1 = mult x x doubleLoop (l : loopS1) : loopS1 = square (l @ i) tripleLoop (l : loopS1) : loopS1 = mult (l @ i) (square (l @ i)) +loopZ4 : Z = winding (doubleLoop (compS1 loop1 loop1)) +loopZ8 : Z = winding (doubleLoop (doubleLoop (compS1 loop1 loop1))) + triv : loopS1 = base --- A nice example -hmtpy : Id loopS1 triv ( loop{S1} @ (i /\ -i)) = loop{S1} @ j /\ i /\ -i \ No newline at end of file +-- 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 diff --git a/examples/demo.ctt b/examples/demo.ctt index 2375f33..f01b1b8 100644 --- a/examples/demo.ctt +++ b/examples/demo.ctt @@ -1,172 +1,418 @@ module demo where +{- + cubicaltt: Cubical type theory +-------------------------------------------------------------------------- + Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg --- Cubical type theory! ------------------------ --- (j.w.w. Cyril Cohen, Thierry Coquand, Anders M\"ortberg) --- Try it: --- https://github.com/mortberg/cubicaltt +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. --- Ordinary type theory (without Id-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. -identity (A : U) (a : A) : A = a +Mini-TT is a variant Martin-Löf type theory with data +types. cubiclaltt extends Mini-TT with: -data bool = false | true + o Name abstraction and application + o Compositions + o Equivalences can be transformed into equalities + o Some higher inductive types -neg : bool -> bool = split - false -> true - true -> false +Try it: https://github.com/mortberg/cubicaltt -data nat = zero - | suc (n : nat) +-} -one : nat = suc zero -two : nat = suc one + ------------------------------------------ + -- Some examples of programs in Mini-TT -- + ------------------------------------------ -data list (A : U) = nil - | cons (a : A) (as : list A) +-- 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 A0 A1 is a line in the universe connecting A0 and A1: +An element in ID A B is a line in the universe connecting A and B: - |- A0 Type |- A1 Type ------------------------------ - |- ID A0 A1 Type + |- A Type |- B Type + ------------------------------ + |- ID A B Type - |- P : ID A0 A1 |- a0 : A0 |- a1 : A1 --------------------------------------------------------- - |- IdP P a0 a1 Type +IdP is heterogeneous equality: -Note: As we have U : U the type ID is not needed in the - implementation. + + |- 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 --- Here " A" is a constant path in the universe: -constPath (A : U) : Id U A A = A - --- "" abstracts the name/color/dimension i. +-- "" abstracts the name/color/dimension i: refl (A : U) (a : A) : Id A a a = a -inv (A : U) (a b : A) (p : Id A a b) : Id A b a = p @ -i -test0 (A : U) (a b : A) (p : Id A a b) : Id A a a = refl A (p @ 0) -test1 (A : U) (a b : A) (p : Id A a b) : Id A b b = refl A (p @ 1) +{- -mapOnPath (A B : U) (f : A -> B) (a b : A) - (p : Id A a b) : Id B (f a) (f b) = +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 = + (p : (x : A) -> Id (B x) (f x) (g x)) : Id ((y : A) -> B y) f g = \(a : A) -> (p a) @ 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 : 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)) + (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 -reflRefl (A : U) (a : A) : Id (Id A a a) (refl A a) (refl A a) = - refl (Id A a a) (refl A a) --- a +{- + +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 -test2 (A : U) (a b : A) (p : Id A a b) : Id A a a = - p @ (i /\ -i) -test3 (A : U) (a b : A) (p : Id A a b) : Id A b b = - p @ (i \/ -i) +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 ] --- Transport. +-- Names and compisitions provides a convenient way for reasoning with +-- equalities: --- transport is another built-in. --- It takes a path p in U and an element --- in p @ 0; produces an element in p @ 1 -subst (A : U) (P : A -> U) (a b : A) - (p : Id A a b) (e : P a) : P b = - transport (mapOnPath A U P a b p) e +data nat = zero + | suc (n : nat) -substEq (A : U) (P : A -> U) (a : A) (e : P a) : - Id (P a) (subst A P a a (refl A a) e) e = - refl (P a) e +one : nat = suc zero +two : nat = suc one + +add (a : nat) : nat -> nat = split + zero -> a + suc b -> suc (add a b) + +addZero : (a : nat) -> Id nat (add zero a) a = split + zero -> zero + suc a' -> suc (addZero a' @ i) + +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) + +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 ] +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 is defined internally as a composition with an empty system. + +-} + +-- 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 (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) + where T (bp : singl A a) : U = C bp.1 bp.2 + +-- Note: Transporting with refl is not the identity function: --- Examples: +-- transRefl (A : U) (a : A) : Id A a a = refl A (transport (refl U A) a) -ptU : U = (X : U) * X +-- This implies that the elimination rule for J does not hold definitonally: -lemPt (A B : U) (p : Id U A B) (a : A) : Id ptU (A,a) (B,transport p a) = - (p @ i,transport ( p @ (i/\j)) a) +-- 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 -S : U = (A : U) (a : A) * (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. -lemS (A B : U) (p : Id U A B) (a : A) (f : A -> A) : - Id S (A,a,f) (B, transport p a, transport ( p @ i -> p @ i) f) = - ( p @ i - , transport ( p @ (i/\j)) a - , transport ( p @ (i /\ j) -> p @ (i /\ j)) f) --- Composition. --- Any type is a weak omega-groupoid. --- Given a cube, we form a new cube by replacing some faces along equalities. +{- + Glueing +-------------------------------------------------------------------------- -transitive (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 = 1) -> q ] +The univalence axiom says that equivalent (written as ~) types are +equal: ---- comp A (p @ (i /\ j)) [ (i=1)(j=1) -> q] + (A = B) ~ (A ~ B) -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 @ j, (i = 1) -> r ] +Glueing is a weaker form of this for producing non-trivial equalities +from equivalences. In particular glueing gives a map from Equiv(A,B) +to A = B. This weak form of univalence is useful for developing a lot +of examples. For examples see: -regKan (A : U) (a b : A) (p : Id A a b) : - Id (Id A a b) p (kan A a b a b p (refl A a) (refl A b)) = - refl (Id A a b) p + - examples/bool.ctt: Non-trivial equality between bool and bool + given by negation. --- Example: any proposition is a set. + - examples/int.ctt: Non-trivial equality between Z and Z given by + successor and predecessor. -prop (A : U) : U = (a b : A) -> Id A a b -set (A : U) : U = (a b : A) -> prop (Id A a b) + - examples/pi.ctt: Equality in pi types. -propSet (A : U) (h : prop A) (a b : A) (p q : Id A a b) - : Id (Id A a b) p q = - comp A a [ (i=0) -> h a a - , (i=1) -> h a b - , (j=0) -> h a (p @ i) - , (j=1) -> h a (q @ i)] +Further, the full form of univalence is provable in the system. See +the file examples/univalence.ctt for a proof of this. +-} --- Glueing. --- A way to produce non-trivial equalities. - -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 B [ (i = 0) -> (A,f,g,s,t) ] -negK : (b : bool) -> Id bool (neg (neg b)) b = split - false -> refl bool false - true -> refl bool true -negEq : Id U bool bool = - (glue bool [ (i = 0) -> (bool,neg,neg,negK,negK) ]) +{- + 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. For further examples see: -testFalse : bool = transport negEq true + - examples/circle.ctt: The circle as a HIT. --- Continue with: integer, circle, suspension + - examples/integer.ctt: The integers as a HIT. +-} diff --git a/examples/gradLemma.ctt b/examples/gradLemma.ctt index da89690..c1d5367 100644 --- a/examples/gradLemma.ctt +++ b/examples/gradLemma.ctt @@ -70,10 +70,6 @@ isoId (A B : U) (f : A -> B) (g : B -> A) , (i = 1) -> (B,transDelta B) ] - - - - -- OLD CODE: -- lemIso with equalities on other direction: -- lemIso (A B : U) (f : A -> B) (g : B -> A) diff --git a/examples/int.ctt b/examples/int.ctt index f593479..46f14ce 100644 --- a/examples/int.ctt +++ b/examples/int.ctt @@ -4,9 +4,22 @@ import nat import discor import gradLemma --- inl = neg, inr = pos + --------------------------------------------------- + -- Example: Non-trivial equality between Z and Z -- + --------------------------------------------------- + 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 @@ -41,6 +54,11 @@ predsucZ : (x : Z) -> Id Z (predZ (sucZ x)) x = split suc n -> refl Z (inl (suc n)) inr v -> refl Z (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 sucIdZ zeroZ +testNOneZ : Z = transport ( sucIdZ @ - i) zeroZ + ZSet : set Z = hedberg Z (orDisc nat nat natDec natDec) \ No newline at end of file diff --git a/examples/integer.ctt b/examples/integer.ctt index fdf55a5..948def4 100644 --- a/examples/integer.ctt +++ b/examples/integer.ctt @@ -2,11 +2,16 @@ module integer where import int + ------------------------------------ + -- Example: The integers as a HIT -- + ------------------------------------ + data int = pos (n : nat) | neg (n : nat) | zeroP [(i=0) -> pos zero, (i=1) -> neg zero] -zeroP' : Id int (pos zero) (neg zero) = zeroP {int} @ i +-- 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) @@ -30,7 +35,7 @@ toZ : int -> Z = split where auxToZ : nat -> Z = split zero -> inr zero suc n -> inl n - zeroP @ i -> zeroZ + zeroP @ i -> inr zero fromZ : Z -> int = split inl n -> neg (suc n) @@ -44,9 +49,9 @@ fromZK : (a : int) -> Id int (fromZ (toZ a)) a = split pos n -> refl int (pos n) neg n -> rem n where rem : (n : nat) -> Id int (fromZ (toZ (neg n))) (neg n) = split - zero -> zeroP' + zero -> zeroZ suc m -> refl int (neg (suc m)) - zeroP @ i -> zeroP' @ i /\ j + zeroP @ i -> zeroZ @ i /\ j isoIntZ : Id U Z int = isoId Z int fromZ toZ fromZK toZK @@ -56,7 +61,7 @@ intSet : set int = subst U set Z int isoIntZ ZSet T : U = Id int (pos zero) (pos zero) p0 : T = refl int (pos zero) -p1 : T = compId int (pos zero) (neg zero) (pos zero) zeroP' (zeroP'@-i) +p1 : T = compId int (pos zero) (neg zero) (pos zero) zeroZ (zeroZ@-i) test0 : Id (Id Z (inr zero) (inr zero)) (refl Z (inr zero)) (refl Z (inr zero)) = ZSet (inr zero) (inr zero) (refl Z (inr zero)) (refl Z (inr zero)) diff --git a/examples/pi.ctt b/examples/pi.ctt index 34b0733..ef82c8c 100644 --- a/examples/pi.ctt +++ b/examples/pi.ctt @@ -1,6 +1,10 @@ module pi where -import prelude +import gradLemma + + ----------------------------------- + -- Example: Equality in pi types -- + ----------------------------------- pi (A:U) (P:A->U) : U = (x:A) -> P x -- 2.34.1