From 1d9c17342a88ca21e1720562df47f9370eba762c Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Thu, 9 Apr 2015 21:45:18 -0400
Subject: [PATCH] feat(hit): define mapping cylinder, coequalizer and quotient
 in terms of colimit

---
 hott/hit/coeq.hlean       | 79 ++++++++++++++++++++++++++++++++++++++
 hott/hit/cylinder.hlean   | 75 +++++++++++++++++++++++++++++-------
 hott/hit/pushout.hlean    | 10 ++---
 hott/hit/quotient.hlean   | 80 +++++++++++++++++++++++++++++++++++++++
 hott/hit/suspension.hlean |  2 +-
 hott/init/hit.hlean       | 49 +-----------------------
 6 files changed, 227 insertions(+), 68 deletions(-)
 create mode 100644 hott/hit/coeq.hlean
 create mode 100644 hott/hit/quotient.hlean

diff --git a/hott/hit/coeq.hlean b/hott/hit/coeq.hlean
new file mode 100644
index 000000000..6ebe1c410
--- /dev/null
+++ b/hott/hit/coeq.hlean
@@ -0,0 +1,79 @@
+/-
+Copyright (c) 2015 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: hit.coeq
+Authors: Floris van Doorn
+
+Declaration of the coequalizer
+-/
+
+import .colimit
+
+open colimit bool eq
+
+namespace coeq
+context
+
+universe u
+parameters {A B : Type.{u}} (f g : A → B)
+
+  definition coeq_diag [reducible] : diagram :=
+  diagram.mk bool
+             bool
+             (λi, bool.rec_on i A B)
+             (λj, ff)
+             (λj, tt)
+             (λj, bool.rec_on j f g)
+
+  local notation `D` := coeq_diag
+
+  definition coeq := colimit coeq_diag -- TODO: define this in root namespace
+  local attribute coeq_diag [instance]
+
+  definition coeq_i (x : B) : coeq :=
+  @ι _ _ x
+
+  /- cp is the name Coq uses. I don't know what it abbreviates, but at least it's short :-) -/
+  definition cp (x : A) : coeq_i (f x) = coeq_i (g x) :=
+  @cglue _ _ x ⬝ (@cglue _ _ x)⁻¹
+
+  protected definition rec {P : coeq → Type} (P_i : Π(x : B), P (coeq_i x))
+    (Pcp : Π(x : A), cp x ▹ P_i (f x) = P_i (g x)) (y : coeq) : P y :=
+  begin
+    fapply (@colimit.rec_on _ _ y),
+    { intros [i, x], cases i,
+        exact (@cglue _ _ x ▹ P_i (f x)),
+        apply P_i},
+    { intros [j, x], cases j,
+        exact idp,
+      esimp [coeq_diag],
+      apply tr_eq_of_eq_inv_tr,
+      apply concat, rotate 1, apply tr_con,
+      rewrite -Pcp}
+  end
+
+  protected definition rec_on [reducible] {P : coeq → Type} (y : coeq)
+    (P_i : Π(x : B), P (coeq_i x)) (Pcp : Π(x : A), cp x ▹ P_i (f x) = P_i (g x)) : P y :=
+  rec P_i Pcp y
+
+  protected definition elim {P : Type} (P_i : B → P)
+    (Pcp : Π(x : A), P_i (f x) = P_i (g x)) (y : coeq) : P :=
+  rec P_i (λx, !tr_constant ⬝ Pcp x) y
+
+  protected definition elim_on [reducible] {P : Type} (y : coeq) (P_i : B → P)
+    (Pcp : Π(x : A), P_i (f x) = P_i (g x)) : P :=
+  elim P_i Pcp y
+
+  definition rec_cp {P : coeq → Type} (P_i : Π(x : B), P (coeq_i x))
+    (Pcp : Π(x : A), cp x ▹ P_i (f x) = P_i (g x))
+      (x : A) : apD (rec P_i Pcp) (cp x) = sorry ⬝ Pcp x ⬝ sorry :=
+  sorry
+
+  definition elim_cp {P : Type} (P_i : B → P) (Pcp : Π(x : A), P_i (f x) = P_i (g x))
+    (x : A) : ap (elim P_i Pcp) (cp x) = sorry ⬝ Pcp x ⬝ sorry :=
+  sorry
+
+end
+
+end coeq
diff --git a/hott/hit/cylinder.hlean b/hott/hit/cylinder.hlean
index 1f0dd963e..62c098cac 100644
--- a/hott/hit/cylinder.hlean
+++ b/hott/hit/cylinder.hlean
@@ -5,29 +5,76 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Module: hit.cylinder
 Authors: Floris van Doorn
 
