From 111c8e1529bb886ae3f401a9b541365fbb86c19a Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Thu, 7 May 2015 16:35:14 -0400
Subject: [PATCH] feat(hott): add [unfold-c] and [constructor] attributes for
 HITs

---
 hott/hit/circle.hlean        | 40 ++++++++++++++++++++++++++++--------
 hott/hit/coeq.hlean          |  6 ++++++
 hott/hit/colimit.hlean       | 10 +++++++++
 hott/hit/cylinder.hlean      |  6 ++++++
 hott/hit/pushout.hlean       |  6 ++++++
 hott/hit/quotient.hlean      |  4 ++++
 hott/hit/suspension.hlean    |  6 ++++++
 hott/hit/trunc.hlean         |  3 +++
 hott/hit/type_quotient.hlean |  5 +++++
 hott/init/hit.hlean          |  4 ++++
 10 files changed, 82 insertions(+), 8 deletions(-)

diff --git a/hott/hit/circle.hlean b/hott/hit/circle.hlean
index c1ce10b50..08680449f 100644
--- a/hott/hit/circle.hlean
+++ b/hott/hit/circle.hlean
@@ -12,7 +12,7 @@ import .sphere types.bool types.eq types.int.hott types.arrow types.equiv
 
 open eq suspension bool sphere_index is_equiv equiv equiv.ops is_trunc
 
-definition circle [reducible] := sphere 1
+definition circle : Type₀ := sphere 1
 
 namespace circle
 
@@ -50,7 +50,7 @@ namespace circle
       : apd (rec2 Pb1 Pb2 Ps1 Ps2) seg2 = Ps2 :=
   !rec_merid
 
-  definition elim2 {P : Type} (Pb1 Pb2 : P) (Ps1 : Pb1 = Pb2) (Ps2 : Pb1 = Pb2) (x : circle) : P :=
+  definition elim2 {P : Type} (Pb1 Pb2 : P) (Ps1 Ps2 : Pb1 = Pb2) (x : circle) : P :=
   rec2 Pb1 Pb2 (!tr_constant ⬝ Ps1) (!tr_constant ⬝ Ps2) x
 
   definition elim2_on [reducible] {P : Type} (x : circle) (Pb1 Pb2 : P)
@@ -71,6 +71,21 @@ namespace circle
     rewrite [-apd_eq_tr_constant_con_ap,↑elim2,rec2_seg2],
   end
 
+  definition elim2_type (Pb1 Pb2 : Type) (Ps1 Ps2 : Pb1 ≃ Pb2) (x : circle) : Type :=
+  elim2 Pb1 Pb2 (ua Ps1) (ua Ps2) x
+
+  definition elim2_type_on [reducible] (x : circle) (Pb1 Pb2 : Type) (Ps1 Ps2 : Pb1 ≃ Pb2)
+    : Type :=
+  elim2_type Pb1 Pb2 Ps1 Ps2 x
+
+  theorem elim2_type_seg1 (Pb1 Pb2 : Type) (Ps1 Ps2 : Pb1 ≃ Pb2)
+    : transport (elim2_type Pb1 Pb2 Ps1 Ps2) seg1 = Ps1 :=
+  by rewrite [tr_eq_cast_ap_fn,↑elim2_type,elim2_seg1];apply cast_ua_fn
+
+  theorem elim2_type_seg2 (Pb1 Pb2 : Type) (Ps1 Ps2 : Pb1 ≃ Pb2)
+    : transport (elim2_type Pb1 Pb2 Ps1 Ps2) seg2 = Ps2 :=
+  by rewrite [tr_eq_cast_ap_fn,↑elim2_type,elim2_seg2];apply cast_ua_fn
+
   protected definition rec {P : circle → Type} (Pbase : P base) (Ploop : loop ▸ Pbase = Pbase)
     (x : circle) : P x :=
   begin
@@ -133,7 +148,19 @@ namespace circle
   theorem elim_type_loop_inv (Pbase : Type) (Ploop : Pbase ≃ Pbase) :
     transport (elim_type Pbase Ploop) loop⁻¹ = to_inv Ploop :=
   by rewrite [tr_inv_fn,↑to_inv]; apply inv_eq_inv; apply elim_type_loop
+end circle
 
