From 9265094f96086bdcf152421dd26495326ef29d20 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Wed, 14 Jun 2017 21:28:31 -0400 Subject: [PATCH] feat(pointed): redefine pequiv Now the underlying pointed function and pointed inverse are the functions which were put in definitionally --- hott/algebra/group_theory.hlean | 6 +- hott/homotopy/EM.hlean | 2 +- hott/homotopy/LES_of_homotopy_groups.hlean | 5 +- hott/homotopy/chain_complex.hlean | 2 +- hott/init/pointed.hlean | 9 - hott/types/equiv.hlean | 46 ++++- hott/types/fiber.hlean | 6 +- hott/types/pointed.hlean | 190 ++++++++++++--------- hott/types/sigma.hlean | 4 + hott/types/trunc.hlean | 3 + 10 files changed, 167 insertions(+), 106 deletions(-) diff --git a/hott/algebra/group_theory.hlean b/hott/algebra/group_theory.hlean index f3164c62b..339c64796 100644 --- a/hott/algebra/group_theory.hlean +++ b/hott/algebra/group_theory.hlean @@ -184,9 +184,9 @@ namespace group begin induction p, apply pequiv_eq, - fapply pmap_eq, - { intro g, reflexivity}, - { apply is_prop.elim} + fapply phomotopy.mk, + { intro g, reflexivity }, + { apply is_prop.elim } end definition to_ginv [constructor] (φ : G₁ ≃g G₂) : G₂ →g G₁ := diff --git a/hott/homotopy/EM.hlean b/hott/homotopy/EM.hlean index 6d44bdfc0..43dfa982a 100644 --- a/hott/homotopy/EM.hlean +++ b/hott/homotopy/EM.hlean @@ -179,7 +179,7 @@ namespace EM [is_conn 0 X] [is_trunc 1 X] : EM1 G ≃* X := begin apply EM1_pequiv' (pequiv_of_isomorphism e ⬝e* ptrunc_pequiv 0 (Ω X)), - refine is_equiv.preserve_binary_of_inv_preserve _ mul concat _, + refine equiv.preserve_binary_of_inv_preserve _ mul concat _, intro p q, exact to_respect_mul e⁻¹ᵍ (tr p) (tr q) end diff --git a/hott/homotopy/LES_of_homotopy_groups.hlean b/hott/homotopy/LES_of_homotopy_groups.hlean index e4b2a6847..6e1a358af 100644 --- a/hott/homotopy/LES_of_homotopy_groups.hlean +++ b/hott/homotopy/LES_of_homotopy_groups.hlean @@ -75,7 +75,7 @@ We get the long exact sequence of homotopy groups by taking the set-truncation o import .chain_complex algebra.homotopy_group eq2 -open eq pointed sigma fiber equiv is_equiv is_trunc nat trunc algebra function sum +open eq pointed sigma fiber equiv is_equiv is_trunc nat trunc algebra function /-------------- PART 1 --------------/ @@ -247,7 +247,8 @@ namespace chain_complex fiber_sequence_carrier_pequiv n (fiber_sequence_fun (n + 3) x) = ap1 (fiber_sequence_fun n) (fiber_sequence_carrier_pequiv (n + 1) x)⁻¹ := begin - apply homotopy_of_inv_homotopy_pre (fiber_sequence_carrier_pequiv (n + 1)), + refine @(homotopy_of_inv_homotopy_pre (fiber_sequence_carrier_pequiv (n + 1))) + !pequiv.to_is_equiv _ _ _, apply fiber_sequence_fun_eq_helper n end diff --git a/hott/homotopy/chain_complex.hlean b/hott/homotopy/chain_complex.hlean index c947a13a7..9959c3ad5 100644 --- a/hott/homotopy/chain_complex.hlean +++ b/hott/homotopy/chain_complex.hlean @@ -239,7 +239,7 @@ namespace chain_complex intro y q, esimp at *, have H2 : tcc_to_fn X (f m) ((equiv_of_eq (ap (λx, X x) (c m)))⁻¹ᵉ (e⁻¹ y)) = pt, begin - refine _ ⬝ ap e⁻¹ᵉ* q ⬝ (respect_pt (e⁻¹ᵉ*)), apply eq_inv_of_eq, clear q, revert y, + refine _ ⬝ ap e⁻¹ᵉ* q ⬝ (respect_pt (e⁻¹ᵉ*)), apply @eq_inv_of_eq _ _ e, clear q, revert y, apply inv_homotopy_of_homotopy_pre e, apply inv_homotopy_of_homotopy_pre, apply p end, diff --git a/hott/init/pointed.hlean b/hott/init/pointed.hlean index ecedb0e92..6d96ffca5 100644 --- a/hott/init/pointed.hlean +++ b/hott/init/pointed.hlean @@ -119,13 +119,4 @@ namespace pointed abbreviation to_homotopy [coercion] [unfold 5] (p : f ~* g) : Πa, f a = g a := phomotopy.homotopy p - /- pointed equivalences -/ - structure pequiv (A B : Type*) extends equiv A B, pmap A B - - attribute pequiv._trans_of_to_pmap pequiv._trans_of_to_equiv pequiv.to_pmap pequiv.to_equiv - [unfold 3] - attribute pequiv.to_is_equiv [instance] - attribute pequiv.to_pmap [coercion] - infix ` ≃* `:25 := pequiv - end pointed diff --git a/hott/types/equiv.hlean b/hott/types/equiv.hlean index 0af87c124..eedd82aac 100644 --- a/hott/types/equiv.hlean +++ b/hott/types/equiv.hlean @@ -308,11 +308,49 @@ namespace equiv end equiv namespace pointed - open equiv is_equiv - definition pequiv_eq {A B : Type*} {p q : A ≃* B} (H : p = q :> (A →* B)) : p = q := + open equiv is_equiv pointed prod + definition pequiv.sigma_char {A B : Type*} : + (A ≃* B) ≃ Σ(f : A →* B), (Σ(g : B →* A), f ∘* g ~* pid B) × (Σ(h : B →* A), h ∘* f ~* pid A) := begin - cases p with f Hf, cases q with g Hg, esimp at *, - exact apd011 pequiv_of_pmap H !is_prop.elimo + fapply equiv.MK, + { intro f, exact ⟨f, (⟨pequiv.to_pinv1 f, pequiv.pright_inv f⟩, + ⟨pequiv.to_pinv2 f, pequiv.pleft_inv f⟩)⟩, }, + { intro f, exact pequiv.mk' f.1 (pr1 f.2).1 (pr2 f.2).1 (pr1 f.2).2 (pr2 f.2).2 }, + { intro f, induction f with f v, induction v with hl hr, induction hl, induction hr, + reflexivity }, + { intro f, induction f, reflexivity } end + variables {A B : Type*} + definition is_contr_pright_inv (f : A ≃* B) : is_contr (Σ(g : B →* A), f ∘* g ~* pid B) := + begin + fapply is_trunc_equiv_closed, + { exact !fiber.sigma_char ⬝e sigma_equiv_sigma_right (λg, !pmap_eq_equiv) }, + fapply is_contr_fiber_of_is_equiv, + exact pequiv.to_is_equiv (pequiv_ppcompose_left f) + end + + definition is_contr_pleft_inv (f : A ≃* B) : is_contr (Σ(h : B →* A), h ∘* f ~* pid A) := + begin + fapply is_trunc_equiv_closed, + { exact !fiber.sigma_char ⬝e sigma_equiv_sigma_right (λg, !pmap_eq_equiv) }, + fapply is_contr_fiber_of_is_equiv, + exact pequiv.to_is_equiv (pequiv_ppcompose_right f) + end + + definition pequiv_eq_equiv (f g : A ≃* B) : (f = g) ≃ f ~* g := + have Π(f : A →* B), is_prop ((Σ(g : B →* A), f ∘* g ~* pid B) × (Σ(h : B →* A), h ∘* f ~* pid A)), + begin + intro f, apply is_prop_of_imp_is_contr, intro v, + let f' := pequiv.sigma_char⁻¹ᵉ ⟨f, v⟩, + apply is_trunc_prod, exact is_contr_pright_inv f', exact is_contr_pleft_inv f' + end, + calc (f = g) ≃ (pequiv.sigma_char f = pequiv.sigma_char g) + : eq_equiv_fn_eq pequiv.sigma_char f g + ... ≃ (f = g :> (A →* B)) : subtype_eq_equiv + ... ≃ (f ~* g) : pmap_eq_equiv f g + + definition pequiv_eq {f g : A ≃* B} (H : f ~* g) : f = g := + (pequiv_eq_equiv f g)⁻¹ᵉ H + end pointed diff --git a/hott/types/fiber.hlean b/hott/types/fiber.hlean index 3c450bf08..0cf58c340 100644 --- a/hott/types/fiber.hlean +++ b/hott/types/fiber.hlean @@ -266,9 +266,9 @@ namespace fiber lemma pequiv_precompose_ppoint {A A' B : Type*} (f : A →* B) (g : A' ≃* A) : ppoint f ∘* fiber.pequiv_precompose f g ~* g ∘* ppoint (f ∘* g) := begin - induction f with f f₀, induction g with g hg g₀, induction B with B b₀, - induction A with A a₀', esimp at *, induction g₀, induction f₀, - reflexivity, + induction f with f f₀, induction g with g h₁ h₂ p₁ p₂, induction B with B b₀, + induction g with g g₀, induction A with A a₀', esimp at *, induction g₀, induction f₀, + reflexivity end definition pfiber_pequiv_of_square_ppoint {A B C D : Type*} {f : A →* B} {g : C →* D} diff --git a/hott/types/pointed.hlean b/hott/types/pointed.hlean index cf027f091..fd26f7ab9 100644 --- a/hott/types/pointed.hlean +++ b/hott/types/pointed.hlean @@ -116,18 +116,18 @@ namespace pointed /- categorical properties of pointed maps -/ - definition pmap_of_map [constructor] {A B : Type} (f : A → B) (a : A) : - pointed.MK A a →* pointed.MK B (f a) := - pmap.mk f idp - definition pid [constructor] [refl] (A : Type*) : A →* A := pmap.mk id idp - definition pcompose [constructor] [trans] (g : B →* C) (f : A →* B) : A →* C := + definition pcompose [constructor] [trans] {A B C : Type*} (g : B →* C) (f : A →* B) : A →* C := pmap.mk (λa, g (f a)) (ap g (respect_pt f) ⬝ respect_pt g) infixr ` ∘* `:60 := pcompose + definition pmap_of_map [constructor] {A B : Type} (f : A → B) (a : A) : + pointed.MK A a →* pointed.MK B (f a) := + pmap.mk f idp + definition respect_pt_pcompose {A B C : Type*} (g : B →* C) (f : A →* B) : respect_pt (g ∘* f) = ap g (respect_pt f) ⬝ respect_pt g := idp @@ -373,6 +373,19 @@ namespace pointed p a = q a := ap010 to_homotopy r a + definition pwhisker_left [constructor] (h : B →* C) (p : f ~* g) : h ∘* f ~* h ∘* g := + phomotopy.mk (λa, ap h (p a)) + abstract !con.assoc⁻¹ ⬝ whisker_right _ (!ap_con⁻¹ ⬝ ap02 _ (to_homotopy_pt p)) end + + definition pwhisker_right [constructor] (h : C →* A) (p : f ~* g) : f ∘* h ~* g ∘* h := + phomotopy.mk (λa, p (h a)) + abstract !con.assoc⁻¹ ⬝ whisker_right _ (!ap_con_eq_con_ap)⁻¹ ⬝ !con.assoc ⬝ + whisker_left _ (to_homotopy_pt p) end + + definition pconcat2 [constructor] {A B C : Type*} {h i : B →* C} {f g : A →* B} + (q : h ~* i) (p : f ~* g) : h ∘* f ~* i ∘* g := + pwhisker_left _ p ⬝* pwhisker_right _ q + definition pmap_eq_equiv_internal {A B : Type*} (f g : A →* B) : (f = g) ≃ (f ~* g) := calc (f = g) ≃ pmap.sigma_char f = pmap.sigma_char g : eq_equiv_fn_eq pmap.sigma_char f g @@ -676,9 +689,65 @@ namespace pointed /- pointed equivalences -/ - /- constructors / projections + variants -/ + structure pequiv (A B : Type*) := + mk' :: (to_pmap : A →* B) + (to_pinv1 : B →* A) + (to_pinv2 : B →* A) + (pright_inv : to_pmap ∘* to_pinv1 ~* pid B) + (pleft_inv : to_pinv2 ∘* to_pmap ~* pid A) + + attribute pequiv.to_pmap [coercion] + infix ` ≃* `:25 := pequiv + + definition to_pinv [unfold 3] (f : A ≃* B) : B →* A := + pequiv.to_pinv1 f + + definition pleft_inv' (f : A ≃* B) : to_pinv f ∘* f ~* pid A := + let g := to_pinv f in + let h := pequiv.to_pinv2 f in + calc g ∘* f ~* pid A ∘* (g ∘* f) : by exact !pid_pcompose⁻¹* + ... ~* (h ∘* f) ∘* (g ∘* f) : by exact pwhisker_right _ (pequiv.pleft_inv f)⁻¹* + ... ~* h ∘* (f ∘* g) ∘* f : by exact !passoc ⬝* pwhisker_left _ !passoc⁻¹* + ... ~* h ∘* pid B ∘* f : by exact !pwhisker_left (!pwhisker_right !pequiv.pright_inv) + ... ~* h ∘* f : by exact pwhisker_left _ !pid_pcompose + ... ~* pid A : by exact pequiv.pleft_inv f + + definition equiv_of_pequiv [coercion] [constructor] (f : A ≃* B) : A ≃ B := + have is_equiv f, from adjointify f (to_pinv f) (pequiv.pright_inv f) (pleft_inv' f), + equiv.mk f _ + + attribute pointed._trans_of_equiv_of_pequiv pequiv._trans_of_to_pmap [unfold 3] + + definition pequiv.to_is_equiv [instance] [constructor] (f : A ≃* B) : + is_equiv (pointed._trans_of_equiv_of_pequiv f) := + adjointify f (to_pinv f) (pequiv.pright_inv f) (pleft_inv' f) + + definition pequiv.to_is_equiv' [instance] [constructor] (f : A ≃* B) : + is_equiv (pequiv._trans_of_to_pmap f) := + pequiv.to_is_equiv f + + protected definition pequiv.MK2 [constructor] (f : A →* B) (g : B →* A) + (gf : g ∘* f ~* !pid) (fg : f ∘* g ~* !pid) : A ≃* B := + pequiv.mk' f g g fg gf + + definition pinv [constructor] (f : A →* B) (H : is_equiv f) : B →* A := + pmap.mk f⁻¹ᶠ (ap f⁻¹ᶠ (respect_pt f)⁻¹ ⬝ (left_inv f pt)) + definition pequiv_of_pmap [constructor] (f : A →* B) (H : is_equiv f) : A ≃* B := - pequiv.mk f _ (respect_pt f) + pequiv.mk' f (pinv f H) (pinv f H) + abstract begin + fapply phomotopy.mk, exact right_inv f, + induction f with f f₀, induction B with B b₀, esimp at *, induction f₀, esimp, + exact adj f pt ⬝ ap02 f !idp_con⁻¹ + end end + abstract begin + fapply phomotopy.mk, exact left_inv f, + induction f with f f₀, induction B with B b₀, esimp at *, induction f₀, esimp, + exact !idp_con⁻¹ ⬝ !idp_con⁻¹ + end end + + definition pequiv.mk [constructor] (f : A → B) (H : is_equiv f) (p : f pt = pt) : A ≃* B := + pequiv_of_pmap (pmap.mk f p) H definition pequiv_of_equiv [constructor] (f : A ≃ B) (H : f pt = pt) : A ≃* B := pequiv.mk f _ H @@ -687,15 +756,30 @@ namespace pointed (gf : Πa, g (f a) = a) (fg : Πb, f (g b) = b) : A ≃* B := pequiv.mk f (adjointify f g fg gf) (respect_pt f) - definition equiv_of_pequiv [constructor] (f : A ≃* B) : A ≃ B := - equiv.mk f _ + /- categorical properties of pointed equivalences -/ - definition to_pinv [constructor] (f : A ≃* B) : B →* A := - pmap.mk f⁻¹ ((ap f⁻¹ (respect_pt f))⁻¹ ⬝ left_inv f pt) + protected definition pequiv.refl [refl] [constructor] (A : Type*) : A ≃* A := + pequiv.mk' (pid A) (pid A) (pid A) !pid_pcompose !pcompose_pid + + protected definition pequiv.rfl [constructor] : A ≃* A := + pequiv.refl A + + protected definition pequiv.symm [symm] [constructor] (f : A ≃* B) : B ≃* A := + pequiv.mk' (pequiv.to_pinv1 f) f f (pleft_inv' f) (pequiv.pright_inv f) + + protected definition pequiv.trans [trans] [constructor] (f : A ≃* B) (g : B ≃* C) : A ≃* C := + pequiv_of_pmap (g ∘* f) !is_equiv_compose + + definition pequiv_compose {A B C : Type*} (g : B ≃* C) (f : A ≃* B) : A ≃* C := + pequiv_of_pmap (g ∘* f) (is_equiv_compose g f) + + postfix `⁻¹ᵉ*`:(max + 1) := pequiv.symm + infix ` ⬝e* `:75 := pequiv.trans + infixr ` ∘*ᵉ `:60 := pequiv_compose definition to_pmap_pequiv_of_pmap {A B : Type*} (f : A →* B) (H : is_equiv f) : pequiv.to_pmap (pequiv_of_pmap f H) = f := - by cases f; reflexivity + by reflexivity /- A version of pequiv.MK with stronger conditions. @@ -704,47 +788,14 @@ namespace pointed This is not the case when using `pequiv.MK` (if g is a pointed map), that will only give an ordinary homotopy. -/ - protected definition pequiv.MK2 [constructor] (f : A →* B) (g : B →* A) - (gf : g ∘* f ~* !pid) (fg : f ∘* g ~* !pid) : A ≃* B := - pequiv.MK f g gf fg definition to_pmap_pequiv_MK2 [constructor] (f : A →* B) (g : B →* A) (gf : g ∘* f ~* !pid) (fg : f ∘* g ~* !pid) : pequiv.MK2 f g gf fg ~* f := - phomotopy.mk (λb, idp) !idp_con + by reflexivity definition to_pinv_pequiv_MK2 [constructor] (f : A →* B) (g : B →* A) (gf : g ∘* f ~* !pid) (fg : f ∘* g ~* !pid) : to_pinv (pequiv.MK2 f g gf fg) ~* g := - phomotopy.mk (λb, idp) - abstract [irreducible] begin - esimp, - note H := to_homotopy_pt gf, note H2 := to_homotopy_pt fg, - note H3 := eq_top_of_square (natural_square (to_homotopy fg) (respect_pt f)), - rewrite [▸* at *, H, H3, H2, ap_id, - +con.assoc, ap_compose' f g, con_inv, - - ap_inv, - +ap_con g], - apply whisker_right, apply ap02 g, - rewrite [ap_con, - + con.assoc, +ap_inv, +inv_con_cancel_right, con.left_inv], - end end - - /- categorical properties of pointed equivalences -/ - - protected definition pequiv.refl [refl] [constructor] (A : Type*) : A ≃* A := - pequiv_of_pmap !pid !is_equiv_id - - protected definition pequiv.rfl [constructor] : A ≃* A := - pequiv.refl A - - protected definition pequiv.symm [symm] [constructor] (f : A ≃* B) : B ≃* A := - pequiv_of_pmap (to_pinv f) !is_equiv_inv - - protected definition pequiv.trans [trans] [constructor] (f : A ≃* B) (g : B ≃* C) : A ≃* C := - pequiv_of_pmap (g ∘* f) !is_equiv_compose - - definition pequiv_compose {A B C : Type*} (g : B ≃* C) (f : A ≃* B) : A ≃* C := - pequiv_of_pmap (g ∘* f) (is_equiv_compose g f) - - infixr ` ∘*ᵉ `:60 := pequiv_compose - postfix `⁻¹ᵉ*`:(max + 1) := pequiv.symm - infix ` ⬝e* `:75 := pequiv.trans + by reflexivity /- more on pointed equivalences -/ @@ -754,7 +805,7 @@ namespace pointed definition to_pmap_pequiv_trans {A B C : Type*} (f : A ≃* B) (g : B ≃* C) : pequiv.to_pmap (f ⬝e* g) = g ∘* f := - !to_pmap_pequiv_of_pmap + by reflexivity definition to_fun_pequiv_trans {X Y Z : Type*} (f : X ≃* Y) (g :Y ≃* Z) : f ⬝e* g ~ g ∘ f := λx, idp @@ -796,8 +847,8 @@ namespace pointed {a₁ a₂ : A} (p : a₁ = a₂) : pequiv_of_eq (ap C p) ∘* f a₁ ~* f a₂ ∘* pequiv_of_eq (ap B p) := pcast_commute f p - definition pequiv.eta_expand [constructor] {A B : Type*} (f : A ≃* B) : A ≃* B := - pequiv.mk f _ (pequiv.resp_pt f) + -- definition pequiv.eta_expand [constructor] {A B : Type*} (f : A ≃* B) : A ≃* B := + -- pequiv.mk' f (to_pinv f) (pequiv.to_pinv2 f) (pright_inv f) _ /- the theorem pequiv_eq, which gives a condition for two pointed equivalences are equal @@ -805,35 +856,11 @@ namespace pointed -/ /- computation rules of pointed homotopies, possibly combined with pointed equivalences -/ - definition pwhisker_left [constructor] (h : B →* C) (p : f ~* g) : h ∘* f ~* h ∘* g := - phomotopy.mk (λa, ap h (p a)) - abstract !con.assoc⁻¹ ⬝ whisker_right _ (!ap_con⁻¹ ⬝ ap02 _ (to_homotopy_pt p)) end - - definition pwhisker_right [constructor] (h : C →* A) (p : f ~* g) : f ∘* h ~* g ∘* h := - phomotopy.mk (λa, p (h a)) - abstract !con.assoc⁻¹ ⬝ whisker_right _ (!ap_con_eq_con_ap)⁻¹ ⬝ !con.assoc ⬝ - whisker_left _ (to_homotopy_pt p) end - - definition pconcat2 [constructor] {A B C : Type*} {h i : B →* C} {f g : A →* B} - (q : h ~* i) (p : f ~* g) : h ∘* f ~* i ∘* g := - pwhisker_left _ p ⬝* pwhisker_right _ q - definition pleft_inv (f : A ≃* B) : f⁻¹ᵉ* ∘* f ~* pid A := - phomotopy.mk (left_inv f) - abstract begin - esimp, symmetry, apply con_inv_cancel_left - end end + pleft_inv' f definition pright_inv (f : A ≃* B) : f ∘* f⁻¹ᵉ* ~* pid B := - phomotopy.mk (right_inv f) - abstract begin - induction f with f H p, esimp, - rewrite [ap_con, +ap_inv, -adj f, -ap_compose], - note q := natural_square (right_inv f) p, - rewrite [ap_id at q], - apply eq_bot_of_square, - exact q - end end + pequiv.pright_inv f definition pcancel_left (f : B ≃* C) {g h : A →* B} (p : f ∘* g ~* f ∘* h) : g ~* h := begin @@ -1003,11 +1030,11 @@ namespace pointed definition to_pmap_loopn_pequiv_loopn [constructor] (n : ℕ) (f : A ≃* B) : loopn_pequiv_loopn n f ~* apn n f := - !to_pmap_pequiv_MK2 + by reflexivity definition to_pinv_loopn_pequiv_loopn [constructor] (n : ℕ) (f : A ≃* B) : (loopn_pequiv_loopn n f)⁻¹ᵉ* ~* apn n f⁻¹ᵉ* := - !to_pinv_pequiv_MK2 + by reflexivity definition loopn_pequiv_loopn_con (n : ℕ) (f : A ≃* B) (p q : Ω[n+1] A) : loopn_pequiv_loopn (n+1) f (p ⬝ q) = @@ -1030,9 +1057,7 @@ namespace pointed definition apn_pinv (n : ℕ) {A B : Type*} (f : A ≃* B) : Ω→[n] f⁻¹ᵉ* ~* (loopn_pequiv_loopn n f)⁻¹ᵉ* := - begin - refine !to_pinv_pequiv_MK2⁻¹* - end + by reflexivity definition pmap_functor [constructor] {A A' B B' : Type*} (f : A' →* A) (g : B →* B') : ppmap A B →* ppmap A' B' := @@ -1061,8 +1086,7 @@ namespace pointed begin fapply phomotopy.mk, { reflexivity}, - { esimp [pequiv.trans, pequiv.symm], - exact !con.right_inv⁻¹ ⬝ ((!idp_con⁻¹ ⬝ !ap_id⁻¹) ◾ (!ap_id⁻¹⁻² ⬝ !idp_con⁻¹)), } + { symmetry, exact (!ap_id ⬝ !idp_con) ◾ (!idp_con ⬝ !ap_id) ⬝ !con.right_inv } end /- properties of iterated loop space -/ diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean index e0a26e996..bc7f00f0f 100644 --- a/hott/types/sigma.hlean +++ b/hott/types/sigma.hlean @@ -502,6 +502,10 @@ namespace sigma (u.1 = v.1) ≃ (u = v) := equiv.mk !subtype_eq _ + definition subtype_eq_equiv [constructor] [H : Πa, is_prop (B a)] (u v : {a | B a}) : + (u = v) ≃ (u.1 = v.1) := + (equiv_subtype u v)⁻¹ᵉ + definition subtype_eq_inv {A : Type} {B : A → Type} [H : Πa, is_prop (B a)] (u v : Σa, B a) : u = v → u.1 = v.1 := subtype_eq⁻¹ᶠ diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean index bcce386a0..aff7fcd9e 100644 --- a/hott/types/trunc.hlean +++ b/hott/types/trunc.hlean @@ -567,6 +567,9 @@ namespace trunc : (tr a = tr a' :> trunc n.+1 A) ≃ trunc n (a = a') := !trunc_eq_equiv + definition trunc_eq {n : ℕ₋₂} {a a' : A} (p : trunc n (a = a')) :tr a = tr a' :> trunc n.+1 A := + !tr_eq_tr_equiv⁻¹ᵉ p + definition code_mul {n : ℕ₋₂} {aa₁ aa₂ aa₃ : trunc n.+1 A} (g : trunc.code n aa₁ aa₂) (h : trunc.code n aa₂ aa₃) : trunc.code n aa₁ aa₃ := begin