From aa5e188179ae1cc8debc675bfa9f888a5340de43 Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <javra@web.de>
Date: Fri, 22 Jan 2016 17:06:41 +0000
Subject: [PATCH] feat(hott): add symmetry of pushouts and pointed pushouts

---
 hott/hit/pointed_pushout.hlean | 14 +++++++++++++-
 hott/hit/pushout.hlean         | 27 +++++++++++++++++++++++++++
 hott/types/pointed.hlean       |  4 ++++
 3 files changed, 44 insertions(+), 1 deletion(-)

diff --git a/hott/hit/pointed_pushout.hlean b/hott/hit/pointed_pushout.hlean
index 0183d43e46..34a3ccda5e 100644
--- a/hott/hit/pointed_pushout.hlean
+++ b/hott/hit/pointed_pushout.hlean
@@ -17,7 +17,7 @@ namespace pointed
 
 end pointed
 
-open pointed
+open pointed Pointed
 
 namespace pushout
   section
@@ -39,6 +39,18 @@ namespace pushout
   definition prec {P : Pushout → Type} (Pinl : Π x, P (pinl x)) (Pinr : Π x, P (pinr x))
     (H : Π x, Pinl (f x) =[pglue x] Pinr (g x)) : (Π y, P y) :=
   pushout.rec Pinl Pinr H
+  end
+
+  section
+  variables {TL BL TR : Type*} (f : TL →* BL) (g : TL →* TR)
+
+  protected definition psymm : Pushout f g ≃* Pushout g f :=
+  begin
+    fapply pequiv.mk,
+    { fapply pmap.mk, exact !pushout.transpose,
+      exact ap inr (respect_pt f)⁻¹ ⬝ !glue⁻¹ ⬝ ap inl (respect_pt g) },
+    { esimp, apply equiv.to_is_equiv !pushout.symm },
+  end
 
   end
 end pushout
diff --git a/hott/hit/pushout.hlean b/hott/hit/pushout.hlean
index a743486a0c..66b1d263a2 100644
--- a/hott/hit/pushout.hlean
+++ b/hott/hit/pushout.hlean
@@ -200,4 +200,31 @@ namespace pushout
     end
   end
 
+  -- Commutativity of pushouts
+  section
+  variables {TL BL TR : Type} (f : TL → BL) (g : TL → TR)
+
+  protected definition transpose [constructor] : pushout f g → pushout g f :=
+  begin
+    intro x, induction x, apply inr a, apply inl a, apply !glue⁻¹
+  end
+
+  --TODO prove without krewrite?
+  protected definition transpose_involutive (x : pushout f g) :
+    pushout.transpose g f (pushout.transpose f g x) = x :=
+  begin
+      induction x, apply idp, apply idp,
+      apply eq_pathover, refine _ ⬝hp !ap_id⁻¹, 
+      refine !(ap_compose (pushout.transpose _ _)) ⬝ph _, esimp[pushout.transpose],
+      krewrite [elim_glue, ap_inv, elim_glue, inv_inv], apply hrfl
+  end
+
+  protected definition symm : pushout f g ≃ pushout g f :=
+  begin
+    fapply equiv.MK, do 2 exact !pushout.transpose,
+    do 2 (intro x; apply pushout.transpose_involutive),
+  end
+
+  end
+
 end pushout
diff --git a/hott/types/pointed.hlean b/hott/types/pointed.hlean
index 4f977474e5..6438ce6955 100644
--- a/hott/types/pointed.hlean
+++ b/hott/types/pointed.hlean
@@ -353,6 +353,10 @@ namespace pointed
   attribute pequiv.to_pmap [coercion]
   attribute pequiv.is_equiv_to_pmap [instance]
 
+  definition pequiv.mk' (to_pmap : A →* B) [is_equiv_to_pmap : is_equiv to_pmap] :
+    pequiv A B :=
+  pequiv.mk to_pmap is_equiv_to_pmap
+
   definition equiv_of_pequiv [constructor] (f : A ≃* B) : A ≃ B :=
   equiv.mk f _