+attribute circle.base circle.base1 circle.base2 [constructor]
+attribute circle.rec circle.elim [unfold-c 4]
+attribute circle.elim_type [unfold-c 3]
+attribute circle.rec_on circle.elim_on [unfold-c 2]
+attribute circle.elim_type_on [unfold-c 1]
+attribute circle.rec2 circle.elim2 [unfold-c 6]
+attribute circle.elim2_type [unfold-c 5]
+attribute circle.rec2_on circle.elim2_on [unfold-c 2]
+attribute circle.elim2_type [unfold-c 1]
+
+namespace circle
   definition loop_neq_idp : loop ≠ idp :=
   assume H : loop = idp,
   have H2 : Π{A : Type₁} {a : A} (p : a = a), p = idp,
@@ -155,7 +182,7 @@ namespace circle
 
   open int
 
-  protected definition code (x : circle) : Type₀ :=
+  protected definition code [unfold-c 1] (x : circle) : Type₀ :=
   circle.elim_type_on x ℤ equiv_succ
 
   definition transport_code_loop (a : ℤ) : transport code loop a = succ a :=
@@ -168,7 +195,6 @@ namespace circle
   protected definition encode {x : circle} (p : base = x) : code x :=
   transport code p (of_num 0) -- why is the explicit coercion needed here?
 
-  --attribute type_quotient.rec_on [unfold-c 4]
   definition circle_eq_equiv (x : circle) : (base = x) ≃ code x :=
   begin
     fapply equiv.MK,
@@ -179,9 +205,7 @@ namespace circle
         refine !arrow.arrow_transport ⬝ !transport_eq_r ⬝ _,
         rewrite [transport_code_loop_inv,power_con,succ_pred]}},
     { refine circle.rec_on x _ _,
-      { intro a, esimp [circle.rec_on, circle.rec, base, rec2_on, rec2, base1,
-          suspension.rec_on, suspension.rec, north, pushout.rec_on, pushout.rec,
-          pushout.inl, type_quotient.rec_on], --simplify after #587
+      { intro a, esimp [base,base1], --simplify after #587
         apply rec_nat_on a,
         { exact idp},
         { intros n p,
@@ -191,7 +215,7 @@ namespace circle
           apply transport (λ(y : base = base), transport code y _ = _),
           { exact !power_con_inv ⬝ ap (power loop) !neg_succ⁻¹},
           rewrite [▸*,con_tr,transport_code_loop_inv, ↑[encode,code] at p, p, -neg_succ]}},
-      { apply eq_of_homotopy, intro a, apply @is_hset.elim, change is_hset ℤ, exact _}},
+      { apply eq_of_homotopy, intro a, esimp [base,base1] at *, }},
         --simplify after #587
     { intro p, cases p, exact idp},
   end
diff --git a/hott/hit/coeq.hlean b/hott/hit/coeq.hlean
index 0c06798d3..691e582a7 100644
--- a/hott/hit/coeq.hlean
+++ b/hott/hit/coeq.hlean
@@ -79,3 +79,9 @@ parameters {A B : Type.{u}} (f g : A → B)
 end
 
 end coeq
+
+attribute coeq.coeq_i [constructor]
+attribute coeq.rec coeq.elim [unfold-c 8]
+attribute coeq.elim_type [unfold-c 7]
+attribute coeq.rec_on coeq.elim_on [unfold-c 6]
+attribute coeq.elim_type_on [unfold-c 5]
diff --git a/hott/hit/colimit.hlean b/hott/hit/colimit.hlean
index 71120d2aa..24beda7ec 100644
--- a/hott/hit/colimit.hlean
+++ b/hott/hit/colimit.hlean
@@ -171,3 +171,13 @@ section
 
 end
 end seq_colim
+
+attribute colimit.incl seq_colim.inclusion [constructor]
+attribute colimit.rec colimit.elim [unfold-c 10]
+attribute colimit.elim_type [unfold-c 9]
+attribute colimit.rec_on colimit.elim_on [unfold-c 8]
+attribute colimit.elim_type_on [unfold-c 7]
+attribute seq_colim.rec seq_colim.elim [unfold-c 6]
+attribute seq_colim.elim_type [unfold-c 5]
+attribute seq_colim.rec_on seq_colim.elim_on [unfold-c 4]
+attribute seq_colim.elim_type_on [unfold-c 3]
diff --git a/hott/hit/cylinder.hlean b/hott/hit/cylinder.hlean
index d18cb65d1..5f6ec0801 100644
--- a/hott/hit/cylinder.hlean
+++ b/hott/hit/cylinder.hlean
@@ -89,3 +89,9 @@ parameters {A B : Type.{u}} (f : A → B)
 end
 
 end cylinder
