Library UniMath.CategoryTheory.IndexedCategories.CartesianToIndexedFunctor
Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Isos.
Require Import UniMath.CategoryTheory.DisplayedCats.Functors.
Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations.
Require Import UniMath.CategoryTheory.DisplayedCats.Fiber.
Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.
Require Import UniMath.CategoryTheory.IndexedCategories.IndexedCategory.
Require Import UniMath.CategoryTheory.IndexedCategories.IndexedFunctor.
Require Import UniMath.CategoryTheory.IndexedCategories.FibrationToIndexedCategory.
Local Open Scope cat.
Section CartesianFunctorToIndexedFunctor.
Context {C : category}
{D₁ D₂ : disp_univalent_category C}
(HD₁ : cleaving D₁)
(HD₂ : cleaving D₂)
(F : cartesian_disp_functor (functor_identity C) D₁ D₂).
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Isos.
Require Import UniMath.CategoryTheory.DisplayedCats.Functors.
Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations.
Require Import UniMath.CategoryTheory.DisplayedCats.Fiber.
Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.
Require Import UniMath.CategoryTheory.IndexedCategories.IndexedCategory.
Require Import UniMath.CategoryTheory.IndexedCategories.IndexedFunctor.
Require Import UniMath.CategoryTheory.IndexedCategories.FibrationToIndexedCategory.
Local Open Scope cat.
Section CartesianFunctorToIndexedFunctor.
Context {C : category}
{D₁ D₂ : disp_univalent_category C}
(HD₁ : cleaving D₁)
(HD₂ : cleaving D₂)
(F : cartesian_disp_functor (functor_identity C) D₁ D₂).
1. The data
Definition cartesian_disp_functor_to_indexed_functor_data
: indexed_functor_data
(cleaving_to_indexed_cat D₁ HD₁)
(cleaving_to_indexed_cat D₂ HD₂).
Show proof.
: indexed_functor_data
(cleaving_to_indexed_cat D₁ HD₁)
(cleaving_to_indexed_cat D₂ HD₂).
Show proof.
use make_indexed_functor_data.
- exact (fiber_functor F).
- exact (λ x y f, fiber_functor_natural_nat_z_iso HD₁ HD₂ F f).
- exact (fiber_functor F).
- exact (λ x y f, fiber_functor_natural_nat_z_iso HD₁ HD₂ F f).
2. The laws
Proposition cartesian_disp_functor_to_indexed_functor_laws
: indexed_functor_laws
cartesian_disp_functor_to_indexed_functor_data.
Show proof.
: indexed_functor_laws
cartesian_disp_functor_to_indexed_functor_data.
Show proof.
split.
- intros x xx ; cbn.
use (cartesian_factorisation_unique
(cartesian_disp_functor_on_cartesian F (HD₁ _ _ _ _))).
rewrite mor_disp_transportf_postwhisker.
rewrite assoc_disp_var.
rewrite transport_f_f.
rewrite cartesian_factorisation_commutes.
rewrite mor_disp_transportf_prewhisker.
rewrite transport_f_f.
rewrite cartesian_factorisation_commutes.
unfold transportb.
rewrite transport_f_f.
refine (!_).
etrans.
{
refine (!_).
apply (disp_functor_comp_var F).
}
rewrite cartesian_factorisation_commutes.
rewrite disp_functor_transportf.
rewrite transport_f_f.
rewrite disp_functor_id.
unfold transportb.
rewrite transport_f_f.
apply maponpaths_2.
apply homset_property.
- intros x y z f g xx ; cbn.
rewrite mor_disp_transportf_postwhisker.
use (cartesian_factorisation_unique
(cartesian_disp_functor_on_cartesian F (HD₁ _ _ _ _))).
rewrite !mor_disp_transportf_postwhisker.
rewrite transport_f_f.
rewrite assoc_disp_var.
rewrite transport_f_f.
rewrite cartesian_factorisation_commutes.
rewrite mor_disp_transportf_prewhisker.
rewrite transport_f_f.
rewrite cartesian_factorisation_commutes.
unfold transportb.
rewrite transport_f_f.
refine (!_).
rewrite assoc_disp_var.
rewrite transport_f_f.
rewrite assoc_disp_var.
rewrite transport_f_f.
etrans.
{
do 3 apply maponpaths.
refine (!_).
apply (disp_functor_comp_var F).
}
rewrite !mor_disp_transportf_prewhisker.
rewrite transport_f_f.
rewrite cartesian_factorisation_commutes.
rewrite disp_functor_transportf.
rewrite !mor_disp_transportf_prewhisker.
rewrite !transport_f_f.
rewrite disp_functor_comp.
unfold transportb.
rewrite !mor_disp_transportf_prewhisker.
rewrite transport_f_f.
etrans.
{
do 2 apply maponpaths.
rewrite assoc_disp.
apply idpath.
}
unfold transportb.
rewrite mor_disp_transportf_prewhisker.
rewrite transport_f_f.
rewrite cartesian_factorisation_commutes.
rewrite mor_disp_transportf_postwhisker.
rewrite mor_disp_transportf_prewhisker.
rewrite transport_f_f.
rewrite assoc_disp.
unfold transportb.
rewrite transport_f_f.
rewrite cartesian_factorisation_commutes.
rewrite mor_disp_transportf_postwhisker.
rewrite transport_f_f.
rewrite assoc_disp_var.
rewrite transport_f_f.
rewrite cartesian_factorisation_commutes.
rewrite mor_disp_transportf_prewhisker.
rewrite transport_f_f.
apply maponpaths_2.
apply homset_property.
- intros x xx ; cbn.
use (cartesian_factorisation_unique
(cartesian_disp_functor_on_cartesian F (HD₁ _ _ _ _))).
rewrite mor_disp_transportf_postwhisker.
rewrite assoc_disp_var.
rewrite transport_f_f.
rewrite cartesian_factorisation_commutes.
rewrite mor_disp_transportf_prewhisker.
rewrite transport_f_f.
rewrite cartesian_factorisation_commutes.
unfold transportb.
rewrite transport_f_f.
refine (!_).
etrans.
{
refine (!_).
apply (disp_functor_comp_var F).
}
rewrite cartesian_factorisation_commutes.
rewrite disp_functor_transportf.
rewrite transport_f_f.
rewrite disp_functor_id.
unfold transportb.
rewrite transport_f_f.
apply maponpaths_2.
apply homset_property.
- intros x y z f g xx ; cbn.
rewrite mor_disp_transportf_postwhisker.
use (cartesian_factorisation_unique
(cartesian_disp_functor_on_cartesian F (HD₁ _ _ _ _))).
rewrite !mor_disp_transportf_postwhisker.
rewrite transport_f_f.
rewrite assoc_disp_var.
rewrite transport_f_f.
rewrite cartesian_factorisation_commutes.
rewrite mor_disp_transportf_prewhisker.
rewrite transport_f_f.
rewrite cartesian_factorisation_commutes.
unfold transportb.
rewrite transport_f_f.
refine (!_).
rewrite assoc_disp_var.
rewrite transport_f_f.
rewrite assoc_disp_var.
rewrite transport_f_f.
etrans.
{
do 3 apply maponpaths.
refine (!_).
apply (disp_functor_comp_var F).
}
rewrite !mor_disp_transportf_prewhisker.
rewrite transport_f_f.
rewrite cartesian_factorisation_commutes.
rewrite disp_functor_transportf.
rewrite !mor_disp_transportf_prewhisker.
rewrite !transport_f_f.
rewrite disp_functor_comp.
unfold transportb.
rewrite !mor_disp_transportf_prewhisker.
rewrite transport_f_f.
etrans.
{
do 2 apply maponpaths.
rewrite assoc_disp.
apply idpath.
}
unfold transportb.
rewrite mor_disp_transportf_prewhisker.
rewrite transport_f_f.
rewrite cartesian_factorisation_commutes.
rewrite mor_disp_transportf_postwhisker.
rewrite mor_disp_transportf_prewhisker.
rewrite transport_f_f.
rewrite assoc_disp.
unfold transportb.
rewrite transport_f_f.
rewrite cartesian_factorisation_commutes.
rewrite mor_disp_transportf_postwhisker.
rewrite transport_f_f.
rewrite assoc_disp_var.
rewrite transport_f_f.
rewrite cartesian_factorisation_commutes.
rewrite mor_disp_transportf_prewhisker.
rewrite transport_f_f.
apply maponpaths_2.
apply homset_property.
3. The indexed functor from a cartesian functor
Definition cartesian_disp_functor_to_indexed_functor
: indexed_functor
(cleaving_to_indexed_cat D₁ HD₁)
(cleaving_to_indexed_cat D₂ HD₂).
Show proof.
: indexed_functor
(cleaving_to_indexed_cat D₁ HD₁)
(cleaving_to_indexed_cat D₂ HD₂).
Show proof.
use make_indexed_functor.
- exact cartesian_disp_functor_to_indexed_functor_data.
- exact cartesian_disp_functor_to_indexed_functor_laws.
End CartesianFunctorToIndexedFunctor.- exact cartesian_disp_functor_to_indexed_functor_data.
- exact cartesian_disp_functor_to_indexed_functor_laws.