define pointed maps, and prove some equivalences between types involving pointed...

diff --git a/examples/bool.ctt b/examples/bool.ctt
index 0759a624cd6a51b4f30ff269d8b61ad1094228d3..82e66b641bcc1fd6b5a12ce59ee4bf8c1ad51d79 100644 (file)
--- a/examples/bool.ctt
+++ b/examples/bool.ctt
@@ -11,6 +11,10 @@ caseBool (A : U) (f t : A) : bool -> A = split
  false -> f
  true  -> t
 
+indBool (A : bool -> U) (f : A false) (t : A true) : (b : bool) -> A b = split
+  false -> f
+  true  -> t
+
 falseNeqTrue : neg (Path bool false true) =
   \(h : Path bool false true) -> subst bool (caseBool U bool N0) false true h false
 
@@ -195,4 +199,3 @@ ntestUniv2 : bool =
  comp (<i> comp (<_>U) (comp (<_>U) bool [ (i = 0) -> <j> comp (<_>U) bool [ (j = 0) -> <i> Glue bool [ (i = 0) -> (bool,(\(x : bool) -> x,\(a : bool) -> ((a,<i> a),\(z : ((x : bool) * PathP (<i> bool) a x)) -> <i> (z.2 @ i,<j> z.2 @ (i /\ j))))), (i = 1) -> (bool,(comp (<i> bool -> bool) (\(x : bool) -> x) [],comp (<i> (y : bool) ->
   ((x : ((x : bool) * PathP (<j> bool) y (comp (<j> bool) (comp (<i> bool) x []) [ (i = 0) -> <j> comp (<k> bool) x [ (j = 1) -> <k> x ] ]))) * (y0 : ((x0 : bool) * PathP (<j> bool) y (comp (<j> bool) (comp (<i> bool) x0 []) [ (i = 0) -> <j> comp (<k> bool) x0 [ (j = 1) -> <k> x0 ] ]))) -> PathP (<j> ((x0 : bool) * PathP (<k> bool) y (comp (<j> bool) (comp (<i> bool) x0 []) [ (i = 0) -> <j> comp (<k> bool) x0 [ (j = 1) -> <k> x0 ] ]))) x y0)) (\(a : bool) -> ((a,<i> a),\(z : ((x : bool) * PathP (<i> bool) a x)) -> <i> (z.2 @ i,<j> z.2 @ (i /\ j)))) [])) ], (j = 1) -> <i> Glue bool [ (i = 0) -> (bool,(\(x : bool) -> x,\(a : bool) -> ((a,<i> a),\(z : ((x : bool) * PathP (<i> bool) a x)) -> <i> (z.2 @ i,<j> z.2 @ (i /\ j))))), (i = 1) -> (bool,(comp (<i> bool -> bool) (\(x : bool) -> x) [],comp (<i> (y : bool) ->
   ((x : ((x : bool) * PathP (<j> bool) y (comp (<j> bool) (comp (<i> bool) x []) [ (i = 0) -> <j> comp (<k> bool) x [ (j = 1) -> <k> x ] ]))) * (y0 : ((x0 : bool) * PathP (<j> bool) y (comp (<j> bool) (comp (<i> bool) x0 []) [ (i = 0) -> <j> comp (<k> bool) x0 [ (j = 1) -> <k> x0 ] ]))) -> PathP (<j> ((x0 : bool) * PathP (<k> bool) y (comp (<j> bool) (comp (<i> bool) x0 []) [ (i = 0) -> <j> comp (<k> bool) x0 [ (j = 1) -> <k> x0 ] ]))) x y0)) (\(a : bool) -> ((a,<i> a),\(z : ((x : bool) * PathP (<i> bool) a x)) -> <i> (z.2 @ i,<j> z.2 @ (i /\ j)))) [])) ] ], (i = 1) -> <j> bool ]) [ (i = 0) -> <j> bool, (i = 1) -> <j> bool ]) true []
-

