From: Anders Mörtberg Date: Thu, 14 Jan 2016 14:59:51 +0000 (-0500) Subject: make bool compile and move tests using univalence for bool X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=c0237f5181741e9181cb2b70c049c42e219e082c;p=cubicaltt.git make bool compile and move tests using univalence for bool --- diff --git a/examples/bool.ctt b/examples/bool.ctt index c542ce4..a101367 100644 --- a/examples/bool.ctt +++ b/examples/bool.ctt @@ -1,13 +1,11 @@ module bool where import hedberg +import univalence data bool = false | true - -- Proof that bool is a set using hedberg: - - caseBool (A : U) (f t : A) : bool -> A = split false -> f true -> t @@ -32,9 +30,7 @@ boolDec : (b1 b2 : bool) -> dec (Id bool b1 b2) = split setbool' : set bool = hedberg bool boolDec - -- Direct proof that bool is a set: - lem1 : (y:bool) (p:Id bool true y) -> Id bool true y = split false -> \ (p : Id bool true false) -> p true -> \ (p : Id bool true true) -> true @@ -48,7 +44,7 @@ lem3 : prop (Id bool true true) = lem4 : (y:bool) (p:Id bool false y) -> Id bool false y = split false -> \ (p : Id bool false false) -> false - true -> \ (p : Id bool false true) -> p + true -> \ (p : Id bool false true) -> p lem5 : (x y :bool) (p:Id bool false x) (q:Id bool false y) -> Id bool x y = split false -> \ (y:bool) (p:Id bool false false) (q:Id bool false y) -> lem4 y q @@ -114,7 +110,7 @@ boolToF2K : (b : bool) -> Id bool (f2ToBool (boolToF2 b)) b = split boolEqF2 : Id U bool F2 = isoId bool F2 boolToF2 f2ToBool f2ToBoolK boolToF2K - + negF2 : F2 -> F2 = subst U (\(X : U) -> (X -> X)) bool F2 boolEqF2 negBool -- lemTest (A : U) : (B : U) (p : Id U A B) (a : A) -> IdP p a (transport p a) = @@ -145,7 +141,7 @@ squareBoolF2 : Square U bool bool bool F2 (refl U bool) boolEqF2 (refl U bool) boolEqF2 = boolEqF2 @ i /\ j -test5 : IdP boolEqF2 true oneF2 = +test5 : IdP boolEqF2 true oneF2 = comp ( boolEqF2 @ i /\ j) true [] test6 : Id bool true true = @@ -161,4 +157,16 @@ test9 : Id U F2 F2 = comp ( Id U (boolEqF2 @ i) (boolEqF2 @ i)) (refl U bool) [] p : Id U F2 bool = comp (<_> U) bool [ (i = 0) -> boolEqF2, (i = 1) -> <_> bool] -q : Id U F2 F2 = p @ (i /\ - i) \ No newline at end of file +q : Id U F2 F2 = p @ (i /\ - i) + + +-- A small test of univalence using boolean negation +isEquivNegBool : isEquiv bool bool negBool = + gradLemma bool bool negBool negBool negBoolK negBoolK + +eqBool : Id U bool bool = + trans (equiv bool bool) (Id U bool bool) + ( corrUniv bool bool @ -i) (negBool,isEquivNegBool) + +testf : bool = trans bool bool eqBool true +testt : bool = trans bool bool eqBool false diff --git a/examples/univalence.ctt b/examples/univalence.ctt index 58c6920..2a18e4f 100644 --- a/examples/univalence.ctt +++ b/examples/univalence.ctt @@ -6,7 +6,6 @@ module univalence where import equiv --- import bool ------------------------------------------------------------------------------ -- Proof of univalence using unglue: @@ -164,20 +163,6 @@ corrUniv' (A B : U) : equiv (Id U A B) (equiv A B) = -- ((x : ((x : bool) * IdP ( bool) y (comp ( bool) (comp ( bool) x []) [ (i = 0) -> comp ( bool) x [ (j = 1) -> x ] ]))) * (y0 : ((x0 : bool) * IdP ( bool) y (comp ( bool) (comp ( bool) x0 []) [ (i = 0) -> comp ( bool) x0 [ (j = 1) -> x0 ] ]))) -> IdP ( ((x0 : bool) * IdP ( bool) y (comp ( bool) (comp ( bool) x0 []) [ (i = 0) -> comp ( bool) x0 [ (j = 1) -> x0 ] ]))) x y0)) (\(a : bool) -> ((a, a),\(z : ((x : bool) * IdP ( bool) a x)) -> (z.2 @ i, z.2 @ (i /\ j)))) [])) ] ], (i = 1) -> bool ]) [ (i = 0) -> bool, (i = 1) -> bool ]) true [] --- -- A small test of univalence using boolean negation --- isEquivNegBool : isEquiv bool bool negBool = --- gradLemma bool bool negBool negBool negBoolK negBoolK - --- eqBool : Id U bool bool = --- trans (equiv bool bool) (Id U bool bool) --- ( corrUniv bool bool @ -i) (negBool,isEquivNegBool) - --- test1 : bool = trans bool bool eqBool true --- test2 : bool = trans bool bool eqBool false - - - - -- ------------------------------------------------------------------------------ -- -- The direct proof of univalence using transEquiv which is too slow -- -- to normalize: