From 5328486d49adecb078d60035e20d08263db9474e Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Fri, 20 Nov 2015 17:47:11 -0500
Subject: [PATCH] feat(hit): add elimination rule to propositions

---
 hott/algebra/trunc_group.hlean | 10 +++++-----
 hott/hit/coeq.hlean            |  9 ++++++++-
 hott/hit/colimit.hlean         | 19 ++++++++++++++++++-
 hott/hit/pushout.hlean         | 10 +++++++++-
 hott/hit/quotient.hlean        |  9 ++++++++-
 hott/hit/set_quotient.hlean    | 22 +++++++++++++++-------
 6 files changed, 63 insertions(+), 16 deletions(-)

diff --git a/hott/algebra/trunc_group.hlean b/hott/algebra/trunc_group.hlean
index efbf6b79f6..969961d0a6 100644
--- a/hott/algebra/trunc_group.hlean
+++ b/hott/algebra/trunc_group.hlean
@@ -41,7 +41,7 @@ namespace algebra
   local postfix ⁻¹ := trunc_inv
   local infix * := trunc_mul
 
-  definition trunc_mul_assoc [unfold 9 10 11] (g₁ g₂ g₃ : G) : g₁ * g₂ * g₃ = g₁ * (g₂ * g₃) :=
+  theorem trunc_mul_assoc (g₁ g₂ g₃ : G) : g₁ * g₂ * g₃ = g₁ * (g₂ * g₃) :=
   begin
     apply trunc.rec_on g₁, intro p₁,
     apply trunc.rec_on g₂, intro p₂,
@@ -49,25 +49,25 @@ namespace algebra
     exact ap tr !mul_assoc,
   end
 
-  definition trunc_one_mul [unfold 9] (g : G) : 1 * g = g :=
+  theorem trunc_one_mul (g : G) : 1 * g = g :=
   begin
     apply trunc.rec_on g, intro p,
     exact ap tr !one_mul
   end
 
-  definition trunc_mul_one [unfold 9] (g : G) : g * 1 = g :=
+  theorem trunc_mul_one (g : G) : g * 1 = g :=
   begin
     apply trunc.rec_on g, intro p,
     exact ap tr !mul_one
   end
 
-  definition trunc_mul_left_inv [unfold 9] (g : G) : g⁻¹ * g = 1 :=
+  theorem trunc_mul_left_inv (g : G) : g⁻¹ * g = 1 :=
   begin
     apply trunc.rec_on g, intro p,
     exact ap tr !mul_left_inv
   end
 
-  definition trunc_mul_comm [unfold 10 11] (mul_comm : ∀a b, mul a b = mul b a) (g h : G)
+  theorem trunc_mul_comm (mul_comm : ∀a b, mul a b = mul b a) (g h : G)
     : g * h = h * g :=
   begin
     apply trunc.rec_on g, intro p,
diff --git a/hott/hit/coeq.hlean b/hott/hit/coeq.hlean
index 7cc5975fb7..2b1d311a03 100644
--- a/hott/hit/coeq.hlean
+++ b/hott/hit/coeq.hlean
@@ -8,7 +8,7 @@ Declaration of the coequalizer
 
 import .quotient
 
-open quotient eq equiv equiv.ops
+open quotient eq equiv equiv.ops is_trunc
 
 namespace coeq
 section
@@ -74,6 +74,13 @@ parameters {A B : Type.{u}} (f g : A → B)
     (x : A) : transport (elim_type P_i Pcp) (cp x) = Pcp x :=
   by rewrite [tr_eq_cast_ap_fn,↑elim_type,elim_cp];apply cast_ua_fn
 
+  protected definition rec_hprop {P : coeq → Type} [H : Πx, is_hprop (P x)]
+    (P_i : Π(x : B), P (coeq_i x)) (y : coeq) : P y :=
+  rec P_i (λa, !is_hprop.elimo) y
+
+  protected definition elim_hprop {P : Type} [H : is_hprop P] (P_i : B → P) (y : coeq) : P :=
+  elim P_i (λa, !is_hprop.elim) y
+
 end
 
 end coeq
diff --git a/hott/hit/colimit.hlean b/hott/hit/colimit.hlean
index 9b50036746..93a938e167 100644
--- a/hott/hit/colimit.hlean
+++ b/hott/hit/colimit.hlean
@@ -7,7 +7,7 @@ Definition of general colimits and sequential colimits.
 -/
 
 /- definition of a general colimit -/
-open eq nat quotient sigma equiv equiv.ops
+open eq nat quotient sigma equiv equiv.ops is_trunc
 
 namespace colimit
 section
@@ -85,6 +85,14 @@ section
       {j : J} (x : A (dom j)) : transport (elim_type Pincl Pglue) (cglue j x) = Pglue j x :=
   by rewrite [tr_eq_cast_ap_fn,↑elim_type,elim_cglue];apply cast_ua_fn
 
+  protected definition rec_hprop {P : colimit → Type} [H : Πx, is_hprop (P x)]
+    (Pincl : Π⦃i : I⦄ (x : A i), P (ι x)) (y : colimit) : P y :=
+  rec Pincl (λa b, !is_hprop.elimo) y
+
+  protected definition elim_hprop {P : Type} [H : is_hprop P] (Pincl : Π⦃i : I⦄ (x : A i), P)
+    (y : colimit) : P :=
+  elim Pincl (λa b, !is_hprop.elim) y
+
 end
 end colimit
 
@@ -167,6 +175,15 @@ section
       : transport (elim_type Pincl Pglue) (glue a) = Pglue a :=
   by rewrite [tr_eq_cast_ap_fn,↑elim_type,elim_glue];apply cast_ua_fn
 
+  protected definition rec_hprop {P : seq_colim → Type} [H : Πx, is_hprop (P x)]
+    (Pincl : Π⦃n : ℕ⦄ (a : A n), P (sι a)) (aa : seq_colim) : P aa :=
+  rec Pincl (λa b, !is_hprop.elimo) aa
+
+  protected definition elim_hprop {P : Type} [H : is_hprop P] (Pincl : Π⦃n : ℕ⦄ (a : A n), P)
+    : seq_colim → P :=
+  elim Pincl (λa b, !is_hprop.elim)
+
+
 end
 end seq_colim
 
diff --git a/hott/hit/pushout.hlean b/hott/hit/pushout.hlean
index 5608a3ccc8..cc0a6b7d04 100644
--- a/hott/hit/pushout.hlean
+++ b/hott/hit/pushout.hlean
@@ -8,7 +8,7 @@ Declaration of the pushout
 
 import .quotient cubical.square
 
-open quotient eq sum equiv equiv.ops
+open quotient eq sum equiv equiv.ops is_trunc
 
 namespace pushout
 section
@@ -83,6 +83,14 @@ parameters {TL BL TR : Type} (f : TL → BL) (g : TL → TR)
     : transport (elim_type Pinl Pinr Pglue) (glue x) = Pglue x :=
   by rewrite [tr_eq_cast_ap_fn,↑elim_type,elim_glue];apply cast_ua_fn
 
+  protected definition rec_hprop {P : pushout → Type} [H : Πx, is_hprop (P x)]
+    (Pinl : Π(x : BL), P (inl x)) (Pinr : Π(x : TR), P (inr x)) (y : pushout) :=
+  rec Pinl Pinr (λx, !is_hprop.elimo) y
+
+  protected definition elim_hprop {P : Type} [H : is_hprop P] (Pinl : BL → P) (Pinr : TR → P)
+    (y : pushout) : P :=
+  elim Pinl Pinr (λa, !is_hprop.elim) y
+
 end
 end pushout
 
diff --git a/hott/hit/quotient.hlean b/hott/hit/quotient.hlean
index 7602b66ca5..a2bada60fa 100644
--- a/hott/hit/quotient.hlean
+++ b/hott/hit/quotient.hlean
@@ -16,7 +16,7 @@ See also .set_quotient
 
 import arity cubical.squareover types.arrow cubical.pathover2
 
-open eq equiv sigma sigma.ops equiv.ops pi
+open eq equiv sigma sigma.ops equiv.ops pi is_trunc
 
 namespace quotient
 
