feat(hott/algebra/category): show that functor category is univalent if codomain is

This commit is contained in:
Floris van Doorn 2015-03-13 18:27:29 -04:00 committed by Leonardo de Moura
parent ebba33057c
commit c914b79341
13 changed files with 261 additions and 123 deletions

View file

@ -36,7 +36,7 @@ namespace category
-- TODO: Unsafe class instance? -- TODO: Unsafe class instance?
attribute iso_of_path_equiv [instance] attribute iso_of_path_equiv [instance]
definition eq_of_iso {a b : ob} : a ≅ b → a = b := definition eq_of_iso [reducible] {a b : ob} : a ≅ b → a = b :=
iso_of_eq⁻¹ᵉ iso_of_eq⁻¹ᵉ
set_option apply.class_instance false -- disable class instance resolution in the apply tactic set_option apply.class_instance false -- disable class instance resolution in the apply tactic

View file

@ -93,9 +93,9 @@ namespace category
definition eq_of_iso_functor (η : F ≅ G) : F = G := definition eq_of_iso_functor (η : F ≅ G) : F = G :=
begin begin
fapply functor_eq_mk, fapply functor_eq,
{exact (eq_of_iso_functor_ob η)}, {exact (eq_of_iso_functor_ob η)},
{intros (c, c', f), {intros (c, c', f), --unfold eq_of_iso_functor_ob, --TODO: report: this fails
apply concat, apply concat,
{apply (ap (λx, to_hom x ∘ to_fun_hom F f ∘ _)), apply (retr iso_of_eq)}, {apply (ap (λx, to_hom x ∘ to_fun_hom F f ∘ _)), apply (retr iso_of_eq)},
apply concat, apply concat,
@ -107,33 +107,42 @@ namespace category
-- definition is_univalent_functor (C : Precategory) (D : Category) : is_univalent (D ^c C) := -- definition is_univalent_functor (C : Precategory) (D : Category) : is_univalent (D ^c C) :=
-- λ(F G : D ^c C), adjointify _ eq_of_iso_functor sorry sorry -- λ(F G : D ^c C), adjointify _ eq_of_iso_functor sorry sorry
-- definition iso_of_hom
definition iso_of_eq_eq_of_iso_functor (η : F ≅ G) : iso_of_eq (eq_of_iso_functor η) = η := definition iso_of_eq_eq_of_iso_functor (η : F ≅ G) : iso_of_eq (eq_of_iso_functor η) = η :=
begin begin
apply iso.eq_mk, apply iso.eq_mk,
apply nat_trans_eq_mk, apply nat_trans_eq_mk,
intro c, intro c,
apply concat, apply natural_map_hom_of_eq, rewrite natural_map_hom_of_eq, esimp {eq_of_iso_functor},
apply concat, {apply (ap hom_of_eq), apply ap010_functor_eq_mk}, rewrite ap010_functor_eq, esimp {hom_of_eq,eq_of_iso_functor_ob},
apply concat, {apply (ap to_hom), apply (retr iso_of_eq)}, rewrite (retr iso_of_eq),
apply idp
end
--check natural_map_
definition eq_of_iso_functor_iso_of_eq (p : F = G) : eq_of_iso_functor (iso_of_eq p) = p :=
begin
apply sorry
end end
definition is_univalent_functor (C : Precategory) (D : Category) : is_univalent (D ^c C) := definition eq_of_iso_functor_iso_of_eq (p : F = G) : eq_of_iso_functor (iso_of_eq p) = p :=
begin
apply functor_eq2,
intro c,
esimp {eq_of_iso_functor},
rewrite ap010_functor_eq,
esimp {eq_of_iso_functor_ob},
rewrite componentwise_iso_iso_of_eq,
rewrite (sect iso_of_eq)
end
definition is_univalent_functor (D : Category) (C : Precategory) : is_univalent (D ^c C) :=
λF G, adjointify _ eq_of_iso_functor λF G, adjointify _ eq_of_iso_functor
iso_of_eq_eq_of_iso_functor iso_of_eq_eq_of_iso_functor
eq_of_iso_functor_iso_of_eq eq_of_iso_functor_iso_of_eq
end functor end functor
definition Category_functor_of_precategory (D : Category) (C : Precategory) : Category :=
category.MK (D ^c C) (is_univalent_functor D C)
definition category_functor (C : Precategory) (D : Category) : Category := definition Category_functor (D : Category) (C : Category) : Category :=
category.MK (D ^c C) (is_univalent_functor C D) Category_functor_of_precategory D C
namespace ops
infixr `^c2`:35 := Category_functor
end ops
end category end category

View file

@ -47,7 +47,8 @@ namespace category
definition id_comp (a : ob) : ID a ∘ ID a = ID a := !id_left definition id_comp (a : ob) : ID a ∘ ID a = ID a := !id_left
definition id_leftright (f : hom a b) : id ∘ f ∘ id = f := !id_left ⬝ !id_right definition id_leftright (f : hom a b) : id ∘ f ∘ id = f := !id_left ⬝ !id_right
definition comp_id_eq_id_comp (f : hom a b) : f ∘ id = id ∘ f := !id_right ⬝ !id_left⁻¹
definition left_id_unique (H : Π{b} {f : hom b a}, i ∘ f = f) : i = id := definition left_id_unique (H : Π{b} {f : hom b a}, i ∘ f = f) : i = id :=
calc i = i ∘ id : by rewrite id_right calc i = i ∘ id : by rewrite id_right

View file

@ -244,6 +244,13 @@ namespace category
@iso.mk _ _ _ _ (natural_map (to_hom η) c) @iso.mk _ _ _ _ (natural_map (to_hom η) c)
(@componentwise_is_iso _ _ _ _ (to_hom η) (struct η) c) (@componentwise_is_iso _ _ _ _ (to_hom η) (struct η) c)
definition componentwise_iso_id (c : C) : componentwise_iso (iso.refl F) c = iso.refl (F c) :=
iso.eq_mk (idpath id)
definition componentwise_iso_iso_of_eq (p : F = G) (c : C)
: componentwise_iso (iso_of_eq p) c = iso_of_eq (ap010 to_fun_ob p c) :=
eq.rec_on p !componentwise_iso_id
definition natural_map_hom_of_eq (p : F = G) (c : C) definition natural_map_hom_of_eq (p : F = G) (c : C)
: natural_map (hom_of_eq p) c = hom_of_eq (ap010 to_fun_ob p c) := : natural_map (hom_of_eq p) c = hom_of_eq (ap010 to_fun_ob p c) :=
eq.rec_on p idp eq.rec_on p idp

View file

@ -21,7 +21,7 @@ structure functor (C D : Precategory) : Type :=
namespace functor namespace functor
infixl `⇒`:25 := functor infixl `⇒`:25 := functor
variables {C D E : Precategory} variables {A B C D E : Precategory}
attribute to_fun_ob [coercion] attribute to_fun_ob [coercion]
attribute to_fun_hom [coercion] attribute to_fun_hom [coercion]
@ -46,17 +46,22 @@ namespace functor
protected definition ID [reducible] (C : Precategory) : functor C C := id protected definition ID [reducible] (C : Precategory) : functor C C := id
definition functor_eq_mk'' {F₁ F₂ : C → D} {H₁ : Π(a b : C), hom a b → hom (F₁ a) (F₁ b)} definition functor_mk_eq' {F₁ F₂ : C → D} {H₁ : Π(a b : C), hom a b → hom (F₁ a) (F₁ b)}
{H₂ : Π(a b : C), hom a b → hom (F₂ a) (F₂ b)} (id₁ id₂ comp₁ comp₂) {H₂ : Π(a b : C), hom a b → hom (F₂ a) (F₂ b)} (id₁ id₂ comp₁ comp₂)
(pF : F₁ = F₂) (pH : pF ▹ H₁ = H₂) (pF : F₁ = F₂) (pH : pF ▹ H₁ = H₂)
: functor.mk F₁ H₁ id₁ comp₁ = functor.mk F₂ H₂ id₂ comp₂ := : functor.mk F₁ H₁ id₁ comp₁ = functor.mk F₂ H₂ id₂ comp₂ :=
apD01111 functor.mk pF pH !is_hprop.elim !is_hprop.elim apD01111 functor.mk pF pH !is_hprop.elim !is_hprop.elim
definition functor_eq_mk' {F₁ F₂ : C → D} {H₁ : Π(a b : C), hom a b → hom (F₁ a) (F₁ b)} definition functor_eq' {F₁ F₂ : C ⇒ D}
: Π(p : to_fun_ob F₁ = to_fun_ob F₂),
(transport (λx, Πa b f, hom (x a) (x b)) p (to_fun_hom F₁) = to_fun_hom F₂) → F₁ = F₂ :=
functor.rec_on F₁ (λO₁ H₁ id₁ comp₁, functor.rec_on F₂ (λO₂ H₂ id₂ comp₂ p, !functor_mk_eq'))
definition functor_mk_eq {F₁ F₂ : C → D} {H₁ : Π(a b : C), hom a b → hom (F₁ a) (F₁ b)}
{H₂ : Π(a b : C), hom a b → hom (F₂ a) (F₂ b)} (id₁ id₂ comp₁ comp₂) (pF : F₁ F₂) {H₂ : Π(a b : C), hom a b → hom (F₂ a) (F₂ b)} (id₁ id₂ comp₁ comp₂) (pF : F₁ F₂)
(pH : Π(a b : C) (f : hom a b), hom_of_eq (pF b) ∘ H₁ a b f ∘ inv_of_eq (pF a) = H₂ a b f) (pH : Π(a b : C) (f : hom a b), hom_of_eq (pF b) ∘ H₁ a b f ∘ inv_of_eq (pF a) = H₂ a b f)
: functor.mk F₁ H₁ id₁ comp₁ = functor.mk F₂ H₂ id₂ comp₂ := : functor.mk F₁ H₁ id₁ comp₁ = functor.mk F₂ H₂ id₂ comp₂ :=
functor_eq_mk'' id₁ id₂ comp₁ comp₂ (eq_of_homotopy pF) functor_mk_eq' id₁ id₂ comp₁ comp₂ (eq_of_homotopy pF)
(eq_of_homotopy (λc, eq_of_homotopy (λc', eq_of_homotopy (λf, (eq_of_homotopy (λc, eq_of_homotopy (λc', eq_of_homotopy (λf,
begin begin
apply concat, rotate_left 1, exact (pH c c' f), apply concat, rotate_left 1, exact (pH c c' f),
@ -72,26 +77,35 @@ namespace functor
apply idp apply idp
end)))) end))))
definition functor_eq_mk_constant {F : C → D} {H₁ : Π(a b : C), hom a b → hom (F a) (F b)} -- definition functor_mk_eq_constant {F : C → D} {H₁ : Π(a b : C), hom a b → hom (F a) (F b)}
-- {H₂ : Π(a b : C), hom a b → hom (F a) (F b)} (id₁ id₂ comp₁ comp₂)
-- (pH : Π(a b : C) (f : hom a b), H₁ a b f = H₂ a b f)
-- : functor.mk F H₁ id₁ comp₁ = functor.mk F H₂ id₂ comp₂ :=
-- functor_mk_eq' id₁ id₂ comp₁ comp₂ idp
-- (eq_of_homotopy (λc, eq_of_homotopy (λc', eq_of_homotopy (pH c c'))))
definition functor_eq {F₁ F₂ : C ⇒ D} : Π(p : to_fun_ob F₁ to_fun_ob F₂),
(Π(a b : C) (f : hom a b), hom_of_eq (p b) ∘ F₁ f ∘ inv_of_eq (p a) = F₂ f) → F₁ = F₂ :=
functor.rec_on F₁ (λO₁ H₁ id₁ comp₁, functor.rec_on F₂ (λO₂ H₂ id₂ comp₂ p, !functor_mk_eq))
definition functor_mk_eq_constant {F : C → D} {H₁ : Π(a b : C), hom a b → hom (F a) (F b)}
{H₂ : Π(a b : C), hom a b → hom (F a) (F b)} (id₁ id₂ comp₁ comp₂) {H₂ : Π(a b : C), hom a b → hom (F a) (F b)} (id₁ id₂ comp₁ comp₂)
(pH : Π(a b : C) (f : hom a b), H₁ a b f = H₂ a b f) (pH : Π(a b : C) (f : hom a b), H₁ a b f = H₂ a b f)
: functor.mk F H₁ id₁ comp₁ = functor.mk F H₂ id₂ comp₂ := : functor.mk F H₁ id₁ comp₁ = functor.mk F H₂ id₂ comp₂ :=
functor_eq_mk'' id₁ id₂ comp₁ comp₂ idp functor_eq (λc, idp) (λa b f, !id_leftright ⬝ !pH)
(eq_of_homotopy (λc, eq_of_homotopy (λc', eq_of_homotopy (pH c c'))))
definition functor_eq_mk {F₁ F₂ : C ⇒ D} : Π(p : to_fun_ob F₁ to_fun_ob F₂), protected definition assoc (H : C ⇒ D) (G : B ⇒ C) (F : A ⇒ B) :
(Π(a b : C) (f : hom a b), hom_of_eq (p b) ∘ F₁ f ∘ inv_of_eq (p a) = F₂ f) → F₁ = F₂ :=
functor.rec_on F₁ (λO₁ H₁ id₁ comp₁, functor.rec_on F₂ (λO₂ H₂ id₂ comp₂ p, !functor_eq_mk'))
protected definition assoc {A B C D : Precategory} (H : functor C D) (G : functor B C) (F : functor A B) :
H ∘f (G ∘f F) = (H ∘f G) ∘f F := H ∘f (G ∘f F) = (H ∘f G) ∘f F :=
!functor_eq_mk_constant (λa b f, idp) !functor_mk_eq_constant (λa b f, idp)
protected definition id_left (F : functor C D) : id ∘f F = F := protected definition id_left (F : C ⇒ D) : id ∘f F = F :=
functor.rec_on F (λF1 F2 F3 F4, !functor_eq_mk_constant (λa b f, idp)) functor.rec_on F (λF1 F2 F3 F4, !functor_mk_eq_constant (λa b f, idp))
protected definition id_right (F : functor C D) : F ∘f id = F := protected definition id_right (F : C ⇒ D) : F ∘f id = F :=
functor.rec_on F (λF1 F2 F3 F4, !functor_eq_mk_constant (λa b f, idp)) functor.rec_on F (λF1 F2 F3 F4, !functor_mk_eq_constant (λa b f, idp))
protected definition comp_id_eq_id_comp (F : C ⇒ D) : F ∘f functor.id = functor.id ∘f F :=
!functor.id_right ⬝ !functor.id_left⁻¹
set_option apply.class_instance false set_option apply.class_instance false
-- "functor C D" is equivalent to a certain sigma type -- "functor C D" is equivalent to a certain sigma type
@ -136,39 +150,75 @@ namespace functor
apply is_trunc_eq, apply is_trunc_succ, apply !homH}, apply is_trunc_eq, apply is_trunc_succ, apply !homH},
end end
definition functor_eq_eta' {ob₁ ob₂ : C → D} {hom₁ hom₂ id₁ id₂ comp₁ comp₂} --STRANGE ERROR:
(p : functor.mk ob₁ hom₁ id₁ comp₁ = functor.mk ob₂ hom₂ id₂ comp₂) -- definition functor_mk_eq'_idp {F₁ : C → D} {H₁ : Π(a b : C), hom a b → hom (F₁ a) (F₁ b)}
: p = p := --functor_eq_mk' _ _ _ _ (ap010 to_fun_ob p) _ := -- (id₁ id₂ comp₁ comp₂) : functor_mk_eq' id₁ id₂ comp₁ comp₂ idp idp = idp :=
sorry -- sorry
definition functor_mk_eq'_idp (F : C → D) (H : Π(a b : C), hom a b → hom (F a) (F b))
(id comp) : functor_mk_eq' id id comp comp (idpath F) (idpath H) = idp :=
begin
fapply (apD011 (apD01111 functor.mk idp idp)),
apply is_hset.elim,
apply is_hset.elim
end
definition functor_eq'_idp (F : C ⇒ D) : functor_eq' idp idp = (idpath F) :=
by (cases F; apply functor_mk_eq'_idp)
--TODO: do we want a similar theorem for functor_eq?
definition functor_eq_eta' {F₁ F₂ : C ⇒ D} (p : F₁ = F₂)
: functor_eq' (ap to_fun_ob p) (!transport_compose⁻¹ ⬝ apD to_fun_hom p) = p :=
begin
cases p, cases F₁,
apply concat, rotate_left 1, apply functor_eq'_idp,
apply (ap (functor_eq' idp)),
apply idp_con,
end
-- definition functor_eq_eta {ob₁ ob₂ : C → D} {hom₁ hom₂ id₁ id₂ comp₁ comp₂}
-- (p : functor.mk ob₁ hom₁ id₁ comp₁ = functor.mk ob₂ hom₂ id₂ comp₂)
-- : functor_mk_eq' _ _ _ _ (ap010 to_fun_ob p) _ = p :=
-- sorry
--set_option pp.universes true --set_option pp.universes true
-- set_option pp.notation false -- set_option pp.notation false
-- set_option pp.implicit true -- set_option pp.implicit true
-- TODO: REMOVE?
definition functor_eq2'' {ob₁ ob₂ : C → D} {hom₁ hom₂ id₁ id₂ comp₁ comp₂}
{pob₁ pob₂ : ob₁ = ob₂} (phom₁ : pob₁ ▹ hom₁ = hom₂) (phom₂ : pob₂ ▹ hom₁ = hom₂)
(r : pob₁ = pob₂) : functor_eq_mk'' id₁ id₂ comp₁ comp₂ pob₁ phom₁
= functor_eq_mk'' id₁ id₂ comp₁ comp₂ pob₂ phom₂ :=
begin
cases r,
apply (ap (functor_eq_mk'' id₁ id₂ @comp₁ @comp₂ pob₂)),
apply is_hprop.elim
end
definition functor_eq2' {ob₁ ob₂ : C → D} {hom₁ hom₂ id₁ id₂ comp₁ comp₂} {pob₁ pob₂ : ob₁ ob₂} -- TODO: REMOVE?
(phom₁ : Π(a b : C) (f : hom a b), hom_of_eq (pob₁ b) ∘ hom₁ a b f ∘ inv_of_eq (pob₁ a) = hom₂ a b f) -- definition functor_mk_eq'2 {ob₁ ob₂ : C → D} {hom₁ hom₂ id₁ id₂ comp₁ comp₂}
(phom₂ : Π(a b : C) (f : hom a b), hom_of_eq (pob₂ b) ∘ hom₁ a b f ∘ inv_of_eq (pob₂ a) = hom₂ a b f) -- {pob₁ pob₂ : ob₁ = ob₂} (phom₁ : pob₁ ▹ hom₁ = hom₂) (phom₂ : pob₂ ▹ hom₁ = hom₂)
(r : pob₁ = pob₂) : functor_eq_mk' id₁ id₂ comp₁ comp₂ pob₁ phom₁ -- (r : pob₁ = pob₂) : functor_mk_eq' id₁ id₂ comp₁ comp₂ pob₁ phom₁
= functor_eq_mk' id₁ id₂ comp₁ comp₂ pob₂ phom₂ := -- = functor_mk_eq' id₁ id₂ comp₁ comp₂ pob₂ phom₂ :=
begin -- begin
cases r, -- cases r,
apply (ap (functor_eq_mk' id₁ id₂ @comp₁ @comp₂ pob₂)), -- apply (ap (functor_mk_eq' id₁ id₂ @comp₁ @comp₂ pob₂)),
apply is_hprop.elim -- apply is_hprop.elim
end -- end
-- definition functor_mk_eq2 {ob₁ ob₂ : C → D} {hom₁ hom₂ id₁ id₂ comp₁ comp₂} {pob₁ pob₂ : ob₁ ob₂}
-- (phom₁ : Π(a b : C) (f : hom a b), hom_of_eq (pob₁ b) ∘ hom₁ a b f ∘ inv_of_eq (pob₁ a) = hom₂ a b f)
-- (phom₂ : Π(a b : C) (f : hom a b), hom_of_eq (pob₂ b) ∘ hom₁ a b f ∘ inv_of_eq (pob₂ a) = hom₂ a b f)
-- (r : pob₁ = pob₂) : functor_mk_eq id₁ id₂ comp₁ comp₂ pob₁ phom₁
-- = functor_mk_eq id₁ id₂ comp₁ comp₂ pob₂ phom₂ :=
-- begin
-- cases r,
-- apply (ap (functor_mk_eq id₁ id₂ @comp₁ @comp₂ pob₂)),
-- apply is_hprop.elim
-- end
definition functor_eq2' {F₁ F₂ : C ⇒ D} {p₁ p₂ : to_fun_ob F₁ = to_fun_ob F₂} (q₁ q₂)
(r : p₁ = p₂) : functor_eq' p₁ q₁ = functor_eq' p₂ q₂ :=
by cases r; apply (ap (functor_eq' p₂)); apply is_hprop.elim
definition functor_eq2 {F₁ F₂ : C ⇒ D} (p q : F₁ = F₂) (r : ap010 to_fun_ob p ap010 to_fun_ob q) definition functor_eq2 {F₁ F₂ : C ⇒ D} (p q : F₁ = F₂) (r : ap010 to_fun_ob p ap010 to_fun_ob q)
: p = q := : p = q :=
begin begin
apply sorry cases F₁ with (ob₁, hom₁, id₁, comp₁),
cases F₂ with (ob₂, hom₂, id₂, comp₂),
rewrite [-functor_eq_eta' p, -functor_eq_eta' q],
apply functor_eq2',
apply ap_eq_ap_of_homotopy,
exact r,
end end
-- definition ap010_functor_eq_mk' {F₁ F₂ : C ⇒ D} (p : to_fun_ob F₁ = to_fun_ob F₂) -- definition ap010_functor_eq_mk' {F₁ F₂ : C ⇒ D} (p : to_fun_ob F₁ = to_fun_ob F₂)
@ -180,28 +230,45 @@ namespace functor
-- end -- end
-- TODO: remove sorry -- TODO: remove sorry
-- maybe some lemma "recursion on homotopy (and equiv)" could be useful definition ap010_functor_eq {F₁ F₂ : C ⇒ D} (p : to_fun_ob F₁ to_fun_ob F₂)
definition ap010_functor_eq_mk {F₁ F₂ : C ⇒ D} (p : to_fun_ob F₁ to_fun_ob F₂)
(q : (λ(a b : C) (f : hom a b), hom_of_eq (p b) ∘ F₁ f ∘ inv_of_eq (p a)) 3 to_fun_hom F₂) (c : C) : (q : (λ(a b : C) (f : hom a b), hom_of_eq (p b) ∘ F₁ f ∘ inv_of_eq (p a)) 3 to_fun_hom F₂) (c : C) :
ap010 to_fun_ob (functor_eq_mk p q) c = p c := ap010 to_fun_ob (functor_eq p q) c = p c :=
begin begin
cases F₂, revert q, apply (homotopy.rec_on p), clear p, esimp, intros (p, q), cases F₂, revert q, apply (homotopy.rec_on p), clear p, esimp, intros (p, q),
apply sorry, apply sorry,
--cases p, clears (e_1, e_2, p), --apply (homotopy3.rec_on q), clear q, intro q,
--cases p, --TODO: report: this fails
--exact (homotopy3.rec_on q sorry)
-- apply (homotopy3.rec_on q),
end end
-- definition ap010_functor_eq_mk {F₁ F₂ : C ⇒ D} (p : to_fun_ob F₁ to_fun_ob F₂) definition ap010_functor_mk_eq_constant {F : C → D} {H₁ : Π(a b : C), hom a b → hom (F a) (F b)}
-- (q : Π(a b : C) (f : hom a b), hom_of_eq (p b) ∘ F₁ f ∘ inv_of_eq (p a) = F₂ f) (c : C) : {H₂ : Π(a b : C), hom a b → hom (F a) (F b)} {id₁ id₂ comp₁ comp₂}
-- ap010 to_fun_ob (functor_eq_mk p q) c = p c := (pH : Π(a b : C) (f : hom a b), H₁ a b f = H₂ a b f) (c : C) :
ap010 to_fun_ob (functor_mk_eq_constant id₁ id₂ comp₁ comp₂ pH) c = idp :=
!ap010_functor_eq
--do we need this theorem?
definition compose_pentagon (K : D ⇒ E) (H : C ⇒ D) (G : B ⇒ C) (F : A ⇒ B) :
(calc K ∘f H ∘f G ∘f F = (K ∘f H) ∘f G ∘f F : functor.assoc
... = ((K ∘f H) ∘f G) ∘f F : functor.assoc)
=
(calc K ∘f H ∘f G ∘f F = K ∘f (H ∘f G) ∘f F : ap (λx, K ∘f x) !functor.assoc
... = (K ∘f H ∘f G) ∘f F : functor.assoc
... = ((K ∘f H) ∘f G) ∘f F : ap (λx, x ∘f F) !functor.assoc) :=
sorry
-- begin -- begin
-- cases F₂, revert q, apply (homotopy.rec_on p), clear p, esimp, intros (p, q), -- apply functor_eq2,
-- cases p, clears (e_1, e_2, p), -- intro a,
-- apply (homotopy3.rec_on q), -- rewrite +ap010_con,
-- -- rewrite +ap010_ap,
-- -- apply sorry
-- /-to prove this we need a stronger ap010-lemma, something like
-- ap010 (λy, to_fun_ob (f y)) (functor_mk_eq_constant ...) c = idp
-- or something another way of getting ap out of ap010
-- -/
-- --rewrite +ap010_ap,
-- --unfold functor.assoc,
-- --rewrite ap010_functor_mk_eq_constant,
-- end -- end
-- ⊢ ap010 to_fun_ob (functor_eq_mk rfl q) c = rfl
end functor end functor

View file

@ -10,6 +10,8 @@ import algebra.precategory.basic types.sigma arity
open eq category prod equiv is_equiv sigma sigma.ops is_trunc open eq category prod equiv is_equiv sigma sigma.ops is_trunc
namespace iso namespace iso
structure split_mono [class] {ob : Type} [C : precategory ob] {a b : ob} (f : a ⟶ b) := structure split_mono [class] {ob : Type} [C : precategory ob] {a b : ob} (f : a ⟶ b) :=
{retraction_of : b ⟶ a} {retraction_of : b ⟶ a}
@ -193,10 +195,10 @@ namespace iso
definition iso_of_eq (p : a = b) : a ≅ b := definition iso_of_eq (p : a = b) : a ≅ b :=
eq.rec_on p (iso.refl a) eq.rec_on p (iso.refl a)
definition hom_of_eq (p : a = b) : a ⟶ b := definition hom_of_eq [reducible] (p : a = b) : a ⟶ b :=
iso.to_hom (iso_of_eq p) iso.to_hom (iso_of_eq p)
definition inv_of_eq (p : a = b) : b ⟶ a := definition inv_of_eq [reducible] (p : a = b) : b ⟶ a :=
iso.to_inv (iso_of_eq p) iso.to_inv (iso_of_eq p)
definition iso_of_eq_inv (p : a = b) : iso_of_eq p⁻¹ = iso.symm (iso_of_eq p) := definition iso_of_eq_inv (p : a = b) : iso_of_eq p⁻¹ = iso.symm (iso_of_eq p) :=
@ -206,7 +208,6 @@ namespace iso
: iso_of_eq (p ⬝ q) = iso.trans (iso_of_eq p) (iso_of_eq q) := : iso_of_eq (p ⬝ q) = iso.trans (iso_of_eq p) (iso_of_eq q) :=
eq.rec_on q (eq.rec_on p (iso.eq_mk !id_comp⁻¹)) eq.rec_on q (eq.rec_on p (iso.eq_mk !id_comp⁻¹))
section section
open funext open funext
variables {X : Type} {x y : X} {F G : X → ob} variables {X : Type} {x y : X} {F G : X → ob}

View file

@ -7,7 +7,7 @@ Author: Floris van Doorn, Jakob von Raumer
-/ -/
import .functor .iso import .functor .iso
open eq category functor is_trunc equiv sigma.ops sigma is_equiv function pi funext open eq category functor is_trunc equiv sigma.ops sigma is_equiv function pi funext iso
structure nat_trans {C D : Precategory} (F G : C ⇒ D) := structure nat_trans {C D : Precategory} (F G : C ⇒ D) :=
(natural_map : Π (a : C), hom (F a) (G a)) (natural_map : Π (a : C), hom (F a) (G a))
@ -16,7 +16,7 @@ structure nat_trans {C D : Precategory} (F G : C ⇒ D) :=
namespace nat_trans namespace nat_trans
infixl `⟹`:25 := nat_trans -- \==> infixl `⟹`:25 := nat_trans -- \==>
variables {C D : Precategory} {F G H I : C ⇒ D} variables {C D E : Precategory} {F G H I : C ⇒ D} {F' G' : D ⇒ E}
attribute natural_map [coercion] attribute natural_map [coercion]
@ -88,4 +88,27 @@ namespace nat_trans
apply is_trunc_eq, apply is_trunc_succ, exact (@homH (Precategory.carrier D) _ (F a) (G b)), apply is_trunc_eq, apply is_trunc_succ, exact (@homH (Precategory.carrier D) _ (F a) (G b)),
end end
definition nat_trans_functor_compose [reducible] (η : G ⟹ H) (F : E ⇒ C) : G ∘f F ⟹ H ∘f F :=
nat_trans.mk
(λ a, η (F a))
(λ a b f, naturality η (F f))
definition functor_nat_trans_compose [reducible] (F : D ⇒ E) (η : G ⟹ H) : F ∘f G ⟹ F ∘f H :=
nat_trans.mk
(λ a, F (η a))
(λ a b f, calc
F (H f) ∘ F (η a) = F (H f ∘ η a) : respect_comp
... = F (η b ∘ G f) : by rewrite (naturality η f)
... = F (η b) ∘ F (G f) : respect_comp)
infixr `∘nf`:60 := nat_trans_functor_compose
infixr `∘fn`:60 := functor_nat_trans_compose
definition functor_nat_trans_compose_commute (η : F ⟹ G) (θ : F' ⟹ G')
: (θ ∘nf G) ∘n (F' ∘fn η) = (G' ∘fn η) ∘n (θ ∘nf F) :=
nat_trans_eq_mk (λc, (naturality θ (η c))⁻¹)
definition nat_trans_of_eq [reducible] (p : F = G) : F ⟹ G :=
nat_trans.mk (λc, hom_of_eq (ap010 to_fun_ob p c))
(λa b f, eq.rec_on p (!id_right ⬝ !id_left⁻¹))
end nat_trans end nat_trans

View file

@ -128,7 +128,7 @@ namespace functor
(functor_uncurry_comp G) (functor_uncurry_comp G)
theorem functor_uncurry_functor_curry : functor_uncurry (functor_curry F) = F := theorem functor_uncurry_functor_curry : functor_uncurry (functor_curry F) = F :=
functor_eq_mk (λp, ap (to_fun_ob F) !prod.eta) functor_eq (λp, ap (to_fun_ob F) !prod.eta)
begin begin
intros (cd, cd', fg), intros (cd, cd', fg),
cases cd with (c,d), cases cd' with (c',d'), cases fg with (f,g), cases cd with (c,d), cases cd' with (c',d'), cases fg with (f,g),
@ -144,7 +144,7 @@ namespace functor
definition functor_curry_functor_uncurry_ob (c : C) definition functor_curry_functor_uncurry_ob (c : C)
: functor_curry (functor_uncurry G) c = G c := : functor_curry (functor_uncurry G) c = G c :=
begin begin
fapply functor_eq_mk, fapply functor_eq,
{intro d, apply idp}, {intro d, apply idp},
{intros (d, d', g), {intros (d, d', g),
apply concat, apply id_leftright, apply concat, apply id_leftright,
@ -159,17 +159,17 @@ namespace functor
theorem functor_curry_functor_uncurry : functor_curry (functor_uncurry G) = G := theorem functor_curry_functor_uncurry : functor_curry (functor_uncurry G) = G :=
begin begin
fapply functor_eq_mk, exact (functor_curry_functor_uncurry_ob G), fapply functor_eq, exact (functor_curry_functor_uncurry_ob G),
intros (c, c', f), intros (c, c', f),
fapply nat_trans_eq_mk, fapply nat_trans_eq_mk,
intro d, intro d,
apply concat, apply concat,
{apply (ap (λx, x ∘ _)), {apply (ap (λx, x ∘ _)),
apply concat, apply natural_map_hom_of_eq, apply (ap hom_of_eq), apply ap010_functor_eq_mk}, apply concat, apply natural_map_hom_of_eq, apply (ap hom_of_eq), apply ap010_functor_eq},
apply concat, apply concat,
{apply (ap (λx, _ ∘ x)), apply (ap (λx, _ ∘ x)), {apply (ap (λx, _ ∘ x)), apply (ap (λx, _ ∘ x)),
apply concat, apply natural_map_inv_of_eq, apply concat, apply natural_map_inv_of_eq,
apply (ap (λx, hom_of_eq x⁻¹)), apply ap010_functor_eq_mk}, apply (ap (λx, hom_of_eq x⁻¹)), apply ap010_functor_eq},
apply concat, apply id_leftright, apply concat, apply id_leftright,
apply concat, apply (ap (λx, x ∘ _)), apply respect_id, apply concat, apply (ap (λx, x ∘ _)), apply respect_id,
apply id_left apply id_left
@ -192,7 +192,7 @@ namespace functor
definition functor_prod_flip_functor_prod_flip (C D : Precategory) definition functor_prod_flip_functor_prod_flip (C D : Precategory)
: functor_prod_flip D C ∘f (functor_prod_flip C D) = functor.id := : functor_prod_flip D C ∘f (functor_prod_flip C D) = functor.id :=
begin begin
fapply functor_eq_mk, {intro p, apply prod.eta}, fapply functor_eq, {intro p, apply prod.eta},
intros (p, p', h), cases p with (c, d), cases p' with (c', d'), intros (p, p', h), cases p with (c, d), cases p' with (c', d'),
apply id_leftright, apply id_leftright,
end end

View file

@ -10,7 +10,7 @@ Theorems about functions with multiple arguments
variables {A U V W X Y Z : Type} {B : A → Type} {C : Πa, B a → Type} {D : Πa b, C a b → Type} variables {A U V W X Y Z : Type} {B : A → Type} {C : Πa, B a → Type} {D : Πa b, C a b → Type}
{E : Πa b c, D a b c → Type} {E : Πa b c, D a b c → Type}
variables {a a' : A} {u u' : U} {v v' : V} {w w' : W} {x x' : X} {y y' : Y} variables {a a' : A} {u u' : U} {v v' : V} {w w' : W} {x x' x'' : X} {y y' : Y}
{b : B a} {b' : B a'} {b : B a} {b' : B a'}
{c : C a b} {c' : C a' b'} {c : C a b} {c' : C a' b'}
{d : D a b c} {d' : D a' b' c'} {d : D a b c} {d' : D a' b' c'}
@ -88,6 +88,18 @@ namespace eq
definition apD1000 {f g : Πa b c, D a b c} (p : f = g) : f 3 g := definition apD1000 {f g : Πa b c, D a b c} (p : f = g) : f 3 g :=
λa b c, apD100 (apD10 p a) b c λa b c, apD100 (apD10 p a) b c
/- some properties of these variants of ap -/
-- we only prove what is needed somewhere
definition ap010_con (f : X → Πa, B a) (p : x = x') (q : x' = x'') :
ap010 f (p ⬝ q) a = ap010 f p a ⬝ ap010 f q a :=
eq.rec_on q (eq.rec_on p idp)
definition ap010_ap (f : X → Πa, B a) (g : Y → X) (p : y = y') :
ap010 f (ap g p) a = ap010 (λy, f (g y)) p a :=
eq.rec_on p idp
/- the following theorems are function extentionality for functions with multiple arguments -/ /- the following theorems are function extentionality for functions with multiple arguments -/
definition eq_of_homotopy2 {f g : Πa b, C a b} (H : f 2 g) : f = g := definition eq_of_homotopy2 {f g : Πa b, C a b} (H : f 2 g) : f = g :=
@ -111,9 +123,10 @@ namespace eq
{apply (ap (λx, eq_of_homotopy x)), apply eq_of_homotopy, intro a, apply eq_of_homotopy2_id}, {apply (ap (λx, eq_of_homotopy x)), apply eq_of_homotopy, intro a, apply eq_of_homotopy2_id},
apply eq_of_homotopy_id apply eq_of_homotopy_id
end end
end eq end eq
open is_equiv eq open eq is_equiv
namespace funext namespace funext
definition is_equiv_apD100 [instance] (f g : Πa b, C a b) : is_equiv (@apD100 A B C f g) := definition is_equiv_apD100 [instance] (f g : Πa b, C a b) : is_equiv (@apD100 A B C f g) :=
adjointify _ adjointify _
@ -156,4 +169,20 @@ namespace eq
protected definition homotopy3.rec_on {f g : Πa b c, D a b c} {P : (f 3 g) → Type} protected definition homotopy3.rec_on {f g : Πa b c, D a b c} {P : (f 3 g) → Type}
(p : f 3 g) (H : Π(q : f = g), P (apD1000 q)) : P p := (p : f 3 g) (H : Π(q : f = g), P (apD1000 q)) : P p :=
retr apD1000 p ▹ H (eq_of_homotopy3 p) retr apD1000 p ▹ H (eq_of_homotopy3 p)
definition apD10_ap (f : X → Πa, B a) (p : x = x')
: apD10 (ap f p) = ap010 f p :=
eq.rec_on p idp
definition eq_of_homotopy_ap010 (f : X → Πa, B a) (p : x = x')
: eq_of_homotopy (ap010 f p) = ap f p :=
inv_eq_of_eq !apD10_ap⁻¹
definition ap_eq_ap_of_homotopy {f : X → Πa, B a} {p q : x = x'} (H : ap010 f p ap010 f q)
: ap f p = ap f q :=
calc
ap f p = eq_of_homotopy (ap010 f p) : eq_of_homotopy_ap010
... = eq_of_homotopy (ap010 f q) : eq_of_homotopy H
... = ap f q : eq_of_homotopy_ap010
end eq end eq

View file

@ -85,7 +85,7 @@ context
local attribute weak_funext [reducible] local attribute weak_funext [reducible]
local attribute homotopy_ind [reducible] local attribute homotopy_ind [reducible]
definition homotopy_ind_comp : homotopy_ind f (homotopy.refl f) = d := definition homotopy_ind_comp : homotopy_ind f (homotopy.refl f) = d :=
(@hprop_eq _ _ _ _ !center_eq idp)⁻¹ ▹ idp (@hprop_eq_of_is_contr _ _ _ _ !center_eq idp)⁻¹ ▹ idp
end end

View file

@ -139,39 +139,20 @@ namespace is_equiv
end end
section section
variables {A B: Type} (f : A → B) variables {A B C : Type} (f : A → B) {f' : A → B} [Hf : is_equiv f] (g : B → C)
--The inverse of an equivalence is, again, an equivalence.
definition is_equiv_inv [instance] [Hf : is_equiv f] : (is_equiv (inv f)) :=
adjointify (inv f) f (sect f) (retr f)
end
section
variables {A B C : Type} (f : A → B) {f' : A → B} [Hf : is_equiv f]
include Hf include Hf
variable (g : B → C) --The inverse of an equivalence is, again, an equivalence.
definition is_equiv_inv [instance] : (is_equiv f⁻¹) :=
adjointify f⁻¹ f (sect f) (retr f)
definition cancel_right (g : B → C) [Hgf : is_equiv (g ∘ f)] : (is_equiv g) := definition cancel_right (g : B → C) [Hgf : is_equiv (g ∘ f)] : (is_equiv g) :=
have Hfinv [visible] : is_equiv f⁻¹, from is_equiv_inv f, have Hfinv [visible] : is_equiv f⁻¹, from is_equiv_inv f,
@homotopy_closed _ _ _ _ (is_equiv_compose f⁻¹ (g ∘ f)) (λb, ap g (@retr _ _ f _ b)) @homotopy_closed _ _ _ _ (is_equiv_compose f⁻¹ (g ∘ f)) (λb, ap g (@retr _ _ f _ b))
definition cancel_left (g : C → A) [Hgf : is_equiv (f ∘ g)] : (is_equiv g) := definition cancel_left (g : C → A) [Hgf : is_equiv (f ∘ g)] : (is_equiv g) :=
have Hfinv [visible] : is_equiv f⁻¹, from is_equiv_inv f, have Hfinv [visible] : is_equiv f⁻¹, from is_equiv_inv f,
@homotopy_closed _ _ _ _ (is_equiv_compose (f ∘ g) f⁻¹) (λa, sect f (g a)) @homotopy_closed _ _ _ _ (is_equiv_compose (f ∘ g) f⁻¹) (λa, sect f (g a))
--Rewrite rules
definition eq_of_eq_inv {x : A} {y : B} (p : x = (inv f) y) : (f x = y) :=
(ap f p) ⬝ (@retr _ _ f _ y)
definition eq_of_inv_eq {x : A} {y : B} (p : (inv f) y = x) : (y = f x) :=
(eq_of_eq_inv f p⁻¹)⁻¹
definition inv_eq_of_eq {x : B} {y : A} (p : x = f y) : (inv f) x = y :=
ap f⁻¹ p ⬝ sect f y
definition eq_inv_of_eq {x : B} {y : A} (p : f y = x) : y = (inv f) x :=
(inv_eq_of_eq f p⁻¹)⁻¹
definition is_equiv_ap [instance] (x y : A) : is_equiv (ap f) := definition is_equiv_ap [instance] (x y : A) : is_equiv (ap f) :=
adjointify (ap f) adjointify (ap f)
@ -211,6 +192,25 @@ namespace is_equiv
end end
section
variables {A B : Type} {f : A → B} [Hf : is_equiv f] {a : A} {b : B}
include Hf
--Rewrite rules
definition eq_of_eq_inv (p : a = f⁻¹ b) : f a = b :=
ap f p ⬝ retr f b
definition eq_of_inv_eq (p : f⁻¹ b = a) : b = f a :=
(eq_of_eq_inv p⁻¹)⁻¹
definition inv_eq_of_eq (p : b = f a) : f⁻¹ b = a :=
ap f⁻¹ p ⬝ sect f a
definition eq_inv_of_eq (p : f a = b) : a = f⁻¹ b :=
(inv_eq_of_eq p⁻¹)⁻¹
end
--Transporting is an equivalence --Transporting is an equivalence
definition is_equiv_tr [instance] {A : Type} (P : A → Type) {x y : A} (p : x = y) : (is_equiv (transport P p)) := definition is_equiv_tr [instance] {A : Type} (P : A → Type) {x y : A} (p : x = y) : (is_equiv (transport P p)) :=
is_equiv.mk (transport P p⁻¹) (tr_inv_tr P p) (inv_tr_tr P p) (tr_inv_tr_lemma P p) is_equiv.mk (transport P p⁻¹) (tr_inv_tr P p) (inv_tr_tr P p) (tr_inv_tr_lemma P p)

View file

@ -101,16 +101,16 @@ namespace is_trunc
definition contr [H : is_contr A] (a : A) : !center = a := definition contr [H : is_contr A] (a : A) : !center = a :=
@contr_internal.contr A !is_trunc.to_internal a @contr_internal.contr A !is_trunc.to_internal a
--TODO: rename
definition center_eq [H : is_contr A] (x y : A) : x = y := definition center_eq [H : is_contr A] (x y : A) : x = y :=
(contr x)⁻¹ ⬝ (contr y) (contr x)⁻¹ ⬝ (contr y)
definition hprop_eq {A : Type} [H : is_contr A] {x y : A} (p q : x = y) : p = q := definition hprop_eq_of_is_contr {A : Type} [H : is_contr A] {x y : A} (p q : x = y) : p = q :=
have K : ∀ (r : x = y), center_eq x y = r, from (λ r, eq.rec_on r !con.left_inv), have K : ∀ (r : x = y), center_eq x y = r, from (λ r, eq.rec_on r !con.left_inv),
(K p)⁻¹ ⬝ K q (K p)⁻¹ ⬝ K q
definition is_contr_eq {A : Type} [H : is_contr A] (x y : A) : is_contr (x = y) definition is_contr_eq {A : Type} [H : is_contr A] (x y : A) : is_contr (x = y) :=
:= is_contr.mk !center_eq (λ p, !hprop_eq_of_is_contr)
is_contr.mk !center_eq (λ p, !hprop_eq)
local attribute is_contr_eq [instance] local attribute is_contr_eq [instance]
/- truncation is upward close -/ /- truncation is upward close -/
@ -210,11 +210,12 @@ namespace is_trunc
--should we remove the following two theorems as they are special cases of --should we remove the following two theorems as they are special cases of
--"is_trunc_is_equiv_closed" --"is_trunc_is_equiv_closed"
definition is_contr_is_equiv_closed (f : A → B) [Hf : is_equiv f] [HA: is_contr A] : (is_contr B) := definition is_contr_is_equiv_closed (f : A → B) [Hf : is_equiv f] [HA: is_contr A]
is_contr.mk (f (center A)) (λp, eq_of_eq_inv f !contr) : (is_contr B) :=
is_contr.mk (f (center A)) (λp, eq_of_eq_inv !contr)
theorem is_contr_equiv_closed (H : A ≃ B) [HA: is_contr A] : is_contr B := theorem is_contr_equiv_closed (H : A ≃ B) [HA: is_contr A] : is_contr B :=
@is_contr_is_equiv_closed _ _ (to_fun H) (to_is_equiv H) _ @is_contr_is_equiv_closed _ _ (to_fun H) (to_is_equiv H) _
definition equiv_of_is_contr_of_is_contr [HA : is_contr A] [HB : is_contr B] : A ≃ B := definition equiv_of_is_contr_of_is_contr [HA : is_contr A] [HB : is_contr B] : A ≃ B :=
equiv.mk equiv.mk

View file

@ -270,7 +270,7 @@ namespace sigma
equiv.mk _ (adjointify equiv.mk _ (adjointify
(λu, (contr u.1)⁻¹ ▹ u.2) (λu, (contr u.1)⁻¹ ▹ u.2)
(λb, ⟨!center, b⟩) (λb, ⟨!center, b⟩)
(λb, ap (λx, x ▹ b) !hprop_eq) (λb, ap (λx, x ▹ b) !hprop_eq_of_is_contr)
(λu, sigma_eq !contr !tr_inv_tr)) (λu, sigma_eq !contr !tr_inv_tr))
/- Associativity -/ /- Associativity -/