fix(hott): small fixes

This commit is contained in:
Floris van Doorn 2017-03-07 22:49:06 -05:00
parent 8bdd699fca
commit 540d451e01
12 changed files with 65 additions and 62 deletions

View file

@ -7,13 +7,13 @@ Authors: Jakob von Raumer
The Rezk completion
-/
import algebra.category hit.two_quotient types.trunc types.arrow algebra.category.functor.attributes
import hit.two_quotient types.trunc types.arrow algebra.category.functor.exponential_laws
open eq category equiv trunc_two_quotient is_trunc iso e_closure function pi trunctype
namespace rezk
section
universes l k
parameters {A : Type.{l}} [C : precategory.{l k} A]
include C
@ -57,7 +57,7 @@ namespace rezk
(Pe : Π a, P (elt a)) (Pp : Π ⦃a b⦄ (f : a ≅ b), Pe a =[pth f] Pe b)
(Pcomp : Π ⦃a b c⦄ (g : b ≅ c) (f : a ≅ b),
change_path (resp_comp g f) (Pp (f ⬝i g)) = Pp f ⬝o Pp g) : P x :=
rec Pe Pp Pcomp x
rec Pe Pp Pcomp x
protected definition set_rec {P : rezk_carrier → Type} [Π x, is_set (P x)]
(Pe : Π a, P (elt a)) (Pp : Π⦃a b⦄ (f : a ≅ b), Pe a =[pth f] Pe b)
@ -68,7 +68,7 @@ namespace rezk
(Pe : Π a, P (elt a)) (x : rezk_carrier) : P x :=
rec Pe !center !center x
protected definition elim {P : Type} [is_trunc 1 P] (Pe : A → P)
protected definition elim {P : Type} [is_trunc 1 P] (Pe : A → P)
(Pp : Π ⦃a b⦄ (f : a ≅ b), Pe a = Pe b)
(Pcomp : Π ⦃a b c⦄ (g : b ≅ c) (f : a ≅ b), Pp (f ⬝i g) = Pp f ⬝ Pp g)
(x : rezk_carrier) : P :=
@ -79,7 +79,7 @@ namespace rezk
{ induction q with a b c g f, exact Pcomp g f }
end
protected definition elim_on [reducible] {P : Type} [is_trunc 1 P] (x : rezk_carrier)
protected definition elim_on [reducible] {P : Type} [is_trunc 1 P] (x : rezk_carrier)
(Pe : A → P) (Pp : Π ⦃a b⦄ (f : a ≅ b), Pe a = Pe b)
(Pcomp : Π ⦃a b c⦄ (g : b ≅ c) (f : a ≅ b), Pp (f ⬝i g) = Pp f ⬝ Pp g) : P :=
elim Pe Pp Pcomp x
@ -157,9 +157,9 @@ namespace rezk
--induction b using rezk.rec with b' b' b g, --why does this not work if it works below?
refine @rezk.rec _ _ _ (rezk_hom_left_pth_1_trunc a a' f) _ _ _ b,
intro b, apply equiv_precompose (to_hom f⁻¹ⁱ), --how do i unfold properly at this point?
{ intro b b' g, apply equiv_pathover, intro g' g'' H,
{ intro b b' g, apply equiv_pathover, intro g' g'' H,
refine !pathover_rezk_hom_left_pt ⬝op _,
refine !assoc ⬝ ap (λ x, x ∘ _) _, refine eq_of_parallel_po_right _ H,
refine !assoc ⬝ ap (λ x, x ∘ _) _, refine eq_of_parallel_po_right _ H,
apply pathover_rezk_hom_left_pt },
intro b b' b'' g g', apply @is_prop.elim, apply is_trunc_pathover, apply is_trunc_equiv
end
@ -211,8 +211,8 @@ namespace rezk
induction c using rezk.set_rec with c c c' ic,
exact g ∘ f,
{ apply arrow_pathover_left, intro d,
apply concato !pathover_rezk_hom_left_pt, apply pathover_idp_of_eq,
apply concat, apply assoc, apply ap (λ x, x ∘ f),
apply concato !pathover_rezk_hom_left_pt, apply pathover_idp_of_eq,
apply concat, apply assoc, apply ap (λ x, x ∘ f),
apply inverse, apply tr_eq_of_pathover, apply pathover_rezk_hom_left_pt },
end
@ -223,13 +223,13 @@ namespace rezk
apply arrow_pathover_left, intro x,
apply arrow_pathover_left, intro y,
induction c using rezk.set_rec with c c c' ic,
{ apply pathover_of_eq, apply inverse,
{ apply pathover_of_eq, apply inverse,
apply concat, apply ap (λ x, rezk_comp_pt_pt x _), apply tr_eq_of_pathover,
apply pathover_rezk_hom_left,
apply concat, apply ap (rezk_comp_pt_pt _), apply tr_eq_of_pathover,
apply pathover_rezk_hom_left_pt,
refine !assoc ⬝ ap (λ x, x ∘ y) _,
refine !assoc⁻¹ ⬝ _,
refine !assoc ⬝ ap (λ x, x ∘ y) _,
refine !assoc⁻¹ ⬝ _,
refine ap (λ y, x ∘ y) !iso.left_inverse ⬝ _,
apply id_right },
apply @is_prop.elimo
@ -241,8 +241,8 @@ namespace rezk
induction a using rezk.set_rec with a a a' ia,
{ induction b using rezk.set_rec with b b b' ib,
apply rezk_comp_pt_pt g f, apply rezk_comp_pt_pth },
{ induction b using rezk.set_rec with b b b' ib,
apply arrow_pathover_left, intro f,
{ induction b using rezk.set_rec with b b b' ib,
apply arrow_pathover_left, intro f,
induction c using rezk.set_rec with c c c' ic,
{ apply concato, apply pathover_rezk_hom_left,
apply pathover_idp_of_eq, refine !assoc⁻¹ ⬝ ap (λ x, g ∘ x) _⁻¹,
@ -291,7 +291,7 @@ namespace rezk
intro C, apply Precategory.mk (@rezk_carrier (Precategory.carrier C) C),
apply rezk_precategory _ _,
end
definition rezk_functor [constructor] (C : Precategory) : functor C (to_rezk_Precategory C) :=
begin
fapply functor.mk, apply elt,
@ -337,7 +337,7 @@ namespace rezk
(p : a = a') : to_hom (transport (λ x, iso x b) p f) = transport (λ x, hom _ _) p (to_hom f) :=
by cases p; reflexivity
private definition pathover_iso_pth {a b b' : A} (f : elt a ≅ elt b)
private definition pathover_iso_pth {a b b' : A} (f : elt a ≅ elt b)
(ib : b ≅ b') : pathover (λ x, iso (elt a) x) f (pth ib) (f ⬝i elt_iso_of_iso ib) :=
begin
apply pathover_of_tr_eq, apply iso_eq,
@ -361,9 +361,9 @@ namespace rezk
apply pth, apply iso_of_elt_iso f,
apply arrow_pathover, intro f g p, apply eq_pathover,
refine !ap_constant ⬝ph _ ⬝hp !ap_id⁻¹, apply square_of_eq,
refine !resp_comp⁻¹ ⬝ (ap pth _)⁻¹ ⬝ !idp_con⁻¹,
apply concat, apply inverse, apply ap rezk.iso_of_elt_iso,
apply eq_of_parallel_po_right (pathover_iso_pth _ _) p,
refine !resp_comp⁻¹ ⬝ (ap pth _)⁻¹ ⬝ !idp_con⁻¹,
apply concat, apply inverse, apply ap rezk.iso_of_elt_iso,
apply eq_of_parallel_po_right (pathover_iso_pth _ _) p,
apply concat, apply iso_of_elt_iso_distrib,
apply ap (λ x, _ ⬝i x), apply equiv.to_left_inv !iso_equiv_elt_iso
end
@ -377,12 +377,12 @@ namespace rezk
{ induction b using rezk.set_rec with b b b' ib,
{ apply arrow_pathover, intro f g p, apply eq_pathover,
refine !ap_id ⬝ph _ ⬝hp !ap_constant⁻¹, apply square_of_eq,
refine (ap pth _) ⬝ !resp_comp,
refine (ap pth _) ⬝ !resp_comp,
assert H : g = (elt_iso_of_iso (iso.symm ia) ⬝i f),
apply eq_of_parallel_po_right p (pathover_iso_pth' _ _),
rewrite H, apply inverse,
rewrite H, apply inverse,
apply concat, apply ap (λ x, ia ⬝i x), apply iso_of_elt_iso_distrib,
apply concat, apply ap (λ x, _ ⬝i (x ⬝i _)), apply equiv.to_left_inv !iso_equiv_elt_iso,
apply concat, apply ap (λ x, _ ⬝i (x ⬝i _)), apply equiv.to_left_inv !iso_equiv_elt_iso,
apply iso_eq, apply inverse_comp_cancel_right },
apply @is_prop.elimo }
end
@ -437,5 +437,5 @@ namespace rezk
prod.mk (fully_faithful_rezk_functor C) (essentially_surj_rezk_functor C)
end
end rezk

View file

@ -4,4 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Floris van Doorn
-/
import .homotopy_group .ordered_field
import .homotopy_group .ordered_field .lattice

View file

@ -30,12 +30,12 @@ namespace eq
{p₁₂₀ : a₀₂₀ = a₂₂₀} {p₂₁₀ : a₂₀₀ = a₂₂₀} {p₂₀₁ : a₂₀₀ = a₂₀₂}
{p₁₀₂ : a₀₀₂ = a₂₀₂} {p₀₁₂ : a₀₀₂ = a₀₂₂} {p₀₂₁ : a₀₂₀ = a₀₂₂}
{p₁₂₂ : a₀₂₂ = a₂₂₂} {p₂₁₂ : a₂₀₂ = a₂₂₂} {p₂₂₁ : a₂₂₀ = a₂₂₂}
{s₁₁₀ : square p₀₁₀ p₂₁₀ p₁₀₀ p₁₂₀}
{s₁₁₂ : square p₀₁₂ p₂₁₂ p₁₀₂ p₁₂₂}
{s₀₁₁ : square p₀₁₀ p₀₁₂ p₀₀₁ p₀₂₁}
{s₂₁₁ : square p₂₁₀ p₂₁₂ p₂₀₁ p₂₂₁}
{s₁₀₁ : square p₁₀₀ p₁₀₂ p₀₀₁ p₂₀₁}
{s₁₂₁ : square p₁₂₀ p₁₂₂ p₀₂₁ p₂₂₁}
{s₁₁₀ : square p₀₁₀ p₂₁₀ p₁₀₀ p₁₂₀}
{s₁₁₂ : square p₀₁₂ p₂₁₂ p₁₀₂ p₁₂₂}
{b₁ b₂ b₃ b₄ : B}
(c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂)
@ -126,6 +126,7 @@ namespace eq
/- Transporting along a square -/
-- TODO: remove: they are defined again below
definition cube_transport110 {s₁₁₀' : square p₀₁₀ p₂₁₀ p₁₀₀ p₁₂₀}
(p : s₁₁₀ = s₁₁₀') (c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) :
cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀' s₁₁₂ :=
@ -339,11 +340,11 @@ namespace eq
infix ` ⬝1 `:75 := cube_concat1
infix ` ⬝2 `:75 := cube_concat2
infix ` ⬝3 `:75 := cube_concat3
infix ` ⬝p1 `:75 := eq_concat1
infix ` ⬝1p `:75 := concat1_eq
infix ` ⬝p2 `:75 := eq_concat3
infix ` ⬝2p `:75 := concat2_eq
infix ` ⬝p3 `:75 := eq_concat3
infix ` ⬝3p `:75 := concat3_eq
infixr ` ⬝p1 `:75 := eq_concat1
infixl ` ⬝1p `:75 := concat1_eq
infixr ` ⬝p2 `:75 := eq_concat2
infixl ` ⬝2p `:75 := concat2_eq
infixr ` ⬝p3 `:75 := eq_concat3
infixl ` ⬝3p `:75 := concat3_eq
end eq

View file

@ -88,10 +88,10 @@ namespace eq
infix ` ⬝h `:69 := hconcat --type using \tr
infix ` ⬝v `:70 := vconcat --type using \tr
infix ` ⬝hp `:71 := hconcat_eq --type using \tr
infix ` ⬝vp `:73 := vconcat_eq --type using \tr
infix ` ⬝ph `:72 := eq_hconcat --type using \tr
infix ` ⬝pv `:74 := eq_vconcat --type using \tr
infixl ` ⬝hp `:71 := hconcat_eq --type using \tr
infixl ` ⬝vp `:73 := vconcat_eq --type using \tr
infixr ` ⬝ph `:72 := eq_hconcat --type using \tr
infixr ` ⬝pv `:74 := eq_vconcat --type using \tr
postfix `⁻¹ʰ`:(max+1) := hinverse --type using \-1h
postfix `⁻¹ᵛ`:(max+1) := vinverse --type using \-1v

View file

@ -206,7 +206,7 @@ namespace pushout
krewrite [elim_glue, ap_inv, elim_glue, inv_inv], apply hrfl
end
protected definition symm : pushout f g ≃ pushout g f :=
protected definition symm [constructor] : pushout f g ≃ pushout g f :=
begin
fapply equiv.MK, do 2 exact !pushout.transpose,
do 2 (intro x; apply pushout.transpose_involutive),
@ -234,7 +234,7 @@ namespace pushout
(fh : bl ∘ f ~ f' ∘ tl) (gh : tr ∘ g ~ g' ∘ tl)
include fh gh
protected definition functor [reducible] : pushout f g → pushout f' g' :=
protected definition functor [reducible] [unfold 16] : pushout f g → pushout f' g' :=
begin
intro x, induction x with a b z,
{ exact inl (bl a) },
@ -254,7 +254,7 @@ namespace pushout
include ietl iebl ietr
open equiv is_equiv arrow
protected definition is_equiv_functor [instance]
protected definition is_equiv_functor [instance] [constructor]
: is_equiv (pushout.functor tl bl tr fh gh) :=
adjointify
(pushout.functor tl bl tr fh gh)
@ -336,7 +336,7 @@ namespace pushout
(fh : bl ∘ f ~ f' ∘ tl) (gh : tr ∘ g ~ g' ∘ tl)
include fh gh
protected definition equiv : pushout f g ≃ pushout f' g' :=
protected definition equiv [constructor] : pushout f g ≃ pushout f' g' :=
equiv.mk (pushout.functor tl bl tr fh gh) _
end

View file

@ -11,7 +11,7 @@ open eq pushout pointed unit trunc_index
definition wedge (A B : Type*) : Type := ppushout (pconst punit A) (pconst punit B)
local attribute wedge [reducible]
definition pwedge (A B : Type*) : Type* := pointed.mk' (wedge A B)
definition pwedge [constructor] (A B : Type*) : Type* := pointed.mk' (wedge A B)
infixr ` ` := pwedge
namespace wedge

View file

@ -88,6 +88,7 @@ structure ppi (A : Type*) (P : A → Type*) :=
(to_fun : Π a : A, P a)
(resp_pt : to_fun (Point A) = Point (P (Point A)))
-- We could try to define pmap as a special case of ppi
-- definition pmap (A B : Type*) := @ppi A (λa, B)
structure pmap (A B : Type*) :=
(to_fun : A → B)

View file

@ -325,7 +325,7 @@ namespace is_trunc
open equiv
/- A contractible type is equivalent to unit. -/
variable (A)
definition equiv_unit_of_is_contr [H : is_contr A] : A ≃ unit :=
definition equiv_unit_of_is_contr [constructor] [H : is_contr A] : A ≃ unit :=
equiv.MK (λ (x : A), ⋆)
(λ (u : unit), center A)
(λ (u : unit), unit.rec_on u idp)

View file

@ -21,73 +21,73 @@ namespace eq
/- some lemmas about whiskering or other higher paths -/
theorem whisker_left_con_right (p : a₁ = a₂) {q q' q'' : a₂ = a₃} (r : q = q') (s : q' = q'')
definition whisker_left_con_right (p : a₁ = a₂) {q q' q'' : a₂ = a₃} (r : q = q') (s : q' = q'')
: whisker_left p (r ⬝ s) = whisker_left p r ⬝ whisker_left p s :=
begin
induction p, induction r, induction s, reflexivity
end
theorem whisker_right_con_right (q : a₂ = a₃) (r : p = p') (s : p' = p'')
definition whisker_right_con_right (q : a₂ = a₃) (r : p = p') (s : p' = p'')
: whisker_right q (r ⬝ s) = whisker_right q r ⬝ whisker_right q s :=
begin
induction q, induction r, induction s, reflexivity
end
theorem whisker_left_con_left (p : a₁ = a₂) (p' : a₂ = a₃) {q q' : a₃ = a₄} (r : q = q')
definition whisker_left_con_left (p : a₁ = a₂) (p' : a₂ = a₃) {q q' : a₃ = a₄} (r : q = q')
: whisker_left (p ⬝ p') r = !con.assoc ⬝ whisker_left p (whisker_left p' r) ⬝ !con.assoc' :=
begin
induction p', induction p, induction r, induction q, reflexivity
end
theorem whisker_right_con_left {p p' : a₁ = a₂} (q : a₂ = a₃) (q' : a₃ = a₄) (r : p = p')
definition whisker_right_con_left {p p' : a₁ = a₂} (q : a₂ = a₃) (q' : a₃ = a₄) (r : p = p')
: whisker_right (q ⬝ q') r = !con.assoc' ⬝ whisker_right q' (whisker_right q r) ⬝ !con.assoc :=
begin
induction q', induction q, induction r, induction p, reflexivity
end
theorem whisker_left_inv_left (p : a₂ = a₁) {q q' : a₂ = a₃} (r : q = q')
definition whisker_left_inv_left (p : a₂ = a₁) {q q' : a₂ = a₃} (r : q = q')
: !con_inv_cancel_left⁻¹ ⬝ whisker_left p (whisker_left p⁻¹ r) ⬝ !con_inv_cancel_left = r :=
begin
induction p, induction r, induction q, reflexivity
end
theorem whisker_left_inv (p : a₁ = a₂) {q q' : a₂ = a₃} (r : q = q')
definition whisker_left_inv (p : a₁ = a₂) {q q' : a₂ = a₃} (r : q = q')
: whisker_left p r⁻¹ = (whisker_left p r)⁻¹ :=
by induction r; reflexivity
theorem whisker_right_inv {p p' : a₁ = a₂} (q : a₂ = a₃) (r : p = p')
definition whisker_right_inv {p p' : a₁ = a₂} (q : a₂ = a₃) (r : p = p')
: whisker_right q r⁻¹ = (whisker_right q r)⁻¹ :=
by induction r; reflexivity
theorem ap_eq_apd10 {B : A → Type} {f g : Πa, B a} (p : f = g) (a : A) :
definition ap_eq_apd10 [unfold 5] {B : A → Type} {f g : Πa, B a} (p : f = g) (a : A) :
ap (λh, h a) p = apd10 p a :=
by induction p; reflexivity
theorem inverse2_right_inv (r : p = p') : r ◾ inverse2 r ⬝ con.right_inv p' = con.right_inv p :=
definition inverse2_right_inv (r : p = p') : r ◾ inverse2 r ⬝ con.right_inv p' = con.right_inv p :=
by induction r;induction p;reflexivity
theorem inverse2_left_inv (r : p = p') : inverse2 r ◾ r ⬝ con.left_inv p' = con.left_inv p :=
definition inverse2_left_inv (r : p = p') : inverse2 r ◾ r ⬝ con.left_inv p' = con.left_inv p :=
by induction r;induction p;reflexivity
theorem ap_con_right_inv (f : A → B) (p : a₁ = a₂)
definition ap_con_right_inv (f : A → B) (p : a₁ = a₂)
: ap_con f p p⁻¹ ⬝ whisker_left _ (ap_inv f p) ⬝ con.right_inv (ap f p)
= ap (ap f) (con.right_inv p) :=
by induction p;reflexivity
theorem ap_con_left_inv (f : A → B) (p : a₁ = a₂)
definition ap_con_left_inv (f : A → B) (p : a₁ = a₂)
: ap_con f p⁻¹ p ⬝ whisker_right _ (ap_inv f p) ⬝ con.left_inv (ap f p)
= ap (ap f) (con.left_inv p) :=
by induction p;reflexivity
theorem idp_con_whisker_left {q q' : a₂ = a₃} (r : q = q') :
definition idp_con_whisker_left {q q' : a₂ = a₃} (r : q = q') :
!idp_con⁻¹ ⬝ whisker_left idp r = r ⬝ !idp_con⁻¹ :=
by induction r;induction q;reflexivity
theorem whisker_left_idp_con {q q' : a₂ = a₃} (r : q = q') :
definition whisker_left_idp_con {q q' : a₂ = a₃} (r : q = q') :
whisker_left idp r ⬝ !idp_con = !idp_con ⬝ r :=
by induction r;induction q;reflexivity
theorem idp_con_idp {p : a = a} (q : p = idp) : idp_con p ⬝ q = ap (λp, idp ⬝ p) q :=
definition idp_con_idp {p : a = a} (q : p = idp) : idp_con p ⬝ q = ap (λp, idp ⬝ p) q :=
by cases q;reflexivity
definition ap_is_constant [unfold 8] {A B : Type} {f : A → B} {b : B} (p : Πx, f x = b)
@ -105,13 +105,13 @@ namespace eq
: (r₁ ◾ r₂)⁻¹ = r₁⁻¹ ◾ r₂⁻¹ :=
by induction r₁;induction r₂;reflexivity
theorem eq_con_inv_of_con_eq_whisker_left {A : Type} {a a₂ a₃ : A}
definition eq_con_inv_of_con_eq_whisker_left {A : Type} {a a₂ a₃ : A}
{p : a = a₂} {q q' : a₂ = a₃} {r : a = a₃} (s' : q = q') (s : p ⬝ q' = r) :
eq_con_inv_of_con_eq (whisker_left p s' ⬝ s)
= eq_con_inv_of_con_eq s ⬝ whisker_left r (inverse2 s')⁻¹ :=
by induction s';induction q;induction s;reflexivity
theorem right_inv_eq_idp {A : Type} {a : A} {p : a = a} (r : p = idpath a) :
definition right_inv_eq_idp {A : Type} {a : A} {p : a = a} (r : p = idpath a) :
con.right_inv p = r ◾ inverse2 r :=
by cases r;reflexivity

View file

@ -305,7 +305,7 @@ namespace pointed
{ apply idp_con}
end
protected definition phomotopy.rfl [constructor] {f : A →* B} : f ~* f :=
protected definition phomotopy.rfl [constructor] [reducible] {f : A →* B} : f ~* f :=
phomotopy.refl f
protected definition phomotopy.trans [constructor] [trans] (p : f ~* g) (q : g ~* h)
@ -782,7 +782,7 @@ namespace pointed
(p : h ~* f⁻¹ᵉ* ∘* g) : f ∘* h ~* g :=
(phomotopy_of_pinv_left_phomotopy p⁻¹*)⁻¹*
definition pcompose2 {A B C : Type*} {g g' : B →* C} {f f' : A →* B} (p : f ~* f') (q : g ~* g') :
definition pcompose2 {A B C : Type*} {g g' : B →* C} {f f' : A →* B} (q : g ~* g') (p : f ~* f') :
g ∘* f ~* g' ∘* f' :=
pwhisker_right f q ⬝* pwhisker_left g' p

View file

@ -116,7 +116,7 @@ namespace sum
/- Equivalences -/
definition is_equiv_sum_functor [constructor] [Hf : is_equiv f] [Hg : is_equiv g]
definition is_equiv_sum_functor [constructor] [instance] [Hf : is_equiv f] [Hg : is_equiv g]
: is_equiv (sum_functor f g) :=
adjointify (sum_functor f g)
(sum_functor f⁻¹ g⁻¹)

View file

@ -356,6 +356,7 @@ order for the change to take effect."
("-1s" . ("⁻¹ˢ"))
("-1v" . ("⁻¹ᵛ"))
("-1E" . ("⁻¹ᴱ"))
("-1hty" . ("⁻¹ʰᵗʸ"))
("-2" . ("⁻²" "₋₂"))
("-2o" . ("⁻²ᵒ"))
("-3" . ("⁻³"))