univalence

diff --git a/examples/sigma.ctt b/examples/sigma.ctt
index 4f0bee7d62da1485be14defbda8c4f93ef2ebc39..a442e9b7b5431b28de933cc4fdc697d440192a10 100644 (file)
--- a/examples/sigma.ctt
+++ b/examples/sigma.ctt
@@ -104,11 +104,6 @@ lemSigProp (A:U) (B:A-> U) (pB : (x:A) -> prop (B x)) (t u : sig A B) : Id U (Id
    rem1 : Id U ((p:T) * C p) T = lem6 T C rem
    rem2 : Id U (Id (sig A B) t u) ((p:T) * C p) = lemIdSig A B t u
 
-{-
-idSigProp (A:U)(B:A->U)(pB: (x:A) -> prop (B x))(t u : sig A B) (h: Id A t.1 u.1) : Id (sig A B) t u
- = fun2 A B t u (h,pB u.1  (subst A B t.1 u.1 h t.2) u.2)
--}
-
 setGroupoid (A:U) (sA:set A) (a0 a1:A) : set (Id A a0 a1) = propSet (Id A a0 a1) (sA a0 a1)
 
 propGroupoid (A:U) (pA: prop A) : groupoid A = setGroupoid A (propSet A pA)

diff --git a/examples/univalence.ctt b/examples/univalence.ctt
new file mode 100644 (file)
index 0000000..c6c5d5c
--- /dev/null
+++ b/examples/univalence.ctt
@@ -0,0 +1,18 @@
+module univalence where
+
+import retract
+import equiv
+
+-- we do something simpler than univalence
+
+transpIsEquiv (A B:U) (p:Id U A B) : isEquiv A B (\ (x:A) -> transport p x) =
+ transport (<i>isEquiv A (p@i) (\ (x:A) -> transport (<j>p@i/\j) x)) (idIsEquiv A)
+
+IdToEquiv (A B:U) (p: Id U A B) : Equiv A B = (\ (x:A) -> transport p x, transpIsEquiv A B p)
+
+EquivToId (A B:U) (z:Equiv A B) : Id U A B = isEquivEq A B z.1 z.2
+
+secIdEquiv (A B :U) (p : Id U A B) : Id (Id U A B) (EquivToId A B (IdToEquiv A B p)) p =
+ transport (<i>Id (Id U A (p@i)) (EquivToId A (p@i) (IdToEquiv A (p@i) (<j>p@i/\j))) (<j>p@i/\j))
+           (<i>isoIdRef A@-i)
+