feat(hott): many changes is the HoTT library
Prove that 'is_left_adjoint F' is a mere proposition, although this proof is commented out because it takes ~10 seconds
This commit is contained in:
Floris van Doorn
Leonardo de Moura
parent
f555120428
commit
7e52c49dce
22 changed files with 618 additions and 153 deletions
|
|
@ -4,12 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Floris van Doorn
|
||||
-/
|
||||
|
||||
import algebra.category.constructions .constructions function arity
|
||||
import algebra.category.constructions function arity
|
||||
|
||||
open category functor nat_trans eq is_trunc iso equiv prod trunc function
|
||||
open category functor nat_trans eq is_trunc iso equiv prod trunc function pi is_equiv
|
||||
|
||||
namespace category
|
||||
variables {C D : Precategory} {F : C ⇒ D}
|
||||
variables {C D : Precategory} {F : C ⇒ D} {G : D ⇒ C}
|
||||
|
||||
-- do we want to have a structure "is_adjoint" and define
|
||||
-- structure is_left_adjoint (F : C ⇒ D) :=
|
||||
|
|
@ -18,8 +18,8 @@ namespace category
|
|||
|
||||
structure is_left_adjoint [class] (F : C ⇒ D) :=
|
||||
(G : D ⇒ C)
|
||||
(η : functor.id ⟹ G ∘f F)
|
||||
(ε : F ∘f G ⟹ functor.id)
|
||||
(η : 1 ⟹ G ∘f F)
|
||||
(ε : F ∘f G ⟹ 1)
|
||||
(H : Π(c : C), (ε (F c)) ∘ (F (η c)) = ID (F c))
|
||||
(K : Π(d : D), (G (ε d)) ∘ (η (G d)) = ID (G d))
|
||||
|
||||
|
|
@ -39,31 +39,23 @@ namespace category
|
|||
(is_iso_unit : is_iso η)
|
||||
(is_iso_counit : is_iso ε)
|
||||
|
||||
abbreviation inverse := @is_equivalence.G
|
||||
postfix `⁻¹` := inverse
|
||||
--a second notation for the inverse, which is not overloaded
|
||||
postfix [parsing-only] `⁻¹F`:std.prec.max_plus := inverse
|
||||
|
||||
structure equivalence (C D : Precategory) :=
|
||||
(to_functor : C ⇒ D)
|
||||
(struct : is_equivalence to_functor)
|
||||
|
||||
--TODO: review and change
|
||||
--TODO: make some or all of these structures?
|
||||
definition faithful (F : C ⇒ D) :=
|
||||
Π⦃c c' : C⦄ (f f' : c ⟶ c'), F f = F f' → f = f'
|
||||
|
||||
definition full (F : C ⇒ D) := Π⦃c c' : C⦄ (g : F c ⟶ F c'), ∃(f : c ⟶ c'), F f = g
|
||||
|
||||
definition fully_faithful [reducible] (F : C ⇒ D) :=
|
||||
Π⦃c c' : C⦄, is_equiv (@(to_fun_hom F) c c')
|
||||
|
||||
definition split_essentially_surjective (F : C ⇒ D) :=
|
||||
Π⦃d : D⦄, Σ(c : C), F c ≅ d
|
||||
|
||||
definition essentially_surjective (F : C ⇒ D) :=
|
||||
Π⦃d : D⦄, ∃(c : C), F c ≅ d
|
||||
|
||||
definition is_weak_equivalence (F : C ⇒ D) :=
|
||||
fully_faithful F × essentially_surjective F
|
||||
|
||||
definition is_isomorphism (F : C ⇒ D) :=
|
||||
fully_faithful F × is_equiv (to_fun_ob F)
|
||||
definition faithful [class] (F : C ⇒ D) := Π⦃c c' : C⦄ ⦃f f' : c ⟶ c'⦄, F f = F f' → f = f'
|
||||
definition full [class] (F : C ⇒ D) := Π⦃c c' : C⦄, is_surjective (@(to_fun_hom F) c c')
|
||||
definition fully_faithful [class] (F : C ⇒ D) := Π(c c' : C), is_equiv (@(to_fun_hom F) c c')
|
||||
definition split_essentially_surjective [class] (F : C ⇒ D) := Π(d : D), Σ(c : C), F c ≅ d
|
||||
definition essentially_surjective [class] (F : C ⇒ D) := Π(d : D), ∃(c : C), F c ≅ d
|
||||
definition is_weak_equivalence [class] (F : C ⇒ D) := fully_faithful F × essentially_surjective F
|
||||
definition is_isomorphism [class] (F : C ⇒ D) := fully_faithful F × is_equiv (to_fun_ob F)
|
||||
|
||||
structure isomorphism (C D : Precategory) :=
|
||||
(to_functor : C ⇒ D)
|
||||
|
|
@ -73,43 +65,115 @@ namespace category
|
|||
infix `⋍`:25 := equivalence -- \backsimeq or \equiv
|
||||
infix `≌`:25 := isomorphism -- \backcong or \iso
|
||||
|
||||
/-
|
||||
definition is_hprop_is_left_adjoint {C : Category} {D : Precategory} (F : C ⇒ D)
|
||||
: is_hprop (is_left_adjoint F) :=
|
||||
begin
|
||||
apply is_hprop.mk,
|
||||
intro G G', cases G with G η ε H K, cases G' with G' η' ε' H' K',
|
||||
fapply (apd011111 is_left_adjoint.mk),
|
||||
{ fapply functor_eq,
|
||||
{ intro d, apply eq_of_iso, fapply iso.MK,
|
||||
{ exact (G' (ε d) ∘ η' (G d))},
|
||||
{ exact (G (ε' d) ∘ η (G' d))},
|
||||
{ apply sorry /-rewrite [assoc, -{((G (ε' d)) ∘ (η (G' d))) ∘ (G' (ε d))}(assoc)],-/
|
||||
-- apply concat, apply (ap (λc, c ∘ η' _)), rewrite -assoc, apply idp
|
||||
},
|
||||
-- rewrite [-nat_trans.assoc] apply sorry
|
||||
---assoc (G (ε' d)) (η (G' d)) (G' (ε d))
|
||||
{ apply sorry}},
|
||||
{ apply sorry},
|
||||
},
|
||||
{ apply sorry},
|
||||
{ apply sorry},
|
||||
{ apply is_hprop.elim},
|
||||
{ apply is_hprop.elim},
|
||||
definition is_equiv_of_fully_faithful [instance] (F : C ⇒ D) [H : fully_faithful F] (c c' : C)
|
||||
: is_equiv (@(to_fun_hom F) c c') :=
|
||||
!H
|
||||
|
||||
definition is_iso_unit [instance] (F : C ⇒ D) (H : is_equivalence F) : is_iso (unit F) :=
|
||||
!is_equivalence.is_iso_unit
|
||||
|
||||
definition is_iso_counit [instance] (F : C ⇒ D) (H : is_equivalence F) : is_iso (counit F) :=
|
||||
!is_equivalence.is_iso_counit
|
||||
|
||||
-- theorem is_hprop_is_left_adjoint {C : Category} {D : Precategory} (F : C ⇒ D)
|
||||
-- : is_hprop (is_left_adjoint F) :=
|
||||
-- begin
|
||||
-- apply is_hprop.mk,
|
||||
-- intro G G', cases G with G η ε H K, cases G' with G' η' ε' H' K',
|
||||
-- assert lem : Π(p : G = G'), p ▸ η = η' → p ▸ ε = ε'
|
||||
-- → is_left_adjoint.mk G η ε H K = is_left_adjoint.mk G' η' ε' H' K',
|
||||
-- { intros p q r, induction p, induction q, induction r, esimp,
|
||||
-- apply apd011 (is_left_adjoint.mk G η ε) !is_hprop.elim !is_hprop.elim},
|
||||
-- fapply lem,
|
||||
-- { fapply functor.eq_of_pointwise_iso,
|
||||
-- { fapply change_natural_map,
|
||||
-- { exact (G' ∘fn1 ε) ∘n !assoc_natural_rev ∘n (η' ∘1nf G)},
|
||||
-- { intro d, exact (G' (ε d) ∘ η' (G d))},
|
||||
-- { intro d, exact ap (λx, _ ∘ x) !id_left}},
|
||||
-- { intro d, fconstructor,
|
||||
-- { exact (G (ε' d) ∘ η (G' d))},
|
||||
-- { krewrite [▸*,assoc,-assoc (G (ε' d))],
|
||||
-- krewrite [nf_fn_eq_fn_nf_pt' G' ε η d],
|
||||
-- krewrite [assoc,-assoc],
|
||||
-- rewrite [↑functor.compose, -respect_comp G],
|
||||
-- krewrite [nf_fn_eq_fn_nf_pt ε ε' d,nf_fn_eq_fn_nf_pt η' η (G d),▸*],
|
||||
-- rewrite [respect_comp G],
|
||||
-- krewrite [assoc,-assoc (G (ε d))],
|
||||
-- rewrite [↑functor.compose, -respect_comp G],
|
||||
-- krewrite [H' (G d)],
|
||||
-- rewrite [respect_id,id_right],
|
||||
-- apply K},
|
||||
-- { krewrite [▸*,assoc,-assoc (G' (ε d))],
|
||||
-- krewrite [nf_fn_eq_fn_nf_pt' G ε' η' d],
|
||||
-- krewrite [assoc,-assoc],
|
||||
-- rewrite [↑functor.compose, -respect_comp G'],
|
||||
-- krewrite [nf_fn_eq_fn_nf_pt ε' ε d,nf_fn_eq_fn_nf_pt η η' (G' d),▸*],
|
||||
-- rewrite [respect_comp G'],
|
||||
-- krewrite [assoc,-assoc (G' (ε' d))],
|
||||
-- rewrite [↑functor.compose, -respect_comp G'],
|
||||
-- krewrite [H (G' d)],
|
||||
-- rewrite [respect_id,id_right],
|
||||
-- apply K'}}},
|
||||
-- { clear lem, refine transport_hom_of_eq_right _ η ⬝ _,
|
||||
-- krewrite hom_of_eq_compose_right,
|
||||
-- rewrite functor.hom_of_eq_eq_of_pointwise_iso,
|
||||
-- apply nat_trans_eq, intro c, esimp,
|
||||
-- refine !assoc⁻¹ ⬝ ap (λx, _ ∘ x) (nf_fn_eq_fn_nf_pt η η' c) ⬝ !assoc ⬝ _,
|
||||
-- rewrite [▸*,-respect_comp G',H c,respect_id G',id_left]},
|
||||
-- { clear lem, refine transport_hom_of_eq_left _ ε ⬝ _,
|
||||
-- krewrite inv_of_eq_compose_left,
|
||||
-- rewrite functor.inv_of_eq_eq_of_pointwise_iso,
|
||||
-- apply nat_trans_eq, intro d, esimp,
|
||||
-- rewrite [respect_comp,assoc,nf_fn_eq_fn_nf_pt ε' ε d,-assoc,▸*,H (G' d),id_right]},
|
||||
-- end
|
||||
|
||||
section
|
||||
variables (F G)
|
||||
variables (η : G ∘f F ≅ 1) (ε : F ∘f G ≅ 1)
|
||||
include η ε
|
||||
--definition inverse_of_unit_counit
|
||||
|
||||
definition is_equivalence.mk : is_equivalence F :=
|
||||
begin
|
||||
exact sorry
|
||||
end
|
||||
|
||||
end
|
||||
|
||||
definition is_equivalence.mk (F : C ⇒ D) (G : D ⇒ C) (η : G ∘f F ≅ functor.id)
|
||||
(ε : F ∘f G ≅ functor.id) : is_equivalence F :=
|
||||
sorry
|
||||
|
||||
definition full_of_fully_faithful (H : fully_faithful F) : full F :=
|
||||
sorry -- λc c' g, exists.intro ((@(to_fun_hom F) c c')⁻¹ g) _
|
||||
λc c', is_surjective.mk (λg, tr (fiber.mk ((@(to_fun_hom F) c c')⁻¹ᶠ g) !right_inv))
|
||||
|
||||
definition faithful_of_fully_faithful (H : fully_faithful F) : faithful F :=
|
||||
λc c' f f' p, is_injective_of_is_embedding p
|
||||
|
||||
definition fully_faithful_of_full_of_faithful (H : faithful F) (K : full F) : fully_faithful F :=
|
||||
sorry
|
||||
begin
|
||||
intro c c',
|
||||
apply is_equiv_of_is_surjective_of_is_embedding,
|
||||
{ apply is_embedding_of_is_injective,
|
||||
intros f f' p, exact H p},
|
||||
{ apply K}
|
||||
end
|
||||
|
||||
definition fully_faithful_of_is_equivalence (F : C ⇒ D) [H : is_equivalence F]
|
||||
: fully_faithful F :=
|
||||
begin
|
||||
intro c c',
|
||||
fapply adjointify,
|
||||
{ intro g, exact natural_map (@(iso.inverse (unit F)) !is_iso_unit) c' ∘ F⁻¹ g ∘ unit F c},
|
||||
{ intro g, rewrite [+respect_comp], exact sorry},
|
||||
{ exact sorry},
|
||||
end
|
||||
|
||||
definition split_essentially_surjective_of_is_equivalence (F : C ⇒ D) [H : is_equivalence F]
|
||||
: split_essentially_surjective F :=
|
||||
begin
|
||||
intro d, fconstructor,
|
||||
{ exact F⁻¹ d},
|
||||
{ exact componentwise_iso (@(iso.mk (counit F)) !is_iso_counit) d}
|
||||
end
|
||||
|
||||
/-
|
||||
|
||||
definition fully_faithful_equiv (F : C ⇒ D) : fully_faithful F ≃ (faithful F × full F) :=
|
||||
sorry
|
||||
|
|
@ -132,12 +196,12 @@ namespace category
|
|||
sorry
|
||||
|
||||
definition is_isomorphism_equiv1 (F : C ⇒ D) : is_equivalence F
|
||||
≃ Σ(G : D ⇒ C) (η : functor.id = G ∘f F) (ε : F ∘f G = functor.id),
|
||||
≃ Σ(G : D ⇒ C) (η : 1 = G ∘f F) (ε : F ∘f G = 1),
|
||||
sorry ▸ ap (λ(H : C ⇒ C), F ∘f H) η = ap (λ(H : D ⇒ D), H ∘f F) ε⁻¹ :=
|
||||
sorry
|
||||
|
||||
definition is_isomorphism_equiv2 (F : C ⇒ D) : is_equivalence F
|
||||
≃ ∃(G : D ⇒ C), functor.id = G ∘f F × F ∘f G = functor.id :=
|
||||
≃ ∃(G : D ⇒ C), 1 = G ∘f F × F ∘f G = 1 :=
|
||||
sorry
|
||||
|
||||
definition is_equivalence_of_isomorphism (H : is_isomorphism F) : is_equivalence F :=
|
||||
|
|
|
|||
|
|
@ -31,7 +31,7 @@ namespace category
|
|||
variables {C D : Precategory} {F G : C ⇒ D} (η : F ⟹ G) [iso : Π(a : C), is_iso (η a)]
|
||||
include iso
|
||||
|
||||
definition nat_trans_inverse : G ⟹ F :=
|
||||
definition nat_trans_inverse [constructor] : G ⟹ F :=
|
||||
nat_trans.mk
|
||||
(λc, (η c)⁻¹)
|
||||
(λc d f,
|
||||
|
|
@ -58,16 +58,20 @@ namespace category
|
|||
apply is_hset.elim
|
||||
end
|
||||
|
||||
definition is_iso_nat_trans : is_iso η :=
|
||||
definition is_iso_nat_trans [constructor] [instance] : is_iso η :=
|
||||
is_iso.mk (nat_trans_left_inverse η) (nat_trans_right_inverse η)
|
||||
|
||||
variable (iso)
|
||||
definition functor_iso [constructor] : F ≅ G :=
|
||||
@(iso.mk η) !is_iso_nat_trans
|
||||
|
||||
end
|
||||
|
||||
section
|
||||
/- and conversely, if a natural transformation is an iso, it is componentwise an iso -/
|
||||
variables {C D : Precategory} {F G : D ^c C} (η : hom F G) [isoη : is_iso η] (c : C)
|
||||
variables {A B C D : Precategory} {F G : D ^c C} (η : hom F G) [isoη : is_iso η] (c : C)
|
||||
include isoη
|
||||
definition componentwise_is_iso : is_iso (η c) :=
|
||||
definition componentwise_is_iso [instance] : is_iso (η c) :=
|
||||
@is_iso.mk _ _ _ _ _ (natural_map η⁻¹ c) (ap010 natural_map ( left_inverse η) c)
|
||||
(ap010 natural_map (right_inverse η) c)
|
||||
|
||||
|
|
@ -107,6 +111,61 @@ namespace category
|
|||
: natural_map (inv_of_eq p) c = hom_of_eq (ap010 to_fun_ob p c)⁻¹ :=
|
||||
eq.rec_on p idp
|
||||
|
||||
definition hom_of_eq_compose_right {H : C ^c B} (p : F = G)
|
||||
: hom_of_eq (ap (λx, x ∘f H) p) = hom_of_eq p ∘nf H :=
|
||||
eq.rec_on p idp
|
||||
|
||||
definition inv_of_eq_compose_right {H : C ^c B} (p : F = G)
|
||||
: inv_of_eq (ap (λx, x ∘f H) p) = inv_of_eq p ∘nf H :=
|
||||
eq.rec_on p idp
|
||||
|
||||
definition hom_of_eq_compose_left {H : B ^c D} (p : F = G)
|
||||
: hom_of_eq (ap (λx, H ∘f x) p) = H ∘fn hom_of_eq p :=
|
||||
by induction p; exact !fn_id⁻¹
|
||||
|
||||
definition inv_of_eq_compose_left {H : B ^c D} (p : F = G)
|
||||
: inv_of_eq (ap (λx, H ∘f x) p) = H ∘fn inv_of_eq p :=
|
||||
by induction p; exact !fn_id⁻¹
|
||||
|
||||
definition assoc_natural [constructor] (H : C ⇒ D) (G : B ⇒ C) (F : A ⇒ B)
|
||||
: H ∘f (G ∘f F) ⟹ (H ∘f G) ∘f F :=
|
||||
change_natural_map (hom_of_eq !functor.assoc)
|
||||
(λa, id)
|
||||
(λa, !natural_map_hom_of_eq ⬝ ap hom_of_eq !ap010_assoc)
|
||||
|
||||
definition assoc_natural_rev [constructor] (H : C ⇒ D) (G : B ⇒ C) (F : A ⇒ B)
|
||||
: (H ∘f G) ∘f F ⟹ H ∘f (G ∘f F) :=
|
||||
change_natural_map (inv_of_eq !functor.assoc)
|
||||
(λa, id)
|
||||
(λa, !natural_map_inv_of_eq ⬝ ap (λx, hom_of_eq x⁻¹) !ap010_assoc)
|
||||
|
||||
definition id_left_natural [constructor] (F : C ⇒ D) : functor.id ∘f F ⟹ F :=
|
||||
change_natural_map
|
||||
(hom_of_eq !functor.id_left)
|
||||
(λc, id)
|
||||
(λc, by induction F; exact !natural_map_hom_of_eq ⬝ ap hom_of_eq !ap010_functor_mk_eq_constant)
|
||||
|
||||
|
||||
definition id_left_natural_rev [constructor] (F : C ⇒ D) : F ⟹ functor.id ∘f F :=
|
||||
change_natural_map
|
||||
(inv_of_eq !functor.id_left)
|
||||
(λc, id)
|
||||
(λc, by induction F; exact !natural_map_inv_of_eq ⬝
|
||||
ap (λx, hom_of_eq x⁻¹) !ap010_functor_mk_eq_constant)
|
||||
|
||||
definition id_right_natural [constructor] (F : C ⇒ D) : F ∘f functor.id ⟹ F :=
|
||||
change_natural_map
|
||||
(hom_of_eq !functor.id_right)
|
||||
(λc, id)
|
||||
(λc, by induction F; exact !natural_map_hom_of_eq ⬝ ap hom_of_eq !ap010_functor_mk_eq_constant)
|
||||
|
||||
definition id_right_natural_rev [constructor] (F : C ⇒ D) : F ⟹ F ∘f functor.id :=
|
||||
change_natural_map
|
||||
(inv_of_eq !functor.id_right)
|
||||
(λc, id)
|
||||
(λc, by induction F; exact !natural_map_inv_of_eq ⬝
|
||||
ap (λx, hom_of_eq x⁻¹) !ap010_functor_mk_eq_constant)
|
||||
|
||||
end
|
||||
|
||||
namespace functor
|
||||
|
|
@ -171,5 +230,24 @@ namespace category
|
|||
infixr `^c2`:35 := Category_functor
|
||||
end ops
|
||||
|
||||
namespace functor
|
||||
variables {C : Precategory} {D : Category} {F G : D ^c C}
|
||||
|
||||
definition eq_of_pointwise_iso (η : F ⟹ G) (iso : Π(a : C), is_iso (η a)) : F = G :=
|
||||
eq_of_iso (functor_iso η iso)
|
||||
|
||||
definition iso_of_eq_eq_of_pointwise_iso (η : F ⟹ G) (iso : Π(c : C), is_iso (η c))
|
||||
: iso_of_eq (eq_of_pointwise_iso η iso) = functor_iso η iso :=
|
||||
!iso_of_eq_eq_of_iso
|
||||
|
||||
definition hom_of_eq_eq_of_pointwise_iso (η : F ⟹ G) (iso : Π(c : C), is_iso (η c))
|
||||
: hom_of_eq (eq_of_pointwise_iso η iso) = η :=
|
||||
!hom_of_eq_eq_of_iso
|
||||
|
||||
definition inv_of_eq_eq_of_pointwise_iso (η : F ⟹ G) (iso : Π(c : C), is_iso (η c))
|
||||
: inv_of_eq (eq_of_pointwise_iso η iso) = nat_trans_inverse η :=
|
||||
!inv_of_eq_eq_of_iso
|
||||
|
||||
end functor
|
||||
|
||||
end category
|
||||
|
|
|
|||
|
|
@ -38,7 +38,7 @@ namespace category
|
|||
definition opposite_opposite : Opposite (Opposite C) = C :=
|
||||
(ap (Precategory.mk C) (opposite_opposite' C)) ⬝ !Precategory.eta
|
||||
|
||||
postfix `ᵒᵖ`:(max+1) := Opposite
|
||||
postfix `ᵒᵖ`:(max+2) := Opposite
|
||||
|
||||
definition opposite_functor [reducible] {C D : Precategory} (F : C ⇒ D) : Cᵒᵖ ⇒ Dᵒᵖ :=
|
||||
begin
|
||||
|
|
@ -47,6 +47,6 @@ namespace category
|
|||
intros, apply (@respect_comp C D)
|
||||
end
|
||||
|
||||
infixr `ᵒᵖᶠ`:(max+1) := opposite_functor
|
||||
infixr `ᵒᵖᶠ`:(max+2) := opposite_functor
|
||||
|
||||
end category
|
||||
|
|
|
|||
|
|
@ -26,7 +26,8 @@ namespace functor
|
|||
|
||||
-- The following lemmas will later be used to prove that the type of
|
||||
-- precategories forms a precategory itself
|
||||
protected definition compose [reducible] (G : functor D E) (F : functor C D) : functor C E :=
|
||||
protected definition compose [reducible] [constructor] (G : functor D E) (F : functor C D)
|
||||
: functor C E :=
|
||||
functor.mk
|
||||
(λ x, G (F x))
|
||||
(λ a b f, G (F f))
|
||||
|
|
@ -39,10 +40,11 @@ namespace functor
|
|||
|
||||
infixr `∘f`:60 := functor.compose
|
||||
|
||||
protected definition id [reducible] {C : Precategory} : functor C C :=
|
||||
protected definition id [reducible] [constructor] {C : Precategory} : functor C C :=
|
||||
mk (λa, a) (λ a b f, f) (λ a, idp) (λ a b c f g, idp)
|
||||
|
||||
protected definition ID [reducible] (C : Precategory) : functor C C := @functor.id C
|
||||
protected definition ID [reducible] [constructor] (C : Precategory) : functor C C := @functor.id C
|
||||
notation 1 := functor.id
|
||||
|
||||
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₂)
|
||||
|
|
@ -53,7 +55,7 @@ namespace functor
|
|||
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'))
|
||||
by induction F₁; induction F₂; apply 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₂)
|
||||
|
|
@ -68,7 +70,7 @@ namespace functor
|
|||
|
||||
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))
|
||||
by induction F₁; induction F₂; apply 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₂)
|
||||
|
|
@ -108,13 +110,13 @@ namespace functor
|
|||
H ∘f (G ∘f F) = (H ∘f G) ∘f F :=
|
||||
!functor_mk_eq_constant (λa b f, idp)
|
||||
|
||||
protected definition id_left (F : C ⇒ D) : functor.id ∘f F = F :=
|
||||
protected definition id_left (F : C ⇒ D) : 1 ∘f F = F :=
|
||||
functor.rec_on F (λF1 F2 F3 F4, !functor_mk_eq_constant (λa b f, idp))
|
||||
|
||||
protected definition id_right (F : C ⇒ D) : F ∘f functor.id = F :=
|
||||
protected definition id_right (F : C ⇒ D) : F ∘f 1 = F :=
|
||||
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 :=
|
||||
protected definition comp_id_eq_id_comp (F : C ⇒ D) : F ∘f 1 = 1 ∘f F :=
|
||||
!functor.id_right ⬝ !functor.id_left⁻¹
|
||||
|
||||
-- "functor C D" is equivalent to a certain sigma type
|
||||
|
|
|
|||
|
|
@ -206,7 +206,15 @@ namespace iso
|
|||
variables {X : Type} {x y : X} {F G : X → ob}
|
||||
definition transport_hom_of_eq (p : F = G) (f : hom (F x) (F y))
|
||||
: p ▸ f = hom_of_eq (apd10 p y) ∘ f ∘ inv_of_eq (apd10 p x) :=
|
||||
eq.rec_on p !id_leftright⁻¹
|
||||
by induction p; exact !id_leftright⁻¹
|
||||
|
||||
definition transport_hom_of_eq_right (p : x = y) (f : hom c (F x))
|
||||
: p ▸ f = hom_of_eq (ap F p) ∘ f :=
|
||||
by induction p; exact !id_left⁻¹
|
||||
|
||||
definition transport_hom_of_eq_left (p : x = y) (f : hom (F x) c)
|
||||
: p ▸ f = f ∘ inv_of_eq (ap F p) :=
|
||||
by induction p; exact !id_right⁻¹
|
||||
|
||||
definition transport_hom (p : F ~ G) (f : hom (F x) (F y))
|
||||
: eq_of_homotopy p ▸ f = hom_of_eq (p y) ∘ f ∘ inv_of_eq (p x) :=
|
||||
|
|
|
|||
|
|
@ -13,11 +13,11 @@ structure nat_trans {C D : Precategory} (F G : C ⇒ D) :=
|
|||
namespace nat_trans
|
||||
|
||||
infixl `⟹`:25 := nat_trans -- \==>
|
||||
variables {B C D E : Precategory} {F G H I : C ⇒ D} {F' G' : D ⇒ E}
|
||||
variables {B C D E : Precategory} {F G H I : C ⇒ D} {F' G' : D ⇒ E} {F'' G'' : E ⇒ B} {J : C ⇒ C}
|
||||
|
||||
attribute natural_map [coercion]
|
||||
|
||||
protected definition compose [reducible] (η : G ⟹ H) (θ : F ⟹ G) : F ⟹ H :=
|
||||
protected definition compose [constructor] (η : G ⟹ H) (θ : F ⟹ G) : F ⟹ H :=
|
||||
nat_trans.mk
|
||||
(λ a, η a ∘ θ a)
|
||||
(λ a b f,
|
||||
|
|
@ -31,12 +31,14 @@ namespace nat_trans
|
|||
|
||||
infixr `∘n`:60 := nat_trans.compose
|
||||
|
||||
protected definition id [reducible] {C D : Precategory} {F : functor C D} : nat_trans F F :=
|
||||
protected definition id [reducible] {F : C ⇒ D} : nat_trans F F :=
|
||||
mk (λa, id) (λa b f, !id_right ⬝ !id_left⁻¹)
|
||||
|
||||
protected definition ID [reducible] {C D : Precategory} (F : functor C D) : nat_trans F F :=
|
||||
protected definition ID [reducible] (F : C ⇒ D) : nat_trans F F :=
|
||||
(@nat_trans.id C D F)
|
||||
|
||||
notation 1 := nat_trans.id
|
||||
|
||||
definition nat_trans_mk_eq {η₁ η₂ : Π (a : C), hom (F a) (G a)}
|
||||
(nat₁ : Π (a b : C) (f : hom a b), G f ∘ η₁ a = η₁ b ∘ F f)
|
||||
(nat₂ : Π (a b : C) (f : hom a b), G f ∘ η₂ a = η₂ b ∘ F f)
|
||||
|
|
@ -45,16 +47,16 @@ namespace nat_trans
|
|||
apd011 nat_trans.mk (eq_of_homotopy p) !is_hprop.elim
|
||||
|
||||
definition nat_trans_eq {η₁ η₂ : F ⟹ G} : natural_map η₁ ~ natural_map η₂ → η₁ = η₂ :=
|
||||
nat_trans.rec_on η₁ (λf₁ nat₁, nat_trans.rec_on η₂ (λf₂ nat₂ p, !nat_trans_mk_eq p))
|
||||
by induction η₁; induction η₂; apply nat_trans_mk_eq
|
||||
|
||||
protected definition assoc (η₃ : H ⟹ I) (η₂ : G ⟹ H) (η₁ : F ⟹ G) :
|
||||
η₃ ∘n (η₂ ∘n η₁) = (η₃ ∘n η₂) ∘n η₁ :=
|
||||
nat_trans_eq (λa, !assoc)
|
||||
|
||||
protected definition id_left (η : F ⟹ G) : nat_trans.id ∘n η = η :=
|
||||
protected definition id_left (η : F ⟹ G) : 1 ∘n η = η :=
|
||||
nat_trans_eq (λa, !id_left)
|
||||
|
||||
protected definition id_right (η : F ⟹ G) : η ∘n nat_trans.id = η :=
|
||||
protected definition id_right (η : F ⟹ G) : η ∘n 1 = η :=
|
||||
nat_trans_eq (λa, !id_right)
|
||||
|
||||
protected definition sigma_char (F G : C ⇒ D) :
|
||||
|
|
@ -78,12 +80,18 @@ namespace nat_trans
|
|||
definition is_hset_nat_trans [instance] : is_hset (F ⟹ G) :=
|
||||
by apply is_trunc_is_equiv_closed; apply (equiv.to_is_equiv !nat_trans.sigma_char)
|
||||
|
||||
definition nat_trans_functor_compose [reducible] (η : G ⟹ H) (F : E ⇒ C) : G ∘f F ⟹ H ∘f F :=
|
||||
definition change_natural_map [constructor] (η : F ⟹ G) (f : Π (a : C), F a ⟶ G a)
|
||||
(p : Πa, η a = f a) : F ⟹ G :=
|
||||
nat_trans.mk f (λa b g, p a ▸ p b ▸ naturality η g)
|
||||
|
||||
definition nat_trans_functor_compose [constructor] (η : 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 :=
|
||||
definition functor_nat_trans_compose [constructor] (F : D ⇒ E) (η : G ⟹ H)
|
||||
: F ∘f G ⟹ F ∘f H :=
|
||||
nat_trans.mk
|
||||
(λ a, F (η a))
|
||||
(λ a b f, calc
|
||||
|
|
@ -91,13 +99,53 @@ namespace nat_trans
|
|||
... = F (η b ∘ G f) : by rewrite (naturality η f)
|
||||
... = F (η b) ∘ F (G f) : by rewrite respect_comp)
|
||||
|
||||
definition nat_trans_id_functor_compose [constructor] (η : J ⟹ 1) (F : E ⇒ C)
|
||||
: J ∘f F ⟹ F :=
|
||||
nat_trans.mk
|
||||
(λ a, η (F a))
|
||||
(λ a b f, naturality η (F f))
|
||||
|
||||
definition id_nat_trans_functor_compose [constructor] (η : 1 ⟹ J) (F : E ⇒ C)
|
||||
: F ⟹ J ∘f F :=
|
||||
nat_trans.mk
|
||||
(λ a, η (F a))
|
||||
(λ a b f, naturality η (F f))
|
||||
|
||||
definition functor_nat_trans_id_compose [constructor] (F : C ⇒ D) (η : J ⟹ 1)
|
||||
: F ∘f J ⟹ F :=
|
||||
nat_trans.mk
|
||||
(λ a, F (η a))
|
||||
(λ a b f, calc
|
||||
F f ∘ F (η a) = F (f ∘ η a) : by rewrite respect_comp
|
||||
... = F (η b ∘ J f) : by rewrite (naturality η f)
|
||||
... = F (η b) ∘ F (J f) : by rewrite respect_comp)
|
||||
|
||||
definition functor_id_nat_trans_compose [constructor] (F : C ⇒ D) (η : 1 ⟹ J)
|
||||
: F ⟹ F ∘f J :=
|
||||
nat_trans.mk
|
||||
(λ a, F (η a))
|
||||
(λ a b f, calc
|
||||
F (J f) ∘ F (η a) = F (J f ∘ η a) : by rewrite respect_comp
|
||||
... = F (η b ∘ f) : by rewrite (naturality η f)
|
||||
... = F (η b) ∘ F f : by rewrite respect_comp)
|
||||
|
||||
infixr `∘nf`:62 := nat_trans_functor_compose
|
||||
infixr `∘fn`:62 := functor_nat_trans_compose
|
||||
infixr `∘n1f`:62 := nat_trans_id_functor_compose
|
||||
infixr `∘1nf`:62 := id_nat_trans_functor_compose
|
||||
infixr `∘f1n`:62 := functor_id_nat_trans_compose
|
||||
infixr `∘fn1`:62 := functor_nat_trans_id_compose
|
||||
|
||||
definition nf_fn_eq_fn_nf_pt (η : F ⟹ G) (θ : F' ⟹ G') (c : C)
|
||||
: (θ (G c)) ∘ (F' (η c)) = (G' (η c)) ∘ (θ (F c)) :=
|
||||
(naturality θ (η c))⁻¹
|
||||
|
||||
variable (F')
|
||||
definition nf_fn_eq_fn_nf_pt' (η : F ⟹ G) (θ : F'' ⟹ G'') (c : C)
|
||||
: (θ (F' (G c))) ∘ (F'' (F' (η c))) = (G'' (F' (η c))) ∘ (θ (F' (F c))) :=
|
||||
(naturality θ (F' (η c)))⁻¹
|
||||
variable {F'}
|
||||
|
||||
definition nf_fn_eq_fn_nf (η : F ⟹ G) (θ : F' ⟹ G')
|
||||
: (θ ∘nf G) ∘n (F' ∘fn η) = (G' ∘fn η) ∘n (θ ∘nf F) :=
|
||||
nat_trans_eq (λ c, nf_fn_eq_fn_nf_pt η θ c)
|
||||
|
|
@ -110,19 +158,20 @@ namespace nat_trans
|
|||
: (η ∘n θ) ∘nf F' = (η ∘nf F') ∘n (θ ∘nf F') :=
|
||||
nat_trans_eq (λc, idp)
|
||||
|
||||
definition fn_id (F' : D ⇒ E) : F' ∘fn nat_trans.ID F = nat_trans.id :=
|
||||
definition fn_id (F' : D ⇒ E) : F' ∘fn nat_trans.ID F = 1 :=
|
||||
nat_trans_eq (λc, by apply respect_id)
|
||||
|
||||
definition id_nf (F' : B ⇒ C) : nat_trans.ID F ∘nf F' = nat_trans.id :=
|
||||
definition id_nf (F' : B ⇒ C) : nat_trans.ID F ∘nf F' = 1 :=
|
||||
nat_trans_eq (λc, idp)
|
||||
|
||||
definition id_fn (η : G ⟹ H) (c : C) : (functor.id ∘fn η) c = η c :=
|
||||
definition id_fn (η : G ⟹ H) (c : C) : (1 ∘fn η) c = η c :=
|
||||
idp
|
||||
|
||||
definition nf_id (η : G ⟹ H) (c : C) : (η ∘nf functor.id) c = η c :=
|
||||
definition nf_id (η : G ⟹ H) (c : C) : (η ∘nf 1) c = η c :=
|
||||
idp
|
||||
|
||||
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
|
||||
|
|
|
|||
|
|
@ -23,7 +23,7 @@ The rows indicate the chapters, the columns the sections.
|
|||
| Ch 6 | . | + | + | + | + | ½ | ½ | ¼ | ¼ | ¼ | ¾ | - | . | | |
|
||||
| Ch 7 | + | + | + | - | - | - | - | | | | | | | | |
|
||||
| Ch 8 | ¾ | - | - | - | - | - | - | - | - | - | | | | | |
|
||||
| Ch 9 | ¾ | + | ¼ | ¼ | ½ | ½ | - | - | - | | | | | | |
|
||||
| Ch 9 | ¾ | + | + | ¼ | ½ | ½ | - | - | - | | | | | | |
|
||||
| Ch 10 | - | - | - | - | - | | | | | | | | | | |
|
||||
| Ch 11 | - | - | - | - | - | - | | | | | | | | | |
|
||||
|
||||
|
|
@ -155,7 +155,7 @@ Every file is in the folder [algebra.category](algebra/category/category.md)
|
|||
|
||||
- 9.1 (Categories and precategories): [precategory](algebra/category/precategory.hlean), [iso](algebra/category/iso.hlean), [category](algebra/category/category.hlean), [groupoid](algebra/category/groupoid.hlean) (mostly)
|
||||
- 9.2 (Functors and transformations): [functor](algebra/category/functor.hlean), [nat_trans](algebra/category/nat_trans.hlean), [constructions.functor](algebra/category/constructions/functor.hlean)
|
||||
- 9.3 (Adjunctions): [adjoint](algebra/category/adjoint.hlean) (only definition)
|
||||
- 9.3 (Adjunctions): [adjoint](algebra/category/adjoint.hlean)
|
||||
- 9.4 (Equivalences): [adjoint](algebra/category/adjoint.hlean) (only definitions)
|
||||
- 9.5 (The Yoneda lemma): [constructions.opposite](algebra/category/constructions/opposite.hlean), [constructions.product](algebra/category/constructions/product.hlean), [yoneda](algebra/category/yoneda.hlean) (up to definition of Yoneda embedding)
|
||||
- 9.6 (Strict categories): [strict](algebra/category/strict.hlean) (only definition)
|
||||
|
|
|
|||
|
|
@ -101,14 +101,103 @@ namespace eq
|
|||
square (p a) (p a') (ap f q) (ap g q) :=
|
||||
eq.rec_on q vrfl
|
||||
|
||||
/- canceling, whiskering and moving thinks along the sides of the square -/
|
||||
definition whisker_tl (p : a = a₀₀) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁)
|
||||
: square (p ⬝ p₁₀) p₁₂ (p ⬝ p₀₁) p₂₁ :=
|
||||
by induction s₁₁;induction p;exact ids
|
||||
by induction s₁₁;induction p;constructor
|
||||
|
||||
definition whisker_br (p : a₂₂ = a) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁)
|
||||
: square p₁₀ (p₁₂ ⬝ p) p₀₁ (p₂₁ ⬝ p) :=
|
||||
by induction p;exact s₁₁
|
||||
|
||||
definition whisker_rt (p : a = a₂₀) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁)
|
||||
: square (p₁₀ ⬝ p⁻¹) p₁₂ p₀₁ (p ⬝ p₂₁) :=
|
||||
by induction s₁₁;induction p;constructor
|
||||
|
||||
definition whisker_tr (p : a₂₀ = a) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁)
|
||||
: square (p₁₀ ⬝ p) p₁₂ p₀₁ (p⁻¹ ⬝ p₂₁) :=
|
||||
by induction s₁₁;induction p;constructor
|
||||
|
||||
definition whisker_bl (p : a = a₀₂) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁)
|
||||
: square p₁₀ (p ⬝ p₁₂) (p₀₁ ⬝ p⁻¹) p₂₁ :=
|
||||
by induction s₁₁;induction p;constructor
|
||||
|
||||
definition whisker_lb (p : a₀₂ = a) (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁)
|
||||
: square p₁₀ (p⁻¹ ⬝ p₁₂) (p₀₁ ⬝ p) p₂₁ :=
|
||||
by induction s₁₁;induction p;constructor
|
||||
|
||||
definition cancel_tl (p : a = a₀₀) (s₁₁ : square (p ⬝ p₁₀) p₁₂ (p ⬝ p₀₁) p₂₁)
|
||||
: square p₁₀ p₁₂ p₀₁ p₂₁ :=
|
||||
by induction p; rewrite +idp_con at s₁₁; exact s₁₁
|
||||
|
||||
definition cancel_br (p : a₂₂ = a) (s₁₁ : square p₁₀ (p₁₂ ⬝ p) p₀₁ (p₂₁ ⬝ p))
|
||||
: square p₁₀ p₁₂ p₀₁ p₂₁ :=
|
||||
by induction p;exact s₁₁
|
||||
|
||||
definition cancel_rt (p : a = a₂₀) (s₁₁ : square (p₁₀ ⬝ p⁻¹) p₁₂ p₀₁ (p ⬝ p₂₁))
|
||||
: square p₁₀ p₁₂ p₀₁ p₂₁ :=
|
||||
by induction p; rewrite idp_con at s₁₁; exact s₁₁
|
||||
|
||||
definition cancel_tr (p : a₂₀ = a) (s₁₁ : square (p₁₀ ⬝ p) p₁₂ p₀₁ (p⁻¹ ⬝ p₂₁))
|
||||
: square p₁₀ p₁₂ p₀₁ p₂₁ :=
|
||||
by induction p; rewrite [▸* at s₁₁,idp_con at s₁₁]; exact s₁₁
|
||||
|
||||
definition cancel_bl (p : a = a₀₂) (s₁₁ : square p₁₀ (p ⬝ p₁₂) (p₀₁ ⬝ p⁻¹) p₂₁)
|
||||
: square p₁₀ p₁₂ p₀₁ p₂₁ :=
|
||||
by induction p; rewrite idp_con at s₁₁; exact s₁₁
|
||||
|
||||
definition cancel_lb (p : a₀₂ = a) (s₁₁ : square p₁₀ (p⁻¹ ⬝ p₁₂) (p₀₁ ⬝ p) p₂₁)
|
||||
: square p₁₀ p₁₂ p₀₁ p₂₁ :=
|
||||
by induction p; rewrite [▸* at s₁₁,idp_con at s₁₁]; exact s₁₁
|
||||
|
||||
definition move_top_of_left {p : a₀₀ = a} {q : a = a₀₂} (s : square p₁₀ p₁₂ (p ⬝ q) p₂₁)
|
||||
: square (p⁻¹ ⬝ p₁₀) p₁₂ q p₂₁ :=
|
||||
by apply cancel_tl p; rewrite con_inv_cancel_left; exact s
|
||||
|
||||
definition move_top_of_left' {p : a = a₀₀} {q : a = a₀₂} (s : square p₁₀ p₁₂ (p⁻¹ ⬝ q) p₂₁)
|
||||
: square (p ⬝ p₁₀) p₁₂ q p₂₁ :=
|
||||
by apply cancel_tl p⁻¹; rewrite inv_con_cancel_left; exact s
|
||||
|
||||
definition move_left_of_top {p : a₀₀ = a} {q : a = a₂₀} (s : square (p ⬝ q) p₁₂ p₀₁ p₂₁)
|
||||
: square q p₁₂ (p⁻¹ ⬝ p₀₁) p₂₁ :=
|
||||
by apply cancel_tl p; rewrite con_inv_cancel_left; exact s
|
||||
|
||||
definition move_left_of_top' {p : a = a₀₀} {q : a = a₂₀} (s : square (p⁻¹ ⬝ q) p₁₂ p₀₁ p₂₁)
|
||||
: square q p₁₂ (p ⬝ p₀₁) p₂₁ :=
|
||||
by apply cancel_tl p⁻¹; rewrite inv_con_cancel_left; exact s
|
||||
|
||||
definition move_bot_of_right {p : a₂₀ = a} {q : a = a₂₂} (s : square p₁₀ p₁₂ p₀₁ (p ⬝ q))
|
||||
: square p₁₀ (p₁₂ ⬝ q⁻¹) p₀₁ p :=
|
||||
by apply cancel_br q; rewrite inv_con_cancel_right; exact s
|
||||
|
||||
definition move_bot_of_right' {p : a₂₀ = a} {q : a₂₂ = a} (s : square p₁₀ p₁₂ p₀₁ (p ⬝ q⁻¹))
|
||||
: square p₁₀ (p₁₂ ⬝ q) p₀₁ p :=
|
||||
by apply cancel_br q⁻¹; rewrite con_inv_cancel_right; exact s
|
||||
|
||||
definition move_right_of_bot {p : a₀₂ = a} {q : a = a₂₂} (s : square p₁₀ (p ⬝ q) p₀₁ p₂₁)
|
||||
: square p₁₀ p p₀₁ (p₂₁ ⬝ q⁻¹) :=
|
||||
by apply cancel_br q; rewrite inv_con_cancel_right; exact s
|
||||
|
||||
definition move_right_of_bot' {p : a₀₂ = a} {q : a₂₂ = a} (s : square p₁₀ (p ⬝ q⁻¹) p₀₁ p₂₁)
|
||||
: square p₁₀ p p₀₁ (p₂₁ ⬝ q) :=
|
||||
by apply cancel_br q⁻¹; rewrite con_inv_cancel_right; exact s
|
||||
|
||||
definition move_top_of_right {p : a₂₀ = a} {q : a = a₂₂} (s : square p₁₀ p₁₂ p₀₁ (p ⬝ q))
|
||||
: square (p₁₀ ⬝ p) p₁₂ p₀₁ q :=
|
||||
by apply cancel_rt p; rewrite con_inv_cancel_right; exact s
|
||||
|
||||
definition move_right_of_top {p : a₀₀ = a} {q : a = a₂₀} (s : square (p ⬝ q) p₁₂ p₀₁ p₂₁)
|
||||
: square p p₁₂ p₀₁ (q ⬝ p₂₁) :=
|
||||
by apply cancel_tr q; rewrite inv_con_cancel_left; exact s
|
||||
|
||||
definition move_bot_of_left {p : a₀₀ = a} {q : a = a₀₂} (s : square p₁₀ p₁₂ (p ⬝ q) p₂₁)
|
||||
: square p₁₀ (q ⬝ p₁₂) p p₂₁ :=
|
||||
by apply cancel_lb q; rewrite inv_con_cancel_left; exact s
|
||||
|
||||
definition move_left_of_bot {p : a₀₂ = a} {q : a = a₂₂} (s : square p₁₀ (p ⬝ q) p₀₁ p₂₁)
|
||||
: square p₁₀ q (p₀₁ ⬝ p) p₂₁ :=
|
||||
by apply cancel_bl p; rewrite con_inv_cancel_right; exact s
|
||||
|
||||
/- some higher ∞-groupoid operations -/
|
||||
|
||||
definition vconcat_vrfl (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁)
|
||||
|
|
@ -125,7 +214,7 @@ namespace eq
|
|||
by induction s₁₁; apply idp
|
||||
|
||||
definition square_of_eq (r : p₁₀ ⬝ p₂₁ = p₀₁ ⬝ p₁₂) : square p₁₀ p₁₂ p₀₁ p₂₁ :=
|
||||
by induction p₁₂; esimp [concat] at r; induction r; induction p₂₁; induction p₁₀; exact ids
|
||||
by induction p₁₂; esimp at r; induction r; induction p₂₁; induction p₁₀; exact ids
|
||||
|
||||
definition eq_top_of_square [unfold 10] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁)
|
||||
: p₁₀ = p₀₁ ⬝ p₁₂ ⬝ p₂₁⁻¹ :=
|
||||
|
|
|
|||
|
|
@ -103,10 +103,18 @@ namespace eq
|
|||
square.rec_on q idso
|
||||
|
||||
-- relating pathovers to squareovers
|
||||
definition pathover_of_squareover (t₁₁ : squareover B s₁₁ q₁₀ q₁₂ q₀₁ q₂₁)
|
||||
definition pathover_of_squareover' (t₁₁ : squareover B s₁₁ q₁₀ q₁₂ q₀₁ q₂₁)
|
||||
: q₁₀ ⬝o q₂₁ =[eq_of_square s₁₁] q₀₁ ⬝o q₁₂ :=
|
||||
by induction t₁₁; constructor
|
||||
|
||||
definition pathover_of_squareover {s : p₁₀ ⬝ p₂₁ = p₀₁ ⬝ p₁₂}
|
||||
(t₁₁ : squareover B (square_of_eq s) q₁₀ q₁₂ q₀₁ q₂₁)
|
||||
: q₁₀ ⬝o q₂₁ =[s] q₀₁ ⬝o q₁₂ :=
|
||||
begin
|
||||
revert s t₁₁, refine equiv_rect' !square_equiv_eq⁻¹ᵉ (λa b, squareover B b _ _ _ _ → _) _,
|
||||
intro s, exact pathover_of_squareover'
|
||||
end
|
||||
|
||||
definition squareover_of_pathover {s : p₁₀ ⬝ p₂₁ = p₀₁ ⬝ p₁₂}
|
||||
(r : q₁₀ ⬝o q₂₁ =[s] q₀₁ ⬝o q₁₂) : squareover B (square_of_eq s) q₁₀ q₁₂ q₀₁ q₂₁ :=
|
||||
by induction q₁₂; esimp [concato] at r;induction r;induction q₂₁;induction q₁₀;constructor
|
||||
|
|
@ -120,6 +128,14 @@ namespace eq
|
|||
: squareover B (square_of_eq_top s) q₁₀ q₁₂ q₀₁ q₂₁ :=
|
||||
by induction q₂₁; induction q₁₂; esimp at r;induction r;induction q₁₀;constructor
|
||||
|
||||
definition pathover_of_hdeg_squareover {p₀₁' : a₀₀ = a₀₂} {r : p₀₁ = p₀₁'} {q₀₁' : b₀₀ =[p₀₁'] b₀₂}
|
||||
(t : squareover B (hdeg_square r) idpo idpo q₀₁ q₀₁') : q₀₁ =[r] q₀₁' :=
|
||||
by induction r; induction q₀₁'; exact (pathover_of_squareover' t)⁻¹ᵒ
|
||||
|
||||
definition pathover_of_vdeg_squareover {p₁₀' : a₀₀ = a₂₀} {r : p₁₀ = p₁₀'} {q₁₀' : b₀₀ =[p₁₀'] b₂₀}
|
||||
(t : squareover B (vdeg_square r) q₁₀ q₁₀' idpo idpo) : q₁₀ =[r] q₁₀' :=
|
||||
by induction r; induction q₁₀'; exact pathover_of_squareover' t
|
||||
|
||||
definition squareover_of_eq_top (r : change_path (eq_top_of_square s₁₁) q₁₀ = q₀₁ ⬝o q₁₂ ⬝o q₂₁⁻¹ᵒ)
|
||||
: squareover B s₁₁ q₁₀ q₁₂ q₀₁ q₂₁ :=
|
||||
begin
|
||||
|
|
|
|||
|
|
@ -91,6 +91,39 @@ namespace function
|
|||
exact H,
|
||||
end
|
||||
|
||||
-- definition is_hprop_is_split_surjective [instance] (f : A → B) : is_hprop (is_split_surjective f) :=
|
||||
-- begin
|
||||
-- have H : (Π(b : B), fiber f b) ≃ is_split_surjective f,
|
||||
-- begin
|
||||
-- fapply equiv.MK,
|
||||
-- {exact is_split_surjective.mk},
|
||||
-- {intro h, cases h, exact elim},
|
||||
-- {intro h, cases h, apply idp},
|
||||
-- {intro p, apply idp},
|
||||
-- end,
|
||||
-- apply is_trunc_equiv_closed,
|
||||
-- exact H,
|
||||
-- apply is_trunc_pi, intro b,
|
||||
-- apply is_trunc_equiv_closed_rev,
|
||||
-- apply fiber.sigma_char,
|
||||
-- end
|
||||
|
||||
-- definition is_hprop_is_retraction [instance] (f : A → B) : is_hprop (is_retraction f) :=
|
||||
-- begin
|
||||
-- have H : (Σ(g : B → A), Πb, f (g b) = b) ≃ is_retraction f,
|
||||
-- begin
|
||||
-- fapply equiv.MK,
|
||||
-- {intro x, induction x with g p, constructor, exact p},
|
||||
-- {intro h, induction h, apply sigma.mk, assumption},
|
||||
-- {intro h, induction h, reflexivity},
|
||||
-- {intro x, induction x, reflexivity},
|
||||
-- end,
|
||||
-- apply is_trunc_equiv_closed,
|
||||
-- exact H,
|
||||
-- apply is_trunc_of_imp_is_trunc, intro x, induction x with g p,
|
||||
-- apply is_contr_right_inverse
|
||||
-- end
|
||||
|
||||
definition is_embedding_of_is_equiv [instance] (f : A → B) [H : is_equiv f] : is_embedding f :=
|
||||
is_embedding.mk _
|
||||
|
||||
|
|
|
|||
|
|
@ -69,7 +69,7 @@ namespace is_equiv
|
|||
parameters {A B : Type} (f : A → B) (g : B → A)
|
||||
(ret : Πb, f (g b) = b) (sec : Πa, g (f a) = a)
|
||||
|
||||
private definition adjointify_left_inv' (a : A) : g (f a) = a :=
|
||||
private abbreviation adjointify_left_inv' (a : A) : g (f a) = a :=
|
||||
ap g (ap f (inverse (sec a))) ⬝ ap g (ret (f a)) ⬝ sec a
|
||||
|
||||
private definition adjointify_adj' (a : A) : ret (f a) = ap f (adjointify_left_inv' a) :=
|
||||
|
|
@ -93,7 +93,7 @@ namespace is_equiv
|
|||
... = (ap f (sec a)⁻¹ ⬝ (ret fgfa)⁻¹) ⬝ (fgretrfa ⬝ ap f (sec a)) : by rewrite ap_inv
|
||||
... = ((ap f (sec a)⁻¹ ⬝ (ret fgfa)⁻¹) ⬝ fgretrfa) ⬝ ap f (sec a) : by rewrite con.assoc'
|
||||
... = ((retrfa⁻¹ ⬝ ap (f ∘ g) (ap f (sec a)⁻¹)) ⬝ fgretrfa) ⬝ ap f (sec a) : by rewrite con_ap_eq_con
|
||||
... = ((retrfa⁻¹ ⬝ fgfinvsect) ⬝ fgretrfa) ⬝ ap f (sec a) : by rewrite ap_compose
|
||||
... = ((retrfa⁻¹ ⬝ fgfinvsect) ⬝ fgretrfa) ⬝ ap f (sec a) : by rewrite ap_compose
|
||||
... = (retrfa⁻¹ ⬝ (fgfinvsect ⬝ fgretrfa)) ⬝ ap f (sec a) : by rewrite con.assoc'
|
||||
... = retrfa⁻¹ ⬝ ap f (ap g (ap f (sec a)⁻¹) ⬝ ap g (ret (f a))) ⬝ ap f (sec a) : by rewrite ap_con
|
||||
... = retrfa⁻¹ ⬝ (ap f (ap g (ap f (sec a)⁻¹) ⬝ ap g (ret (f a))) ⬝ ap f (sec a)) : by rewrite con.assoc'
|
||||
|
|
@ -121,7 +121,8 @@ namespace is_equiv
|
|||
(λ b, ap f !Hty⁻¹ ⬝ right_inv f b)
|
||||
(λ a, !Hty⁻¹ ⬝ left_inv f a)
|
||||
|
||||
definition is_equiv_up [instance] [constructor] (A : Type) : is_equiv (up : A → lift A) :=
|
||||
definition is_equiv_up [instance] [constructor] (A : Type)
|
||||
: is_equiv (up : A → lift A) :=
|
||||
adjointify up down (λa, by induction a;reflexivity) (λa, idp)
|
||||
|
||||
section
|
||||
|
|
@ -143,6 +144,12 @@ namespace is_equiv
|
|||
definition eq_of_fn_eq_fn' {x y : A} (q : f x = f y) : x = y :=
|
||||
(left_inv f x)⁻¹ ⬝ ap f⁻¹ q ⬝ left_inv f y
|
||||
|
||||
theorem ap_eq_of_fn_eq_fn' {x y : A} (q : f x = f y) : ap f (eq_of_fn_eq_fn' f q) = q :=
|
||||
begin
|
||||
rewrite [↑eq_of_fn_eq_fn',+ap_con,ap_inv,-+adj,-ap_compose,con.assoc,
|
||||
ap_con_eq_con_ap (right_inv f) q,inv_con_cancel_left,ap_id],
|
||||
end
|
||||
|
||||
definition is_equiv_ap [instance] (x y : A) : is_equiv (ap f : x = y → f x = f y) :=
|
||||
adjointify
|
||||
(ap f)
|
||||
|
|
@ -168,9 +175,11 @@ namespace is_equiv
|
|||
-- once pulled back along an equivalence f : A → B, then it has a section
|
||||
-- over all of B.
|
||||
|
||||
definition is_equiv_rect (P : B → Type) :
|
||||
(Πx, P (f x)) → (Πy, P y) :=
|
||||
(λg y, eq.transport _ (right_inv f y) (g (f⁻¹ y)))
|
||||
definition is_equiv_rect (P : B → Type) (g : Πa, P (f a)) (b : B) : P b :=
|
||||
right_inv f b ▸ g (f⁻¹ b)
|
||||
|
||||
definition is_equiv_rect' (P : A → B → Type) (g : Πb, P (f⁻¹ b) b) (a : A) : P a (f a) :=
|
||||
left_inv f a ▸ g (f a)
|
||||
|
||||
definition is_equiv_rect_comp (P : B → Type)
|
||||
(df : Π (x : A), P (f x)) (x : A) : is_equiv_rect f P df (f x) = df x :=
|
||||
|
|
@ -181,6 +190,13 @@ namespace is_equiv
|
|||
... = left_inv f x ▸ df (f⁻¹ (f x)) : by rewrite -tr_compose
|
||||
... = df x : by rewrite (apd df (left_inv f x))
|
||||
|
||||
theorem adj_inv (b : B) : left_inv f (f⁻¹ b) = ap f⁻¹ (right_inv f b) :=
|
||||
is_equiv_rect f _
|
||||
(λa,
|
||||
eq.cancel_right (whisker_left _ !ap_id⁻¹ ⬝ (ap_con_eq_con_ap (left_inv f) (left_inv f a))⁻¹) ⬝
|
||||
!ap_compose ⬝ ap02 f⁻¹ (adj f a)⁻¹)
|
||||
b
|
||||
|
||||
end
|
||||
|
||||
section
|
||||
|
|
@ -202,10 +218,29 @@ namespace is_equiv
|
|||
end
|
||||
|
||||
--Transporting is an equivalence
|
||||
definition is_equiv_tr [instance] [constructor] {A : Type} (P : A → Type) {x y : A} (p : x = y)
|
||||
: (is_equiv (transport P p)) :=
|
||||
definition is_equiv_tr [instance] [constructor] {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) (inv_tr_tr p) (tr_inv_tr_lemma p)
|
||||
|
||||
section
|
||||
variables {A : Type} {B C : A → Type} (f : Π{a}, B a → C a) [H : Πa, is_equiv (@f a)]
|
||||
{g : A → A} (h : Π{a}, B a → B (g a)) (h' : Π{a}, C a → C (g a))
|
||||
include H
|
||||
definition inv_commute' (p : Π⦃a : A⦄ (b : B a), f (h b) = h' (f b)) {a : A} (c : C a) :
|
||||
f⁻¹ (h' c) = h (f⁻¹ c) :=
|
||||
eq_of_fn_eq_fn' f (right_inv f (h' c) ⬝ ap h' (right_inv f c)⁻¹ ⬝ (p (f⁻¹ c))⁻¹)
|
||||
|
||||
definition fun_commute_of_inv_commute' (p : Π⦃a : A⦄ (c : C a), f⁻¹ (h' c) = h (f⁻¹ c))
|
||||
{a : A} (b : B a) : f (h b) = h' (f b) :=
|
||||
eq_of_fn_eq_fn' f⁻¹ (left_inv f (h b) ⬝ ap h (left_inv f b)⁻¹ ⬝ (p (f b))⁻¹)
|
||||
|
||||
definition ap_inv_commute' (p : Π⦃a : A⦄ (b : B a), f (h b) = h' (f b)) {a : A} (c : C a) :
|
||||
ap f (inv_commute' @f @h @h' p c)
|
||||
= right_inv f (h' c) ⬝ ap h' (right_inv f c)⁻¹ ⬝ (p (f⁻¹ c))⁻¹ :=
|
||||
!ap_eq_of_fn_eq_fn'
|
||||
|
||||
end
|
||||
|
||||
end is_equiv
|
||||
open is_equiv
|
||||
|
||||
|
|
@ -216,7 +251,7 @@ namespace eq
|
|||
p⁻¹ ▸ b = (transport B p)⁻¹ b := idp
|
||||
|
||||
definition cast_inv_fn {A B : Type} (p : A = B) : cast p⁻¹ = (cast p)⁻¹ := idp
|
||||
definition cast_inv {A B : Type} (p : A = B) (b : B) : cast p⁻¹ b = (cast p)⁻¹ b := idp
|
||||
definition cast_inv {A B : Type} (p : A = B) (b : B) : cast p⁻¹ b = (cast p)⁻¹ b := idp
|
||||
end eq
|
||||
|
||||
namespace equiv
|
||||
|
|
@ -228,6 +263,7 @@ namespace equiv
|
|||
|
||||
infix `≃`:25 := equiv
|
||||
|
||||
section
|
||||
variables {A B C : Type}
|
||||
|
||||
protected definition MK [reducible] [constructor] (f : A → B) (g : B → A)
|
||||
|
|
@ -291,9 +327,11 @@ namespace equiv
|
|||
|
||||
definition equiv_lift (A : Type) : A ≃ lift A := equiv.mk up _
|
||||
|
||||
definition equiv_rect (f : A ≃ B) (P : B → Type) :
|
||||
(Πx, P (f x)) → (Πy, P y) :=
|
||||
(λg y, eq.transport _ (right_inv f y) (g (f⁻¹ y)))
|
||||
definition equiv_rect (f : A ≃ B) (P : B → Type) (g : Πa, P (f a)) (b : B) : P b :=
|
||||
right_inv f b ▸ g (f⁻¹ b)
|
||||
|
||||
definition equiv_rect' (f : A ≃ B) (P : A → B → Type) (g : Πb, P (f⁻¹ b) b) (a : A) : P a (f a) :=
|
||||
left_inv f a ▸ g (f a)
|
||||
|
||||
definition equiv_rect_comp (f : A ≃ B) (P : B → Type)
|
||||
(df : Π (x : A), P (f x)) (x : A) : equiv_rect f P df (f x) = df x :=
|
||||
|
|
@ -303,6 +341,20 @@ namespace equiv
|
|||
... = ap f (left_inv f x) ▸ df (f⁻¹ (f x)) : by rewrite -adj
|
||||
... = left_inv f x ▸ df (f⁻¹ (f x)) : by rewrite -tr_compose
|
||||
... = df x : by rewrite (apd df (left_inv f x))
|
||||
end
|
||||
|
||||
section
|
||||
variables {A : Type} {B C : A → Type} (f : Π{a}, B a ≃ C a)
|
||||
{g : A → A} (h : Π{a}, B a → B (g a)) (h' : Π{a}, C a → C (g a))
|
||||
|
||||
definition inv_commute (p : Π⦃a : A⦄ (b : B a), f (h b) = h' (f b)) {a : A} (c : C a) :
|
||||
f⁻¹ (h' c) = h (f⁻¹ c) :=
|
||||
inv_commute' @f @h @h' p c
|
||||
|
||||
definition fun_commute_of_inv_commute (p : Π⦃a : A⦄ (c : C a), f⁻¹ (h' c) = h (f⁻¹ c))
|
||||
{a : A} (b : B a) : f (h b) = h' (f b) :=
|
||||
fun_commute_of_inv_commute' @f @h @h' p b
|
||||
end
|
||||
|
||||
|
||||
namespace ops
|
||||
|
|
@ -310,4 +362,13 @@ namespace equiv
|
|||
end ops
|
||||
end equiv
|
||||
|
||||
open equiv equiv.ops
|
||||
namespace is_equiv
|
||||
|
||||
definition is_equiv_of_equiv_of_homotopy [constructor] {A B : Type} (f : A ≃ B)
|
||||
{f' : A → B} (Hty : f ~ f') : is_equiv f' :=
|
||||
homotopy_closed f Hty
|
||||
|
||||
end is_equiv
|
||||
|
||||
export [unfold-hints] equiv [unfold-hints] is_equiv
|
||||
|
|
|
|||
|
|
@ -9,7 +9,7 @@ import init.reserved_notation
|
|||
|
||||
/- not -/
|
||||
|
||||
definition not (a : Type) := a → empty
|
||||
definition not [reducible] (a : Type) := a → empty
|
||||
prefix `¬` := not
|
||||
|
||||
definition absurd {a b : Type} (H₁ : a) (H₂ : ¬a) : b :=
|
||||
|
|
|
|||
|
|
@ -218,6 +218,9 @@ namespace eq
|
|||
(H1 : f ~ g) (H2 : g ~ h) : f ~ h :=
|
||||
λ x, H1 x ⬝ H2 x
|
||||
|
||||
definition homotopy_of_eq {f g : Πx, P x} (H1 : f = g) : f ~ g :=
|
||||
H1 ▸ homotopy.refl f
|
||||
|
||||
definition apd10 [unfold 5] {f g : Πx, P x} (H : f = g) : f ~ g :=
|
||||
λx, eq.rec_on H idp
|
||||
|
||||
|
|
@ -298,6 +301,7 @@ namespace eq
|
|||
eq.rec_on p idp
|
||||
|
||||
-- Naturality of [ap].
|
||||
-- see also natural_square in cubical.square
|
||||
definition ap_con_eq_con_ap {f g : A → B} (p : f ~ g) {x y : A} (q : x = y) :
|
||||
ap f q ⬝ p y = p x ⬝ ap g q :=
|
||||
eq.rec_on q !idp_con
|
||||
|
|
@ -484,7 +488,6 @@ namespace eq
|
|||
ap (transport P p) s ⬝ transport2 P r w = transport2 P r z ⬝ ap (transport P q) s :=
|
||||
eq.rec_on r !idp_con⁻¹
|
||||
|
||||
|
||||
definition fn_tr_eq_tr_fn {P Q : A → Type} {x y : A} (p : x = y) (f : Πx, P x → Q x) (z : P x) :
|
||||
f y (p ▸ z) = (p ▸ (f x z)) :=
|
||||
eq.rec_on p idp
|
||||
|
|
|
|||
|
|
@ -11,10 +11,10 @@ import .path .equiv
|
|||
|
||||
open equiv is_equiv equiv.ops
|
||||
|
||||
variables {A A' : Type} {B B' : A → Type} {C : Πa, B a → Type}
|
||||
variables {A A' : Type} {B B' : A → Type} {C : Π⦃a⦄, B a → Type}
|
||||
{a a₂ a₃ a₄ : A} {p p' : a = a₂} {p₂ : a₂ = a₃} {p₃ : a₃ = a₄}
|
||||
{b b' : B a} {b₂ b₂' : B a₂} {b₃ : B a₃} {b₄ : B a₄}
|
||||
{c : C a b} {c₂ : C a₂ b₂}
|
||||
{c : C b} {c₂ : C b₂}
|
||||
|
||||
namespace eq
|
||||
inductive pathover.{l} (B : A → Type.{l}) (b : B a) : Π{a₂ : A}, a = a₂ → B a₂ → Type.{l} :=
|
||||
|
|
@ -26,10 +26,10 @@ namespace eq
|
|||
pathover.idpatho b
|
||||
|
||||
/- equivalences with equality using transport -/
|
||||
definition pathover_of_tr_eq (r : p ▸ b = b₂) : b =[p] b₂ :=
|
||||
definition pathover_of_tr_eq [unfold 5 8] (r : p ▸ b = b₂) : b =[p] b₂ :=
|
||||
by cases p; cases r; exact idpo
|
||||
|
||||
definition pathover_of_eq_tr (r : b = p⁻¹ ▸ b₂) : b =[p] b₂ :=
|
||||
definition pathover_of_eq_tr [unfold 5 8] (r : b = p⁻¹ ▸ b₂) : b =[p] b₂ :=
|
||||
by cases p; cases r; exact idpo
|
||||
|
||||
definition tr_eq_of_pathover [unfold 8] (r : b =[p] b₂) : p ▸ b = b₂ :=
|
||||
|
|
@ -205,7 +205,17 @@ namespace eq
|
|||
definition tr_pathover_of_eq (q : b₂ = b₂') : p⁻¹ ▸ b₂ =[p] b₂' :=
|
||||
by cases q;apply tr_pathover
|
||||
|
||||
definition apo (f : Πa, B a → B' a) (Ha : a = a₂) (Hb : b =[Ha] b₂)
|
||||
variable (C)
|
||||
definition transporto (r : b =[p] b₂) (c : C b) : C b₂ :=
|
||||
by induction r;exact c
|
||||
infix `▸o`:75 := transporto _
|
||||
|
||||
definition fn_tro_eq_tro_fn (C' : Π ⦃a : A⦄, B a → Type) (q : b =[p] b₂)
|
||||
(f : Π(b : B a), C b → C' b) (c : C b) : f b (q ▸o c) = (q ▸o (f b c)) :=
|
||||
by induction q;reflexivity
|
||||
variable {C}
|
||||
|
||||
definition apo (f : Πa, B a → B' a) {Ha : a = a₂} (Hb : b =[Ha] b₂)
|
||||
: f a b =[Ha] f a₂ b₂ :=
|
||||
by induction Hb; exact idpo
|
||||
|
||||
|
|
@ -213,15 +223,15 @@ namespace eq
|
|||
: f a b = f a₂ b₂ :=
|
||||
by cases Hb; exact idp
|
||||
|
||||
definition apo0111 (f : Πa b, C a b → A') (Ha : a = a₂) (Hb : b =[Ha] b₂)
|
||||
definition apo0111 (f : Πa b, C b → A') (Ha : a = a₂) (Hb : b =[Ha] b₂)
|
||||
(Hc : c =[apo011 C Ha Hb] c₂) : f a b c = f a₂ b₂ c₂ :=
|
||||
by cases Hb; apply (idp_rec_on Hc); apply idp
|
||||
|
||||
definition apo11 {f : Πb, C a b} {g : Πb₂, C a₂ b₂} (r : f =[p] g)
|
||||
definition apo11 {f : Πb, C b} {g : Πb₂, C b₂} (r : f =[p] g)
|
||||
{b : B a} {b₂ : B a₂} (q : b =[p] b₂) : f b =[apo011 C p q] g b₂ :=
|
||||
by cases r; apply (idp_rec_on q); exact idpo
|
||||
|
||||
definition apdo10 {f : Πb, C a b} {g : Πb₂, C a₂ b₂} (r : f =[p] g)
|
||||
definition apdo10 {f : Πb, C b} {g : Πb₂, C b₂} (r : f =[p] g)
|
||||
(b : B a) : f b =[apo011 C p !pathover_tr] g (p ▸ b) :=
|
||||
by cases r; exact idpo
|
||||
|
||||
|
|
|
|||
|
|
@ -143,6 +143,16 @@ namespace is_trunc
|
|||
@is_trunc_succ_intro A m (λx y, IHm n (x = y) (trunc_index.le_of_succ_le_succ Hnm) _)),
|
||||
trunc_index.rec_on m base step n A Hnm Hn
|
||||
|
||||
definition is_trunc_of_imp_is_trunc {n : trunc_index} (H : A → is_trunc (n.+1) A)
|
||||
: is_trunc (n.+1) A :=
|
||||
@is_trunc_succ_intro _ _ (λx y, @is_trunc_eq _ _ (H x) x y)
|
||||
|
||||
definition is_trunc_of_imp_is_trunc_of_leq {n : trunc_index} (Hn : -1 ≤ n) (H : A → is_trunc n A)
|
||||
: is_trunc n A :=
|
||||
trunc_index.rec_on n (λHn H, empty.rec _ Hn)
|
||||
(λn IH Hn, is_trunc_of_imp_is_trunc)
|
||||
Hn H
|
||||
|
||||
-- the following cannot be instances in their current form, because they are looping
|
||||
theorem is_trunc_of_is_contr (A : Type) (n : trunc_index) [H : is_contr A] : is_trunc n A :=
|
||||
trunc_index.rec_on n H _
|
||||
|
|
|
|||
|
|
@ -44,6 +44,9 @@ namespace pi
|
|||
definition arrow_equiv_arrow_left (f0 : A ≃ A') : (A → B) ≃ (A' → B) :=
|
||||
arrow_equiv_arrow f0 equiv.refl
|
||||
|
||||
definition arrow_equiv_arrow_right' (f1 : A → (B ≃ B')) : (A → B) ≃ (A → B') :=
|
||||
pi_equiv_pi_id f1
|
||||
|
||||
/- Transport -/
|
||||
|
||||
definition arrow_transport {B C : A → Type} (p : a = a') (f : B a → C a)
|
||||
|
|
|
|||
|
|
@ -20,14 +20,14 @@ namespace is_equiv
|
|||
(fiber.mk (f⁻¹ b) (right_inv f b))
|
||||
(λz, fiber.rec_on z (λa p,
|
||||
fiber_eq ((ap f⁻¹ p)⁻¹ ⬝ left_inv f a) (calc
|
||||
right_inv f b
|
||||
= (ap (f ∘ f⁻¹) p)⁻¹ ⬝ ((ap (f ∘ f⁻¹) p) ⬝ right_inv f b) : by rewrite inv_con_cancel_left
|
||||
... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ (right_inv f (f a) ⬝ p) : by rewrite ap_con_eq_con
|
||||
... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ (ap f (left_inv f a) ⬝ p) : by rewrite adj
|
||||
... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ ap f (left_inv f a) ⬝ p : by rewrite con.assoc
|
||||
... = (ap f (ap f⁻¹ p))⁻¹ ⬝ ap f (left_inv f a) ⬝ p : by rewrite ap_compose
|
||||
... = ap f (ap f⁻¹ p)⁻¹ ⬝ ap f (left_inv f a) ⬝ p : by rewrite ap_inv
|
||||
... = ap f ((ap f⁻¹ p)⁻¹ ⬝ left_inv f a) ⬝ p : by rewrite ap_con)))
|
||||
right_inv f b = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ ((ap (f ∘ f⁻¹) p) ⬝ right_inv f b)
|
||||
: by rewrite inv_con_cancel_left
|
||||
... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ (right_inv f (f a) ⬝ p) : by rewrite ap_con_eq_con
|
||||
... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ (ap f (left_inv f a) ⬝ p) : by rewrite adj
|
||||
... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ ap f (left_inv f a) ⬝ p : by rewrite con.assoc
|
||||
... = (ap f (ap f⁻¹ p))⁻¹ ⬝ ap f (left_inv f a) ⬝ p : by rewrite ap_compose
|
||||
... = ap f (ap f⁻¹ p)⁻¹ ⬝ ap f (left_inv f a) ⬝ p : by rewrite ap_inv
|
||||
... = ap f ((ap f⁻¹ p)⁻¹ ⬝ left_inv f a) ⬝ p : by rewrite ap_con)))
|
||||
|
||||
definition is_contr_right_inverse : is_contr (Σ(g : B → A), f ∘ g ~ id) :=
|
||||
begin
|
||||
|
|
@ -76,7 +76,8 @@ namespace is_equiv
|
|||
local attribute is_contr_right_coherence [instance] [priority 1600]
|
||||
|
||||
theorem is_hprop_is_equiv [instance] : is_hprop (is_equiv f) :=
|
||||
is_hprop_of_imp_is_contr (λ(H : is_equiv f), is_trunc_equiv_closed -2 (equiv.symm !is_equiv.sigma_char'))
|
||||
is_hprop_of_imp_is_contr
|
||||
(λ(H : is_equiv f), is_trunc_equiv_closed -2 (equiv.symm !is_equiv.sigma_char'))
|
||||
|
||||
definition inv_eq_inv {A B : Type} {f f' : A → B} {Hf : is_equiv f} {Hf' : is_equiv f'}
|
||||
(p : f = f') : f⁻¹ = f'⁻¹ :=
|
||||
|
|
|
|||
|
|
@ -59,8 +59,7 @@ rfl
|
|||
definition eq_zero_or_eq_succ_pred (n : ℕ) : n = 0 ⊎ n = succ (pred n) :=
|
||||
nat.rec_on n
|
||||
(sum.inl rfl)
|
||||
(take m IH, sum.inr
|
||||
(show succ m = succ (pred (succ m)), from ap succ !pred_succ⁻¹))
|
||||
(take m IH, sum.inr rfl)
|
||||
|
||||
definition exists_eq_succ_of_ne_zero {n : ℕ} (H : n ≠ 0) : Σk : ℕ, n = succ k :=
|
||||
sigma.mk _ (sum_resolve_right !eq_zero_or_eq_succ_pred H)
|
||||
|
|
@ -118,11 +117,8 @@ nat.rec_on n
|
|||
|
||||
definition succ_add (n m : ℕ) : (succ n) + m = succ (n + m) :=
|
||||
nat.rec_on m
|
||||
(!add_zero ▸ !add_zero)
|
||||
(take k IH, calc
|
||||
succ n + succ k = succ (succ n + k) : add_succ
|
||||
... = succ (succ (n + k)) : IH
|
||||
... = succ (n + succ k) : add_succ)
|
||||
(rfl)
|
||||
(take k IH, eq.ap succ IH)
|
||||
|
||||
definition add.comm (n m : ℕ) : n + m = m + n :=
|
||||
nat.rec_on m
|
||||
|
|
|
|||
|
|
@ -47,7 +47,8 @@ namespace pi
|
|||
|
||||
definition pi_eq_equiv (f g : Πx, B x) : (f = g) ≃ (f ~ g) := !eq_equiv_homotopy
|
||||
|
||||
definition is_equiv_eq_of_homotopy (f g : Πx, B x) : is_equiv (@eq_of_homotopy _ _ f g) :=
|
||||
definition is_equiv_eq_of_homotopy (f g : Πx, B x)
|
||||
: is_equiv (eq_of_homotopy : f ~ g → f = g) :=
|
||||
_
|
||||
|
||||
definition homotopy_equiv_eq (f g : Πx, B x) : (f ~ g) ≃ (f = g) :=
|
||||
|
|
@ -57,15 +58,14 @@ namespace pi
|
|||
/- Transport -/
|
||||
|
||||
definition pi_transport (p : a = a') (f : Π(b : B a), C a b)
|
||||
: (transport (λa, Π(b : B a), C a b) p f)
|
||||
~ (λb, transport (C a') !tr_inv_tr (transportD _ p _ (f (p⁻¹ ▸ b)))) :=
|
||||
eq.rec_on p (λx, idp)
|
||||
: (transport (λa, Π(b : B a), C a b) p f) ~ (λb, !tr_inv_tr ▸ (p ▸D (f (p⁻¹ ▸ b)))) :=
|
||||
by induction p; reflexivity
|
||||
|
||||
/- A special case of [transport_pi] where the type [B] does not depend on [A],
|
||||
and so it is just a fixed type [B]. -/
|
||||
definition pi_transport_constant {C : A → A' → Type} (p : a = a') (f : Π(b : A'), C a b) (b : A')
|
||||
: (transport _ p f) b = p ▸ (f b) :=
|
||||
eq.rec_on p idp
|
||||
by induction p; reflexivity
|
||||
|
||||
/- Pathovers -/
|
||||
|
||||
|
|
@ -171,7 +171,7 @@ namespace pi
|
|||
/- Equivalences -/
|
||||
|
||||
definition is_equiv_pi_functor [instance] [H0 : is_equiv f0]
|
||||
[H1 : Πa', @is_equiv (B (f0 a')) (B' a') (f1 a')] : is_equiv (pi_functor f0 f1) :=
|
||||
[H1 : Πa', is_equiv (f1 a')] : is_equiv (pi_functor f0 f1) :=
|
||||
begin
|
||||
apply (adjointify (pi_functor f0 f1) (pi_functor f0⁻¹
|
||||
(λ(a : A) (b' : B' (f0⁻¹ a)), transport B (right_inv f0 a) ((f1 (f0⁻¹ a))⁻¹ b')))),
|
||||
|
|
@ -188,7 +188,7 @@ namespace pi
|
|||
end
|
||||
|
||||
definition pi_equiv_pi_of_is_equiv [H : is_equiv f0]
|
||||
[H1 : Πa', @is_equiv (B (f0 a')) (B' a') (f1 a')] : (Πa, B a) ≃ (Πa', B' a') :=
|
||||
[H1 : Πa', is_equiv (f1 a')] : (Πa, B a) ≃ (Πa', B' a') :=
|
||||
equiv.mk (pi_functor f0 f1) _
|
||||
|
||||
definition pi_equiv_pi (f0 : A' ≃ A) (f1 : Πa', (B (to_fun f0 a') ≃ B' a'))
|
||||
|
|
@ -237,8 +237,11 @@ namespace pi
|
|||
assert H : is_contr A, from is_contr.mk a f,
|
||||
_)
|
||||
|
||||
definition is_hprop_neg (A : Type) : is_hprop (¬A) := _
|
||||
|
||||
/- Symmetry of Π -/
|
||||
definition is_equiv_flip [instance] {P : A → A' → Type} : is_equiv (@function.flip A A' P) :=
|
||||
definition is_equiv_flip [instance] {P : A → A' → Type}
|
||||
: is_equiv (@function.flip A A' P) :=
|
||||
begin
|
||||
fapply is_equiv.mk,
|
||||
exact (@function.flip _ _ (function.flip P)),
|
||||
|
|
|
|||
|
|
@ -6,6 +6,8 @@ Author: Floris van Doorn
|
|||
Theorems about sums/coproducts/disjoint unions
|
||||
-/
|
||||
|
||||
import .pi
|
||||
|
||||
open lift eq is_equiv equiv equiv.ops prod prod.ops is_trunc sigma bool
|
||||
|
||||
namespace sum
|
||||
|
|
@ -16,8 +18,8 @@ namespace sum
|
|||
by induction z; all_goals reflexivity
|
||||
|
||||
protected definition code [unfold 3 4] : A + B → A + B → Type.{max u v}
|
||||
| code (inl a) (inl a') := lift.{u v} (a = a')
|
||||
| code (inr b) (inr b') := lift.{v u} (b = b')
|
||||
| code (inl a) (inl a') := lift (a = a')
|
||||
| code (inr b) (inr b') := lift (b = b')
|
||||
| code _ _ := lift empty
|
||||
|
||||
protected definition decode [unfold 3 4] : Π(z z' : A + B), sum.code z z' → z = z'
|
||||
|
|
@ -72,10 +74,10 @@ namespace sum
|
|||
|
||||
protected definition decodeo (p : a = a') : Π(z : P a + Q a) (z' : P a' + Q a'),
|
||||
sum.codeo p z z' → z =[p] z'
|
||||
| decodeo (inl x) (inl x') := λc, apo (λa, inl) p (down c)
|
||||
| decodeo (inl x) (inl x') := λc, apo (λa, inl) (down c)
|
||||
| decodeo (inl x) (inr y') := λc, empty.elim (down c) _
|
||||
| decodeo (inr y) (inl x') := λc, empty.elim (down c) _
|
||||
| decodeo (inr y) (inr y') := λc, apo (λa, inr) p (down c)
|
||||
| decodeo (inr y) (inr y') := λc, apo (λa, inr) (down c)
|
||||
|
||||
variables {z z'}
|
||||
protected definition encodeo {p : a = a'} {z : P a + Q a} {z' : P a' + Q a'} (q : z =[p] z')
|
||||
|
|
@ -157,12 +159,17 @@ namespace sum
|
|||
definition sum_empty_equiv [constructor] (A : Type) : A + empty ≃ A :=
|
||||
begin
|
||||
fapply equiv.MK,
|
||||
intro z, induction z, assumption, contradiction,
|
||||
exact inl,
|
||||
intro a, reflexivity,
|
||||
intro z, induction z, reflexivity, contradiction
|
||||
{ intro z, induction z, assumption, contradiction},
|
||||
{ exact inl},
|
||||
{ intro a, reflexivity},
|
||||
{ intro z, induction z, reflexivity, contradiction}
|
||||
end
|
||||
|
||||
definition empty_sum_equiv (A : Type) : empty + A ≃ A :=
|
||||
!sum_comm_equiv ⬝e !sum_empty_equiv
|
||||
|
||||
/- universal property -/
|
||||
|
||||
definition sum_rec_unc {P : A + B → Type} (fg : (Πa, P (inl a)) × (Πb, P (inr b))) : Πz, P z :=
|
||||
sum.rec fg.1 fg.2
|
||||
|
||||
|
|
@ -182,6 +189,9 @@ namespace sum
|
|||
: (A → C) × (B → C) ≃ (A + B → C) :=
|
||||
!equiv_sum_rec
|
||||
|
||||
/- truncatedness -/
|
||||
|
||||
variables (A B)
|
||||
definition is_trunc_sum (n : trunc_index) [HA : is_trunc (n.+2) A] [HB : is_trunc (n.+2) B]
|
||||
: is_trunc (n.+2) (A + B) :=
|
||||
begin
|
||||
|
|
@ -191,6 +201,23 @@ namespace sum
|
|||
all_goals exact _,
|
||||
end
|
||||
|
||||
definition is_trunc_sum_excluded (n : trunc_index) [HA : is_trunc n A] [HB : is_trunc n B]
|
||||
(H : A → B → empty) : is_trunc n (A + B) :=
|
||||
begin
|
||||
induction n with n IH,
|
||||
{ exfalso, exact H !center !center},
|
||||
{ clear IH, induction n with n IH,
|
||||
{ apply is_hprop.mk, intros x y,
|
||||
induction x, all_goals induction y, all_goals esimp,
|
||||
all_goals try (exfalso;apply H;assumption;assumption), all_goals apply ap _ !is_hprop.elim},
|
||||
{ apply is_trunc_sum}}
|
||||
end
|
||||
|
||||
variable {B}
|
||||
definition is_contr_sum_left [HA : is_contr A] (H : ¬B) : is_contr (A + B) :=
|
||||
is_contr.mk (inl !center)
|
||||
(λx, sum.rec_on x (λa, ap inl !center_eq) (λb, empty.elim (H b)))
|
||||
|
||||
/-
|
||||
Sums are equivalent to dependent sigmas where the first component is a bool.
|
||||
|
||||
|
|
@ -198,7 +225,6 @@ namespace sum
|
|||
If we need it for A and B in different universes, we need to insert some lifts.
|
||||
-/
|
||||
|
||||
|
||||
definition sum_of_sigma_bool {A B : Type.{u}} (v : Σ(b : bool), bool.rec A B b) : A + B :=
|
||||
by induction v with b x; induction b; exact inl x; exact inr x
|
||||
|
||||
|
|
@ -213,3 +239,24 @@ namespace sum
|
|||
begin intro z, induction z with a b, all_goals reflexivity end
|
||||
|
||||
end sum
|
||||
|
||||
namespace decidable
|
||||
open sum pi
|
||||
|
||||
definition decidable_equiv (A : Type) : decidable A ≃ A + ¬A :=
|
||||
begin
|
||||
fapply equiv.MK:intro a;induction a:try (constructor;assumption;now),
|
||||
all_goals reflexivity
|
||||
end
|
||||
|
||||
definition is_trunc_decidable (A : Type) (n : trunc_index) [H : is_trunc n A] :
|
||||
is_trunc n (decidable A) :=
|
||||
begin
|
||||
apply is_trunc_equiv_closed_rev,
|
||||
apply decidable_equiv,
|
||||
induction n with n IH,
|
||||
{ apply is_contr_sum_left, exact λna, na !center},
|
||||
{ apply is_trunc_sum_excluded, exact λa na, na a}
|
||||
end
|
||||
|
||||
end decidable
|
||||
|
|
|
|||
|
|
@ -16,14 +16,6 @@ open eq sigma sigma.ops pi function equiv is_trunc.trunctype
|
|||
namespace is_trunc
|
||||
variables {A B : Type} {n : trunc_index}
|
||||
|
||||
definition is_trunc_succ_of_imp_is_trunc_succ (H : A → is_trunc (n.+1) A) : is_trunc (n.+1) A :=
|
||||
@is_trunc_succ_intro _ _ (λx y, @is_trunc_eq _ _ (H x) x y)
|
||||
|
||||
definition is_trunc_of_imp_is_trunc_of_leq (Hn : -1 ≤ n) (H : A → is_trunc n A) : is_trunc n A :=
|
||||
trunc_index.rec_on n (λHn H, empty.rec _ Hn)
|
||||
(λn IH Hn, is_trunc_succ_of_imp_is_trunc_succ)
|
||||
Hn H
|
||||
|
||||
/- theorems about trunctype -/
|
||||
protected definition trunctype.sigma_char.{l} (n : trunc_index) :
|
||||
(trunctype.{l} n) ≃ (Σ (A : Type.{l}), is_trunc n A) :=
|
||||
|
|
|
|||
|
|
@ -20,7 +20,7 @@
|
|||
"using" "namespace" "section" "fields" "find_decl"
|
||||
"attribute" "local" "set_option" "extends" "include" "omit" "classes"
|
||||
"instances" "coercions" "metaclasses" "raw" "migrate" "replacing"
|
||||
"calc" "have" "show" "suffices" "by" "in" "at" "let" "forall" "fun"
|
||||
"calc" "have" "show" "suffices" "by" "in" "at" "let" "forall" "Pi" "fun"
|
||||
"exists" "if" "dif" "then" "else" "assume" "assert" "take"
|
||||
"obtain" "from")
|
||||
"lean keywords ending with 'word' (not symbol)")
|
||||
|
|
|
|||
Loading…
Reference in a new issue