@@ -38,6 +38,13 @@ namespace quotient
     rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑quotient.elim,rec_eq_of_rel],
   end
 
+  protected definition rec_hprop {A : Type} {R : A → A → Type} {P : quotient R → Type}
+    [H : Πx, is_hprop (P x)] (Pc : Π(a : A), P (class_of R a)) (x : quotient R) : P x :=
+  quotient.rec Pc (λa a' H, !is_hprop.elimo) x
+
+  protected definition elim_hprop {P : Type} [H : is_hprop P] (Pc : A → P) (x : quotient R) : P :=
+  quotient.elim Pc (λa a' H, !is_hprop.elim) x
+
   protected definition elim_type (Pc : A → Type)
     (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a ≃ Pc a') : quotient R → Type :=
   quotient.elim Pc (λa a' H, ua (Pp H))
diff --git a/hott/hit/set_quotient.hlean b/hott/hit/set_quotient.hlean
index 5b8c6f7a45..89a7eb9dfe 100644
--- a/hott/hit/set_quotient.hlean
+++ b/hott/hit/set_quotient.hlean
@@ -63,6 +63,14 @@ section
     rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑elim,rec_eq_of_rel],
   end
 
+  protected definition rec_hprop {P : set_quotient → Type} [Pt : Πaa, is_hprop (P aa)]
+    (Pc : Π(a : A), P (class_of a)) (x : set_quotient) : P x :=
+  rec Pc (λa a' H, !is_hprop.elimo) x
+
+  protected definition elim_hprop {P : Type} [Pt : is_hprop P] (Pc : A → P) (x : set_quotient)
+    : P :=
+  elim Pc (λa a' H, !is_hprop.elim) x
+
   /-
     there are no theorems to eliminate to the universe here,
     because the universe is generally not a set
@@ -98,7 +106,8 @@ namespace set_quotient
         intro a a' r, apply eq_pathover, apply hdeg_square, apply elim_eq_of_rel}
   end
 
-  definition code [unfold 4] (a : A) (x : set_quotient R) [H : is_equivalence R] : hprop :=
+  protected definition code [unfold 4] (a : A) (x : set_quotient R) [H : is_equivalence R]
+    : hprop :=
   set_quotient.elim_on x (R a)
     begin
       intros a' a'' H1,
@@ -109,22 +118,22 @@ namespace set_quotient
       { intro H2, apply is_transitive.trans R H2, exact is_symmetric.symm R H1}
     end
 
-  definition encode {a : A} {x : set_quotient R} (p : class_of a = x)
-    [H : is_equivalence R] : code R a x :=
+  protected definition encode {a : A} {x : set_quotient R} (p : class_of a = x)
+    [H : is_equivalence R] : set_quotient.code R a x :=
   begin
     induction p, esimp, apply is_reflexive.refl R
   end
 
   definition rel_of_eq {a a' : A} (p : class_of a = class_of a' :> set_quotient R)
     [H : is_equivalence R] : R a a' :=
-  encode R p
+  set_quotient.encode R p
 
   variables {R S T}
-  definition quotient_unary_map (f : A → B) (H : Π{a a'} (r : R a a'), S (f a) (f a')) :
+  definition quotient_unary_map [unfold 7] (f : A → B) (H : Π{a a'} (r : R a a'), S (f a) (f a')) :
     set_quotient R → set_quotient S :=
   set_quotient.elim (class_of ∘ f) (λa a' r, eq_of_rel (H r))
 
-  definition quotient_binary_map (f : A → B → C)
+  definition quotient_binary_map [unfold 10 11] (f : A → B → C)
     (H : Π{a a'} (r : R a a') {b b'} (s : S b b'), T (f a b) (f a' b'))
     [HR : is_reflexive R] [HS : is_reflexive S] :
     set_quotient R → set_quotient S → set_quotient T :=
@@ -138,5 +147,4 @@ namespace set_quotient
       { intro b b' s, apply eq_pathover, esimp, apply is_hset.elims}}
   end
 
-
 end set_quotient