Library UniMath.CategoryTheory.CategoryEquality
Equality of precategories
Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.whiskering.
Require Import UniMath.CategoryTheory.catiso.
Local Open Scope cat.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.whiskering.
Require Import UniMath.CategoryTheory.catiso.
Local Open Scope cat.
Step 1
Definition path_precat
(C D : precategory)
(HD : has_homsets D)
: C = D ≃ precategory_data_from_precategory C = D.
Show proof.
(C D : precategory)
(HD : has_homsets D)
: C = D ≃ precategory_data_from_precategory C = D.
Show proof.
Step 2
Definition data_cat_eq_1
(C D : precategory_data)
(Fo : (ob C) = ob D)
: UU
:= transportf (λ z, z → z → UU) Fo (@precategory_morphisms C)
=
@precategory_morphisms D.
Definition cat_eq_1
(C D : precategory_data)
: UU
:= ∑ (F : ∑ (Fo : ob C = ob D), data_cat_eq_1 C D Fo),
(pr1 (transportf (λ x, precategory_id_comp x)
(total2_paths_f (pr1 F) (pr2 F))
(pr2 C))
= pr1 (pr2 D))
×
pr2 (transportf (λ x, precategory_id_comp x)
(total2_paths_f (pr1 F) (pr2 F))
(pr2 C))
=
pr2(pr2 D).
Definition cat_path_to_cat_eq_1
(C D : precategory_data)
: C = D ≃ cat_eq_1 C D.
Show proof.
(C D : precategory_data)
(Fo : (ob C) = ob D)
: UU
:= transportf (λ z, z → z → UU) Fo (@precategory_morphisms C)
=
@precategory_morphisms D.
Definition cat_eq_1
(C D : precategory_data)
: UU
:= ∑ (F : ∑ (Fo : ob C = ob D), data_cat_eq_1 C D Fo),
(pr1 (transportf (λ x, precategory_id_comp x)
(total2_paths_f (pr1 F) (pr2 F))
(pr2 C))
= pr1 (pr2 D))
×
pr2 (transportf (λ x, precategory_id_comp x)
(total2_paths_f (pr1 F) (pr2 F))
(pr2 C))
=
pr2(pr2 D).
Definition cat_path_to_cat_eq_1
(C D : precategory_data)
: C = D ≃ cat_eq_1 C D.
Show proof.
refine (_ ∘ total2_paths_equiv _ _ _)%weq.
use weqbandf.
- apply total2_paths_equiv.
- intro p ; cbn.
induction C as [C HC].
induction D as [D HD].
cbn in *.
induction p ; cbn.
refine (_ ∘ total2_paths_equiv _ _ _)%weq.
use weqfibtototal.
intros p.
cbn.
rewrite transportf_const.
exact (idweq _).
use weqbandf.
- apply total2_paths_equiv.
- intro p ; cbn.
induction C as [C HC].
induction D as [D HD].
cbn in *.
induction p ; cbn.
refine (_ ∘ total2_paths_equiv _ _ _)%weq.
use weqfibtototal.
intros p.
cbn.
rewrite transportf_const.
exact (idweq _).
Step 3
Definition data_cat_eq_2
(C D : precategory_data)
(Fo : (ob C) = ob D)
: UU
:= ∏ (a b : ob C), C⟦a,b⟧ = D⟦eqweqmap Fo a,eqweqmap Fo b⟧.
Definition cat_eq_2
(C D : precategory_data)
: UU
:= ∑ (F : ∑ (Fo : ob C = ob D), data_cat_eq_2 C D Fo),
(∏ (a : C), eqweqmap (pr2 F a a) (identity a) = identity (eqweqmap (pr1 F) a))
×
(∏ (a b c : C) (f : C⟦a,b⟧) (g : C⟦b,c⟧),
eqweqmap (pr2 F a c) (f · g)
=
eqweqmap (pr2 F a b) f · eqweqmap (pr2 F b c) g).
Definition data_cat_eq_1_to_2
(C D : precategory_data)
(Fo : (ob C) = ob D)
: data_cat_eq_1 C D Fo ≃ data_cat_eq_2 C D Fo.
Show proof.
Definition cat_eq_1_to_cat_eq_2
(C D : precategory_data)
(DS : ∏ (x y : D), isaset (precategory_morphisms x y))
: cat_eq_1 C D ≃ cat_eq_2 C D.
Show proof.
(C D : precategory_data)
(Fo : (ob C) = ob D)
: UU
:= ∏ (a b : ob C), C⟦a,b⟧ = D⟦eqweqmap Fo a,eqweqmap Fo b⟧.
Definition cat_eq_2
(C D : precategory_data)
: UU
:= ∑ (F : ∑ (Fo : ob C = ob D), data_cat_eq_2 C D Fo),
(∏ (a : C), eqweqmap (pr2 F a a) (identity a) = identity (eqweqmap (pr1 F) a))
×
(∏ (a b c : C) (f : C⟦a,b⟧) (g : C⟦b,c⟧),
eqweqmap (pr2 F a c) (f · g)
=
eqweqmap (pr2 F a b) f · eqweqmap (pr2 F b c) g).
Definition data_cat_eq_1_to_2
(C D : precategory_data)
(Fo : (ob C) = ob D)
: data_cat_eq_1 C D Fo ≃ data_cat_eq_2 C D Fo.
Show proof.
induction C as [C HC].
induction C as [CO CM].
induction D as [D HD].
induction D as [DO DM].
cbn in *.
induction Fo.
unfold data_cat_eq_1, data_cat_eq_2.
cbn.
refine (_ ∘ weqtoforallpaths _ _ _)%weq.
use weqonsecfibers.
intros x.
exact (weqtoforallpaths _ _ _)%weq.
induction C as [CO CM].
induction D as [D HD].
induction D as [DO DM].
cbn in *.
induction Fo.
unfold data_cat_eq_1, data_cat_eq_2.
cbn.
refine (_ ∘ weqtoforallpaths _ _ _)%weq.
use weqonsecfibers.
intros x.
exact (weqtoforallpaths _ _ _)%weq.
Definition cat_eq_1_to_cat_eq_2
(C D : precategory_data)
(DS : ∏ (x y : D), isaset (precategory_morphisms x y))
: cat_eq_1 C D ≃ cat_eq_2 C D.
Show proof.
use weqbandf.
- use weqfibtototal.
intro p.
exact (data_cat_eq_1_to_2 C D p).
- intros p.
induction C as [C HC].
induction C as [CO CM].
induction HC as [CI CC].
induction D as [D HD].
induction D as [DO DM].
induction HD as [DI DC].
induction p as [p1 p2] ; cbn in *.
unfold data_cat_eq_1 in p2.
induction p1 ; cbn in *.
induction p2 ; cbn.
use weqdirprodf.
+ use weqimplimpl.
* intros f a.
induction f.
reflexivity.
* intros f.
apply funextsec.
intro z.
apply f.
* intro.
apply impred_isaset.
intro.
apply DS.
* apply impred.
intro.
apply DS.
+ use weqimplimpl.
* intros p.
induction p.
reflexivity.
* intros p.
apply funextsec ; intro a.
apply funextsec ; intro b.
apply funextsec ; intro c.
apply funextsec ; intro f.
apply funextsec ; intro g.
specialize (p a b c f g).
induction p.
reflexivity.
* repeat (apply impred_isaset ; intro).
apply DS.
* repeat (apply impred ; intro).
apply DS.
- use weqfibtototal.
intro p.
exact (data_cat_eq_1_to_2 C D p).
- intros p.
induction C as [C HC].
induction C as [CO CM].
induction HC as [CI CC].
induction D as [D HD].
induction D as [DO DM].
induction HD as [DI DC].
induction p as [p1 p2] ; cbn in *.
unfold data_cat_eq_1 in p2.
induction p1 ; cbn in *.
induction p2 ; cbn.
use weqdirprodf.
+ use weqimplimpl.
* intros f a.
induction f.
reflexivity.
* intros f.
apply funextsec.
intro z.
apply f.
* intro.
apply impred_isaset.
intro.
apply DS.
* apply impred.
intro.
apply DS.
+ use weqimplimpl.
* intros p.
induction p.
reflexivity.
* intros p.
apply funextsec ; intro a.
apply funextsec ; intro b.
apply funextsec ; intro c.
apply funextsec ; intro f.
apply funextsec ; intro g.
specialize (p a b c f g).
induction p.
reflexivity.
* repeat (apply impred_isaset ; intro).
apply DS.
* repeat (apply impred ; intro).
apply DS.
Step 4
Definition cat_equiv
(C D : precategory_data)
: UU
:= ∑ (F : ∑ (Fo : ob C ≃ D), ∏ (a b : ob C), C⟦a,b⟧ ≃ D⟦Fo a,Fo b⟧),
(∏ (a : C), (pr2 F) a a (identity a) = identity (pr1 F a))
×
(∏ (a b c : C) (f : C⟦a,b⟧) (g : C⟦b,c⟧), pr2 F a c (f · g) = pr2 F a b f · pr2 F b c g).
Definition weq_cat_eq_cat_equiv
(C D : precategory_data)
: cat_eq_2 C D ≃ cat_equiv C D.
Show proof.
(C D : precategory_data)
: UU
:= ∑ (F : ∑ (Fo : ob C ≃ D), ∏ (a b : ob C), C⟦a,b⟧ ≃ D⟦Fo a,Fo b⟧),
(∏ (a : C), (pr2 F) a a (identity a) = identity (pr1 F a))
×
(∏ (a b c : C) (f : C⟦a,b⟧) (g : C⟦b,c⟧), pr2 F a c (f · g) = pr2 F a b f · pr2 F b c g).
Definition weq_cat_eq_cat_equiv
(C D : precategory_data)
: cat_eq_2 C D ≃ cat_equiv C D.
Show proof.
use weqbandf.
- use weqbandf.
+ apply univalence.
+ intros p.
unfold data_cat_eq_2.
use weqonsecfibers.
intros x.
use weqonsecfibers.
intros y.
apply univalence.
- intros q.
apply idweq.
- use weqbandf.
+ apply univalence.
+ intros p.
unfold data_cat_eq_2.
use weqonsecfibers.
intros x.
use weqonsecfibers.
intros y.
apply univalence.
- intros q.
apply idweq.
Step 5
Definition cat_equiv_to_catiso
(C D : precategory_data)
: cat_equiv C D → catiso C D.
Show proof.
Definition catiso_to_cat_equiv
(C D : precategory_data)
: catiso C D → cat_equiv C D.
Show proof.
Definition cat_equiv_to_catiso_weq
(C D : precategory)
: cat_equiv C D ≃ catiso C D.
Show proof.
(C D : precategory_data)
: cat_equiv C D → catiso C D.
Show proof.
intros F.
use tpair.
- use tpair.
+ use tpair.
* exact (pr1(pr1 F)).
* exact (pr2(pr1 F)).
+ split.
* exact (pr1(pr2 F)).
* exact (pr2(pr2 F)).
- split.
+ intros a b.
apply (pr2(pr1 F)).
+ apply (pr1(pr1 F)).
use tpair.
- use tpair.
+ use tpair.
* exact (pr1(pr1 F)).
* exact (pr2(pr1 F)).
+ split.
* exact (pr1(pr2 F)).
* exact (pr2(pr2 F)).
- split.
+ intros a b.
apply (pr2(pr1 F)).
+ apply (pr1(pr1 F)).
Definition catiso_to_cat_equiv
(C D : precategory_data)
: catiso C D → cat_equiv C D.
Show proof.
intros F.
use tpair.
- use tpair.
+ use make_weq.
* exact (functor_on_objects F).
* apply F.
+ intros a b.
use make_weq.
* exact (functor_on_morphisms F).
* apply F.
- split.
+ exact (functor_id F).
+ exact (@functor_comp _ _ F).
use tpair.
- use tpair.
+ use make_weq.
* exact (functor_on_objects F).
* apply F.
+ intros a b.
use make_weq.
* exact (functor_on_morphisms F).
* apply F.
- split.
+ exact (functor_id F).
+ exact (@functor_comp _ _ F).
Definition cat_equiv_to_catiso_weq
(C D : precategory)
: cat_equiv C D ≃ catiso C D.
Show proof.
refine (cat_equiv_to_catiso C D ,, _).
use isweq_iso.
- exact (catiso_to_cat_equiv C D).
- reflexivity.
- reflexivity.
use isweq_iso.
- exact (catiso_to_cat_equiv C D).
- reflexivity.
- reflexivity.
All in all, we get
Definition catiso_is_path_precat
(C D : precategory)
(HD : has_homsets D)
: C = D ≃ catiso C D
:= ((cat_equiv_to_catiso_weq C D)
∘ weq_cat_eq_cat_equiv C D
∘ cat_eq_1_to_cat_eq_2 C D HD
∘ cat_path_to_cat_eq_1 C D
∘ path_precat C D HD)%weq.
Definition catiso_is_path_cat
(C D : category)
: C = D ≃ catiso C D.
Show proof.
(C D : precategory)
(HD : has_homsets D)
: C = D ≃ catiso C D
:= ((cat_equiv_to_catiso_weq C D)
∘ weq_cat_eq_cat_equiv C D
∘ cat_eq_1_to_cat_eq_2 C D HD
∘ cat_path_to_cat_eq_1 C D
∘ path_precat C D HD)%weq.
Definition catiso_is_path_cat
(C D : category)
: C = D ≃ catiso C D.
Show proof.
refine (catiso_is_path_precat _ _ (homset_property D) ∘ _)%weq.
refine (path_sigma_hprop _ _ _ _).
apply isaprop_has_homsets.
refine (path_sigma_hprop _ _ _ _).
apply isaprop_has_homsets.