Library UniMath.CategoryTheory.DisplayedCats.FunctorCategory
Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.UnivalenceAxiom.
Require Import UniMath.MoreFoundations.Propositions.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.categories.HSET.Core.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Monads.Monads.
Require Import UniMath.CategoryTheory.DisplayedCats.Auxiliary.
Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.
Require Import UniMath.CategoryTheory.DisplayedCats.SIP.
Local Open Scope cat.
Local Open Scope mor_disp_scope.
Definition base_precategory_ob_mor (C D:precategory_data)
: precategory_ob_mor
:= precategory_ob_mor_pair (C → D)
(λ F₀ G₀ : C → D, ∏ x : C, D ⟦ F₀ x, G₀ x ⟧).
Definition base_precategory_data (C D:precategory_data) : precategory_data
:= precategory_data_pair
(base_precategory_ob_mor C D)
(λ (F₀ : C → D) (x : C), identity (F₀ x))
(λ (F₀ G₀ H₀ : C → D)
(FG : ∏ x : C, D ⟦ F₀ x, G₀ x ⟧)
(GH : ∏ x : C, D ⟦ G₀ x, H₀ x ⟧)
(x : C),
FG x · GH x).
Section FunctorsDisplayed.
Context (C D:category).
Require Import UniMath.Foundations.UnivalenceAxiom.
Require Import UniMath.MoreFoundations.Propositions.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.categories.HSET.Core.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Monads.Monads.
Require Import UniMath.CategoryTheory.DisplayedCats.Auxiliary.
Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.
Require Import UniMath.CategoryTheory.DisplayedCats.SIP.
Local Open Scope cat.
Local Open Scope mor_disp_scope.
Definition base_precategory_ob_mor (C D:precategory_data)
: precategory_ob_mor
:= precategory_ob_mor_pair (C → D)
(λ F₀ G₀ : C → D, ∏ x : C, D ⟦ F₀ x, G₀ x ⟧).
Definition base_precategory_data (C D:precategory_data) : precategory_data
:= precategory_data_pair
(base_precategory_ob_mor C D)
(λ (F₀ : C → D) (x : C), identity (F₀ x))
(λ (F₀ G₀ H₀ : C → D)
(FG : ∏ x : C, D ⟦ F₀ x, G₀ x ⟧)
(GH : ∏ x : C, D ⟦ G₀ x, H₀ x ⟧)
(x : C),
FG x · GH x).
Section FunctorsDisplayed.
Context (C D:category).
Base category.
- Objects: functions F₀ : C₀ → D₀
- Morphisms: transformations γₓ : D₀ ⟦F₀ x, G₀ x⟧
Lemma is_precategory_base_precategory_data
: is_precategory (base_precategory_data C D).
Show proof.
apply mk_is_precategory.
- intros F₀ G₀. cbn. intros γ.
apply funextsec. intros x.
apply id_left.
- intros F₀ G₀. cbn. intros γ.
apply funextsec. intros x.
apply id_right.
- intros F₀ G₀ H₀ K₀. cbn. intros γ θ μ.
apply funextsec. intros x.
apply assoc.
- intros F₀ G₀ H₀ K₀. cbn. intros γ θ μ.
apply funextsec. intros x.
apply assoc'.
- intros F₀ G₀. cbn. intros γ.
apply funextsec. intros x.
apply id_left.
- intros F₀ G₀. cbn. intros γ.
apply funextsec. intros x.
apply id_right.
- intros F₀ G₀ H₀ K₀. cbn. intros γ θ μ.
apply funextsec. intros x.
apply assoc.
- intros F₀ G₀ H₀ K₀. cbn. intros γ θ μ.
apply funextsec. intros x.
apply assoc'.
Definition base_precategory
: precategory
:= precategory_pair (base_precategory_data C D)
is_precategory_base_precategory_data.
Lemma has_homsets_base_precategory_ob_mor
: has_homsets (base_precategory_ob_mor C D).
Show proof.
intros F₀ G₀. cbn. apply (impred 2). intro. apply D.
Definition base_category
: category
:= category_pair base_precategory
has_homsets_base_precategory_ob_mor.
Step 1
- Objects: actions of functors on maps
- Morphisms: naturality of transformations
The univalence of this displayed category can be expressed as a concrete case of the Structure Identity Principle.
Definition disp_morph : disp_cat_data (base_precategory_data C D).
Show proof.
use tpair.
- exists (λ F₀, ∏ {a b : C}, C ⟦a, b⟧ → D ⟦F₀ a, F₀ b⟧).
cbn. intros F₀ G₀ F₁ G₁ γ.
exact (∏ (a b : C) (f : C ⟦a, b⟧), F₁ _ _ f · γ b = γ a · G₁ _ _ f).
- repeat use tpair; cbn.
+ cbn; intros.
etrans. apply id_right.
apply pathsinv0. apply id_left.
+ cbn. intros ???????? S1 S2 a b f.
etrans. apply assoc.
etrans. apply cancel_postcomposition, S1.
etrans. apply assoc'.
etrans. apply cancel_precomposition, S2.
apply assoc.
- exists (λ F₀, ∏ {a b : C}, C ⟦a, b⟧ → D ⟦F₀ a, F₀ b⟧).
cbn. intros F₀ G₀ F₁ G₁ γ.
exact (∏ (a b : C) (f : C ⟦a, b⟧), F₁ _ _ f · γ b = γ a · G₁ _ _ f).
- repeat use tpair; cbn.
+ cbn; intros.
etrans. apply id_right.
apply pathsinv0. apply id_left.
+ cbn. intros ???????? S1 S2 a b f.
etrans. apply assoc.
etrans. apply cancel_postcomposition, S1.
etrans. apply assoc'.
etrans. apply cancel_precomposition, S2.
apply assoc.
Lemma step1_disp_axioms
: disp_cat_axioms base_category disp_morph.
Show proof.
repeat split; intros; repeat (apply impred; intro);
repeat (apply funextsec; intro); try apply homset_property.
cbn.
repeat (apply (impred 2); intro).
apply hlevelntosn.
apply homset_property.
repeat (apply funextsec; intro); try apply homset_property.
cbn.
repeat (apply (impred 2); intro).
apply hlevelntosn.
apply homset_property.
Definition step1_disp : disp_cat base_category.
Show proof.
exists disp_morph.
exact step1_disp_axioms.
exact step1_disp_axioms.
Lemma step1_disp_univalent : is_univalent_disp step1_disp.
Show proof.
apply is_univalent_disp_from_fibers.
hnf; cbn; intros x f g.
apply isweqimplimpl.
- intro i.
unfold iso_disp in i.
cbn in i.
apply funextsec. intro.
destruct i as (ff, Hff).
apply funextsec. intro.
apply funextsec. intro.
etrans.
{ apply pathsinv0. apply id_right. }
etrans.
{ apply ff. }
apply id_left.
- assert (KK : isaset (∏ a b : C, C ⟦ a, b ⟧ → D ⟦ x a, x b ⟧)).
+ repeat (apply (impred 2); intro).
apply homset_property.
+ apply KK.
- apply isaproptotal2.
+ unfold isPredicate.
intro u.
apply (isaprop_is_iso_disp (D := step1_disp)).
+ cbn.
intros u v Hu Hv.
apply funextsec. intro a.
apply funextsec. intro b.
apply funextsec. intro t.
apply homset_property.
hnf; cbn; intros x f g.
apply isweqimplimpl.
- intro i.
unfold iso_disp in i.
cbn in i.
apply funextsec. intro.
destruct i as (ff, Hff).
apply funextsec. intro.
apply funextsec. intro.
etrans.
{ apply pathsinv0. apply id_right. }
etrans.
{ apply ff. }
apply id_left.
- assert (KK : isaset (∏ a b : C, C ⟦ a, b ⟧ → D ⟦ x a, x b ⟧)).
+ repeat (apply (impred 2); intro).
apply homset_property.
+ apply KK.
- apply isaproptotal2.
+ unfold isPredicate.
intro u.
apply (isaprop_is_iso_disp (D := step1_disp)).
+ cbn.
intros u v Hu Hv.
apply funextsec. intro a.
apply funextsec. intro b.
apply funextsec. intro t.
apply homset_property.
Definition step1_total : category
:= total_category step1_disp.
Definition step2_disp : disp_cat step1_total :=
disp_full_sub step1_total
(λ F : step1_total,
let F₁ := pr2 F in
∏ (x : C), F₁ _ _ (identity x) = identity _).
Definition step3_disp : disp_cat step1_total :=
disp_full_sub step1_total
(λ F : step1_total,
let F₁ := pr2 F in
∏ (a b c: C) (f : C⟦a,b⟧) (g : C⟦b,c⟧),
F₁ _ _ (f · g) = F₁ _ _ f · F₁ _ _ g).
Definition functor_disp_cat : disp_cat step1_total
:= dirprod_disp_cat step2_disp step3_disp.
Definition functor_total_cat : category
:= total_category functor_disp_cat.
This construction is univalent
Lemma functor_disp_cat_univalent :
is_univalent_disp functor_disp_cat.
Show proof.
Definition base_category_iso_to_iso_fam (F₀ G₀ : base_category) :
iso F₀ G₀ → (∏ (x : C), iso (F₀ x) (G₀ x)).
Show proof.
Definition base_category_iso_fam_to_iso (F₀ G₀ : base_category) :
(∏ (x : C), iso (F₀ x) (G₀ x)) → iso F₀ G₀.
Show proof.
Lemma base_category_iso_weq (F₀ G₀ : base_category) :
iso F₀ G₀ ≃ (∏ (x : C), iso (F₀ x) (G₀ x)).
Show proof.
Definition base_category_iso_fam_weq (F₀ G₀ : base_category) :
is_univalent D →
F₀ ~ G₀ ≃ (∏ (x : C), iso (F₀ x) (G₀ x)).
Show proof.
Definition base_category_iso_weq_aux
(F₀ G₀ : base_category) :
is_univalent D →
F₀ = G₀ ≃ iso F₀ G₀.
Show proof.
Lemma base_category_univalent
: is_univalent D → is_univalent base_category.
Show proof.
Lemma functor_total_cat_univalent
: is_univalent D → is_univalent functor_total_cat.
Show proof.
End FunctorsDisplayed.
is_univalent_disp functor_disp_cat.
Show proof.
apply dirprod_disp_cat_is_univalent.
- apply disp_full_sub_univalent.
intros [F₀ F₁]. apply impred. intros x.
cbn[pr2].
apply homset_property.
- apply disp_full_sub_univalent.
intros [F₀ F₁].
repeat (apply impred; intros ?).
cbn[pr2].
apply homset_property.
- apply disp_full_sub_univalent.
intros [F₀ F₁]. apply impred. intros x.
cbn[pr2].
apply homset_property.
- apply disp_full_sub_univalent.
intros [F₀ F₁].
repeat (apply impred; intros ?).
cbn[pr2].
apply homset_property.
Definition base_category_iso_to_iso_fam (F₀ G₀ : base_category) :
iso F₀ G₀ → (∏ (x : C), iso (F₀ x) (G₀ x)).
Show proof.
intros [γ Hγ].
apply is_z_iso_from_is_iso in Hγ.
destruct Hγ as [θ [Hγθ Hθγ]].
intros x. apply z_iso_to_iso.
exists (γ x), (θ x). split.
- apply (toforallpaths _ _ _ Hγθ).
- apply (toforallpaths _ _ _ Hθγ).
apply is_z_iso_from_is_iso in Hγ.
destruct Hγ as [θ [Hγθ Hθγ]].
intros x. apply z_iso_to_iso.
exists (γ x), (θ x). split.
- apply (toforallpaths _ _ _ Hγθ).
- apply (toforallpaths _ _ _ Hθγ).
Definition base_category_iso_fam_to_iso (F₀ G₀ : base_category) :
(∏ (x : C), iso (F₀ x) (G₀ x)) → iso F₀ G₀.
Show proof.
intros γ.
apply z_iso_to_iso.
exists γ, (λ x, inv_from_iso (γ x)).
split.
- apply funextsec. intros x. cbn.
apply iso_inv_after_iso.
- apply funextsec. intros x. cbn.
apply iso_after_iso_inv.
apply z_iso_to_iso.
exists γ, (λ x, inv_from_iso (γ x)).
split.
- apply funextsec. intros x. cbn.
apply iso_inv_after_iso.
- apply funextsec. intros x. cbn.
apply iso_after_iso_inv.
Lemma base_category_iso_weq (F₀ G₀ : base_category) :
iso F₀ G₀ ≃ (∏ (x : C), iso (F₀ x) (G₀ x)).
Show proof.
exists (base_category_iso_to_iso_fam F₀ G₀).
use gradth.
- apply base_category_iso_fam_to_iso.
- intros x. apply eq_iso. reflexivity.
- intros x. apply funextsec. intros y.
apply eq_iso. reflexivity.
use gradth.
- apply base_category_iso_fam_to_iso.
- intros x. apply eq_iso. reflexivity.
- intros x. apply funextsec. intros y.
apply eq_iso. reflexivity.
Definition base_category_iso_fam_weq (F₀ G₀ : base_category) :
is_univalent D →
F₀ ~ G₀ ≃ (∏ (x : C), iso (F₀ x) (G₀ x)).
Show proof.
intros HD.
apply weqonsecfibers. intros x.
exists idtoiso. apply HD.
apply weqonsecfibers. intros x.
exists idtoiso. apply HD.
Definition base_category_iso_weq_aux
(F₀ G₀ : base_category) :
is_univalent D →
F₀ = G₀ ≃ iso F₀ G₀.
Show proof.
intros HD.
eapply weqcomp. apply weqtoforallpaths.
eapply weqcomp. apply base_category_iso_fam_weq, HD.
apply invweq. apply base_category_iso_weq.
eapply weqcomp. apply weqtoforallpaths.
eapply weqcomp. apply base_category_iso_fam_weq, HD.
apply invweq. apply base_category_iso_weq.
Lemma base_category_univalent
: is_univalent D → is_univalent base_category.
Show proof.
intros HD.
unfold is_univalent. split; [ | apply base_category ].
unfold base_category. simpl.
intros F₀ G₀.
use isweqhomot.
- apply base_category_iso_weq_aux, HD.
- intros p. induction p. simpl.
apply eq_iso. reflexivity.
- apply base_category_iso_weq_aux.
unfold is_univalent. split; [ | apply base_category ].
unfold base_category. simpl.
intros F₀ G₀.
use isweqhomot.
- apply base_category_iso_weq_aux, HD.
- intros p. induction p. simpl.
apply eq_iso. reflexivity.
- apply base_category_iso_weq_aux.
Lemma functor_total_cat_univalent
: is_univalent D → is_univalent functor_total_cat.
Show proof.
intros HD.
apply is_univalent_total_category.
- apply is_univalent_total_category.
+ apply base_category_univalent, HD.
+ apply step1_disp_univalent.
- apply functor_disp_cat_univalent.
apply is_univalent_total_category.
- apply is_univalent_total_category.
+ apply base_category_univalent, HD.
+ apply step1_disp_univalent.
- apply functor_disp_cat_univalent.
End FunctorsDisplayed.