-Mapping cylinders
+Declaration of mapping cylinders
 -/
 
-/- The hit mapping cylinder is primitive, declared in init.hit. -/
+import .colimit
 
-open eq
+open colimit bool unit eq
 
 namespace cylinder
+context
 
-  variables {A B : Type} {f : A → B}
+universe u
+parameters {A B : Type.{u}} (f : A → B)
 
-  protected definition elim {P : Type} (Pbase : B → P) (Ptop  : A → P)
-    (Pseg  : Π(a : A), Ptop a = Pbase (f a)) {b : B} (x : cylinder f b) : P :=
-  cylinder.rec Pbase Ptop (λa, !tr_constant ⬝ Pseg a) x
+  definition cylinder_diag [reducible] : diagram :=
+  diagram.mk bool
+             unit.{0}
+             (λi, bool.rec_on i A B)
+             (λj, ff)
+             (λj, tt)
+             (λj, f)
 
-  protected definition elim_on [reducible] {P : Type} {b : B} (x : cylinder f b)
-    (Pbase : B → P) (Ptop : A → P)
-    (Pseg  : Π(a : A), Ptop a = Pbase (f a)) : P :=
-  cylinder.elim Pbase Ptop Pseg x
+  local notation `D` := cylinder_diag
 
-  definition elim_seg {P : Type} (Pbase : B → P) (Ptop  : A → P)
-    (Pseg  : Π(a : A), Ptop a = Pbase (f a)) {b : B} (x : cylinder f b) (a : A) :
-      ap (elim Pbase Ptop Pseg) (seg f a) = sorry ⬝ Pseg a ⬝ sorry :=
+  definition cylinder := colimit cylinder_diag -- TODO: define this in root namespace
+  local attribute cylinder_diag [instance]
+
+  definition base (b : B) : cylinder :=
+  @ι _ _ b
+
+  definition top (a : A) : cylinder :=
+  @ι _ _ a
+
+  definition seg (a : A) : base (f a) = top a :=
+  @cglue _ star a
+
+  protected definition rec {P : cylinder → Type}
+    (Pbase : Π(b : B), P (base b)) (Ptop : Π(a : A), P (top a))
+    (Pseg : Π(a : A), seg a ▹ Pbase (f a) = Ptop a) (x : cylinder) : P x :=
+  begin
+    fapply (@colimit.rec_on _ _ x),
+    { intros [i, x], cases i,
+        apply Ptop,
+        apply Pbase},
+    { intros [j, x], cases j, apply Pseg}
+  end
+
+  protected definition rec_on [reducible] {P : cylinder → Type} (x : cylinder)
+    (Pbase : Π(b : B), P (base b)) (Ptop  : Π(a : A), P (top a))
+    (Pseg  : Π(a : A), seg a ▹ Pbase (f a) = Ptop a) : P x :=
+  rec Pbase Ptop Pseg x
+
+  protected definition elim {P : Type} (Pbase : B → P) (Ptop : A → P)
+    (Pseg : Π(a : A), Pbase (f a) = Ptop a) (x : cylinder) : P :=
+  rec Pbase Ptop (λa, !tr_constant ⬝ Pseg a) x
+
+  protected definition elim_on [reducible] {P : Type} (x : cylinder) (Pbase : B → P) (Ptop : A → P)
+    (Pseg : Π(a : A), Pbase (f a) = Ptop a) : P :=
+  elim Pbase Ptop Pseg x
+
+  definition rec_seg {P : cylinder → Type}
+    (Pbase : Π(b : B), P (base b)) (Ptop : Π(a : A), P (top a))
+    (Pseg : Π(a : A), seg a ▹ Pbase (f a) = Ptop a)
+      (a : A) : apD (rec Pbase Ptop Pseg) (seg a) = sorry ⬝ Pseg a ⬝ sorry :=
   sorry
 
