michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

make instances in sigma explicit

Browse source
This commit is contained in:
Floris van Doorn 2018-09-14 17:56:25 +02:00
parent 609da93df0
commit 4b603990fc
5 changed files with 39 additions and 23 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
hott/function.hlean
View file

@ -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' :=

22
hott/homotopy/circle.hlean
View file

@ -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 : ℤ)

16
hott/types/fiber.hlean
View file

@ -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 :=

20
hott/types/sigma.hlean
View file

@ -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

2
hott/types/univ.hlean
View file

@ -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