diff --git a/examples/pointedMaps.ctt b/examples/pointedMaps.ctt
new file mode 100644 (file)
index 0000000..a425ea3
--- /dev/null
+++ b/examples/pointedMaps.ctt
@@ -0,0 +1,84 @@
+module pointedMaps where
+
+import bool
+
+-- Pointed types
+pType : U = (X : U) * X
+
+pt (Z : pType) : Z.1 = Z.2
+
+-- Maps between pointed types
+ppi' (A : pType) (B : A.1 -> U) (b0 : B (pt A)) : U = (f : (a : A.1) -> B a) * Path (B (pt A)) (f (pt A)) b0
+ppi (A : pType) (B : A.1 -> pType) : U = ppi' A (\(a : A.1) -> (B a).1) (pt (B (pt A)))
+pmap (A B : pType) : U = ppi A (\(a : A.1) -> B)
+
+pid (A : pType) : pmap A A = (\(a : A.1) -> a, <_> pt A)
+
+pcompose (A B C : pType) (g : pmap B C) (f : pmap A B) : pmap A C =
+  (\(a : A.1) -> (g.1 (f.1 a)), compPath C.1 (g.1 (f.1 (pt A))) (g.1 (pt B)) (pt C) (<i> g.1 (f.2 @ i)) g.2)
+
+-- constant pointed map
+pconst (A B : pType) : pmap A B = (\(a:A.1) -> pt B, <_> pt B )
+
+ppmap (A B : pType) : pType = (pmap A B, pconst A B)
+
+-- pointed equivalence
+pequiv (A B : pType) : U = (f : pmap A B) * isEquiv A.1 B.1 f.1
+
+pbool : pType = (bool, false)
+
+-- first test case: pointed maps from the booleans to A are the same as points in A
+ppmapBoolEquiv (A : pType) : pequiv (ppmap pbool A) A = (e, h) where
+  B : U = pmap pbool A
+  e1 : B -> A.1 = \(h : B) -> h.1 true
+  p : Path A.1 (e1 (pconst pbool A)) (pt A) = <_> pt A
+  e : pmap (ppmap pbool A) A = (e1, p)
+  inv : A.1 -> B = \(a : A.1) -> (caseBool A.1 (pt A) a, <_> (pt A))
+  q (a : A.1) : Path A.1 (e1 (inv a)) a = <_> a
+  r (f : B) : Path B (inv (e1 f)) f =
+    <i> (\(b : bool) -> indBool (\(b : bool) -> Path A.1 ((inv (e1 f)).1 b) (f.1 b))
+                                (<i> f.2 @ -i)
+                                (<_> f.1 true) b @ i,
+          <j> f.2 @ (-i \/ j))
+  h : isEquiv B A.1 e.1 = isoToEquiv B A.1 e.1 inv q r
+
+-- reversing the arguments of a binary pointed map
+revPpmap (A B C : pType) : pmap (ppmap A (ppmap B C)) (ppmap B (ppmap A C)) = (e1, e0) where
+  bc  : U = pmap B C
+  ac  : U = pmap A C
+  abc : U = pmap A (ppmap B C)
+  bac : U = pmap B (ppmap A C)
+  BC  : pType = ppmap B C
+  AC  : pType = ppmap A C
+  ABC : pType = ppmap A (ppmap B C)
+  BAC : pType = ppmap B (ppmap A C)
+  e111 (f : abc) (b : B.1) (a : A.1) : C.1 = (f.1 a).1 b
+  e110 (f : abc) (b : B.1) : Path C.1 (e111 f b (pt A)) (pt C) = <i> (f.2 @ i).1 b
+  e11 (f : abc) (b : B.1) : ac = (e111 f b, e110 f b)
+  e10 (f : abc) : Path ac (e11 f (pt B)) (pconst A C) =
+    <i> (\(a : A.1) -> (f.1 a).2 @ i, <j> (f.2 @ j).2 @ i)
+  e1 (f : abc) : bac = (e11 f, e10 f)
+  e0 : Path bac (e1 (pconst A BC)) (pconst B AC) =
+    <i> (\(b : B.1) -> (\(a : A.1) -> pt C, <_> pt C), <_> (\(a : A.1) -> pt C, <_> pt C))
+
+revRevPpmap (A B C : pType) (f : pmap A (ppmap B C)) :
+  Path (pmap A (ppmap B C)) ((revPpmap B A C).1 ((revPpmap A B C).1 f)) f = p where
+  bc  : U = pmap B C
+  ac  : U = pmap A C
+  abc : U = pmap A (ppmap B C)
+  bac : U = pmap B (ppmap A C)
+  BC  : pType = ppmap B C
+  AC  : pType = ppmap A C
+  ABC : pType = ppmap A (ppmap B C)
+  BAC : pType = ppmap B (ppmap A C)
+  e   : pmap ABC BAC = revPpmap A B C
+  ei  : pmap BAC ABC = revPpmap B A C
+  p1 (a : A.1) : Path bc ((ei.1 (e.1 f)).1 a) (f.1 a) =
+    <i> (\(b : B.1) -> (f.1 a).1 b, <j> (f.1 a).2 @ j)
+  p   : Path abc (ei.1 (e.1 f)) f =
+    <i> (\(a : A.1) -> p1 a @ i,
+      <j> (\(b : B.1) -> (f.2 @ j).1 b, <k> (f.2 @ j).2 @ k))
+
+symmPpmap (A B C : pType) : pequiv (ppmap A (ppmap B C)) (ppmap B (ppmap A C)) =
+  (revPpmap A B C, isoToEquiv (pmap A (ppmap B C)) (pmap B (ppmap A C))
+    (revPpmap A B C).1 (revPpmap B A C).1 (revRevPpmap B A C) (revRevPpmap A B C))