From 4165f9a613474c49a16dbe3852cffc9447e3207a Mon Sep 17 00:00:00 2001 From: favonia Date: Thu, 8 Jun 2017 14:11:02 -0600 Subject: [PATCH] Add pwedge_pequiv and plift_pwedge. --- homotopy/wedge.hlean | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/homotopy/wedge.hlean b/homotopy/wedge.hlean index a95f366..f3f82fe 100644 --- a/homotopy/wedge.hlean +++ b/homotopy/wedge.hlean @@ -2,7 +2,7 @@ import homotopy.wedge -open wedge pushout eq prod sum pointed equiv is_equiv unit +open wedge pushout eq prod sum pointed equiv is_equiv unit lift namespace wedge @@ -38,4 +38,15 @@ namespace wedge -- TODO: wedge is associative + definition pwedge_pequiv [constructor] {A A' B B' : Type*} (a : A ≃* A') (b : B ≃* B') : A ∨ B ≃* A' ∨ B' := + begin + fapply pequiv_of_equiv, + exact pushout.equiv !pconst !pconst !pconst !pconst !pequiv.refl a b (λdummy, respect_pt a) (λdummy, respect_pt b), + exact ap pushout.inl (respect_pt a) + end + + definition plift_pwedge.{u v} (A B : Type*) : plift.{u v} (A ∨ B) ≃* plift.{u v} A ∨ plift.{u v} B := + calc plift.{u v} (A ∨ B) ≃* A ∨ B : by exact !pequiv_plift⁻¹ᵉ* + ... ≃* plift.{u v} A ∨ plift.{u v} B : by exact pwedge_pequiv !pequiv_plift !pequiv_plift + end wedge