From: Anders Date: Thu, 9 Apr 2015 12:29:27 +0000 (+0200) Subject: Clean examples X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=d45829ab83fff9670434f4a718afc477f7f6ac1b;p=cubicaltt.git Clean examples --- diff --git a/examples/bool.ctt b/examples/bool.ctt index 12469e2..dbbcab8 100644 --- a/examples/bool.ctt +++ b/examples/bool.ctt @@ -1,7 +1,6 @@ module bool where import prelude -import nat data bool = false | true @@ -18,37 +17,34 @@ negEq : Id U bool bool = test : bool = transport negEq true -data F2 = zero | one +data F2 = zeroF2 | oneF2 f2ToBool : F2 -> bool = split - zero -> false - one -> true + zeroF2 -> false + oneF2 -> true boolToF2 : bool -> F2 = split - false -> zero - true -> one + false -> zeroF2 + true -> oneF2 f2ToBoolK : (x : F2) -> Id F2 (boolToF2 (f2ToBool x)) x = split - zero -> refl F2 zero - one -> refl F2 one + zeroF2 -> refl F2 zeroF2 + oneF2 -> refl F2 oneF2 boolToF2K : (b : bool) -> Id bool (f2ToBool (boolToF2 b)) b = split false -> refl bool false true -> refl bool true boolEqF2 : Id U bool F2 = - -- glue F2 [ (i = 0) -> (bool,(boolToF2,(f2ToBool,(f2ToBoolK,boolToF2K))))] isoId bool F2 boolToF2 f2ToBool f2ToBoolK boolToF2K negF2 : F2 -> F2 = subst U (\(X : U) -> (X -> X)) bool F2 boolEqF2 neg - lemTest (A : U) : (B : U) (p : Id U A B) (a : A) -> IdP p a (transport p a) = J U A (\(B : U) (p : Id U A B) -> (a : A) -> IdP p a (transport p a)) (refl A) - -test : IdP boolEqF2 true one = glueElem one [ (i = 0) -> true ] -test1 : IdP boolEqF2 true one = lemTest bool F2 boolEqF2 true +test : IdP boolEqF2 true oneF2 = glueElem oneF2 [ (i = 0) -> true ] +test1 : IdP boolEqF2 true oneF2 = lemTest bool F2 boolEqF2 true F2EqBool : Id U F2 bool = inv U bool F2 boolEqF2 @@ -57,28 +53,22 @@ negBool : bool -> bool = subst U (\(X : U) -> (X -> X)) F2 bool F2EqBool negF2 F2EqBoolComp : Id U F2 bool = compId U F2 bool bool F2EqBool negEq -test2 : bool = transport F2EqBoolComp one +test2 : bool = transport F2EqBoolComp oneF2 negNegEq : Id U bool bool = compId U bool bool bool negEq negEq - test3 : bool = transport negNegEq true - test4 : Id U bool bool = negNegEq @ i kanBool : Id U bool bool = kan U bool bool bool bool negEq negEq negEq --- connectSquare (A : U) (a0 a1 : A) (u : Id A a0 a1) --- (b0 b1 : A) (v : Id A b0 b1) --- (r0 : Id A a0 b0) (r1 : Id A a1 b1) : Square A a0 a1 u b0 b1 v r0 r1= - squareBoolF2 : Square U bool bool (refl U bool) bool F2 boolEqF2 (refl U bool) boolEqF2 = boolEqF2 @ i /\ j -test5 : IdP boolEqF2 true one = +test5 : IdP boolEqF2 true oneF2 = transport ( boolEqF2 @ i /\ j) true test6 : Id bool true true = diff --git a/examples/interval.ctt b/examples/interval.ctt index 01c49e6..ee1f108 100644 --- a/examples/interval.ctt +++ b/examples/interval.ctt @@ -5,8 +5,7 @@ import prelude data I = zero | one | seg @ zero ~ one fext (A B : U) (f g : A -> B) (p : (x : A) -> Id B (f x) (g x)) : - Id (A -> B) f g = mapOnPath I (A -> B) (\(i : I) (x : A) -> htpy x i) - zero one ( seg{I} @ i) + Id (A -> B) f g = (\(x : A) -> htpy x (seg{I} @ j)) where htpy (x : A) : I -> B = split zero -> f x one -> g x diff --git a/examples/list.ctt b/examples/list.ctt new file mode 100644 index 0000000..1073d10 --- /dev/null +++ b/examples/list.ctt @@ -0,0 +1,11 @@ +module list where + +data list (A : U) = nil | cons (a : A) (as : list A) + +append (A : U) : list A -> list A -> list A = split + nil -> id (list A) + cons x xs -> \(ys : list A) -> cons x (append A xs ys) + +reverse (A : U) : list A -> list A = split + nil -> nil + cons x xs -> append A (reverse A xs) (cons x nil) diff --git a/examples/nat.ctt b/examples/nat.ctt index 321a0a6..a3a7be4 100644 --- a/examples/nat.ctt +++ b/examples/nat.ctt @@ -4,7 +4,6 @@ import prelude data nat = zero | suc (n : nat) -zero' : nat = zero one : nat = suc zero two : nat = suc one @@ -23,64 +22,12 @@ add' : nat -> nat -> nat = split sucInj (n m : nat) (p : Id nat (suc n) (suc m)) : Id nat n m = pred (p @ i) --- TODO: Clean the rest of this file! - -id (A : U) (a : A) : A = a - -data list (A : U) = nil | cons (a : A) (as : list A) - -l : list nat = cons one (cons two nil) - -append (A : U) : list A -> list A -> list A = split - nil -> id (list A) - cons x xs -> \(ys : list A) -> cons x (append A xs ys) - -reverse (A : U) : list A -> list A = split - nil -> nil - cons x xs -> append A (reverse A xs) (cons x nil) - idnat : nat -> nat = split zero -> zero suc n -> suc (idnat n) -test : Id (nat -> nat) idnat (id nat) = funExt nat (\(_ : nat) -> nat) idnat (id nat) rem +test : Id (nat -> nat) idnat (idfun nat) = funExt nat (\(_ : nat) -> nat) idnat (idfun nat) rem where rem : (n : nat) -> Id nat (idnat n) n = split zero -> refl nat zero suc n -> mapOnPath nat nat (\(x : nat) -> suc x) (idnat n) n (rem n) - -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) - -compEmpty (A : U) (a b : A) (p : Id A a b) : Id A a b = - comp A (p @ i) [ ] - -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 ] - - --- lemSimpl (A : U) (a b c : A) (p : Id A a b) (q q' : Id A b c) --- (s : Id (Id A a c) (compId A a b c p q) (compId A a b c p q')) : Id (Id A b c) q q' = --- comp A a [ (j = 0) -> ... ] - --- evalPN (i:j:k:_) LemSimpl [v,a,b,c,p,q,q',s] = --- Path j $ Path k $ comp Pos i v ss a --- where ss = mkSystem [(j ~> 0,fill Pos k v (mkSystem [(i ~> 0,a),(i ~> 1,q @@ j)]) (p @@ i)), --- (j ~> 1,fill Pos k v (mkSystem [(i ~> 0,a),(i ~> 1,(q' @@ j))]) (p @@ i)), --- (k ~> 0,p @@ i), --- (k ~> 1,(s @@ j) @@ i)] - -test (A : U) (a b : A) (p : Id A a b) : Id A a a = - p @ (i /\ -i) - --- testRefl (A : U) (a b : A) (p : Id A a b) : Id (Id A a a) (test A a b p) (refl A a) = --- fill j A a [ (i=0) -> p @ (i /\ -i) ] - - -lemSimpl (A : U) (a b c : A) (p : Id A a b) (q q' : Id A b c) - (s : Id (Id A a c) (compId A a b c p q) (compId A a b c p q')) : Id (Id A b c) q q' = - comp A a [ (j = 0) -> comp A (p @ i) [ (i = 1) -> q @ k /\ l], - (j = 1) -> comp A (p @ i) [ (i=1) -> q' @ k /\ l], - (k = 0) -> p, - (k = 1) -> s @ j ] diff --git a/examples/prelude.ctt b/examples/prelude.ctt index c2d7f9a..6e749f1 100644 --- a/examples/prelude.ctt +++ b/examples/prelude.ctt @@ -51,6 +51,25 @@ compDown (A : U) (a a' b b' : A) (p : Id A a a') (q: Id A b b') : Id A a' b' -> Id A a b = compUp A a' a b' b (inv A a a' p) (inv A b b' q) +idfun (A : U) (a : A) : A = a + +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) + +compEmpty (A : U) (a b : A) (p : Id A a b) : Id A a b = + comp A (p @ i) [ ] + +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 ] + +lemSimpl (A : U) (a b c : A) (p : Id A a b) (q q' : Id A b c) + (s : Id (Id A a c) (compId A a b c p q) (compId A a b c p q')) : Id (Id A b c) q q' = + comp A a [ (j = 0) -> comp A (p @ i) [ (i = 1) -> q @ k /\ l], + (j = 1) -> comp A (p @ i) [ (i=1) -> q' @ k /\ l], + (k = 0) -> p, + (k = 1) -> s @ j ] + 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 = diff --git a/examples/susp.ctt b/examples/susp.ctt index 905cbc9..161141d 100644 --- a/examples/susp.ctt +++ b/examples/susp.ctt @@ -1,6 +1,5 @@ module susp where --- import helix import circle data susp (A:U) = north | south | merid (a:A) @ north ~ south @@ -12,8 +11,6 @@ sphere : nat -> U = split -- The circle (S1) is equal to the 1-sphere (aka the suspension of Bool). -- (Similar to HoTT Book, Lemma 6.5.1) -one : nat = suc zero - sone : U = sphere one s1ToCircle : sone -> S1 = split