From b09fdc8c6145ca3a1c19fae7a164f9fbea9d1131 Mon Sep 17 00:00:00 2001 From: Ulrik Buchholtz Date: Fri, 25 Dec 2015 15:11:11 -0500 Subject: [PATCH] feat(hott/hit): flattening lemmas for coeq and pushout --- hott/hit/coeq.hlean | 64 +++++++++++++++++++++++++++++++-- hott/hit/pushout.hlean | 81 +++++++++++++++++++++++++++++++++++++++++- 2 files changed, 142 insertions(+), 3 deletions(-) diff --git a/hott/hit/coeq.hlean b/hott/hit/coeq.hlean index 2b1d311a03..0cb79870e5 100644 --- a/hott/hit/coeq.hlean +++ b/hott/hit/coeq.hlean @@ -6,9 +6,9 @@ Authors: Floris van Doorn Declaration of the coequalizer -/ -import .quotient +import .quotient_functor types.equiv -open quotient eq equiv equiv.ops is_trunc +open quotient eq equiv equiv.ops is_trunc sigma sigma.ops namespace coeq section @@ -90,3 +90,63 @@ attribute coeq.rec coeq.elim [unfold 8] [recursor 8] attribute coeq.elim_type [unfold 7] attribute coeq.rec_on coeq.elim_on [unfold 6] attribute coeq.elim_type_on [unfold 5] + +/- Flattening -/ +namespace coeq +section + open function + + universe u + parameters {A B : Type.{u}} (f g : A → B) (P_i : B → Type) + (Pcp : Πx : A, P_i (f x) ≃ P_i (g x)) + + local abbreviation P := coeq.elim_type f g P_i Pcp + + local abbreviation F : sigma (P_i ∘ f) → sigma P_i := + λz, ⟨f z.1, z.2⟩ + + local abbreviation G : sigma (P_i ∘ f) → sigma P_i := + λz, ⟨g z.1, Pcp z.1 z.2⟩ + + local abbreviation Pr : Π⦃b b' : B⦄, + coeq_rel f g b b' → P_i b ≃ P_i b' := + @coeq_rel.rec A B f g _ Pcp + + local abbreviation P' := quotient.elim_type P_i Pr + + protected definition flattening : sigma P ≃ coeq F G := + begin + assert H : Πz, P z ≃ P' z, + { intro z, apply equiv_of_eq, + assert H1 : coeq.elim_type f g P_i Pcp = quotient.elim_type P_i Pr, + { change + quotient.rec P_i + (λb b' r, coeq_rel.cases_on r (λx, pathover_of_eq (ua (Pcp x)))) + = quotient.rec P_i + (λb b' r, pathover_of_eq (ua (coeq_rel.cases_on r Pcp))), + assert H2 : Π⦃b b' : B⦄ (r : coeq_rel f g b b'), + coeq_rel.cases_on r (λx, pathover_of_eq (ua (Pcp x))) + = pathover_of_eq (ua (coeq_rel.cases_on r Pcp)) + :> P_i b =[eq_of_rel (coeq_rel f g) r] P_i b', + { intros b b' r, cases r, reflexivity }, + rewrite (eq_of_homotopy3 H2) }, + apply ap10 H1 }, + apply equiv.trans (sigma_equiv_sigma_id H), + apply equiv.trans !quotient.flattening.flattening_lemma, + fapply quotient.equiv, + { reflexivity }, + { intros bp bp', + fapply equiv.MK, + { intro r, induction r with b b' r p, + induction r with x, exact coeq_rel.Rmk F G ⟨x, p⟩ }, + { esimp, intro r, induction r with xp, + induction xp with x p, + exact quotient.flattening.flattening_rel.mk Pr + (coeq_rel.Rmk f g x) p }, + { esimp, intro r, induction r with xp, + induction xp with x p, reflexivity }, + { intro r, induction r with b b' r p, + induction r with x, reflexivity } } + end +end +end coeq diff --git a/hott/hit/pushout.hlean b/hott/hit/pushout.hlean index cc0a6b7d04..a743486a0c 100644 --- a/hott/hit/pushout.hlean +++ b/hott/hit/pushout.hlean @@ -6,7 +6,7 @@ Authors: Floris van Doorn Declaration of the pushout -/ -import .quotient cubical.square +import .quotient cubical.square types.sigma open quotient eq sum equiv equiv.ops is_trunc @@ -120,5 +120,84 @@ namespace pushout apply eq_pathover, apply hdeg_square, esimp, apply elim_glue}, end +end pushout + +open function sigma.ops + +namespace pushout + + /- The flattening lemma -/ + section + + universe variable u + parameters {TL BL TR : Type} (f : TL → BL) (g : TL → TR) + (Pinl : BL → Type.{u}) (Pinr : TR → Type.{u}) + (Pglue : Π(x : TL), Pinl (f x) ≃ Pinr (g x)) + include Pglue + + local abbreviation A := BL + TR + local abbreviation R : A → A → Type := pushout_rel f g + local abbreviation P [unfold 5] := pushout.elim_type Pinl Pinr Pglue + + local abbreviation F : sigma (Pinl ∘ f) → sigma Pinl := + λz, ⟨ f z.1 , z.2 ⟩ + + local abbreviation G : sigma (Pinl ∘ f) → sigma Pinr := + λz, ⟨ g z.1 , Pglue z.1 z.2 ⟩ + + local abbreviation Pglue' : Π ⦃a a' : A⦄, + R a a' → sum.rec Pinl Pinr a ≃ sum.rec Pinl Pinr a' := + @pushout_rel.rec TL BL TR f g + (λ ⦃a a' ⦄ (r : R a a'), + (sum.rec Pinl Pinr a) ≃ (sum.rec Pinl Pinr a')) Pglue + + protected definition flattening : sigma P ≃ pushout F G := + begin + assert H : Πz, P z ≃ quotient.elim_type (sum.rec Pinl Pinr) Pglue' z, + { intro z, apply equiv_of_eq, + assert H1 : pushout.elim_type Pinl Pinr Pglue + = quotient.elim_type (sum.rec Pinl Pinr) Pglue', + { change + quotient.rec (sum.rec Pinl Pinr) + (λa a' r, pushout_rel.cases_on r (λx, pathover_of_eq (ua (Pglue x)))) + = quotient.rec (sum.rec Pinl Pinr) + (λa a' r, pathover_of_eq (ua (pushout_rel.cases_on r Pglue))), + assert H2 : Π⦃a a'⦄ r : pushout_rel f g a a', + pushout_rel.cases_on r (λx, pathover_of_eq (ua (Pglue x))) + = pathover_of_eq (ua (pushout_rel.cases_on r Pglue)) + :> sum.rec Pinl Pinr a =[eq_of_rel (pushout_rel f g) r] + sum.rec Pinl Pinr a', + { intros a a' r, cases r, reflexivity }, + rewrite (eq_of_homotopy3 H2) }, + apply ap10 H1 }, + apply equiv.trans (sigma_equiv_sigma_id H), + apply equiv.trans (quotient.flattening.flattening_lemma R (sum.rec Pinl Pinr) Pglue'), + fapply equiv.MK, + { intro q, induction q with z z z' fr, + { induction z with a p, induction a with x x, + { exact inl ⟨x, p⟩ }, + { exact inr ⟨x, p⟩ } }, + { induction fr with a a' r p, induction r with x, + exact glue ⟨x, p⟩ } }, + { intro q, induction q with xp xp xp, + { exact class_of _ ⟨sum.inl xp.1, xp.2⟩ }, + { exact class_of _ ⟨sum.inr xp.1, xp.2⟩ }, + { apply eq_of_rel, constructor } }, + { intro q, induction q with xp xp xp: induction xp with x p, + { apply ap inl, reflexivity }, + { apply ap inr, reflexivity }, + { unfold F, unfold G, apply eq_pathover, + rewrite [ap_id,ap_compose' (quotient.elim _ _)], + krewrite elim_glue, krewrite elim_eq_of_rel, apply hrefl } }, + { intro q, induction q with z z z' fr, + { induction z with a p, induction a with x x, + { reflexivity }, + { reflexivity } }, + { induction fr with a a' r p, induction r with x, + esimp, apply eq_pathover, + rewrite [ap_id,ap_compose' (pushout.elim _ _ _)], + krewrite elim_eq_of_rel, krewrite elim_glue, apply hrefl } } + end + end end pushout