From 227fcad22ab2bc27bb7471be7911075d101ba3f9 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Fri, 4 Aug 2017 15:07:56 +0100
Subject: [PATCH] feat(hott): various small changes

move total_image.rec, redefine hvconcat/hvinverse and change precedence of transporto notation
---
 hott/eq2.hlean             |  4 ++--
 hott/function.hlean        | 11 +++++++++++
 hott/hit/prop_trunc.hlean  | 11 -----------
 hott/hit/pushout.hlean     |  2 +-
 hott/homotopy/circle.hlean |  3 ---
 hott/init/pathover.hlean   |  4 ++--
 6 files changed, 16 insertions(+), 19 deletions(-)

diff --git a/hott/eq2.hlean b/hott/eq2.hlean
index 975344cc9..8bbf07af5 100644
--- a/hott/eq2.hlean
+++ b/hott/eq2.hlean
@@ -238,7 +238,7 @@ namespace eq
 
   definition hvconcat (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) (q : hsquare f₁₂ f₁₄ f₀₃ f₂₃) :
     hsquare f₁₀ f₁₄ (f₀₃ ∘ f₀₁) (f₂₃ ∘ f₂₁) :=
-  (hhconcat p⁻¹ʰᵗʸ q⁻¹ʰᵗʸ)⁻¹ʰᵗʸ
+  hwhisker_left f₂₃ p ⬝hty hwhisker_right f₀₁ q
 
   definition hhinverse {f₁₀ : A₀₀ ≃ A₂₀} {f₁₂ : A₀₂ ≃ A₂₂} (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) :
     hsquare f₁₀⁻¹ᵉ f₁₂⁻¹ᵉ f₂₁ f₀₁ :=
@@ -246,7 +246,7 @@ namespace eq
 
   definition hvinverse {f₀₁ : A₀₀ ≃ A₀₂} {f₂₁ : A₂₀ ≃ A₂₂} (p : hsquare f₁₀ f₁₂ f₀₁ f₂₁) :
     hsquare f₁₂ f₁₀ f₀₁⁻¹ᵉ f₂₁⁻¹ᵉ :=
-  (hhinverse p⁻¹ʰᵗʸ)⁻¹ʰᵗʸ
+  λa, inv_eq_of_eq (p (f₀₁⁻¹ᵉ a) ⬝ ap f₁₂ (to_right_inv f₀₁ a))⁻¹
 
   infix ` ⬝htyh `:73 := hhconcat
   infix ` ⬝htyv `:73 := hvconcat
diff --git a/hott/function.hlean b/hott/function.hlean
index a63df8e54..7161f8ee3 100644
--- a/hott/function.hlean
+++ b/hott/function.hlean
@@ -67,6 +67,17 @@ definition image_pathover {f : A → B} {x y : B} (p : x = y) (u : image f x) (v
   u =[p] v :=
 !is_prop.elimo
 
+definition total_image.rec [unfold 7]
+  {A B : Type} {f : A → B} {C : total_image f → Type} [H : Πx, is_prop (C x)]
+  (g : Πa, C ⟨f a, image.mk a idp⟩)
+  (x : total_image f) : C x :=
+begin
+  induction x with b v,
+  refine @image.rec _ _ _ _ _ (λv, H ⟨b, v⟩) _ v,
+  intro a p,
+  induction p, exact g a
+end
+
 /- total_image.elim_set is in hit.prop_trunc to avoid dependency cycle -/
 
 end image
diff --git a/hott/hit/prop_trunc.hlean b/hott/hit/prop_trunc.hlean
index 092fdaa56..717e9a5f7 100644
--- a/hott/hit/prop_trunc.hlean
+++ b/hott/hit/prop_trunc.hlean
@@ -437,15 +437,4 @@ namespace is_trunc
     { induction x with a p, induction x' with a' p', induction p', exact h _ _ p }
   end
 
-  definition total_image.rec [unfold 7]
-    {A B : Type} {f : A → B} {C : total_image f → Type} [H : Πx, is_prop (C x)]
-    (g : Πa, C ⟨f a, image.mk a idp⟩)
-    (x : total_image f) : C x :=
-  begin
-    induction x with b v,
-    refine @image.rec _ _ _ _ _ (λv, H ⟨b, v⟩) _ v,
-    intro a p,
-    induction p, exact g a
-  end
-
 end is_trunc
diff --git a/hott/hit/pushout.hlean b/hott/hit/pushout.hlean
index 56525a1d1..070fd7c46 100644
--- a/hott/hit/pushout.hlean
+++ b/hott/hit/pushout.hlean
@@ -244,7 +244,7 @@ namespace pushout
               (fh : bl ∘ f ~ f' ∘ tl) (gh : tr ∘ g ~ g' ∘ tl)
     include fh gh
 
-    protected definition functor [reducible] [unfold 16] : pushout f g → pushout f' g' :=
+    protected definition functor [unfold 16] : pushout f g → pushout f' g' :=
     begin
       intro x, induction x with a b z,
       { exact inl (bl a) },
diff --git a/hott/homotopy/circle.hlean b/hott/homotopy/circle.hlean
index 4166fabbd..990806035 100644
--- a/hott/homotopy/circle.hlean
+++ b/hott/homotopy/circle.hlean
@@ -104,9 +104,6 @@ namespace circle
     pathover_tr_of_pathover q ⬝o !pathover_tr⁻¹ᵒ = q :=
   by cases p'; cases q; exact idp
 
-  definition con_refl {A : Type} {x y : A} (p : x = y) : p ⬝ refl _ = p :=
-  eq.rec_on p idp
-
   theorem rec_loop {P : S¹ → Type} (Pbase : P base) (Ploop : Pbase =[loop] Pbase) :
     apd (circle.rec Pbase Ploop) loop = Ploop :=
   begin
diff --git a/hott/init/pathover.hlean b/hott/init/pathover.hlean
index 382152f03..f27c7417b 100644
--- a/hott/init/pathover.hlean
+++ b/hott/init/pathover.hlean
@@ -240,7 +240,7 @@ namespace eq
   end
 
   variable (C)
-  definition transporto (r : b =[p] b₂) (c : C b) : C b₂ :=
+  definition transporto [unfold 9] (r : b =[p] b₂) (c : C b) : C b₂ :=
   by induction r;exact c
   infix ` ▸o `:75 := transporto _
 
@@ -444,7 +444,7 @@ namespace eq
     (s : r = r') (s₂ : r₂ = r₂') : r ⬝o r₂ = r' ⬝o r₂' :=
   by induction s; induction s₂; reflexivity
 
-  infixl ` ◾o `:75 := concato2
+  infixl ` ◾o `:79 := concato2
   postfix [parsing_only] `⁻²ᵒ`:(max+10) := inverseo2 --this notation is abusive, should we use it?
 
   -- find a better name for this