Library UniMath.CategoryTheory.Categories.CategoryOfSetCategories
Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Prelude.
Require Import UniMath.CategoryTheory.Core.Setcategories.
Require Import UniMath.CategoryTheory.catiso.
Require Import UniMath.CategoryTheory.CategoryEquality.
Require Import UniMath.CategoryTheory.Equivalences.Core.
Require Import UniMath.CategoryTheory.FunctorCategory.
Local Open Scope cat.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Prelude.
Require Import UniMath.CategoryTheory.Core.Setcategories.
Require Import UniMath.CategoryTheory.catiso.
Require Import UniMath.CategoryTheory.CategoryEquality.
Require Import UniMath.CategoryTheory.Equivalences.Core.
Require Import UniMath.CategoryTheory.FunctorCategory.
Local Open Scope cat.
Definition precat_ob_mor_of_setcategory
: precategory_ob_mor.
Proof.
use make_precategory_ob_mor.
- exact setcategory.
- exact (λ C₁ C₂, C₁ ⟶ C₂).
Defined.
Definition precat_data_of_setcategory
: precategory_data.
Proof.
use make_precategory_data.
- exact precat_ob_mor_of_setcategory.
- exact (λ C, functor_identity _).
- exact (λ C₁ C₂ C₃ F G, F ∙ G).
Defined.
Definition is_precategory_of_setcategory
: is_precategory precat_data_of_setcategory.
Proof.
use make_is_precategory_one_assoc.
- intros C₁ C₂ F.
use functor_eq.
{
apply homset_property.
}
use functor_data_eq ; cbn.
+ intro ; apply idpath.
+ intros x y f ; cbn.
apply idpath.
- intros C₁ C₂ F.
use functor_eq.
{
apply homset_property.
}
use functor_data_eq ; cbn.
+ intro ; apply idpath.
+ intros x y f ; cbn.
apply idpath.
- intros C₁ C₂ C₃ C₄ F G H.
use functor_eq.
{
apply homset_property.
}
use functor_data_eq ; cbn.
+ intro ; apply idpath.
+ intros x y f ; cbn.
apply idpath.
Qed.
Definition precat_of_setcategory
: precategory.
Proof.
use make_precategory.
- exact precat_data_of_setcategory.
- exact is_precategory_of_setcategory.
Defined.
Definition has_homsets_cat_of_setcategory
: has_homsets precat_of_setcategory.
Proof.
intros C₁ C₂.
use functor_isaset.
- apply homset_property.
- apply C₂.
Qed.
Definition cat_of_setcategory
: category.
Proof.
use make_category.
- exact precat_of_setcategory.
- exact has_homsets_cat_of_setcategory.
Defined.
: precategory_ob_mor.
Proof.
use make_precategory_ob_mor.
- exact setcategory.
- exact (λ C₁ C₂, C₁ ⟶ C₂).
Defined.
Definition precat_data_of_setcategory
: precategory_data.
Proof.
use make_precategory_data.
- exact precat_ob_mor_of_setcategory.
- exact (λ C, functor_identity _).
- exact (λ C₁ C₂ C₃ F G, F ∙ G).
Defined.
Definition is_precategory_of_setcategory
: is_precategory precat_data_of_setcategory.
Proof.
use make_is_precategory_one_assoc.
- intros C₁ C₂ F.
use functor_eq.
{
apply homset_property.
}
use functor_data_eq ; cbn.
+ intro ; apply idpath.
+ intros x y f ; cbn.
apply idpath.
- intros C₁ C₂ F.
use functor_eq.
{
apply homset_property.
}
use functor_data_eq ; cbn.
+ intro ; apply idpath.
+ intros x y f ; cbn.
apply idpath.
- intros C₁ C₂ C₃ C₄ F G H.
use functor_eq.
{
apply homset_property.
}
use functor_data_eq ; cbn.
+ intro ; apply idpath.
+ intros x y f ; cbn.
apply idpath.
Qed.
Definition precat_of_setcategory
: precategory.
Proof.
use make_precategory.
- exact precat_data_of_setcategory.
- exact is_precategory_of_setcategory.
Defined.
Definition has_homsets_cat_of_setcategory
: has_homsets precat_of_setcategory.
Proof.
intros C₁ C₂.
use functor_isaset.
- apply homset_property.
- apply C₂.
Qed.
Definition cat_of_setcategory
: category.
Proof.
use make_category.
- exact precat_of_setcategory.
- exact has_homsets_cat_of_setcategory.
Defined.
Section CatIsoWeqIso.
Context {C D : setcategory}
(F : C ⟶ D).
Section ToIso.
Context (HF : is_catiso F).
Let F_iso : catiso C D := F ,, HF.
Definition is_cat_iso_to_is_z_isomorphism_inv_data
: functor_data D C.
Proof.
use make_functor_data.
- exact (catiso_inv_ob F_iso).
- exact (λ x y f, catiso_inv_mor F_iso f).
Defined.
Proposition is_cat_iso_to_is_z_isomorphism_inv_laws
: is_functor is_cat_iso_to_is_z_isomorphism_inv_data.
Proof.
split.
- intro x ; cbn -[catiso_inv_mor].
use catiso_inv_mor_eq ; cbn -[catiso_inv_mor].
rewrite functor_id.
rewrite id_right.
refine (!_).
etrans.
{
refine (!_).
apply (pr1_idtoiso_concat
(!(catiso_catiso_inv_ob F_iso x))).
}
rewrite pathsinv0l.
apply idpath.
- intros x y z f g ; cbn -[catiso_inv_mor].
use catiso_inv_mor_eq ; cbn -[catiso_inv_mor].
rewrite functor_comp.
rewrite !(catiso_catiso_inv_mor F_iso).
refine (!_).
etrans.
{
rewrite !assoc.
etrans.
{
do 6 apply maponpaths_2.
refine (!_).
apply (pr1_idtoiso_concat
(!(catiso_catiso_inv_ob F_iso x))).
}
rewrite pathsinv0l.
cbn.
rewrite id_left.
rewrite !assoc'.
apply maponpaths.
rewrite !assoc.
etrans.
{
do 3 apply maponpaths_2.
refine (!_).
apply (pr1_idtoiso_concat
(!(catiso_catiso_inv_ob F_iso y))).
}
rewrite pathsinv0l.
cbn.
rewrite id_left.
rewrite !assoc'.
apply maponpaths.
etrans.
{
refine (!_).
apply (pr1_idtoiso_concat
(!(catiso_catiso_inv_ob F_iso z))).
}
rewrite pathsinv0l.
apply idpath.
}
cbn.
rewrite id_right.
apply idpath.
Qed.
Definition is_cat_iso_to_is_z_isomorphism_inv
: D ⟶ C.
Proof.
use make_functor.
- exact is_cat_iso_to_is_z_isomorphism_inv_data.
- exact is_cat_iso_to_is_z_isomorphism_inv_laws.
Defined.
Proposition is_cat_iso_to_is_z_isomorphism_laws
: @is_inverse_in_precat cat_of_setcategory
C D
F
is_cat_iso_to_is_z_isomorphism_inv.
Proof.
split.
- use functor_eq ; [ apply homset_property | ].
use functor_data_eq_alt.
+ intros x ; cbn.
apply homotinvweqweq.
+ intros x y f ; cbn -[catiso_inv_mor].
rewrite (catiso_inv_mor_cat_iso F_iso).
rewrite !assoc'.
apply maponpaths.
refine (_ @ id_right _).
apply maponpaths.
etrans.
{
refine (!_).
apply (pr1_idtoiso_concat
(!(catiso_inv_ob_catiso F_iso y))).
}
rewrite pathsinv0l.
apply idpath.
- use functor_eq ; [ apply homset_property | ].
use functor_data_eq_alt.
+ intros x ; cbn.
exact (homotweqinvweq (catiso_ob_weq F_iso) x).
+ intros x y f ; cbn -[catiso_inv_mor].
rewrite (catiso_catiso_inv_mor F_iso).
rewrite !assoc'.
apply maponpaths.
refine (_ @ id_right _).
apply maponpaths.
etrans.
{
refine (!_).
apply (pr1_idtoiso_concat
(!(catiso_catiso_inv_ob F_iso y))).
}
rewrite pathsinv0l.
apply idpath.
Qed.
Definition is_cat_iso_to_is_z_isomorphism
: @is_z_isomorphism cat_of_setcategory C D F.
Proof.
use make_is_z_isomorphism.
- exact is_cat_iso_to_is_z_isomorphism_inv.
- exact is_cat_iso_to_is_z_isomorphism_laws.
Defined.
End ToIso.
Section FromIso.
Context (HF : @is_z_isomorphism cat_of_setcategory C D F).
Let F_iso : @z_iso cat_of_setcategory C D := F ,, HF.
Let G : D ⟶ C := inv_from_z_iso F_iso.
Lemma is_z_isomorphism_to_is_cat_iso_eq_l
(x : C)
: G(F x) = x.
Proof.
exact (path_functor_ob (z_iso_inv_after_z_iso F_iso) x).
Defined.
Lemma is_z_isomorphism_to_is_cat_iso_eq_r
(y : D)
: F(G y) = y.
Proof.
exact (path_functor_ob (z_iso_after_z_iso_inv F_iso) y).
Defined.
Definition is_z_isomorphism_to_is_cat_iso
: is_catiso F.
Proof.
split.
- intros x y.
use isweq_iso.
+ exact (λ f,
idtoiso (!(is_z_isomorphism_to_is_cat_iso_eq_l _))
· #G f
· idtoiso (is_z_isomorphism_to_is_cat_iso_eq_l _)).
+ intro f.
cbn.
rewrite !assoc'.
unfold is_z_isomorphism_to_is_cat_iso_eq_l.
etrans.
{
apply maponpaths.
exact (path_functor_mor (z_iso_inv_after_z_iso F_iso) f).
}
cbn.
rewrite !assoc.
etrans.
{
apply maponpaths_2.
exact (!(pr1_idtoiso_concat
(!(path_functor_ob (z_iso_inv_after_z_iso F_iso) x))
(path_functor_ob (z_iso_inv_after_z_iso F_iso) x))).
}
rewrite pathsinv0l.
apply id_left.
+ intro f.
refine (_ @ path_functor_mor_left (z_iso_after_z_iso_inv F_iso) f).
cbn.
rewrite !functor_comp.
etrans.
{
apply maponpaths.
refine (!_).
apply (pr1_maponpaths_idtoiso F).
}
etrans.
{
do 2 apply maponpaths_2.
refine (!_).
apply (pr1_maponpaths_idtoiso F).
}
use setcategory_eq_idtoiso_comp.
- use isweq_iso.
+ exact (λ y, G y).
+ exact is_z_isomorphism_to_is_cat_iso_eq_l.
+ exact is_z_isomorphism_to_is_cat_iso_eq_r.
Qed.
End FromIso.
End CatIsoWeqIso.
Definition is_catiso_weq_is_z_isomorphism
{C D : setcategory}
(F : C ⟶ D)
: is_catiso F ≃ @is_z_isomorphism cat_of_setcategory C D F.
Proof.
use weqimplimpl.
- exact (is_cat_iso_to_is_z_isomorphism F).
- exact (is_z_isomorphism_to_is_cat_iso F).
- apply isaprop_is_catiso.
- apply isaprop_is_z_isomorphism.
Defined.
Context {C D : setcategory}
(F : C ⟶ D).
Section ToIso.
Context (HF : is_catiso F).
Let F_iso : catiso C D := F ,, HF.
Definition is_cat_iso_to_is_z_isomorphism_inv_data
: functor_data D C.
Proof.
use make_functor_data.
- exact (catiso_inv_ob F_iso).
- exact (λ x y f, catiso_inv_mor F_iso f).
Defined.
Proposition is_cat_iso_to_is_z_isomorphism_inv_laws
: is_functor is_cat_iso_to_is_z_isomorphism_inv_data.
Proof.
split.
- intro x ; cbn -[catiso_inv_mor].
use catiso_inv_mor_eq ; cbn -[catiso_inv_mor].
rewrite functor_id.
rewrite id_right.
refine (!_).
etrans.
{
refine (!_).
apply (pr1_idtoiso_concat
(!(catiso_catiso_inv_ob F_iso x))).
}
rewrite pathsinv0l.
apply idpath.
- intros x y z f g ; cbn -[catiso_inv_mor].
use catiso_inv_mor_eq ; cbn -[catiso_inv_mor].
rewrite functor_comp.
rewrite !(catiso_catiso_inv_mor F_iso).
refine (!_).
etrans.
{
rewrite !assoc.
etrans.
{
do 6 apply maponpaths_2.
refine (!_).
apply (pr1_idtoiso_concat
(!(catiso_catiso_inv_ob F_iso x))).
}
rewrite pathsinv0l.
cbn.
rewrite id_left.
rewrite !assoc'.
apply maponpaths.
rewrite !assoc.
etrans.
{
do 3 apply maponpaths_2.
refine (!_).
apply (pr1_idtoiso_concat
(!(catiso_catiso_inv_ob F_iso y))).
}
rewrite pathsinv0l.
cbn.
rewrite id_left.
rewrite !assoc'.
apply maponpaths.
etrans.
{
refine (!_).
apply (pr1_idtoiso_concat
(!(catiso_catiso_inv_ob F_iso z))).
}
rewrite pathsinv0l.
apply idpath.
}
cbn.
rewrite id_right.
apply idpath.
Qed.
Definition is_cat_iso_to_is_z_isomorphism_inv
: D ⟶ C.
Proof.
use make_functor.
- exact is_cat_iso_to_is_z_isomorphism_inv_data.
- exact is_cat_iso_to_is_z_isomorphism_inv_laws.
Defined.
Proposition is_cat_iso_to_is_z_isomorphism_laws
: @is_inverse_in_precat cat_of_setcategory
C D
F
is_cat_iso_to_is_z_isomorphism_inv.
Proof.
split.
- use functor_eq ; [ apply homset_property | ].
use functor_data_eq_alt.
+ intros x ; cbn.
apply homotinvweqweq.
+ intros x y f ; cbn -[catiso_inv_mor].
rewrite (catiso_inv_mor_cat_iso F_iso).
rewrite !assoc'.
apply maponpaths.
refine (_ @ id_right _).
apply maponpaths.
etrans.
{
refine (!_).
apply (pr1_idtoiso_concat
(!(catiso_inv_ob_catiso F_iso y))).
}
rewrite pathsinv0l.
apply idpath.
- use functor_eq ; [ apply homset_property | ].
use functor_data_eq_alt.
+ intros x ; cbn.
exact (homotweqinvweq (catiso_ob_weq F_iso) x).
+ intros x y f ; cbn -[catiso_inv_mor].
rewrite (catiso_catiso_inv_mor F_iso).
rewrite !assoc'.
apply maponpaths.
refine (_ @ id_right _).
apply maponpaths.
etrans.
{
refine (!_).
apply (pr1_idtoiso_concat
(!(catiso_catiso_inv_ob F_iso y))).
}
rewrite pathsinv0l.
apply idpath.
Qed.
Definition is_cat_iso_to_is_z_isomorphism
: @is_z_isomorphism cat_of_setcategory C D F.
Proof.
use make_is_z_isomorphism.
- exact is_cat_iso_to_is_z_isomorphism_inv.
- exact is_cat_iso_to_is_z_isomorphism_laws.
Defined.
End ToIso.
Section FromIso.
Context (HF : @is_z_isomorphism cat_of_setcategory C D F).
Let F_iso : @z_iso cat_of_setcategory C D := F ,, HF.
Let G : D ⟶ C := inv_from_z_iso F_iso.
Lemma is_z_isomorphism_to_is_cat_iso_eq_l
(x : C)
: G(F x) = x.
Proof.
exact (path_functor_ob (z_iso_inv_after_z_iso F_iso) x).
Defined.
Lemma is_z_isomorphism_to_is_cat_iso_eq_r
(y : D)
: F(G y) = y.
Proof.
exact (path_functor_ob (z_iso_after_z_iso_inv F_iso) y).
Defined.
Definition is_z_isomorphism_to_is_cat_iso
: is_catiso F.
Proof.
split.
- intros x y.
use isweq_iso.
+ exact (λ f,
idtoiso (!(is_z_isomorphism_to_is_cat_iso_eq_l _))
· #G f
· idtoiso (is_z_isomorphism_to_is_cat_iso_eq_l _)).
+ intro f.
cbn.
rewrite !assoc'.
unfold is_z_isomorphism_to_is_cat_iso_eq_l.
etrans.
{
apply maponpaths.
exact (path_functor_mor (z_iso_inv_after_z_iso F_iso) f).
}
cbn.
rewrite !assoc.
etrans.
{
apply maponpaths_2.
exact (!(pr1_idtoiso_concat
(!(path_functor_ob (z_iso_inv_after_z_iso F_iso) x))
(path_functor_ob (z_iso_inv_after_z_iso F_iso) x))).
}
rewrite pathsinv0l.
apply id_left.
+ intro f.
refine (_ @ path_functor_mor_left (z_iso_after_z_iso_inv F_iso) f).
cbn.
rewrite !functor_comp.
etrans.
{
apply maponpaths.
refine (!_).
apply (pr1_maponpaths_idtoiso F).
}
etrans.
{
do 2 apply maponpaths_2.
refine (!_).
apply (pr1_maponpaths_idtoiso F).
}
use setcategory_eq_idtoiso_comp.
- use isweq_iso.
+ exact (λ y, G y).
+ exact is_z_isomorphism_to_is_cat_iso_eq_l.
+ exact is_z_isomorphism_to_is_cat_iso_eq_r.
Qed.
End FromIso.
End CatIsoWeqIso.
Definition is_catiso_weq_is_z_isomorphism
{C D : setcategory}
(F : C ⟶ D)
: is_catiso F ≃ @is_z_isomorphism cat_of_setcategory C D F.
Proof.
use weqimplimpl.
- exact (is_cat_iso_to_is_z_isomorphism F).
- exact (is_z_isomorphism_to_is_cat_iso F).
- apply isaprop_is_catiso.
- apply isaprop_is_z_isomorphism.
Defined.
Definition path_setcategory_help_fun
{C D : setcategory}
(p : C = D)
: category_from_setcategory C = category_from_setcategory D.
Proof.
induction p.
apply idpath.
Defined.
Definition path_setcategory_help_fun_alt
{C D : setcategory}
(p : C = D)
: category_from_setcategory C = category_from_setcategory D.
Proof.
use total2_paths_f.
- exact (base_paths _ _ p).
- apply isaprop_has_homsets.
Defined.
Proposition path_setcategory_help_fun_eq
{C D : setcategory}
(p : C = D)
: path_setcategory_help_fun p = path_setcategory_help_fun_alt p.
Proof.
induction p.
refine (!_).
refine (_ @ total2_fiber_paths _).
unfold path_setcategory_help_fun_alt.
apply maponpaths.
apply isasetaprop.
apply isaprop_has_homsets.
Qed.
Definition path_setcategory
(C D : setcategory)
: C = D
≃
category_from_setcategory C = category_from_setcategory D.
Proof.
use weq_iso.
- exact path_setcategory_help_fun.
- intro p.
use total2_paths_f.
+ exact (base_paths _ _ p).
+ apply isaprop_is_setcategory.
- abstract
(intro p ;
induction p ;
rewrite path_setcategory_help_fun_eq ;
unfold path_setcategory_help_fun_alt ;
rewrite base_total2_paths ;
refine (_ @ total2_fiber_paths _) ;
apply maponpaths ;
apply isasetaprop ;
apply isaprop_is_setcategory).
- abstract
(intro p ;
induction C as [ C HC ] ;
induction D as [ D HD ] ;
rewrite path_setcategory_help_fun_eq ;
unfold path_setcategory_help_fun_alt ;
rewrite base_total2_paths ;
refine (_ @ total2_fiber_paths _) ;
apply maponpaths ;
apply isasetaprop ;
apply isaprop_has_homsets).
Defined.
Proposition is_univalent_cat_of_setcategory
: is_univalent cat_of_setcategory.
Proof.
intros C D.
use weqhomot.
- exact (weqfibtototal _ _ is_catiso_weq_is_z_isomorphism
∘ catiso_is_path_cat _ _
∘ path_setcategory _ _)%weq.
- intro p.
induction p.
use z_iso_eq.
use subtypePath.
{
intro.
apply isaprop_is_functor.
apply homset_property.
}
apply idpath.
Qed.
Definition univalent_cat_of_setcategory
: univalent_category.
Proof.
use make_univalent_category.
- exact cat_of_setcategory.
- exact is_univalent_cat_of_setcategory.
Defined.
Section IsoToEquivalence.
Context {A B : setcategory}.
Context (f : z_iso (C := cat_of_setcategory) A B).
Let F : A ⟶ B
:= z_iso_mor f.
Let G : B ⟶ A
:= inv_from_z_iso f.
Let η : functor_identity A ⟹ F ∙ G
:= z_iso_mor (idtoiso (C := [A, A]) (!z_iso_inv_after_z_iso f)).
Let ϵ : G ∙ F ⟹ functor_identity B
:= z_iso_mor (idtoiso (C := [B, B]) (z_iso_after_z_iso_inv f)).
Lemma FG_form_adjunction
: Core.form_adjunction F G η ϵ.
Proof.
split.
- intro c.
refine (maponpaths (λ x, # F (z_iso_mor x) · _) (idtoiso_functorcat_compute_pointwise _ _ _ _ _ (!z_iso_inv_after_z_iso f) _) @ _).
refine (!maponpaths (λ x, z_iso_mor x · _) (maponpaths_idtoiso _ _ _ _ _ _) @ _).
refine (maponpaths (λ x, _ · z_iso_mor x) (idtoiso_functorcat_compute_pointwise _ _ _ _ _ (z_iso_after_z_iso_inv f) _) @ _).
refine (!maponpaths z_iso_mor (idtoiso_concat _ _ _ _ _ _) @ _).
apply setcategory_refl_idtoiso.
- intro c.
refine (maponpaths (λ x, _ · #G (z_iso_mor x)) (idtoiso_functorcat_compute_pointwise _ _ _ _ _ (z_iso_after_z_iso_inv f) _) @ _).
refine (!maponpaths (λ x, _ · z_iso_mor x) (maponpaths_idtoiso _ _ _ _ _ _) @ _).
refine (maponpaths (λ x, z_iso_mor x · _) (idtoiso_functorcat_compute_pointwise _ _ _ _ _ (!z_iso_inv_after_z_iso f) _) @ _).
refine (!maponpaths z_iso_mor (idtoiso_concat _ _ _ _ _ _) @ _).
apply setcategory_refl_idtoiso.
Qed.
Lemma FG_forms_equivalence
: forms_equivalence (F ,, G ,, η ,, ϵ).
Proof.
split;
intro;
apply (is_functor_z_iso_pointwise_if_z_iso _ _ _ _ _ _ (z_iso_is_z_isomorphism _)).
Defined.
Definition z_iso_to_equivalence
: adj_equivalence_of_cats F
:= make_adj_equivalence_of_cats _ _ _ _
FG_form_adjunction
FG_forms_equivalence.
End IsoToEquivalence.
{C D : setcategory}
(p : C = D)
: category_from_setcategory C = category_from_setcategory D.
Proof.
induction p.
apply idpath.
Defined.
Definition path_setcategory_help_fun_alt
{C D : setcategory}
(p : C = D)
: category_from_setcategory C = category_from_setcategory D.
Proof.
use total2_paths_f.
- exact (base_paths _ _ p).
- apply isaprop_has_homsets.
Defined.
Proposition path_setcategory_help_fun_eq
{C D : setcategory}
(p : C = D)
: path_setcategory_help_fun p = path_setcategory_help_fun_alt p.
Proof.
induction p.
refine (!_).
refine (_ @ total2_fiber_paths _).
unfold path_setcategory_help_fun_alt.
apply maponpaths.
apply isasetaprop.
apply isaprop_has_homsets.
Qed.
Definition path_setcategory
(C D : setcategory)
: C = D
≃
category_from_setcategory C = category_from_setcategory D.
Proof.
use weq_iso.
- exact path_setcategory_help_fun.
- intro p.
use total2_paths_f.
+ exact (base_paths _ _ p).
+ apply isaprop_is_setcategory.
- abstract
(intro p ;
induction p ;
rewrite path_setcategory_help_fun_eq ;
unfold path_setcategory_help_fun_alt ;
rewrite base_total2_paths ;
refine (_ @ total2_fiber_paths _) ;
apply maponpaths ;
apply isasetaprop ;
apply isaprop_is_setcategory).
- abstract
(intro p ;
induction C as [ C HC ] ;
induction D as [ D HD ] ;
rewrite path_setcategory_help_fun_eq ;
unfold path_setcategory_help_fun_alt ;
rewrite base_total2_paths ;
refine (_ @ total2_fiber_paths _) ;
apply maponpaths ;
apply isasetaprop ;
apply isaprop_has_homsets).
Defined.
Proposition is_univalent_cat_of_setcategory
: is_univalent cat_of_setcategory.
Proof.
intros C D.
use weqhomot.
- exact (weqfibtototal _ _ is_catiso_weq_is_z_isomorphism
∘ catiso_is_path_cat _ _
∘ path_setcategory _ _)%weq.
- intro p.
induction p.
use z_iso_eq.
use subtypePath.
{
intro.
apply isaprop_is_functor.
apply homset_property.
}
apply idpath.
Qed.
Definition univalent_cat_of_setcategory
: univalent_category.
Proof.
use make_univalent_category.
- exact cat_of_setcategory.
- exact is_univalent_cat_of_setcategory.
Defined.
Section IsoToEquivalence.
Context {A B : setcategory}.
Context (f : z_iso (C := cat_of_setcategory) A B).
Let F : A ⟶ B
:= z_iso_mor f.
Let G : B ⟶ A
:= inv_from_z_iso f.
Let η : functor_identity A ⟹ F ∙ G
:= z_iso_mor (idtoiso (C := [A, A]) (!z_iso_inv_after_z_iso f)).
Let ϵ : G ∙ F ⟹ functor_identity B
:= z_iso_mor (idtoiso (C := [B, B]) (z_iso_after_z_iso_inv f)).
Lemma FG_form_adjunction
: Core.form_adjunction F G η ϵ.
Proof.
split.
- intro c.
refine (maponpaths (λ x, # F (z_iso_mor x) · _) (idtoiso_functorcat_compute_pointwise _ _ _ _ _ (!z_iso_inv_after_z_iso f) _) @ _).
refine (!maponpaths (λ x, z_iso_mor x · _) (maponpaths_idtoiso _ _ _ _ _ _) @ _).
refine (maponpaths (λ x, _ · z_iso_mor x) (idtoiso_functorcat_compute_pointwise _ _ _ _ _ (z_iso_after_z_iso_inv f) _) @ _).
refine (!maponpaths z_iso_mor (idtoiso_concat _ _ _ _ _ _) @ _).
apply setcategory_refl_idtoiso.
- intro c.
refine (maponpaths (λ x, _ · #G (z_iso_mor x)) (idtoiso_functorcat_compute_pointwise _ _ _ _ _ (z_iso_after_z_iso_inv f) _) @ _).
refine (!maponpaths (λ x, _ · z_iso_mor x) (maponpaths_idtoiso _ _ _ _ _ _) @ _).
refine (maponpaths (λ x, z_iso_mor x · _) (idtoiso_functorcat_compute_pointwise _ _ _ _ _ (!z_iso_inv_after_z_iso f) _) @ _).
refine (!maponpaths z_iso_mor (idtoiso_concat _ _ _ _ _ _) @ _).
apply setcategory_refl_idtoiso.
Qed.
Lemma FG_forms_equivalence
: forms_equivalence (F ,, G ,, η ,, ϵ).
Proof.
split;
intro;
apply (is_functor_z_iso_pointwise_if_z_iso _ _ _ _ _ _ (z_iso_is_z_isomorphism _)).
Defined.
Definition z_iso_to_equivalence
: adj_equivalence_of_cats F
:= make_adj_equivalence_of_cats _ _ _ _
FG_form_adjunction
FG_forms_equivalence.
End IsoToEquivalence.