+  definition elim_seg {P : Type} (Pbase : B → P) (Ptop : A → P)
+    (Pseg : Π(a : A), Pbase (f a) = Ptop a)
+    (a : A) : ap (elim Pbase Ptop Pseg) (seg a) = sorry ⬝ Pseg a ⬝ sorry :=
+  sorry
+
+end
+
 end cylinder
diff --git a/hott/hit/pushout.hlean b/hott/hit/pushout.hlean
index 85f6a9eac..939343c82 100644
--- a/hott/hit/pushout.hlean
+++ b/hott/hit/pushout.hlean
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Module: hit.pushout
 Authors: Floris van Doorn
 
-Declaration of pushout
+Declaration of the pushout
 -/
 
 import .colimit
@@ -46,15 +46,12 @@ parameters {TL BL TR : Type.{u}} (f : TL → BL) (g : TL → TR)
   definition pushout := colimit pushout_diag -- TODO: define this in root namespace
   local attribute pushout_diag [instance]
 
- definition inl (x : BL) : pushout :=
+  definition inl (x : BL) : pushout :=
   @ι _ _ x
 
   definition inr (x : TR) : pushout :=
   @ι _ _ x
 
-  definition coherence (x : TL) : inl (f x) = @ι _ _ x :=
-  @cglue _ _ x
-
   definition glue (x : TL) : inl (f x) = inr (g x) :=
   @cglue _ _ x ⬝ (@cglue _ _ x)⁻¹
 