+
+attribute cylinder.base cylinder.top [constructor]
+attribute cylinder.rec cylinder.elim [unfold-c 8]
+attribute cylinder.elim_type [unfold-c 7]
+attribute cylinder.rec_on cylinder.elim_on [unfold-c 5]
+attribute cylinder.elim_type_on [unfold-c 4]
diff --git a/hott/hit/pushout.hlean b/hott/hit/pushout.hlean
index 0e7681121..3b471acda 100644
--- a/hott/hit/pushout.hlean
+++ b/hott/hit/pushout.hlean
@@ -111,3 +111,9 @@ end
 
   end test
 end pushout
+
+attribute pushout.inl pushout.inr [constructor]
+attribute pushout.rec pushout.elim [unfold-c 10]
+attribute pushout.elim_type [unfold-c 9]
+attribute pushout.rec_on pushout.elim_on [unfold-c 7]
+attribute pushout.elim_type_on [unfold-c 6]
diff --git a/hott/hit/quotient.hlean b/hott/hit/quotient.hlean
index 281c64421..a30b7148d 100644
--- a/hott/hit/quotient.hlean
+++ b/hott/hit/quotient.hlean
@@ -72,3 +72,7 @@ parameters {A : Type} (R : A → A → hprop)
 
 end
 end quotient
+
+attribute quotient.class_of [constructor]
+attribute quotient.rec quotient.elim [unfold-c 7]
+attribute quotient.rec_on quotient.elim_on [unfold-c 4]
diff --git a/hott/hit/suspension.hlean b/hott/hit/suspension.hlean
index 0dcc91ba2..62b823cbc 100644
--- a/hott/hit/suspension.hlean
+++ b/hott/hit/suspension.hlean
@@ -72,3 +72,9 @@ namespace suspension
   by rewrite [tr_eq_cast_ap_fn,↑elim_type,elim_merid];apply cast_ua_fn
 
 end suspension
+
+attribute suspension.north suspension.south [constructor]
+attribute suspension.rec suspension.elim [unfold-c 6]
+attribute suspension.elim_type [unfold-c 5]
+attribute suspension.rec_on suspension.elim_on [unfold-c 3]
+attribute suspension.elim_type_on [unfold-c 2]
diff --git a/hott/hit/trunc.hlean b/hott/hit/trunc.hlean
index 54146bb42..878d1906c 100644
--- a/hott/hit/trunc.hlean
+++ b/hott/hit/trunc.hlean
@@ -134,3 +134,6 @@ namespace trunc
   end
 
 end trunc
+
+attribute trunc.elim [unfold-c 6]
+attribute trunc.elim_on [unfold-c 4]
diff --git a/hott/hit/type_quotient.hlean b/hott/hit/type_quotient.hlean
index 63fbdf328..57d4f914c 100644
--- a/hott/hit/type_quotient.hlean
+++ b/hott/hit/type_quotient.hlean
@@ -51,3 +51,8 @@ namespace type_quotient
 
 
 end type_quotient
+
+attribute type_quotient.elim [unfold-c 6]
+attribute type_quotient.elim_type [unfold-c 5]
+attribute type_quotient.elim_on [unfold-c 4]
+attribute type_quotient.elim_type_on [unfold-c 3]
diff --git a/hott/init/hit.hlean b/hott/init/hit.hlean
index aa496467e..1301c7777 100644
--- a/hott/init/hit.hlean
+++ b/hott/init/hit.hlean
@@ -84,3 +84,7 @@ namespace type_quotient
     (Pc : Π(a : A), P (class_of R a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel R H ▸ Pc a = Pc a')
     {a a' : A} (H : R a a') : apd (type_quotient.rec Pc Pp) (eq_of_rel R H) = Pp H
 end type_quotient
+
+attribute type_quotient.class_of trunc.tr [constructor]
+attribute type_quotient.rec trunc.rec [unfold-c 6]
+attribute type_quotient.rec_on trunc.rec_on [unfold-c 4]