From 4b603990fc2cfe883436acc2c14a94d23200f758 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Fri, 14 Sep 2018 17:56:25 +0200 Subject: [PATCH] make instances in sigma explicit --- hott/function.hlean | 2 +- hott/homotopy/circle.hlean | 22 +++++++++++++++++----- hott/types/fiber.hlean | 16 ++++++++-------- hott/types/sigma.hlean | 20 ++++++++++++-------- hott/types/univ.hlean | 2 +- 5 files changed, 39 insertions(+), 23 deletions(-) diff --git a/hott/function.hlean b/hott/function.hlean index d10c8f333..b478fa991 100644 --- a/hott/function.hlean +++ b/hott/function.hlean @@ -347,7 +347,7 @@ namespace function definition is_embedding_pr1 [instance] [constructor] {A : Type} (B : A → Type) [H : Π a, is_prop (B a)] : is_embedding (@pr1 A B) := - λv v', to_is_equiv (sigma_eq_equiv v v' ⬝e !sigma_equiv_of_is_contr_right) + λv v', to_is_equiv (sigma_eq_equiv v v' ⬝e sigma_equiv_of_is_contr_right _ _) variables {f f'} definition is_embedding_homotopy_closed (p : f ~ f') (H : is_embedding f) : is_embedding f' := diff --git a/hott/homotopy/circle.hlean b/hott/homotopy/circle.hlean index ac2a94604..4b903409d 100644 --- a/hott/homotopy/circle.hlean +++ b/hott/homotopy/circle.hlean @@ -158,13 +158,25 @@ namespace circle (Ploop : Pbase ≃ Pbase) : Type := circle.elim_type Pbase Ploop x - theorem elim_type_loop (Pbase : Type) (Ploop : Pbase ≃ Pbase) : + theorem elim_type_loop_fn (Pbase : Type) (Ploop : Pbase ≃ Pbase) : transport (circle.elim_type Pbase Ploop) loop = Ploop := by rewrite [tr_eq_cast_ap_fn,↑circle.elim_type,elim_loop];apply cast_ua_fn - theorem elim_type_loop_inv (Pbase : Type) (Ploop : Pbase ≃ Pbase) : + theorem elim_type_loop (Pbase : Type) (Ploop : Pbase ≃ Pbase) (x : Pbase) : + transport (circle.elim_type Pbase Ploop) loop x = Ploop x := + apd10 (elim_type_loop_fn Pbase Ploop) x + + definition elim_type_loop_pathover (Pbase : Type) (Ploop : Pbase ≃ Pbase) (x : Pbase) : + x =[loop; circle.elim_type Pbase Ploop] Ploop x := + pathover_of_tr_eq (elim_type_loop Pbase Ploop x) + + theorem elim_type_loop_inv_fn (Pbase : Type) (Ploop : Pbase ≃ Pbase) : transport (circle.elim_type Pbase Ploop) loop⁻¹ = to_inv Ploop := - by rewrite [tr_inv_fn]; apply inv_eq_inv; apply elim_type_loop + by rewrite [tr_inv_fn]; apply inv_eq_inv; apply elim_type_loop_fn + + theorem elim_type_loop_inv (Pbase : Type) (Ploop : Pbase ≃ Pbase) (x : Pbase) : + transport (circle.elim_type Pbase Ploop) loop⁻¹ x = to_inv Ploop x := + apd10 (elim_type_loop_inv_fn Pbase Ploop) x end circle attribute circle.base1 circle.base2 circle.base [constructor] @@ -244,10 +256,10 @@ namespace circle circle.elim_type_on x ℤ equiv_succ definition transport_code_loop (a : ℤ) : transport circle.code loop a = succ a := - ap10 !elim_type_loop a + !elim_type_loop definition transport_code_loop_inv (a : ℤ) : transport circle.code loop⁻¹ a = pred a := - ap10 !elim_type_loop_inv a + !elim_type_loop_inv protected definition encode [unfold 2] {x : S¹} (p : base = x) : circle.code x := transport circle.code p (0 : ℤ) diff --git a/hott/types/fiber.hlean b/hott/types/fiber.hlean index 9b96c658b..f6fa70c18 100644 --- a/hott/types/fiber.hlean +++ b/hott/types/fiber.hlean @@ -168,13 +168,13 @@ namespace fiber ... ≃ Σa' (b : B a'), a' = a : sigma_assoc_equiv ... ≃ Σa' (p : a' = a), B a' : sigma_equiv_sigma_right (λa', !comm_equiv_nondep) ... ≃ Σu, B u.1 : sigma_assoc_equiv - ... ≃ B a : !sigma_equiv_of_is_contr_left + ... ≃ B a : sigma_equiv_of_is_contr_left _ _ definition sigma_fiber_equiv (f : A → B) : (Σb, fiber f b) ≃ A := calc (Σb, fiber f b) ≃ Σb a, f a = b : sigma_equiv_sigma_right (λb, !fiber.sigma_char) ... ≃ Σa b, f a = b : sigma_comm_equiv - ... ≃ A : sigma_equiv_of_is_contr_right + ... ≃ A : sigma_equiv_of_is_contr_right _ _ definition fiber_compose_equiv {A B C : Type} (g : B → C) (f : A → B) (c : C) : fiber (g ∘ f) c ≃ Σ(x : fiber g c), fiber f (point x) := @@ -281,9 +281,9 @@ namespace fiber ... ≃ fiber (f a) q : fiber.sigma_char - definition fiber_equiv_of_is_contr [constructor] {A B : Type} (f : A → B) (b : B) [is_contr B] : - fiber f b ≃ A := - !fiber.sigma_char ⬝e !sigma_equiv_of_is_contr_right + definition fiber_equiv_of_is_contr [constructor] {A B : Type} (f : A → B) (b : B) + (H : is_contr B) : fiber f b ≃ A := + !fiber.sigma_char ⬝e sigma_equiv_of_is_contr_right _ _ /- the pointed fiber of a pointed map, which is the fiber over the basepoint -/ @@ -413,16 +413,16 @@ namespace fiber [is_trunc n A] [is_trunc (n.+1) B] : is_trunc n (pfiber f) := is_trunc_fiber n f pt - definition pfiber_pequiv_of_is_contr [constructor] {A B : Type*} (f : A →* B) [is_contr B] : + definition pfiber_pequiv_of_is_contr [constructor] {A B : Type*} (f : A →* B) (H : is_contr B) : pfiber f ≃* A := - pequiv_of_equiv (fiber_equiv_of_is_contr f pt) idp + pequiv_of_equiv (fiber_equiv_of_is_contr f pt H) idp definition pfiber_ppoint_equiv {A B : Type*} (f : A →* B) : pfiber (ppoint f) ≃ Ω B := calc pfiber (ppoint f) ≃ Σ(x : pfiber f), ppoint f x = pt : fiber.sigma_char ... ≃ Σ(x : Σa, f a = pt), x.1 = pt : by exact sigma_equiv_sigma !fiber.sigma_char (λa, erfl) ... ≃ Σ(x : Σa, a = pt), f x.1 = pt : by exact !sigma_assoc_comm_equiv - ... ≃ f pt = pt : by exact !sigma_equiv_of_is_contr_left + ... ≃ f pt = pt : by exact sigma_equiv_of_is_contr_left _ _ ... ≃ Ω B : by exact !equiv_eq_closed_left !respect_pt definition pfiber_ppoint_pequiv {A B : Type*} (f : A →* B) : pfiber (ppoint f) ≃* Ω B := diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean index 4f476c119..4b827af04 100644 --- a/hott/types/sigma.hlean +++ b/hott/types/sigma.hlean @@ -265,7 +265,7 @@ namespace sigma definition sigma_pathover_equiv_of_is_prop {A : Type} {B : A → Type} (C : Πa, B a → Type) {a a' : A} (p : a = a') (x : Σb, C a b) (x' : Σb', C a' b') - [Πa b, is_prop (C a b)] : x =[p] x' ≃ x.1 =[p] x'.1 := + (H : Πa b, is_prop (C a b)) : x =[p] x' ≃ x.1 =[p] x'.1 := begin fapply equiv.MK, { exact pathover_pr1 }, @@ -397,13 +397,13 @@ namespace sigma (λa, idp) (λu, sigma_eq idp (pathover_idp_of_eq !center_eq)) - definition sigma_equiv_of_is_contr_right [constructor] [H : Π a, is_contr (B a)] + definition sigma_equiv_of_is_contr_right [constructor] (B : A → Type) (H : Π a, is_contr (B a)) : (Σa, B a) ≃ A := equiv.mk pr1 _ /- definition 3.11.9(ii): Dually, summing up over a contractible type does nothing. -/ - definition sigma_equiv_of_is_contr_left [constructor] (B : A → Type) [H : is_contr A] + definition sigma_equiv_of_is_contr_left [constructor] (B : A → Type) (H : is_contr A) : (Σa, B a) ≃ B (center A) := equiv.MK (λu, (center_eq u.1)⁻¹ ▸ u.2) @@ -484,10 +484,10 @@ namespace sigma end definition sigma_unit_left [constructor] (B : unit → Type) : (Σx, B x) ≃ B star := - !sigma_equiv_of_is_contr_left + sigma_equiv_of_is_contr_left B _ definition sigma_unit_right [constructor] (A : Type) : (Σ(a : A), unit) ≃ A := - !sigma_equiv_of_is_contr_right + sigma_equiv_of_is_contr_right _ _ definition sigma_sum_left [constructor] (B : A + A' → Type) : (Σp, B p) ≃ (Σa, B (inl a)) + (Σa, B (inr a)) := @@ -524,13 +524,17 @@ namespace sigma : (Σ(b : A) (p : a = b), P b p) ≃ P a idp := calc (Σ(b : A) (p : a = b), P b p) ≃ (Σ(v : Σ(b : A), a = b), P v.1 v.2) : sigma_assoc_equiv - ... ≃ P a idp : !sigma_equiv_of_is_contr_left + ... ≃ P a idp : sigma_equiv_of_is_contr_left _ _ definition sigma_sigma_eq_left {A : Type} (a : A) (P : Π(b : A), b = a → Type) : (Σ(b : A) (p : b = a), P b p) ≃ P a idp := calc (Σ(b : A) (p : b = a), P b p) ≃ (Σ(v : Σ(b : A), b = a), P v.1 v.2) : sigma_assoc_equiv - ... ≃ P a idp : !sigma_equiv_of_is_contr_left + ... ≃ P a idp : sigma_equiv_of_is_contr_left _ _ + + definition sigma_assoc_equiv_of_is_contr_left [constructor] (C : (Σa, B a) → Type) + (H : is_contr (Σa, B a)) : (Σa b, C ⟨a, b⟩) ≃ C (@center _ H) := + sigma_assoc_equiv C ⬝e !sigma_equiv_of_is_contr_left /- ** Universal mapping properties -/ /- *** The positive universal property. -/ @@ -604,7 +608,7 @@ namespace sigma begin revert A B HA HB, induction n with n IH, - { intro A B HA HB, exact is_contr_equiv_closed_rev !sigma_equiv_of_is_contr_left _ }, + { intro A B HA HB, exact is_contr_equiv_closed_rev (sigma_equiv_of_is_contr_left _ _) _ }, { intro A B HA HB, apply is_trunc_succ_intro, intro u v, exact is_trunc_equiv_closed_rev n !sigma_eq_equiv (IH _ _ _ _) } end diff --git a/hott/types/univ.hlean b/hott/types/univ.hlean index a4ebb46d7..4db075a89 100644 --- a/hott/types/univ.hlean +++ b/hott/types/univ.hlean @@ -110,7 +110,7 @@ namespace univ (calc A ≃ Σb, fiber f b : sigma_fiber_equiv ... ≃ Σb (v : ΣX, X = fiber f b), v.1 : sigma_equiv_sigma_right - (λb, !sigma_equiv_of_is_contr_left) + (λb, sigma_equiv_of_is_contr_left _ _) ... ≃ Σb X (p : X = fiber f b), X : sigma_equiv_sigma_right (λb, !sigma_assoc_equiv) ... ≃ Σb X (x : X), X = fiber f b : sigma_equiv_sigma_right