@@ -64,7 +61,7 @@ parameters {TL BL TR : Type.{u}} (f : TL → BL) (g : TL → TR)
   begin
     fapply (@colimit.rec_on _ _ y),
     { intros [i, x], cases i,
-       exact (coherence x ▹ Pinl (f x)),
+       exact (@cglue _ _ x ▹ Pinl (f x)),
        apply Pinl,
        apply Pinr},
     { intros [j, x], cases j,
@@ -84,6 +81,7 @@ parameters {TL BL TR : Type.{u}} (f : TL → BL) (g : TL → TR)
     (Pglue : Π(x : TL), glue x ▹ Pinl (f x) = Pinr (g x)) : P y :=
   rec Pinl Pinr Pglue y
 
+  --these definitions are needed until we have them definitionally
   definition rec_inl {P : pushout → Type} (Pinl : Π(x : BL), P (inl x))
     (Pinr : Π(x : TR), P (inr x)) (Pglue : Π(x : TL), glue x ▹ Pinl (f x) = Pinr (g x))
       (x : BL) : rec Pinl Pinr Pglue (inl x) = Pinl x :=
diff --git a/hott/hit/quotient.hlean b/hott/hit/quotient.hlean
new file mode 100644
index 000000000..a0536e672
--- /dev/null
+++ b/hott/hit/quotient.hlean
@@ -0,0 +1,80 @@
+/-
+Copyright (c) 2015 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: hit.quotient
+Authors: Floris van Doorn
+
+Declaration of set-quotients
+-/
+
+/-
+We aim to model
+HIT quotient : Type :=
+   | class_of : A -> quotient
+   | eq_of_rel : Πa a', R a a' → class_of a = class_of a'
+   | is_hset_quotient : is_hset quotient
+-/
+
+import .coeq .trunc
+
+open coeq eq is_trunc trunc
+
+namespace quotient
+context
+universe u
+parameters {A : Type.{u}} (R : A → A → hprop.{u})
+
+  structure total : Type := {pt1 : A} {pt2 : A} (rel : R pt1 pt2)
+  open total
+
+  definition quotient : Type :=
+  trunc 0 (coeq (pt1 : total → A) (pt2 : total → A))
+
+  definition class_of (a : A) : quotient :=
+  tr (coeq_i _ _ a)
+
+  definition eq_of_rel {a a' : A} (H : R a a') : class_of a = class_of a' :=
+  ap tr (cp _ _ (total.mk H))
+
+  definition is_hset_quotient : is_hset quotient :=
+  by unfold quotient; exact _
+
+  protected definition rec {P : quotient → Type} [Pt : Πaa, is_trunc 0 (P aa)]
+    (Pc : Π(a : A), P (class_of a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel H ▹ Pc a = Pc a')
+    (x : quotient) : P x :=
+  begin
+    apply (@trunc.rec_on _ _ P x),
+    { intro x', apply Pt},
+    { intro y, fapply (coeq.rec_on _ _ y),
+      { exact Pc},
+      { intro H, cases H with [a, a', H], esimp [is_typeof],
+        --rewrite (transport_compose P tr (cp pt1 pt2 (total.mk H)) (Pc a))
+        apply concat, apply transport_compose;apply Pp}}
+  end
+
+  protected definition rec_on [reducible] {P : quotient → Type} (x : quotient)
+    [Pt : Πaa, is_trunc 0 (P aa)] (Pc : Π(a : A), P (class_of a))
+    (Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel H ▹ Pc a = Pc a') : P x :=
+  rec Pc Pp x
+
+  definition rec_eq_of_rel {P : quotient → Type} [Pt : Πaa, is_trunc 0 (P aa)]
+    (Pc : Π(a : A), P (class_of a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel H ▹ Pc a = Pc a')
+    {a a' : A} (H : R a a') : apD (rec Pc Pp) (eq_of_rel H) = sorry ⬝ Pp H ⬝ sorry :=
+  sorry
+
+  protected definition elim {P : Type} [Pt : is_trunc 0 P] (Pc : A → P)
+    (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') (x : quotient) : P :=
+  rec Pc (λa a' H, !tr_constant ⬝ Pp H) x
+
+  protected definition elim_on [reducible] {P : Type} (x : quotient) [Pt : is_trunc 0 P]
+    (Pc : A → P) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a')  : P :=
+  elim Pc Pp x
+
+  protected definition elim_eq_of_rel {P : Type} [Pt : is_trunc 0 P] (Pc : A → P)
+    (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') {a a' : A} (H : R a a')
+    : ap (elim Pc Pp) (eq_of_rel H) = sorry ⬝ Pp H ⬝ sorry :=
+  sorry
+
+end
+end quotient
diff --git a/hott/hit/suspension.hlean b/hott/hit/suspension.hlean
index e2215dcaa..d7ddc440e 100644
--- a/hott/hit/suspension.hlean
+++ b/hott/hit/suspension.hlean
@@ -49,7 +49,7 @@ namespace suspension
 
   protected definition elim_on [reducible] {A : Type} {P : Type} (x : suspension A)
     (PN : P) (PS : P)  (Pm : A → PN = PS) : P :=
-  rec PN PS (λa, !tr_constant ⬝ Pm a) x
+  elim PN PS Pm x
 
   protected definition elim_merid {A : Type} {P : Type} (PN : P) (PS : P) (Pm : A → PN = PS)
     (x : suspension A) (a : A) : ap (elim PN PS Pm) (merid a) = sorry ⬝ Pm a ⬝ sorry :=
diff --git a/hott/init/hit.hlean b/hott/init/hit.hlean
index 2f784f5aa..7698f033c 100644
--- a/hott/init/hit.hlean
+++ b/hott/init/hit.hlean
@@ -15,10 +15,9 @@ import .trunc
 open is_trunc eq
 
 /-
-  We take three higher inductive types (hits) as primitive notions in Lean. We define all other hits
-  in terms of these three hits. The hits which are primitive are
+  We take two higher inductive types (hits) as primitive notions in Lean. We define all other hits
+  in terms of these two hits. The hits which are primitive are
     - n-truncation
-    - the mapping cylinder
     - general colimits
   For each of the hits we add the following constants:
     - the type formation
@@ -53,50 +52,6 @@ namespace trunc
 
 end trunc
 
-constant cylinder.{u v} {A : Type.{u}} {B : Type.{v}} (f : A → B) : B → Type.{max u v}
-
-namespace cylinder
-
-  constant base {A B : Type} (f : A → B) (b : B) : cylinder f b
-  constant top  {A B : Type} (f : A → B) (a : A) : cylinder f (f a)
-  constant seg  {A B : Type} (f : A → B) (a : A) : top f a = base f (f a)
-
-  axiom is_trunc_trunc (n : trunc_index) (A : Type) : is_trunc n (trunc n A)
-
-  attribute is_trunc_trunc [instance]
-
-  /-protected-/ constant rec {A B : Type} {f : A → B} {P : Π{b : B}, cylinder f b → Type}
-    (Pbase : Π(b : B), P (base f b)) (Ptop  : Π(a : A), P (top f a))
-    (Pseg  : Π(a : A), seg f a ▹ Ptop a = Pbase (f a))
-      : Π{b : B} (x : cylinder f b), P x
-
-  protected definition rec_on [reducible] {A B : Type} {f : A → B}
-    {P : Π{b : B}, cylinder f b → Type} {b : B} (x : cylinder f b) (Pbase : Π(b : B), P (base f b))
-    (Ptop  : Π(a : A), P (top f a)) (Pseg  : Π(a : A), seg f a ▹ Ptop a = Pbase (f a)) : P x :=
-  cylinder.rec Pbase Ptop Pseg x
-
-  definition rec_base [reducible] {A B : Type} {f : A → B} {P : Π{b : B}, cylinder f b → Type}
-    (Pbase : Π(b : B), P (base f b)) (Ptop  : Π(a : A), P (top f a))
-    (Pseg  : Π(a : A), seg f a ▹ Ptop a = Pbase (f a)) (b : B) :
-      cylinder.rec Pbase Ptop Pseg (base f b) = Pbase b :=
-  sorry --idp
-
-  definition rec_top [reducible] {A B : Type} {f : A → B} {P : Π{b : B}, cylinder f b → Type}
-    (Pbase : Π(b : B), P (base f b)) (Ptop  : Π(a : A), P (top f a))
-    (Pseg  : Π(a : A), seg f a ▹ Ptop a = Pbase (f a)) (a : A) :
-      cylinder.rec Pbase Ptop Pseg (top f a) = Ptop a :=
-  sorry --idp
-
-  definition rec_seg [reducible] {A B : Type} {f : A → B} {P : Π{b : B}, cylinder f b → Type}
-    (Pbase : Π(b : B), P (base f b)) (Ptop  : Π(a : A), P (top f a))
-    (Pseg  : Π(a : A), seg f a ▹ Ptop a = Pbase (f a)) (a : A) :
-      apD (cylinder.rec Pbase Ptop Pseg) (seg f a) = sorry ⬝ Pseg a ⬝ sorry :=
-  --the sorry's in the statement can be removed when rec_base/rec_top are definitional
-  sorry
-
-end cylinder
-
-
 namespace colimit
 structure diagram [class] :=
   (Iob : Type)