Library UniMath.CategoryTheory.Presheaves.Constructions
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Prelude.
Require Import UniMath.CategoryTheory.Monics.
Require Import UniMath.CategoryTheory.Adjunctions.Coreflections.
Require Import UniMath.CategoryTheory.Adjunctions.Core.
Require Import UniMath.CategoryTheory.Presheaf.
Require Import UniMath.CategoryTheory.Limits.Terminal.
Require Import UniMath.CategoryTheory.Limits.BinProducts.
Require Import UniMath.CategoryTheory.Limits.Equalizers.
Require Import UniMath.CategoryTheory.Limits.Initial.
Require Import UniMath.CategoryTheory.Limits.BinCoproducts.
Require Import UniMath.CategoryTheory.Limits.DisjointBinCoproducts.
Require Import UniMath.CategoryTheory.Limits.Pullbacks.
Require Import UniMath.CategoryTheory.Limits.Preservation.
Require Import UniMath.CategoryTheory.opp_precat.
Require Import UniMath.CategoryTheory.Categories.HSET.All.
Require Import UniMath.CategoryTheory.FunctorCategory.
Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Fiber.
Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations.
Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseInitial.
Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseTerminal.
Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseCoproducts.
Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseProducts.
Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseEqualizers.
Require Import UniMath.CategoryTheory.Presheaves.DependentPresheaf.
Require Import UniMath.CategoryTheory.Presheaves.TotalPresheaf.
Require Import UniMath.CategoryTheory.Presheaves.DisplayedCatOfDependentPresheaf.
Local Open Scope cat.
Section ExamplesDepPsh.
Context {C : category}.
Require Import UniMath.CategoryTheory.Core.Prelude.
Require Import UniMath.CategoryTheory.Monics.
Require Import UniMath.CategoryTheory.Adjunctions.Coreflections.
Require Import UniMath.CategoryTheory.Adjunctions.Core.
Require Import UniMath.CategoryTheory.Presheaf.
Require Import UniMath.CategoryTheory.Limits.Terminal.
Require Import UniMath.CategoryTheory.Limits.BinProducts.
Require Import UniMath.CategoryTheory.Limits.Equalizers.
Require Import UniMath.CategoryTheory.Limits.Initial.
Require Import UniMath.CategoryTheory.Limits.BinCoproducts.
Require Import UniMath.CategoryTheory.Limits.DisjointBinCoproducts.
Require Import UniMath.CategoryTheory.Limits.Pullbacks.
Require Import UniMath.CategoryTheory.Limits.Preservation.
Require Import UniMath.CategoryTheory.opp_precat.
Require Import UniMath.CategoryTheory.Categories.HSET.All.
Require Import UniMath.CategoryTheory.FunctorCategory.
Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Fiber.
Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations.
Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseInitial.
Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseTerminal.
Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseCoproducts.
Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseProducts.
Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseEqualizers.
Require Import UniMath.CategoryTheory.Presheaves.DependentPresheaf.
Require Import UniMath.CategoryTheory.Presheaves.TotalPresheaf.
Require Import UniMath.CategoryTheory.Presheaves.DisplayedCatOfDependentPresheaf.
Local Open Scope cat.
Section ExamplesDepPsh.
Context {C : category}.
Definition empty_dep_psh
(Γ : C^op ⟶ HSET)
: dep_psh Γ.
Proof.
use make_dep_psh.
- exact (λ _ _, emptyset).
- intros x y xx yy s p a.
induction a.
- abstract
(intros ; cbn ;
apply isapropempty).
- abstract
(intros ; cbn ;
apply isapropempty).
Defined.
Definition dep_psh_nat_trans_from_empty
{Γ : C^op ⟶ HSET}
(A : dep_psh Γ)
: dep_psh_nat_trans
(empty_dep_psh Γ)
A
(nat_trans_id _).
Proof.
use make_dep_psh_nat_trans.
- intros x xx a.
induction a.
- abstract
(intros x y xx yy f p q a ;
induction a).
Defined.
Proposition dep_psh_nat_trans_from_empty_eq
{Γ : C^op ⟶ HSET}
{A : dep_psh Γ}
(τ₁ τ₂ : dep_psh_nat_trans
(empty_dep_psh Γ)
A
(nat_trans_id _))
: τ₁ = τ₂.
Proof.
use dep_psh_nat_trans_eq.
intros x xx a.
induction a.
Qed.
Definition empty_dep_psh_subst
{Γ₁ Γ₂ : C^op ⟶ HSET}
(s : Γ₁ ⟹ Γ₂)
: dep_psh_nat_trans
(empty_dep_psh Γ₁)
(dep_psh_subst s (empty_dep_psh Γ₂))
(nat_trans_id _).
Proof.
use make_dep_psh_nat_trans.
- exact (λ x xx a, a).
- abstract
(intros x y xx yy f p q a ;
induction a).
Defined.
Definition empty_dep_psh_subst_inv
{Γ₁ Γ₂ : C^op ⟶ HSET}
(s : Γ₁ ⟹ Γ₂)
: dep_psh_nat_trans
(dep_psh_subst s (empty_dep_psh Γ₂))
(empty_dep_psh Γ₁)
(nat_trans_id _).
Proof.
use make_dep_psh_nat_trans.
- exact (λ x xx a, a).
- abstract
(intros x y xx yy f p q a ;
induction a).
Defined.
Definition dep_psh_fiber_initial
(Γ : C^op ⟶ HSET)
: Initial ((disp_cat_dep_psh C) [{ Γ }]).
Proof.
use make_Initial.
- exact (empty_dep_psh Γ).
- intros A.
use make_iscontr.
+ exact (dep_psh_nat_trans_from_empty A).
+ intro.
apply dep_psh_nat_trans_from_empty_eq.
Defined.
Definition dep_psh_preserves_initial
{Γ₁ Γ₂ : C^op ⟶ HSET}
(s : Γ₁ ⟹ Γ₂)
: preserves_initial
(fiber_functor_from_cleaving
(disp_cat_dep_psh C)
(cleaving_disp_cat_dep_psh C)
s).
Proof.
use preserves_initial_if_preserves_chosen.
{
apply dep_psh_fiber_initial.
}
use iso_to_Initial.
{
apply dep_psh_fiber_initial.
}
use make_z_iso.
- exact (empty_dep_psh_subst s).
- exact (empty_dep_psh_subst_inv s).
- split.
+ abstract
(use dep_psh_nat_trans_eq ;
intros x xx a ;
induction a).
+ abstract
(use dep_psh_nat_trans_eq ;
intros x xx a ;
induction a).
Defined.
(Γ : C^op ⟶ HSET)
: dep_psh Γ.
Proof.
use make_dep_psh.
- exact (λ _ _, emptyset).
- intros x y xx yy s p a.
induction a.
- abstract
(intros ; cbn ;
apply isapropempty).
- abstract
(intros ; cbn ;
apply isapropempty).
Defined.
Definition dep_psh_nat_trans_from_empty
{Γ : C^op ⟶ HSET}
(A : dep_psh Γ)
: dep_psh_nat_trans
(empty_dep_psh Γ)
A
(nat_trans_id _).
Proof.
use make_dep_psh_nat_trans.
- intros x xx a.
induction a.
- abstract
(intros x y xx yy f p q a ;
induction a).
Defined.
Proposition dep_psh_nat_trans_from_empty_eq
{Γ : C^op ⟶ HSET}
{A : dep_psh Γ}
(τ₁ τ₂ : dep_psh_nat_trans
(empty_dep_psh Γ)
A
(nat_trans_id _))
: τ₁ = τ₂.
Proof.
use dep_psh_nat_trans_eq.
intros x xx a.
induction a.
Qed.
Definition empty_dep_psh_subst
{Γ₁ Γ₂ : C^op ⟶ HSET}
(s : Γ₁ ⟹ Γ₂)
: dep_psh_nat_trans
(empty_dep_psh Γ₁)
(dep_psh_subst s (empty_dep_psh Γ₂))
(nat_trans_id _).
Proof.
use make_dep_psh_nat_trans.
- exact (λ x xx a, a).
- abstract
(intros x y xx yy f p q a ;
induction a).
Defined.
Definition empty_dep_psh_subst_inv
{Γ₁ Γ₂ : C^op ⟶ HSET}
(s : Γ₁ ⟹ Γ₂)
: dep_psh_nat_trans
(dep_psh_subst s (empty_dep_psh Γ₂))
(empty_dep_psh Γ₁)
(nat_trans_id _).
Proof.
use make_dep_psh_nat_trans.
- exact (λ x xx a, a).
- abstract
(intros x y xx yy f p q a ;
induction a).
Defined.
Definition dep_psh_fiber_initial
(Γ : C^op ⟶ HSET)
: Initial ((disp_cat_dep_psh C) [{ Γ }]).
Proof.
use make_Initial.
- exact (empty_dep_psh Γ).
- intros A.
use make_iscontr.
+ exact (dep_psh_nat_trans_from_empty A).
+ intro.
apply dep_psh_nat_trans_from_empty_eq.
Defined.
Definition dep_psh_preserves_initial
{Γ₁ Γ₂ : C^op ⟶ HSET}
(s : Γ₁ ⟹ Γ₂)
: preserves_initial
(fiber_functor_from_cleaving
(disp_cat_dep_psh C)
(cleaving_disp_cat_dep_psh C)
s).
Proof.
use preserves_initial_if_preserves_chosen.
{
apply dep_psh_fiber_initial.
}
use iso_to_Initial.
{
apply dep_psh_fiber_initial.
}
use make_z_iso.
- exact (empty_dep_psh_subst s).
- exact (empty_dep_psh_subst_inv s).
- split.
+ abstract
(use dep_psh_nat_trans_eq ;
intros x xx a ;
induction a).
+ abstract
(use dep_psh_nat_trans_eq ;
intros x xx a ;
induction a).
Defined.
Definition unit_dep_psh
(Γ : C^op ⟶ HSET)
: dep_psh Γ.
Proof.
use make_dep_psh.
- exact (λ _ _, unitset).
- exact (λ _ _ _ _ _ _ _, tt).
- abstract
(intros ; cbn ;
apply isapropunit).
- abstract
(intros ; cbn ;
apply isapropunit).
Defined.
Definition dep_psh_nat_trans_to_unit
{Γ : C^op ⟶ HSET}
(A : dep_psh Γ)
: dep_psh_nat_trans
A
(unit_dep_psh Γ)
(nat_trans_id _).
Proof.
use make_dep_psh_nat_trans.
- exact (λ x xx a, tt).
- abstract
(intro ; intros ;
apply isapropunit).
Defined.
Proposition dep_psh_nat_trans_to_unit_eq
{Γ : C^op ⟶ HSET}
{A : dep_psh Γ}
(τ₁ τ₂ : dep_psh_nat_trans
A
(unit_dep_psh Γ)
(nat_trans_id _))
: τ₁ = τ₂.
Proof.
use dep_psh_nat_trans_eq.
intros x xx a.
apply isapropunit.
Qed.
Definition unit_dep_psh_subst
{Γ₁ Γ₂ : C^op ⟶ HSET}
(s : Γ₁ ⟹ Γ₂)
: dep_psh_nat_trans
(unit_dep_psh Γ₁)
(dep_psh_subst s (unit_dep_psh Γ₂))
(nat_trans_id _).
Proof.
use make_dep_psh_nat_trans.
- exact (λ x xx a, a).
- abstract
(intros x y xx yy f p q a ;
apply isapropunit).
Defined.
Definition unit_dep_psh_subst_inv
{Γ₁ Γ₂ : C^op ⟶ HSET}
(s : Γ₁ ⟹ Γ₂)
: dep_psh_nat_trans
(dep_psh_subst s (unit_dep_psh Γ₂))
(unit_dep_psh Γ₁)
(nat_trans_id _).
Proof.
use make_dep_psh_nat_trans.
- exact (λ x xx a, a).
- abstract
(intros x y xx yy f p q a ;
apply isapropunit).
Defined.
Definition dep_psh_fiber_terminal
(Γ : C^op ⟶ HSET)
: Terminal ((disp_cat_dep_psh C) [{ Γ }]).
Proof.
use make_Terminal.
- exact (unit_dep_psh Γ).
- intros A.
use make_iscontr.
+ exact (dep_psh_nat_trans_to_unit A).
+ intro.
apply dep_psh_nat_trans_to_unit_eq.
Defined.
Definition dep_psh_preserves_terminal
{Γ₁ Γ₂ : C^op ⟶ HSET}
(s : Γ₁ ⟹ Γ₂)
: preserves_terminal
(fiber_functor_from_cleaving
(disp_cat_dep_psh C)
(cleaving_disp_cat_dep_psh C)
s).
Proof.
use preserves_terminal_if_preserves_chosen.
{
apply dep_psh_fiber_terminal.
}
use iso_to_Terminal.
{
apply dep_psh_fiber_terminal.
}
use make_z_iso.
- exact (unit_dep_psh_subst s).
- exact (unit_dep_psh_subst_inv s).
- split.
+ abstract
(use dep_psh_nat_trans_eq ;
intros x xx a ;
apply isapropunit).
+ abstract
(use dep_psh_nat_trans_eq ;
intros x xx a ;
apply isapropunit).
Defined.
Definition dep_psh_unit_z_iso
(Γ : C^op ⟶ HSET)
: is_z_isomorphism (C := PreShv C) (total_psh_pr (unit_dep_psh Γ)).
Proof.
use make_is_z_isomorphism.
- use make_nat_trans.
+ exact (λ x xx, xx ,, tt).
+ abstract
(intros x y f ; cbn ;
apply idpath).
- abstract
(split ;
(use nat_trans_eq ; [ apply homset_property | ]) ;
intro x ;
use funextsec ;
intros xx ;
[ | apply idpath ] ;
induction xx as [ xx [ ] ] ;
apply idpath).
Defined.
(Γ : C^op ⟶ HSET)
: dep_psh Γ.
Proof.
use make_dep_psh.
- exact (λ _ _, unitset).
- exact (λ _ _ _ _ _ _ _, tt).
- abstract
(intros ; cbn ;
apply isapropunit).
- abstract
(intros ; cbn ;
apply isapropunit).
Defined.
Definition dep_psh_nat_trans_to_unit
{Γ : C^op ⟶ HSET}
(A : dep_psh Γ)
: dep_psh_nat_trans
A
(unit_dep_psh Γ)
(nat_trans_id _).
Proof.
use make_dep_psh_nat_trans.
- exact (λ x xx a, tt).
- abstract
(intro ; intros ;
apply isapropunit).
Defined.
Proposition dep_psh_nat_trans_to_unit_eq
{Γ : C^op ⟶ HSET}
{A : dep_psh Γ}
(τ₁ τ₂ : dep_psh_nat_trans
A
(unit_dep_psh Γ)
(nat_trans_id _))
: τ₁ = τ₂.
Proof.
use dep_psh_nat_trans_eq.
intros x xx a.
apply isapropunit.
Qed.
Definition unit_dep_psh_subst
{Γ₁ Γ₂ : C^op ⟶ HSET}
(s : Γ₁ ⟹ Γ₂)
: dep_psh_nat_trans
(unit_dep_psh Γ₁)
(dep_psh_subst s (unit_dep_psh Γ₂))
(nat_trans_id _).
Proof.
use make_dep_psh_nat_trans.
- exact (λ x xx a, a).
- abstract
(intros x y xx yy f p q a ;
apply isapropunit).
Defined.
Definition unit_dep_psh_subst_inv
{Γ₁ Γ₂ : C^op ⟶ HSET}
(s : Γ₁ ⟹ Γ₂)
: dep_psh_nat_trans
(dep_psh_subst s (unit_dep_psh Γ₂))
(unit_dep_psh Γ₁)
(nat_trans_id _).
Proof.
use make_dep_psh_nat_trans.
- exact (λ x xx a, a).
- abstract
(intros x y xx yy f p q a ;
apply isapropunit).
Defined.
Definition dep_psh_fiber_terminal
(Γ : C^op ⟶ HSET)
: Terminal ((disp_cat_dep_psh C) [{ Γ }]).
Proof.
use make_Terminal.
- exact (unit_dep_psh Γ).
- intros A.
use make_iscontr.
+ exact (dep_psh_nat_trans_to_unit A).
+ intro.
apply dep_psh_nat_trans_to_unit_eq.
Defined.
Definition dep_psh_preserves_terminal
{Γ₁ Γ₂ : C^op ⟶ HSET}
(s : Γ₁ ⟹ Γ₂)
: preserves_terminal
(fiber_functor_from_cleaving
(disp_cat_dep_psh C)
(cleaving_disp_cat_dep_psh C)
s).
Proof.
use preserves_terminal_if_preserves_chosen.
{
apply dep_psh_fiber_terminal.
}
use iso_to_Terminal.
{
apply dep_psh_fiber_terminal.
}
use make_z_iso.
- exact (unit_dep_psh_subst s).
- exact (unit_dep_psh_subst_inv s).
- split.
+ abstract
(use dep_psh_nat_trans_eq ;
intros x xx a ;
apply isapropunit).
+ abstract
(use dep_psh_nat_trans_eq ;
intros x xx a ;
apply isapropunit).
Defined.
Definition dep_psh_unit_z_iso
(Γ : C^op ⟶ HSET)
: is_z_isomorphism (C := PreShv C) (total_psh_pr (unit_dep_psh Γ)).
Proof.
use make_is_z_isomorphism.
- use make_nat_trans.
+ exact (λ x xx, xx ,, tt).
+ abstract
(intros x y f ; cbn ;
apply idpath).
- abstract
(split ;
(use nat_trans_eq ; [ apply homset_property | ]) ;
intro x ;
use funextsec ;
intros xx ;
[ | apply idpath ] ;
induction xx as [ xx [ ] ] ;
apply idpath).
Defined.
Definition prod_dep_psh
{Γ : C^op ⟶ HSET}
(A B : dep_psh Γ)
: dep_psh Γ.
Proof.
use make_dep_psh.
- exact (λ x xx, A x xx × B x xx)%set.
- exact (λ x y xx yy s p ab, #d A s p (pr1 ab) ,, #d B s p (pr2 ab)).
- abstract
(intros x xx p a ;
use pathsdirprod ;
apply dep_psh_mor_id).
- abstract
(intros x y z xx yy zz s₁ s₂ p q r a ;
use pathsdirprod ;
apply dep_psh_mor_comp).
Defined.
Definition prod_dep_psh_pr1
{Γ : C^op ⟶ HSET}
(A B : dep_psh Γ)
: dep_psh_nat_trans
(prod_dep_psh A B)
A
(nat_trans_id _).
Proof.
use make_dep_psh_nat_trans.
- exact (λ x xx ab, pr1 ab).
- abstract
(intro ; intros ; cbn ;
apply dep_psh_mor_path_eq ;
apply idpath).
Defined.
Definition prod_dep_psh_pr2
{Γ : C^op ⟶ HSET}
(A B : dep_psh Γ)
: dep_psh_nat_trans
(prod_dep_psh A B)
B
(nat_trans_id _).
Proof.
use make_dep_psh_nat_trans.
- exact (λ x xx ab, pr2 ab).
- abstract
(intro ; intros ; cbn ;
apply dep_psh_mor_path_eq ;
apply idpath).
Defined.
Definition prod_dep_psh_pair
{Γ : C^op ⟶ HSET}
{Z A B : dep_psh Γ}
(τ₁ : dep_psh_nat_trans Z A (nat_trans_id _))
(τ₂ : dep_psh_nat_trans Z B (nat_trans_id _))
: dep_psh_nat_trans Z (prod_dep_psh A B) (nat_trans_id _).
Proof.
use make_dep_psh_nat_trans.
- exact (λ x xx z, τ₁ x xx z ,, τ₂ x xx z).
- abstract
(intros x y xx yy f p q z ; cbn ;
use (pathsdirprod (dep_psh_nat_trans_ax τ₁ f p q z)) ;
exact (dep_psh_nat_trans_ax τ₂ f p q z)).
Defined.
Definition prod_dep_psh_subst
{Γ₁ Γ₂ : C^op ⟶ HSET}
(s : Γ₁ ⟹ Γ₂)
(A B : dep_psh Γ₂)
: dep_psh_nat_trans
(dep_psh_subst s (prod_dep_psh A B))
(prod_dep_psh (dep_psh_subst s A) (dep_psh_subst s B))
(nat_trans_id _).
Proof.
use make_dep_psh_nat_trans.
- exact (λ x xx ab, ab).
- abstract
(cbn ;
intros ;
apply pathsdirprod ;
apply dep_psh_mor_path_eq ;
apply idpath).
Defined.
Definition prod_dep_psh_subst_inv
{Γ₁ Γ₂ : C^op ⟶ HSET}
(s : Γ₁ ⟹ Γ₂)
(A B : dep_psh Γ₂)
: dep_psh_nat_trans
(prod_dep_psh (dep_psh_subst s A) (dep_psh_subst s B))
(dep_psh_subst s (prod_dep_psh A B))
(nat_trans_id _).
Proof.
use make_dep_psh_nat_trans.
- exact (λ x xx ab, ab).
- abstract
(cbn ;
intros ;
apply pathsdirprod ;
apply dep_psh_mor_path_eq ;
apply idpath).
Defined.
Definition dep_psh_fiber_binproducts
(Γ : C^op ⟶ HSET)
: BinProducts ((disp_cat_dep_psh C) [{ Γ }]).
Proof.
intros A B.
use make_BinProduct.
- exact (prod_dep_psh A B).
- exact (prod_dep_psh_pr1 A B).
- exact (prod_dep_psh_pr2 A B).
- intros Z τ₁ τ₂.
use make_iscontr.
+ simple refine (_ ,, _ ,, _).
* exact (prod_dep_psh_pair τ₁ τ₂).
* abstract
(use dep_psh_nat_trans_eq ;
intros x xx a ;
exact (dep_psh_fiber_comp _ _ _ _)).
* abstract
(use dep_psh_nat_trans_eq ;
intros x xx a ;
exact (dep_psh_fiber_comp _ _ _ _)).
+ abstract
(intros τ ;
use subtypePath ; [ intro ; apply isapropdirprod ; apply homset_property | ] ;
use dep_psh_nat_trans_eq ;
intros x xx a ;
use pathsdirprod ;
[ refine (!_ @ maponpaths (λ (z : dep_psh_nat_trans _ _ _), z x xx a) (pr12 τ)) ;
refine (dep_psh_fiber_comp _ _ _ _ @ _) ;
apply idpath
| refine (!_ @ maponpaths (λ (z : dep_psh_nat_trans _ _ _), z x xx a) (pr22 τ)) ;
refine (dep_psh_fiber_comp _ _ _ _ @ _) ;
apply idpath ]).
Defined.
Definition dep_psh_preserves_binproduct
{Γ₁ Γ₂ : C^op ⟶ HSET}
(s : Γ₁ ⟹ Γ₂)
: preserves_binproduct
(fiber_functor_from_cleaving
(disp_cat_dep_psh C)
(cleaving_disp_cat_dep_psh C)
s).
Proof.
use preserves_binproduct_if_preserves_chosen.
{
apply dep_psh_fiber_binproducts.
}
intros A B.
use (isBinProduct_z_iso (isBinProduct_BinProduct _ (dep_psh_fiber_binproducts Γ₁ _ _))).
- use make_z_iso.
+ exact (prod_dep_psh_subst s A B).
+ exact (prod_dep_psh_subst_inv s A B).
+ abstract
(split ;
use dep_psh_nat_trans_eq ;
intros x xx a ;
refine (dep_psh_fiber_comp _ _ _ _ @ _) ;
cbn ;
apply idpath).
- abstract
(use dep_psh_nat_trans_eq ;
intros x xx a ;
refine (dep_psh_fiber_functor_from_cleaving _ s _ _ @ _) ;
refine (_ @ !(dep_psh_fiber_comp _ _ _ _)) ;
apply idpath).
- abstract
(use dep_psh_nat_trans_eq ;
intros x xx a ;
refine (dep_psh_fiber_functor_from_cleaving _ s _ _ @ _) ;
refine (_ @ !(dep_psh_fiber_comp _ _ _ _)) ;
apply idpath).
Defined.
{Γ : C^op ⟶ HSET}
(A B : dep_psh Γ)
: dep_psh Γ.
Proof.
use make_dep_psh.
- exact (λ x xx, A x xx × B x xx)%set.
- exact (λ x y xx yy s p ab, #d A s p (pr1 ab) ,, #d B s p (pr2 ab)).
- abstract
(intros x xx p a ;
use pathsdirprod ;
apply dep_psh_mor_id).
- abstract
(intros x y z xx yy zz s₁ s₂ p q r a ;
use pathsdirprod ;
apply dep_psh_mor_comp).
Defined.
Definition prod_dep_psh_pr1
{Γ : C^op ⟶ HSET}
(A B : dep_psh Γ)
: dep_psh_nat_trans
(prod_dep_psh A B)
A
(nat_trans_id _).
Proof.
use make_dep_psh_nat_trans.
- exact (λ x xx ab, pr1 ab).
- abstract
(intro ; intros ; cbn ;
apply dep_psh_mor_path_eq ;
apply idpath).
Defined.
Definition prod_dep_psh_pr2
{Γ : C^op ⟶ HSET}
(A B : dep_psh Γ)
: dep_psh_nat_trans
(prod_dep_psh A B)
B
(nat_trans_id _).
Proof.
use make_dep_psh_nat_trans.
- exact (λ x xx ab, pr2 ab).
- abstract
(intro ; intros ; cbn ;
apply dep_psh_mor_path_eq ;
apply idpath).
Defined.
Definition prod_dep_psh_pair
{Γ : C^op ⟶ HSET}
{Z A B : dep_psh Γ}
(τ₁ : dep_psh_nat_trans Z A (nat_trans_id _))
(τ₂ : dep_psh_nat_trans Z B (nat_trans_id _))
: dep_psh_nat_trans Z (prod_dep_psh A B) (nat_trans_id _).
Proof.
use make_dep_psh_nat_trans.
- exact (λ x xx z, τ₁ x xx z ,, τ₂ x xx z).
- abstract
(intros x y xx yy f p q z ; cbn ;
use (pathsdirprod (dep_psh_nat_trans_ax τ₁ f p q z)) ;
exact (dep_psh_nat_trans_ax τ₂ f p q z)).
Defined.
Definition prod_dep_psh_subst
{Γ₁ Γ₂ : C^op ⟶ HSET}
(s : Γ₁ ⟹ Γ₂)
(A B : dep_psh Γ₂)
: dep_psh_nat_trans
(dep_psh_subst s (prod_dep_psh A B))
(prod_dep_psh (dep_psh_subst s A) (dep_psh_subst s B))
(nat_trans_id _).
Proof.
use make_dep_psh_nat_trans.
- exact (λ x xx ab, ab).
- abstract
(cbn ;
intros ;
apply pathsdirprod ;
apply dep_psh_mor_path_eq ;
apply idpath).
Defined.
Definition prod_dep_psh_subst_inv
{Γ₁ Γ₂ : C^op ⟶ HSET}
(s : Γ₁ ⟹ Γ₂)
(A B : dep_psh Γ₂)
: dep_psh_nat_trans
(prod_dep_psh (dep_psh_subst s A) (dep_psh_subst s B))
(dep_psh_subst s (prod_dep_psh A B))
(nat_trans_id _).
Proof.
use make_dep_psh_nat_trans.
- exact (λ x xx ab, ab).
- abstract
(cbn ;
intros ;
apply pathsdirprod ;
apply dep_psh_mor_path_eq ;
apply idpath).
Defined.
Definition dep_psh_fiber_binproducts
(Γ : C^op ⟶ HSET)
: BinProducts ((disp_cat_dep_psh C) [{ Γ }]).
Proof.
intros A B.
use make_BinProduct.
- exact (prod_dep_psh A B).
- exact (prod_dep_psh_pr1 A B).
- exact (prod_dep_psh_pr2 A B).
- intros Z τ₁ τ₂.
use make_iscontr.
+ simple refine (_ ,, _ ,, _).
* exact (prod_dep_psh_pair τ₁ τ₂).
* abstract
(use dep_psh_nat_trans_eq ;
intros x xx a ;
exact (dep_psh_fiber_comp _ _ _ _)).
* abstract
(use dep_psh_nat_trans_eq ;
intros x xx a ;
exact (dep_psh_fiber_comp _ _ _ _)).
+ abstract
(intros τ ;
use subtypePath ; [ intro ; apply isapropdirprod ; apply homset_property | ] ;
use dep_psh_nat_trans_eq ;
intros x xx a ;
use pathsdirprod ;
[ refine (!_ @ maponpaths (λ (z : dep_psh_nat_trans _ _ _), z x xx a) (pr12 τ)) ;
refine (dep_psh_fiber_comp _ _ _ _ @ _) ;
apply idpath
| refine (!_ @ maponpaths (λ (z : dep_psh_nat_trans _ _ _), z x xx a) (pr22 τ)) ;
refine (dep_psh_fiber_comp _ _ _ _ @ _) ;
apply idpath ]).
Defined.
Definition dep_psh_preserves_binproduct
{Γ₁ Γ₂ : C^op ⟶ HSET}
(s : Γ₁ ⟹ Γ₂)
: preserves_binproduct
(fiber_functor_from_cleaving
(disp_cat_dep_psh C)
(cleaving_disp_cat_dep_psh C)
s).
Proof.
use preserves_binproduct_if_preserves_chosen.
{
apply dep_psh_fiber_binproducts.
}
intros A B.
use (isBinProduct_z_iso (isBinProduct_BinProduct _ (dep_psh_fiber_binproducts Γ₁ _ _))).
- use make_z_iso.
+ exact (prod_dep_psh_subst s A B).
+ exact (prod_dep_psh_subst_inv s A B).
+ abstract
(split ;
use dep_psh_nat_trans_eq ;
intros x xx a ;
refine (dep_psh_fiber_comp _ _ _ _ @ _) ;
cbn ;
apply idpath).
- abstract
(use dep_psh_nat_trans_eq ;
intros x xx a ;
refine (dep_psh_fiber_functor_from_cleaving _ s _ _ @ _) ;
refine (_ @ !(dep_psh_fiber_comp _ _ _ _)) ;
apply idpath).
- abstract
(use dep_psh_nat_trans_eq ;
intros x xx a ;
refine (dep_psh_fiber_functor_from_cleaving _ s _ _ @ _) ;
refine (_ @ !(dep_psh_fiber_comp _ _ _ _)) ;
apply idpath).
Defined.
Definition coprod_dep_psh
{Γ : C^op ⟶ HSET}
(A B : dep_psh Γ)
: dep_psh Γ.
Proof.
use make_dep_psh.
- exact (λ x xx, setcoprod (A x xx) (B x xx))%set.
- intros x y xx yy s p ab.
induction ab as [ a | b ].
+ exact (inl (#d A s p a)).
+ exact (inr (#d B s p b)).
- abstract
(intros x xx p ab ;
induction ab ;
cbn ;
apply maponpaths ;
apply dep_psh_mor_id).
- abstract
(intros x y z xx yy zz s₁ s₂ p q r ab ;
induction ab ;
cbn ;
apply maponpaths ;
apply dep_psh_mor_comp).
Defined.
Definition coprod_dep_psh_inl
{Γ : C^op ⟶ HSET}
(A B : dep_psh Γ)
: dep_psh_nat_trans
A
(coprod_dep_psh A B)
(nat_trans_id _).
Proof.
use make_dep_psh_nat_trans.
- exact (λ x xx a, inl a).
- abstract
(intro ; intros ; cbn ;
apply maponpaths ;
apply dep_psh_mor_path_eq ;
apply idpath).
Defined.
Definition coprod_dep_psh_inr
{Γ : C^op ⟶ HSET}
(A B : dep_psh Γ)
: dep_psh_nat_trans
B
(coprod_dep_psh A B)
(nat_trans_id _).
Proof.
use make_dep_psh_nat_trans.
- exact (λ x xx a, inr a).
- abstract
(intro ; intros ; cbn ;
apply maponpaths ;
apply dep_psh_mor_path_eq ;
apply idpath).
Defined.
Definition coprod_dep_psh_copair
{Γ : C^op ⟶ HSET}
{Z A B : dep_psh Γ}
(τ₁ : dep_psh_nat_trans A Z (nat_trans_id _))
(τ₂ : dep_psh_nat_trans B Z (nat_trans_id _))
: dep_psh_nat_trans
(coprod_dep_psh A B)
Z
(nat_trans_id _).
Proof.
use make_dep_psh_nat_trans.
- intros x xx ab.
induction ab as [ a | b ].
+ exact (τ₁ x xx a).
+ exact (τ₂ x xx b).
- abstract
(intros x y xx yy f p q ab ;
induction ab as [ a | b ] ;
[ apply (dep_psh_nat_trans_ax τ₁) | ] ;
apply (dep_psh_nat_trans_ax τ₂)).
Defined.
Definition coprod_dep_psh_subst
{Γ₁ Γ₂ : C^op ⟶ HSET}
(s : Γ₁ ⟹ Γ₂)
(A B : dep_psh Γ₂)
: dep_psh_nat_trans
(dep_psh_subst s (coprod_dep_psh A B))
(coprod_dep_psh (dep_psh_subst s A) (dep_psh_subst s B))
(nat_trans_id _).
Proof.
use make_dep_psh_nat_trans.
- exact (λ x xx ab, ab).
- abstract
(cbn ;
intros x y xx yy f p q ab ;
induction ab ;
cbn ;
apply maponpaths ;
apply dep_psh_mor_path_eq ;
apply idpath).
Defined.
Definition coprod_dep_psh_subst_inv
{Γ₁ Γ₂ : C^op ⟶ HSET}
(s : Γ₁ ⟹ Γ₂)
(A B : dep_psh Γ₂)
: dep_psh_nat_trans
(coprod_dep_psh (dep_psh_subst s A) (dep_psh_subst s B))
(dep_psh_subst s (coprod_dep_psh A B))
(nat_trans_id _).
Proof.
use make_dep_psh_nat_trans.
- exact (λ x xx ab, ab).
- abstract
(cbn ;
intros x y xx yy f p q ab ;
induction ab ;
cbn ;
apply maponpaths ;
apply dep_psh_mor_path_eq ;
apply idpath).
Defined.
Definition dep_psh_fiber_bincoproducts
(Γ : C^op ⟶ HSET)
: BinCoproducts ((disp_cat_dep_psh C) [{ Γ }]).
Proof.
intros A B.
use make_BinCoproduct.
- exact (coprod_dep_psh A B).
- exact (coprod_dep_psh_inl A B).
- exact (coprod_dep_psh_inr A B).
- intros Z τ₁ τ₂.
use make_iscontr.
+ simple refine (_ ,, _ ,, _).
* exact (coprod_dep_psh_copair τ₁ τ₂).
* abstract
(use dep_psh_nat_trans_eq ;
intros x xx a ;
exact (dep_psh_fiber_comp _ _ _ _)).
* abstract
(use dep_psh_nat_trans_eq ;
intros x xx a ;
exact (dep_psh_fiber_comp _ _ _ _)).
+ abstract
(intros τ ;
use subtypePath ; [ intro ; apply isapropdirprod ; apply homset_property | ] ;
use dep_psh_nat_trans_eq ;
intros x xx ab ;
induction ab as [ a | b ] ;
[ refine (!_ @ maponpaths (λ (z : dep_psh_nat_trans _ _ _), z x xx a) (pr12 τ)) ;
refine (dep_psh_fiber_comp _ _ _ _ @ _) ;
apply idpath
| refine (!_ @ maponpaths (λ (z : dep_psh_nat_trans _ _ _), z x xx b) (pr22 τ)) ;
refine (dep_psh_fiber_comp _ _ _ _ @ _) ;
apply idpath ]).
Defined.
Definition disjoint_dep_psh_fiber_bincoproducts
(Γ : C^op ⟶ HSET)
: disjoint_bincoproducts
(dep_psh_fiber_bincoproducts Γ)
(dep_psh_fiber_initial Γ).
Proof.
intros X Y.
repeat split.
- intros W τ₁ τ₂ p.
use dep_psh_nat_trans_eq.
intros x xx w.
exact (ii1_injectivity
_ _
(!(dep_psh_fiber_comp _ _ _ _)
@ dep_psh_nat_trans_eq_pt p xx w
@ dep_psh_fiber_comp _ _ _ _)).
- intros W τ₁ τ₂ p.
use dep_psh_nat_trans_eq.
intros x xx w.
exact (ii2_injectivity
_ _
(!(dep_psh_fiber_comp _ _ _ _)
@ dep_psh_nat_trans_eq_pt p xx w
@ dep_psh_fiber_comp _ _ _ _)).
- intros W τ₁ τ₂ p.
use make_iscontr.
+ simple refine (_ ,, _).
* use make_dep_psh_nat_trans.
** intros x xx w.
exact (negpathsii1ii2
_ _
(!(dep_psh_fiber_comp _ _ _ _)
@ dep_psh_nat_trans_eq_pt p xx w
@ dep_psh_fiber_comp _ _ _ _)).
** abstract
(intros x y xx yy f q₁ q₂ w ;
apply fromempty ;
exact (negpathsii1ii2
_ _
(!(dep_psh_fiber_comp _ _ _ _)
@ dep_psh_nat_trans_eq_pt p xx w
@ dep_psh_fiber_comp _ _ _ _))).
* abstract
(split ;
use dep_psh_nat_trans_eq ;
intros x xx w ;
apply fromempty ;
exact (negpathsii1ii2
_ _
(!(dep_psh_fiber_comp _ _ _ _)
@ dep_psh_nat_trans_eq_pt p xx w
@ dep_psh_fiber_comp _ _ _ _))).
+ intros θ.
use subtypePath.
{
intro.
apply isapropdirprod ; apply homset_property.
}
use dep_psh_nat_trans_eq.
intros x xx w.
apply fromempty.
exact (negpathsii1ii2
_ _
(!(dep_psh_fiber_comp _ _ _ _)
@ dep_psh_nat_trans_eq_pt p xx w
@ dep_psh_fiber_comp _ _ _ _)).
Qed.
Definition dep_psh_preserves_bincoproduct
{Γ₁ Γ₂ : C^op ⟶ HSET}
(s : Γ₁ ⟹ Γ₂)
: preserves_bincoproduct
(fiber_functor_from_cleaving
(disp_cat_dep_psh C)
(cleaving_disp_cat_dep_psh C)
s).
Proof.
use preserves_bincoproduct_if_preserves_chosen.
{
apply dep_psh_fiber_bincoproducts.
}
intros A B.
use (isBinCoproduct_z_iso
(isBinCoproduct_BinCoproduct _ (dep_psh_fiber_bincoproducts Γ₁ _ _))).
- use make_z_iso.
+ exact (coprod_dep_psh_subst s A B).
+ exact (coprod_dep_psh_subst_inv s A B).
+ abstract
(split ;
use dep_psh_nat_trans_eq ;
intros x xx a ;
refine (dep_psh_fiber_comp _ _ _ _ @ _) ;
cbn ;
apply idpath).
- abstract
(use dep_psh_nat_trans_eq ;
intros x xx a ;
refine (dep_psh_fiber_functor_from_cleaving _ s _ _ @ _) ;
refine (_ @ !(dep_psh_fiber_comp _ _ _ _)) ;
apply idpath).
- abstract
(use dep_psh_nat_trans_eq ;
intros x xx a ;
refine (dep_psh_fiber_functor_from_cleaving _ s _ _ @ _) ;
refine (_ @ !(dep_psh_fiber_comp _ _ _ _)) ;
apply idpath).
Defined.
{Γ : C^op ⟶ HSET}
(A B : dep_psh Γ)
: dep_psh Γ.
Proof.
use make_dep_psh.
- exact (λ x xx, setcoprod (A x xx) (B x xx))%set.
- intros x y xx yy s p ab.
induction ab as [ a | b ].
+ exact (inl (#d A s p a)).
+ exact (inr (#d B s p b)).
- abstract
(intros x xx p ab ;
induction ab ;
cbn ;
apply maponpaths ;
apply dep_psh_mor_id).
- abstract
(intros x y z xx yy zz s₁ s₂ p q r ab ;
induction ab ;
cbn ;
apply maponpaths ;
apply dep_psh_mor_comp).
Defined.
Definition coprod_dep_psh_inl
{Γ : C^op ⟶ HSET}
(A B : dep_psh Γ)
: dep_psh_nat_trans
A
(coprod_dep_psh A B)
(nat_trans_id _).
Proof.
use make_dep_psh_nat_trans.
- exact (λ x xx a, inl a).
- abstract
(intro ; intros ; cbn ;
apply maponpaths ;
apply dep_psh_mor_path_eq ;
apply idpath).
Defined.
Definition coprod_dep_psh_inr
{Γ : C^op ⟶ HSET}
(A B : dep_psh Γ)
: dep_psh_nat_trans
B
(coprod_dep_psh A B)
(nat_trans_id _).
Proof.
use make_dep_psh_nat_trans.
- exact (λ x xx a, inr a).
- abstract
(intro ; intros ; cbn ;
apply maponpaths ;
apply dep_psh_mor_path_eq ;
apply idpath).
Defined.
Definition coprod_dep_psh_copair
{Γ : C^op ⟶ HSET}
{Z A B : dep_psh Γ}
(τ₁ : dep_psh_nat_trans A Z (nat_trans_id _))
(τ₂ : dep_psh_nat_trans B Z (nat_trans_id _))
: dep_psh_nat_trans
(coprod_dep_psh A B)
Z
(nat_trans_id _).
Proof.
use make_dep_psh_nat_trans.
- intros x xx ab.
induction ab as [ a | b ].
+ exact (τ₁ x xx a).
+ exact (τ₂ x xx b).
- abstract
(intros x y xx yy f p q ab ;
induction ab as [ a | b ] ;
[ apply (dep_psh_nat_trans_ax τ₁) | ] ;
apply (dep_psh_nat_trans_ax τ₂)).
Defined.
Definition coprod_dep_psh_subst
{Γ₁ Γ₂ : C^op ⟶ HSET}
(s : Γ₁ ⟹ Γ₂)
(A B : dep_psh Γ₂)
: dep_psh_nat_trans
(dep_psh_subst s (coprod_dep_psh A B))
(coprod_dep_psh (dep_psh_subst s A) (dep_psh_subst s B))
(nat_trans_id _).
Proof.
use make_dep_psh_nat_trans.
- exact (λ x xx ab, ab).
- abstract
(cbn ;
intros x y xx yy f p q ab ;
induction ab ;
cbn ;
apply maponpaths ;
apply dep_psh_mor_path_eq ;
apply idpath).
Defined.
Definition coprod_dep_psh_subst_inv
{Γ₁ Γ₂ : C^op ⟶ HSET}
(s : Γ₁ ⟹ Γ₂)
(A B : dep_psh Γ₂)
: dep_psh_nat_trans
(coprod_dep_psh (dep_psh_subst s A) (dep_psh_subst s B))
(dep_psh_subst s (coprod_dep_psh A B))
(nat_trans_id _).
Proof.
use make_dep_psh_nat_trans.
- exact (λ x xx ab, ab).
- abstract
(cbn ;
intros x y xx yy f p q ab ;
induction ab ;
cbn ;
apply maponpaths ;
apply dep_psh_mor_path_eq ;
apply idpath).
Defined.
Definition dep_psh_fiber_bincoproducts
(Γ : C^op ⟶ HSET)
: BinCoproducts ((disp_cat_dep_psh C) [{ Γ }]).
Proof.
intros A B.
use make_BinCoproduct.
- exact (coprod_dep_psh A B).
- exact (coprod_dep_psh_inl A B).
- exact (coprod_dep_psh_inr A B).
- intros Z τ₁ τ₂.
use make_iscontr.
+ simple refine (_ ,, _ ,, _).
* exact (coprod_dep_psh_copair τ₁ τ₂).
* abstract
(use dep_psh_nat_trans_eq ;
intros x xx a ;
exact (dep_psh_fiber_comp _ _ _ _)).
* abstract
(use dep_psh_nat_trans_eq ;
intros x xx a ;
exact (dep_psh_fiber_comp _ _ _ _)).
+ abstract
(intros τ ;
use subtypePath ; [ intro ; apply isapropdirprod ; apply homset_property | ] ;
use dep_psh_nat_trans_eq ;
intros x xx ab ;
induction ab as [ a | b ] ;
[ refine (!_ @ maponpaths (λ (z : dep_psh_nat_trans _ _ _), z x xx a) (pr12 τ)) ;
refine (dep_psh_fiber_comp _ _ _ _ @ _) ;
apply idpath
| refine (!_ @ maponpaths (λ (z : dep_psh_nat_trans _ _ _), z x xx b) (pr22 τ)) ;
refine (dep_psh_fiber_comp _ _ _ _ @ _) ;
apply idpath ]).
Defined.
Definition disjoint_dep_psh_fiber_bincoproducts
(Γ : C^op ⟶ HSET)
: disjoint_bincoproducts
(dep_psh_fiber_bincoproducts Γ)
(dep_psh_fiber_initial Γ).
Proof.
intros X Y.
repeat split.
- intros W τ₁ τ₂ p.
use dep_psh_nat_trans_eq.
intros x xx w.
exact (ii1_injectivity
_ _
(!(dep_psh_fiber_comp _ _ _ _)
@ dep_psh_nat_trans_eq_pt p xx w
@ dep_psh_fiber_comp _ _ _ _)).
- intros W τ₁ τ₂ p.
use dep_psh_nat_trans_eq.
intros x xx w.
exact (ii2_injectivity
_ _
(!(dep_psh_fiber_comp _ _ _ _)
@ dep_psh_nat_trans_eq_pt p xx w
@ dep_psh_fiber_comp _ _ _ _)).
- intros W τ₁ τ₂ p.
use make_iscontr.
+ simple refine (_ ,, _).
* use make_dep_psh_nat_trans.
** intros x xx w.
exact (negpathsii1ii2
_ _
(!(dep_psh_fiber_comp _ _ _ _)
@ dep_psh_nat_trans_eq_pt p xx w
@ dep_psh_fiber_comp _ _ _ _)).
** abstract
(intros x y xx yy f q₁ q₂ w ;
apply fromempty ;
exact (negpathsii1ii2
_ _
(!(dep_psh_fiber_comp _ _ _ _)
@ dep_psh_nat_trans_eq_pt p xx w
@ dep_psh_fiber_comp _ _ _ _))).
* abstract
(split ;
use dep_psh_nat_trans_eq ;
intros x xx w ;
apply fromempty ;
exact (negpathsii1ii2
_ _
(!(dep_psh_fiber_comp _ _ _ _)
@ dep_psh_nat_trans_eq_pt p xx w
@ dep_psh_fiber_comp _ _ _ _))).
+ intros θ.
use subtypePath.
{
intro.
apply isapropdirprod ; apply homset_property.
}
use dep_psh_nat_trans_eq.
intros x xx w.
apply fromempty.
exact (negpathsii1ii2
_ _
(!(dep_psh_fiber_comp _ _ _ _)
@ dep_psh_nat_trans_eq_pt p xx w
@ dep_psh_fiber_comp _ _ _ _)).
Qed.
Definition dep_psh_preserves_bincoproduct
{Γ₁ Γ₂ : C^op ⟶ HSET}
(s : Γ₁ ⟹ Γ₂)
: preserves_bincoproduct
(fiber_functor_from_cleaving
(disp_cat_dep_psh C)
(cleaving_disp_cat_dep_psh C)
s).
Proof.
use preserves_bincoproduct_if_preserves_chosen.
{
apply dep_psh_fiber_bincoproducts.
}
intros A B.
use (isBinCoproduct_z_iso
(isBinCoproduct_BinCoproduct _ (dep_psh_fiber_bincoproducts Γ₁ _ _))).
- use make_z_iso.
+ exact (coprod_dep_psh_subst s A B).
+ exact (coprod_dep_psh_subst_inv s A B).
+ abstract
(split ;
use dep_psh_nat_trans_eq ;
intros x xx a ;
refine (dep_psh_fiber_comp _ _ _ _ @ _) ;
cbn ;
apply idpath).
- abstract
(use dep_psh_nat_trans_eq ;
intros x xx a ;
refine (dep_psh_fiber_functor_from_cleaving _ s _ _ @ _) ;
refine (_ @ !(dep_psh_fiber_comp _ _ _ _)) ;
apply idpath).
- abstract
(use dep_psh_nat_trans_eq ;
intros x xx a ;
refine (dep_psh_fiber_functor_from_cleaving _ s _ _ @ _) ;
refine (_ @ !(dep_psh_fiber_comp _ _ _ _)) ;
apply idpath).
Defined.
Definition equalizer_dep_psh
{Γ : C^op ⟶ HSET}
{A B : dep_psh Γ}
(τ₁ τ₂ : dep_psh_nat_trans A B (nat_trans_id _))
: dep_psh Γ.
Proof.
use make_dep_psh.
- exact (λ x xx, ∑ (a : A x xx), hProp_to_hSet (τ₁ x xx a = τ₂ x xx a)%logic)%set.
- intros x y xx yy s p aq.
simple refine (_ ,, _).
+ exact (#d A s p (pr1 aq)).
+ abstract
(refine (dep_psh_nat_trans_ax τ₁ s p p _ @ _) ;
refine (_ @ !(dep_psh_nat_trans_ax τ₂ s p p _)) ;
apply maponpaths ;
exact (pr2 aq)).
- abstract
(intros x xx p a ;
use subtypePath ; [ intro ; apply setproperty | ] ;
apply dep_psh_mor_id).
- abstract
(intros x y z xx yy zz s₁ s₂ p q r a ;
use subtypePath ; [ intro ; apply setproperty | ] ;
apply dep_psh_mor_comp).
Defined.
Definition equalizer_dep_psh_arrow
{Γ : C^op ⟶ HSET}
{A B : dep_psh Γ}
(τ₁ τ₂ : dep_psh_nat_trans A B (nat_trans_id _))
: dep_psh_nat_trans
(equalizer_dep_psh τ₁ τ₂)
A
(nat_trans_id _).
Proof.
use make_dep_psh_nat_trans.
- exact (λ x xx ap, pr1 ap).
- abstract
(intros x y xx yy f p q ap ; cbn ;
apply dep_psh_mor_path_eq ;
apply idpath).
Defined.
Definition equalizer_dep_psh_in
{Γ : C^op ⟶ HSET}
{Z A B : dep_psh Γ}
{τ₁ τ₂ : dep_psh_nat_trans A B (nat_trans_id _)}
(θ : dep_psh_nat_trans Z A (nat_trans_id _))
(q : ∏ (x : C)
(xx : Γ x : hSet)
(z : Z x xx),
τ₁ x xx (θ x xx z) = τ₂ x xx (θ x xx z))
: dep_psh_nat_trans
Z
(equalizer_dep_psh τ₁ τ₂)
(nat_trans_id _).
Proof.
use make_dep_psh_nat_trans.
- exact (λ x xx z, θ x xx z ,, q x xx z).
- abstract
(intros x y xx yy f r₁ r₂ z ; cbn ;
use subtypePath ; [ intro ; apply setproperty | ] ;
cbn ;
apply (dep_psh_nat_trans_ax θ)).
Defined.
Definition equalizer_dep_psh_subst
{Γ₁ Γ₂ : C^op ⟶ HSET}
(s : Γ₁ ⟹ Γ₂)
{A B : dep_psh Γ₂}
(τ₁ τ₂ : dep_psh_nat_trans A B (nat_trans_id _))
: dep_psh_nat_trans
(dep_psh_subst s (equalizer_dep_psh τ₁ τ₂))
(equalizer_dep_psh
(# (fiber_functor_from_cleaving _ (cleaving_disp_cat_dep_psh C) s) τ₁)
(# (fiber_functor_from_cleaving _ (cleaving_disp_cat_dep_psh C) s) τ₂))
(nat_trans_id _).
Proof.
use make_dep_psh_nat_trans.
- refine (λ x xx ap, pr1 ap ,, _).
abstract
(refine (dep_psh_fiber_functor_from_cleaving _ s _ _ @ _) ;
refine (_ @ !(dep_psh_fiber_functor_from_cleaving _ s _ _)) ;
cbn ;
exact (pr2 ap)).
- abstract
(intros x y xx yy f p q ap ;
use subtypePath ; [ intro ; apply setproperty | ] ;
cbn ;
apply dep_psh_mor_path_eq ;
apply idpath).
Defined.
Definition equalizer_dep_psh_subst_inv
{Γ₁ Γ₂ : C^op ⟶ HSET}
(s : Γ₁ ⟹ Γ₂)
{A B : dep_psh Γ₂}
(τ₁ τ₂ : dep_psh_nat_trans A B (nat_trans_id _))
: dep_psh_nat_trans
(equalizer_dep_psh
(# (fiber_functor_from_cleaving _ (cleaving_disp_cat_dep_psh C) s) τ₁)
(# (fiber_functor_from_cleaving _ (cleaving_disp_cat_dep_psh C) s) τ₂))
(dep_psh_subst s (equalizer_dep_psh τ₁ τ₂))
(nat_trans_id _).
Proof.
use make_dep_psh_nat_trans.
- refine (λ x xx ap, pr1 ap ,, _).
abstract
(refine (!(dep_psh_fiber_functor_from_cleaving _ s _ _) @ _) ;
refine (_ @ dep_psh_fiber_functor_from_cleaving _ s _ _) ;
cbn ;
exact (pr2 ap)).
- abstract
(intros x y xx yy f p q ap ;
use subtypePath ; [ intro ; apply setproperty | ] ;
cbn ;
apply dep_psh_mor_path_eq ;
apply idpath).
Defined.
Proposition dep_psh_fiber_equalizers_eq
{Γ : C^op ⟶ HSET}
{A B Z : dep_psh Γ}
(τ₁ τ₂ : dep_psh_nat_trans A B (nat_trans_id _))
(θ : dep_psh_nat_trans Z A (nat_trans_id _))
(p : compose
(C := (disp_cat_dep_psh C) [{ Γ }])
θ τ₁
=
compose
(C := (disp_cat_dep_psh C) [{ Γ }])
θ τ₂)
(x : C)
(xx : (Γ x : hSet))
(z : Z x xx)
: τ₁ x xx (θ x xx z) = τ₂ x xx (θ x xx z).
Proof.
refine (!(dep_psh_fiber_comp _ _ _ _) @ _ @ dep_psh_fiber_comp _ _ _ _).
exact (maponpaths (λ (ζ : dep_psh_nat_trans _ _ _), ζ x xx z) p).
Qed.
Definition dep_psh_fiber_equalizers
(Γ : C^op ⟶ HSET)
: Equalizers ((disp_cat_dep_psh C) [{ Γ }]).
Proof.
intros A B τ₁ τ₂.
use make_Equalizer.
- exact (equalizer_dep_psh τ₁ τ₂).
- exact (equalizer_dep_psh_arrow τ₁ τ₂).
- abstract
(use dep_psh_nat_trans_eq ;
intros x xx a ;
refine (dep_psh_fiber_comp _ _ _ _ @ _) ;
refine (_ @ !(dep_psh_fiber_comp _ _ _ _)) ;
exact (pr2 a)).
- intros Z θ p.
pose (q := dep_psh_fiber_equalizers_eq τ₁ τ₂ θ p).
use make_iscontr.
+ simple refine (_ ,, _).
* exact (equalizer_dep_psh_in θ q).
* abstract
(use dep_psh_nat_trans_eq ;
intros x xx a ;
exact (dep_psh_fiber_comp _ _ _ _)).
+ abstract
(intros τ ;
use subtypePath ; [ intro ; apply homset_property | ] ;
use dep_psh_nat_trans_eq ;
intros x xx a ;
use subtypePath ; [ intro ; apply setproperty | ] ;
refine (!_ @ maponpaths (λ (z : dep_psh_nat_trans _ _ _), z x xx a) (pr2 τ)) ;
refine (dep_psh_fiber_comp _ _ _ _ @ _) ;
apply idpath).
Defined.
Definition dep_psh_preserves_equalizer
{Γ₁ Γ₂ : C^op ⟶ HSET}
(s : Γ₁ ⟹ Γ₂)
: preserves_equalizer
(fiber_functor_from_cleaving
(disp_cat_dep_psh C)
(cleaving_disp_cat_dep_psh C)
s).
Proof.
use preserves_equalizer_if_preserves_chosen.
{
apply dep_psh_fiber_equalizers.
}
intros A B τ₁ τ₂ p.
use (isEqualizer_z_iso (isEqualizer_Equalizer (dep_psh_fiber_equalizers Γ₁ _ _ _ _))).
- use make_z_iso.
+ exact (equalizer_dep_psh_subst s τ₁ τ₂).
+ exact (equalizer_dep_psh_subst_inv s τ₁ τ₂).
+ abstract
(split ;
use dep_psh_nat_trans_eq ;
intros x xx a ;
refine (dep_psh_fiber_comp _ _ _ _ @ _) ;
(use subtypePath ; [ intro ; apply setproperty | ]) ;
cbn ;
apply idpath).
- abstract
(use dep_psh_nat_trans_eq ;
intros x xx a ;
refine (dep_psh_fiber_functor_from_cleaving _ s _ _ @ _) ;
refine (_ @ !(dep_psh_fiber_comp _ _ _ _)) ;
apply idpath).
Defined.
{Γ : C^op ⟶ HSET}
{A B : dep_psh Γ}
(τ₁ τ₂ : dep_psh_nat_trans A B (nat_trans_id _))
: dep_psh Γ.
Proof.
use make_dep_psh.
- exact (λ x xx, ∑ (a : A x xx), hProp_to_hSet (τ₁ x xx a = τ₂ x xx a)%logic)%set.
- intros x y xx yy s p aq.
simple refine (_ ,, _).
+ exact (#d A s p (pr1 aq)).
+ abstract
(refine (dep_psh_nat_trans_ax τ₁ s p p _ @ _) ;
refine (_ @ !(dep_psh_nat_trans_ax τ₂ s p p _)) ;
apply maponpaths ;
exact (pr2 aq)).
- abstract
(intros x xx p a ;
use subtypePath ; [ intro ; apply setproperty | ] ;
apply dep_psh_mor_id).
- abstract
(intros x y z xx yy zz s₁ s₂ p q r a ;
use subtypePath ; [ intro ; apply setproperty | ] ;
apply dep_psh_mor_comp).
Defined.
Definition equalizer_dep_psh_arrow
{Γ : C^op ⟶ HSET}
{A B : dep_psh Γ}
(τ₁ τ₂ : dep_psh_nat_trans A B (nat_trans_id _))
: dep_psh_nat_trans
(equalizer_dep_psh τ₁ τ₂)
A
(nat_trans_id _).
Proof.
use make_dep_psh_nat_trans.
- exact (λ x xx ap, pr1 ap).
- abstract
(intros x y xx yy f p q ap ; cbn ;
apply dep_psh_mor_path_eq ;
apply idpath).
Defined.
Definition equalizer_dep_psh_in
{Γ : C^op ⟶ HSET}
{Z A B : dep_psh Γ}
{τ₁ τ₂ : dep_psh_nat_trans A B (nat_trans_id _)}
(θ : dep_psh_nat_trans Z A (nat_trans_id _))
(q : ∏ (x : C)
(xx : Γ x : hSet)
(z : Z x xx),
τ₁ x xx (θ x xx z) = τ₂ x xx (θ x xx z))
: dep_psh_nat_trans
Z
(equalizer_dep_psh τ₁ τ₂)
(nat_trans_id _).
Proof.
use make_dep_psh_nat_trans.
- exact (λ x xx z, θ x xx z ,, q x xx z).
- abstract
(intros x y xx yy f r₁ r₂ z ; cbn ;
use subtypePath ; [ intro ; apply setproperty | ] ;
cbn ;
apply (dep_psh_nat_trans_ax θ)).
Defined.
Definition equalizer_dep_psh_subst
{Γ₁ Γ₂ : C^op ⟶ HSET}
(s : Γ₁ ⟹ Γ₂)
{A B : dep_psh Γ₂}
(τ₁ τ₂ : dep_psh_nat_trans A B (nat_trans_id _))
: dep_psh_nat_trans
(dep_psh_subst s (equalizer_dep_psh τ₁ τ₂))
(equalizer_dep_psh
(# (fiber_functor_from_cleaving _ (cleaving_disp_cat_dep_psh C) s) τ₁)
(# (fiber_functor_from_cleaving _ (cleaving_disp_cat_dep_psh C) s) τ₂))
(nat_trans_id _).
Proof.
use make_dep_psh_nat_trans.
- refine (λ x xx ap, pr1 ap ,, _).
abstract
(refine (dep_psh_fiber_functor_from_cleaving _ s _ _ @ _) ;
refine (_ @ !(dep_psh_fiber_functor_from_cleaving _ s _ _)) ;
cbn ;
exact (pr2 ap)).
- abstract
(intros x y xx yy f p q ap ;
use subtypePath ; [ intro ; apply setproperty | ] ;
cbn ;
apply dep_psh_mor_path_eq ;
apply idpath).
Defined.
Definition equalizer_dep_psh_subst_inv
{Γ₁ Γ₂ : C^op ⟶ HSET}
(s : Γ₁ ⟹ Γ₂)
{A B : dep_psh Γ₂}
(τ₁ τ₂ : dep_psh_nat_trans A B (nat_trans_id _))
: dep_psh_nat_trans
(equalizer_dep_psh
(# (fiber_functor_from_cleaving _ (cleaving_disp_cat_dep_psh C) s) τ₁)
(# (fiber_functor_from_cleaving _ (cleaving_disp_cat_dep_psh C) s) τ₂))
(dep_psh_subst s (equalizer_dep_psh τ₁ τ₂))
(nat_trans_id _).
Proof.
use make_dep_psh_nat_trans.
- refine (λ x xx ap, pr1 ap ,, _).
abstract
(refine (!(dep_psh_fiber_functor_from_cleaving _ s _ _) @ _) ;
refine (_ @ dep_psh_fiber_functor_from_cleaving _ s _ _) ;
cbn ;
exact (pr2 ap)).
- abstract
(intros x y xx yy f p q ap ;
use subtypePath ; [ intro ; apply setproperty | ] ;
cbn ;
apply dep_psh_mor_path_eq ;
apply idpath).
Defined.
Proposition dep_psh_fiber_equalizers_eq
{Γ : C^op ⟶ HSET}
{A B Z : dep_psh Γ}
(τ₁ τ₂ : dep_psh_nat_trans A B (nat_trans_id _))
(θ : dep_psh_nat_trans Z A (nat_trans_id _))
(p : compose
(C := (disp_cat_dep_psh C) [{ Γ }])
θ τ₁
=
compose
(C := (disp_cat_dep_psh C) [{ Γ }])
θ τ₂)
(x : C)
(xx : (Γ x : hSet))
(z : Z x xx)
: τ₁ x xx (θ x xx z) = τ₂ x xx (θ x xx z).
Proof.
refine (!(dep_psh_fiber_comp _ _ _ _) @ _ @ dep_psh_fiber_comp _ _ _ _).
exact (maponpaths (λ (ζ : dep_psh_nat_trans _ _ _), ζ x xx z) p).
Qed.
Definition dep_psh_fiber_equalizers
(Γ : C^op ⟶ HSET)
: Equalizers ((disp_cat_dep_psh C) [{ Γ }]).
Proof.
intros A B τ₁ τ₂.
use make_Equalizer.
- exact (equalizer_dep_psh τ₁ τ₂).
- exact (equalizer_dep_psh_arrow τ₁ τ₂).
- abstract
(use dep_psh_nat_trans_eq ;
intros x xx a ;
refine (dep_psh_fiber_comp _ _ _ _ @ _) ;
refine (_ @ !(dep_psh_fiber_comp _ _ _ _)) ;
exact (pr2 a)).
- intros Z θ p.
pose (q := dep_psh_fiber_equalizers_eq τ₁ τ₂ θ p).
use make_iscontr.
+ simple refine (_ ,, _).
* exact (equalizer_dep_psh_in θ q).
* abstract
(use dep_psh_nat_trans_eq ;
intros x xx a ;
exact (dep_psh_fiber_comp _ _ _ _)).
+ abstract
(intros τ ;
use subtypePath ; [ intro ; apply homset_property | ] ;
use dep_psh_nat_trans_eq ;
intros x xx a ;
use subtypePath ; [ intro ; apply setproperty | ] ;
refine (!_ @ maponpaths (λ (z : dep_psh_nat_trans _ _ _), z x xx a) (pr2 τ)) ;
refine (dep_psh_fiber_comp _ _ _ _ @ _) ;
apply idpath).
Defined.
Definition dep_psh_preserves_equalizer
{Γ₁ Γ₂ : C^op ⟶ HSET}
(s : Γ₁ ⟹ Γ₂)
: preserves_equalizer
(fiber_functor_from_cleaving
(disp_cat_dep_psh C)
(cleaving_disp_cat_dep_psh C)
s).
Proof.
use preserves_equalizer_if_preserves_chosen.
{
apply dep_psh_fiber_equalizers.
}
intros A B τ₁ τ₂ p.
use (isEqualizer_z_iso (isEqualizer_Equalizer (dep_psh_fiber_equalizers Γ₁ _ _ _ _))).
- use make_z_iso.
+ exact (equalizer_dep_psh_subst s τ₁ τ₂).
+ exact (equalizer_dep_psh_subst_inv s τ₁ τ₂).
+ abstract
(split ;
use dep_psh_nat_trans_eq ;
intros x xx a ;
refine (dep_psh_fiber_comp _ _ _ _ @ _) ;
(use subtypePath ; [ intro ; apply setproperty | ]) ;
cbn ;
apply idpath).
- abstract
(use dep_psh_nat_trans_eq ;
intros x xx a ;
refine (dep_psh_fiber_functor_from_cleaving _ s _ _ @ _) ;
refine (_ @ !(dep_psh_fiber_comp _ _ _ _)) ;
apply idpath).
Defined.
Definition constant_dep_psh
(Γ : C^op ⟶ HSET)
(A : hSet)
: dep_psh Γ.
Proof.
use make_dep_psh.
- exact (λ _ _, A).
- exact (λ x y xx yy s p a, a).
- abstract
(intros ; apply idpath).
- abstract
(intros ; apply idpath).
Defined.
Definition constant_dep_psh_el
{Γ : C^op ⟶ HSET}
(A : dep_psh Γ)
{B : hSet}
(b : B)
: dep_psh_nat_trans A (constant_dep_psh Γ B) (nat_trans_id _).
Proof.
use make_dep_psh_nat_trans.
- exact (λ _ _ _, b).
- abstract
(intro ; intros ; cbn ;
apply idpath).
Defined.
Definition constant_dep_psh_map
{Γ : C^op ⟶ HSET}
{A B : hSet}
(f : A → B)
: dep_psh_nat_trans
(constant_dep_psh Γ A)
(constant_dep_psh Γ B)
(nat_trans_id _).
Proof.
use make_dep_psh_nat_trans.
- exact (λ x xx a, f a).
- abstract
(intro ; intros ; cbn ;
apply idpath).
Defined.
Definition constant_dep_psh_functor_data
(Γ : C^op ⟶ HSET)
: functor_data SET (disp_cat_dep_psh C)[{Γ}].
Proof.
use make_functor_data.
- exact (constant_dep_psh Γ).
- exact (λ (A B : hSet) (f : A → B), constant_dep_psh_map f).
Defined.
Proposition constant_dep_psh_functor_laws
(Γ : C^op ⟶ HSET)
: is_functor (constant_dep_psh_functor_data Γ).
Proof.
split.
- intro ; intros.
use dep_psh_nat_trans_eq ; intros ; cbn.
apply idpath.
- intro ; intros.
use dep_psh_nat_trans_eq ; intros.
rewrite dep_psh_fiber_comp.
cbn.
apply idpath.
Qed.
Definition constant_dep_psh_functor
(Γ : C^op ⟶ HSET)
: HSET ⟶ (disp_cat_dep_psh C)[{ Γ }].
Proof.
use make_functor.
- exact (constant_dep_psh_functor_data Γ).
- exact (constant_dep_psh_functor_laws Γ).
Defined.
Proposition preserves_terminal_constant_dep_psh_functor
(Γ : C^op ⟶ HSET)
: preserves_terminal (constant_dep_psh_functor Γ).
Proof.
use preserves_terminal_if_preserves_chosen.
{
exact TerminalHSET.
}
use iso_to_Terminal.
{
apply dep_psh_fiber_terminal.
}
use make_z_iso.
- use make_dep_psh_nat_trans.
+ exact (λ x xx z, z).
+ abstract
(intro ; intros ; cbn ;
apply isapropunit).
- use make_dep_psh_nat_trans.
+ exact (λ x xx ab, ab).
+ abstract
(intro ; intros ; cbn ;
apply isapropunit).
- split.
+ abstract
(use dep_psh_nat_trans_eq ;
intros x xx a ;
apply isapropunit).
+ abstract
(use dep_psh_nat_trans_eq ;
intros x xx a ;
apply isapropunit).
Qed.
Proposition preserves_binproduct_constant_dep_psh_functor
(Γ : C^op ⟶ HSET)
: preserves_binproduct (constant_dep_psh_functor Γ).
Proof.
use preserves_binproduct_if_preserves_chosen.
{
exact BinProductsHSET.
}
intros A B.
use (isBinProduct_z_iso (isBinProduct_BinProduct _ (dep_psh_fiber_binproducts Γ _ _))).
- use make_z_iso.
+ use make_dep_psh_nat_trans.
* exact (λ x xx ab, ab).
* abstract
(intro ; intros ; cbn ;
apply idpath).
+ use make_dep_psh_nat_trans.
* exact (λ x xx ab, ab).
* abstract
(intro ; intros ; cbn ;
apply idpath).
+ abstract
(split ;
use dep_psh_nat_trans_eq ;
intros ;
exact (dep_psh_fiber_comp _ _ _ _)).
- use dep_psh_nat_trans_eq.
intros.
refine (_ @ !(dep_psh_fiber_comp _ _ _ _)) ; cbn.
apply idpath.
- use dep_psh_nat_trans_eq.
intros.
refine (_ @ !(dep_psh_fiber_comp _ _ _ _)) ; cbn.
apply idpath.
Qed.
Proposition preserves_equalizer_constant_dep_psh_functor
(Γ : C^op ⟶ HSET)
: preserves_equalizer (constant_dep_psh_functor Γ).
Proof.
use preserves_equalizer_if_preserves_chosen.
{
exact Equalizers_in_HSET.
}
intros A B τ₁ τ₂ p.
use (isEqualizer_z_iso (isEqualizer_Equalizer (dep_psh_fiber_equalizers Γ _ _ _ _))).
- use make_z_iso.
+ use make_dep_psh_nat_trans.
* exact (λ x xx ab, ab).
* abstract
(intro ; intros ;
use subtypePath ;
[ intro ; apply setproperty | ] ;
apply idpath).
+ use make_dep_psh_nat_trans.
* exact (λ x xx ab, ab).
* abstract
(intro ; intros ;
use subtypePath ;
[ intro ; apply setproperty | ] ;
apply idpath).
+ abstract
(split ;
use dep_psh_nat_trans_eq ;
intros ;
exact (dep_psh_fiber_comp _ _ _ _)).
- use dep_psh_nat_trans_eq.
intros.
refine (_ @ !(dep_psh_fiber_comp _ _ _ _)) ; cbn.
apply idpath.
Qed.
Section ConstantAdjoint.
Context {Γ : C^op ⟶ HSET}
(A : dep_psh Γ).
Definition dep_psh_limit
: hSet.
Proof.
use make_hSet.
- exact (dep_psh_nat_trans (unit_dep_psh _) A (nat_trans_id _)).
- abstract
(apply isaset_nat_trans ;
apply homset_property).
Defined.
Definition constant_dep_psh_limit
: dep_psh_nat_trans (constant_dep_psh Γ dep_psh_limit) A (nat_trans_id _).
Proof.
use make_dep_psh_nat_trans.
- exact (λ (x : C) (xx : (Γ x : hSet)) (ff : dep_psh_nat_trans _ _ _), ff x xx tt).
- abstract
(intros x y xx yy f p q ff ;
cbn in * ;
exact (dep_psh_nat_trans_ax ff f p q tt)).
Defined.
Definition dep_psh_limit_map
{B : hSet}
(τ : dep_psh_nat_trans (constant_dep_psh Γ B) A (nat_trans_id _))
(b : B)
: dep_psh_nat_trans (unit_dep_psh Γ) A (nat_trans_id Γ).
Proof.
use make_dep_psh_nat_trans.
- exact (λ x xx _, τ x xx b).
- abstract
(intros x y xx yy f p q _ ;
cbn in * ;
exact (dep_psh_nat_trans_ax τ f p q b)).
Defined.
End ConstantAdjoint.
Definition is_left_adjoint_constant_dep_psh_functor
(Γ : C^op ⟶ HSET)
: is_left_adjoint (constant_dep_psh_functor Γ).
Proof.
use coreflections_to_is_left_adjoint ; cbn.
intros A.
use make_coreflection.
- use make_coreflection_data.
+ exact (dep_psh_limit A).
+ exact (constant_dep_psh_limit A).
- intros W.
use make_iscontr.
+ simple refine (_ ,, _).
* exact (dep_psh_limit_map A (coreflection_data_arrow W)).
* abstract
(use dep_psh_nat_trans_eq ;
intros x xx a ;
refine (_ @ !(dep_psh_fiber_comp _ _ _ _)) ; cbn ;
apply idpath).
+ abstract
(intros τ ;
use subtypePath ;
[ intro ; apply homset_property | ] ;
induction τ as [ τ p ] ;
cbn in τ ;
use funextsec ;
intro b ;
use dep_psh_nat_trans_eq ;
intros x xx z ;
induction z ;
cbn ;
rewrite p ;
refine (_ @ !(dep_psh_fiber_comp _ _ _ _)) ;
cbn ;
apply idpath).
Defined.
(Γ : C^op ⟶ HSET)
(A : hSet)
: dep_psh Γ.
Proof.
use make_dep_psh.
- exact (λ _ _, A).
- exact (λ x y xx yy s p a, a).
- abstract
(intros ; apply idpath).
- abstract
(intros ; apply idpath).
Defined.
Definition constant_dep_psh_el
{Γ : C^op ⟶ HSET}
(A : dep_psh Γ)
{B : hSet}
(b : B)
: dep_psh_nat_trans A (constant_dep_psh Γ B) (nat_trans_id _).
Proof.
use make_dep_psh_nat_trans.
- exact (λ _ _ _, b).
- abstract
(intro ; intros ; cbn ;
apply idpath).
Defined.
Definition constant_dep_psh_map
{Γ : C^op ⟶ HSET}
{A B : hSet}
(f : A → B)
: dep_psh_nat_trans
(constant_dep_psh Γ A)
(constant_dep_psh Γ B)
(nat_trans_id _).
Proof.
use make_dep_psh_nat_trans.
- exact (λ x xx a, f a).
- abstract
(intro ; intros ; cbn ;
apply idpath).
Defined.
Definition constant_dep_psh_functor_data
(Γ : C^op ⟶ HSET)
: functor_data SET (disp_cat_dep_psh C)[{Γ}].
Proof.
use make_functor_data.
- exact (constant_dep_psh Γ).
- exact (λ (A B : hSet) (f : A → B), constant_dep_psh_map f).
Defined.
Proposition constant_dep_psh_functor_laws
(Γ : C^op ⟶ HSET)
: is_functor (constant_dep_psh_functor_data Γ).
Proof.
split.
- intro ; intros.
use dep_psh_nat_trans_eq ; intros ; cbn.
apply idpath.
- intro ; intros.
use dep_psh_nat_trans_eq ; intros.
rewrite dep_psh_fiber_comp.
cbn.
apply idpath.
Qed.
Definition constant_dep_psh_functor
(Γ : C^op ⟶ HSET)
: HSET ⟶ (disp_cat_dep_psh C)[{ Γ }].
Proof.
use make_functor.
- exact (constant_dep_psh_functor_data Γ).
- exact (constant_dep_psh_functor_laws Γ).
Defined.
Proposition preserves_terminal_constant_dep_psh_functor
(Γ : C^op ⟶ HSET)
: preserves_terminal (constant_dep_psh_functor Γ).
Proof.
use preserves_terminal_if_preserves_chosen.
{
exact TerminalHSET.
}
use iso_to_Terminal.
{
apply dep_psh_fiber_terminal.
}
use make_z_iso.
- use make_dep_psh_nat_trans.
+ exact (λ x xx z, z).
+ abstract
(intro ; intros ; cbn ;
apply isapropunit).
- use make_dep_psh_nat_trans.
+ exact (λ x xx ab, ab).
+ abstract
(intro ; intros ; cbn ;
apply isapropunit).
- split.
+ abstract
(use dep_psh_nat_trans_eq ;
intros x xx a ;
apply isapropunit).
+ abstract
(use dep_psh_nat_trans_eq ;
intros x xx a ;
apply isapropunit).
Qed.
Proposition preserves_binproduct_constant_dep_psh_functor
(Γ : C^op ⟶ HSET)
: preserves_binproduct (constant_dep_psh_functor Γ).
Proof.
use preserves_binproduct_if_preserves_chosen.
{
exact BinProductsHSET.
}
intros A B.
use (isBinProduct_z_iso (isBinProduct_BinProduct _ (dep_psh_fiber_binproducts Γ _ _))).
- use make_z_iso.
+ use make_dep_psh_nat_trans.
* exact (λ x xx ab, ab).
* abstract
(intro ; intros ; cbn ;
apply idpath).
+ use make_dep_psh_nat_trans.
* exact (λ x xx ab, ab).
* abstract
(intro ; intros ; cbn ;
apply idpath).
+ abstract
(split ;
use dep_psh_nat_trans_eq ;
intros ;
exact (dep_psh_fiber_comp _ _ _ _)).
- use dep_psh_nat_trans_eq.
intros.
refine (_ @ !(dep_psh_fiber_comp _ _ _ _)) ; cbn.
apply idpath.
- use dep_psh_nat_trans_eq.
intros.
refine (_ @ !(dep_psh_fiber_comp _ _ _ _)) ; cbn.
apply idpath.
Qed.
Proposition preserves_equalizer_constant_dep_psh_functor
(Γ : C^op ⟶ HSET)
: preserves_equalizer (constant_dep_psh_functor Γ).
Proof.
use preserves_equalizer_if_preserves_chosen.
{
exact Equalizers_in_HSET.
}
intros A B τ₁ τ₂ p.
use (isEqualizer_z_iso (isEqualizer_Equalizer (dep_psh_fiber_equalizers Γ _ _ _ _))).
- use make_z_iso.
+ use make_dep_psh_nat_trans.
* exact (λ x xx ab, ab).
* abstract
(intro ; intros ;
use subtypePath ;
[ intro ; apply setproperty | ] ;
apply idpath).
+ use make_dep_psh_nat_trans.
* exact (λ x xx ab, ab).
* abstract
(intro ; intros ;
use subtypePath ;
[ intro ; apply setproperty | ] ;
apply idpath).
+ abstract
(split ;
use dep_psh_nat_trans_eq ;
intros ;
exact (dep_psh_fiber_comp _ _ _ _)).
- use dep_psh_nat_trans_eq.
intros.
refine (_ @ !(dep_psh_fiber_comp _ _ _ _)) ; cbn.
apply idpath.
Qed.
Section ConstantAdjoint.
Context {Γ : C^op ⟶ HSET}
(A : dep_psh Γ).
Definition dep_psh_limit
: hSet.
Proof.
use make_hSet.
- exact (dep_psh_nat_trans (unit_dep_psh _) A (nat_trans_id _)).
- abstract
(apply isaset_nat_trans ;
apply homset_property).
Defined.
Definition constant_dep_psh_limit
: dep_psh_nat_trans (constant_dep_psh Γ dep_psh_limit) A (nat_trans_id _).
Proof.
use make_dep_psh_nat_trans.
- exact (λ (x : C) (xx : (Γ x : hSet)) (ff : dep_psh_nat_trans _ _ _), ff x xx tt).
- abstract
(intros x y xx yy f p q ff ;
cbn in * ;
exact (dep_psh_nat_trans_ax ff f p q tt)).
Defined.
Definition dep_psh_limit_map
{B : hSet}
(τ : dep_psh_nat_trans (constant_dep_psh Γ B) A (nat_trans_id _))
(b : B)
: dep_psh_nat_trans (unit_dep_psh Γ) A (nat_trans_id Γ).
Proof.
use make_dep_psh_nat_trans.
- exact (λ x xx _, τ x xx b).
- abstract
(intros x y xx yy f p q _ ;
cbn in * ;
exact (dep_psh_nat_trans_ax τ f p q b)).
Defined.
End ConstantAdjoint.
Definition is_left_adjoint_constant_dep_psh_functor
(Γ : C^op ⟶ HSET)
: is_left_adjoint (constant_dep_psh_functor Γ).
Proof.
use coreflections_to_is_left_adjoint ; cbn.
intros A.
use make_coreflection.
- use make_coreflection_data.
+ exact (dep_psh_limit A).
+ exact (constant_dep_psh_limit A).
- intros W.
use make_iscontr.
+ simple refine (_ ,, _).
* exact (dep_psh_limit_map A (coreflection_data_arrow W)).
* abstract
(use dep_psh_nat_trans_eq ;
intros x xx a ;
refine (_ @ !(dep_psh_fiber_comp _ _ _ _)) ; cbn ;
apply idpath).
+ abstract
(intros τ ;
use subtypePath ;
[ intro ; apply homset_property | ] ;
induction τ as [ τ p ] ;
cbn in τ ;
use funextsec ;
intro b ;
use dep_psh_nat_trans_eq ;
intros x xx z ;
induction z ;
cbn ;
rewrite p ;
refine (_ @ !(dep_psh_fiber_comp _ _ _ _)) ;
cbn ;
apply idpath).
Defined.
Definition psh_to_dep_psh
(Γ : C^op ⟶ HSET)
: dep_psh (constant_functor C^op HSET unitHSET).
Proof.
use make_dep_psh.
- exact (λ x _, (Γ x : hSet)).
- exact (λ x y _ _ f p a, #Γ f a).
- abstract
(intros x ? ? a ; cbn ;
exact (eqtohomot (functor_id Γ _) a)).
- abstract
(intros x y z ? ? ? s₁ s₂ ? ? ? a ;
exact (eqtohomot (functor_comp Γ _ _) a)).
Defined.
Definition psh_to_dep_psh_z_iso_mor
(Γ : C^op ⟶ HSET)
: Γ ⟹ total_psh (psh_to_dep_psh Γ).
Proof.
use make_nat_trans.
- exact (λ x xx, tt ,, xx).
- abstract
(intros x y f ;
apply idpath).
Defined.
Definition psh_to_dep_psh_z_iso_inv
(Γ : C^op ⟶ HSET)
: total_psh (psh_to_dep_psh Γ) ⟹ Γ.
Proof.
use make_nat_trans.
- exact (λ x xx, pr2 xx).
- abstract
(intros x y f ;
apply idpath).
Defined.
Definition psh_to_dep_psh_z_iso
(Γ : C^op ⟶ HSET)
: z_iso (C := PreShv C) Γ (total_psh (psh_to_dep_psh Γ)).
Proof.
use make_z_iso.
- exact (psh_to_dep_psh_z_iso_mor Γ).
- exact (psh_to_dep_psh_z_iso_inv Γ).
- abstract
(split ;
(use nat_trans_eq ; [ apply homset_property | ]) ;
intros ; cbn ; [ apply idpath | ] ;
use funextsec ;
intro xx ;
induction xx as [ [ ] xx ] ;
cbn ;
apply idpath).
Defined.
(Γ : C^op ⟶ HSET)
: dep_psh (constant_functor C^op HSET unitHSET).
Proof.
use make_dep_psh.
- exact (λ x _, (Γ x : hSet)).
- exact (λ x y _ _ f p a, #Γ f a).
- abstract
(intros x ? ? a ; cbn ;
exact (eqtohomot (functor_id Γ _) a)).
- abstract
(intros x y z ? ? ? s₁ s₂ ? ? ? a ;
exact (eqtohomot (functor_comp Γ _ _) a)).
Defined.
Definition psh_to_dep_psh_z_iso_mor
(Γ : C^op ⟶ HSET)
: Γ ⟹ total_psh (psh_to_dep_psh Γ).
Proof.
use make_nat_trans.
- exact (λ x xx, tt ,, xx).
- abstract
(intros x y f ;
apply idpath).
Defined.
Definition psh_to_dep_psh_z_iso_inv
(Γ : C^op ⟶ HSET)
: total_psh (psh_to_dep_psh Γ) ⟹ Γ.
Proof.
use make_nat_trans.
- exact (λ x xx, pr2 xx).
- abstract
(intros x y f ;
apply idpath).
Defined.
Definition psh_to_dep_psh_z_iso
(Γ : C^op ⟶ HSET)
: z_iso (C := PreShv C) Γ (total_psh (psh_to_dep_psh Γ)).
Proof.
use make_z_iso.
- exact (psh_to_dep_psh_z_iso_mor Γ).
- exact (psh_to_dep_psh_z_iso_inv Γ).
- abstract
(split ;
(use nat_trans_eq ; [ apply homset_property | ]) ;
intros ; cbn ; [ apply idpath | ] ;
use funextsec ;
intro xx ;
induction xx as [ [ ] xx ] ;
cbn ;
apply idpath).
Defined.
Definition mor_dep_psh
{Γ : C^op ⟶ HSET}
{x : C}
(xx : (Γ x : hSet))
: dep_psh Γ.
Proof.
use make_dep_psh.
- intros y yy.
use make_hSet.
+ exact (∑ (f : y --> x), #Γ f xx = yy).
+ abstract
(use isaset_total2 ; [ apply homset_property | ] ;
intro ;
apply isasetaprop ;
apply setproperty).
- intros y₁ y₂ yy₁ yy₂ s p a.
refine (s · pr1 a ,, _).
abstract
(cbn in a ;
refine (_ @ p) ;
refine (eqtohomot (functor_comp Γ _ _) _ @ _) ;
cbn ;
apply maponpaths ;
exact (pr2 a)).
- abstract
(intros y yy p a ;
use subtypePath ; [ intro ; apply setproperty | ] ;
cbn ;
apply id_left).
- abstract
(intros y₁ y₂ y₃ yy₁ yy₂ yy₃ s₁ s₂ p q r a ;
use subtypePath ; [ intro ; apply setproperty | ] ;
cbn ;
apply assoc').
Defined.
Definition id_mor_dep_psh
{Γ : C^op ⟶ HSET}
{x : C}
(xx : (Γ x : hSet))
: mor_dep_psh xx x xx.
Proof.
refine (identity _ ,, _).
exact (eqtohomot (functor_id Γ _) _).
Defined.
Definition dep_psh_nat_trans_from_mor_dep_psh
{Γ : C^op ⟶ HSET}
{A : dep_psh Γ}
{x : C}
{xx : (Γ x : hSet)}
(a : A x xx)
: dep_psh_nat_trans (mor_dep_psh xx) A (nat_trans_id _).
Proof.
use make_dep_psh_nat_trans.
- exact (λ y yy b, #d A (pr1 b) (pr2 b) a).
- abstract
(intros y₁ y₂ yy₁ yy₂ f p q b ;
cbn ;
rewrite dep_psh_mor_comp' ;
apply dep_psh_mor_path_eq ;
apply idpath).
Defined.
{Γ : C^op ⟶ HSET}
{x : C}
(xx : (Γ x : hSet))
: dep_psh Γ.
Proof.
use make_dep_psh.
- intros y yy.
use make_hSet.
+ exact (∑ (f : y --> x), #Γ f xx = yy).
+ abstract
(use isaset_total2 ; [ apply homset_property | ] ;
intro ;
apply isasetaprop ;
apply setproperty).
- intros y₁ y₂ yy₁ yy₂ s p a.
refine (s · pr1 a ,, _).
abstract
(cbn in a ;
refine (_ @ p) ;
refine (eqtohomot (functor_comp Γ _ _) _ @ _) ;
cbn ;
apply maponpaths ;
exact (pr2 a)).
- abstract
(intros y yy p a ;
use subtypePath ; [ intro ; apply setproperty | ] ;
cbn ;
apply id_left).
- abstract
(intros y₁ y₂ y₃ yy₁ yy₂ yy₃ s₁ s₂ p q r a ;
use subtypePath ; [ intro ; apply setproperty | ] ;
cbn ;
apply assoc').
Defined.
Definition id_mor_dep_psh
{Γ : C^op ⟶ HSET}
{x : C}
(xx : (Γ x : hSet))
: mor_dep_psh xx x xx.
Proof.
refine (identity _ ,, _).
exact (eqtohomot (functor_id Γ _) _).
Defined.
Definition dep_psh_nat_trans_from_mor_dep_psh
{Γ : C^op ⟶ HSET}
{A : dep_psh Γ}
{x : C}
{xx : (Γ x : hSet)}
(a : A x xx)
: dep_psh_nat_trans (mor_dep_psh xx) A (nat_trans_id _).
Proof.
use make_dep_psh_nat_trans.
- exact (λ y yy b, #d A (pr1 b) (pr2 b) a).
- abstract
(intros y₁ y₂ yy₁ yy₂ f p q b ;
cbn ;
rewrite dep_psh_mor_comp' ;
apply dep_psh_mor_path_eq ;
apply idpath).
Defined.
Section Image.
Context {A B : C^op ⟶ HSET}
(τ : A ⟹ B).
Definition psh_nat_trans_im_data
: functor_data C^op SET.
Proof.
use make_functor_data.
- exact (λ x,
∑ (yy : (B x : hSet)),
hProp_to_hSet (∃ (xx : (A x : hSet)), τ x xx = yy))%set%logic.
- intros x y f yy.
refine (#B f (pr1 yy) ,, _).
abstract
(induction yy as [ yy p ] ;
revert p ;
cbn -[hProp_to_hSet] ;
use factor_through_squash_hProp ;
intros (xx & p) ;
use hinhpr ;
refine (#A f xx ,, _) ;
rewrite <- p ;
exact (eqtohomot (nat_trans_ax τ _ _ f) xx)).
Defined.
Proposition psh_nat_trans_im_laws
: is_functor psh_nat_trans_im_data.
Proof.
split.
- intros x.
use funextsec.
intros xx.
use subtypePath_prop.
cbn.
exact (eqtohomot (functor_id B x) (pr1 xx)).
- intros x y z f g.
use funextsec.
intros xx.
use subtypePath_prop.
cbn.
exact (eqtohomot (functor_comp B f g) (pr1 xx)).
Qed.
Definition psh_nat_trans_im
: C^op ⟶ HSET.
Proof.
use make_functor.
- exact psh_nat_trans_im_data.
- exact psh_nat_trans_im_laws.
Defined.
Definition psh_nat_trans_to_im
: A ⟹ psh_nat_trans_im.
Proof.
use make_nat_trans.
- refine (λ x xx, τ x xx ,, _).
abstract
(use hinhpr ;
refine (xx ,, _) ;
apply idpath).
- abstract
(intros x y f ;
use funextsec ;
intro xx ;
use subtypePath_prop ;
cbn ;
exact (eqtohomot (nat_trans_ax τ _ _ f) xx)).
Defined.
Definition psh_nat_trans_im_incl
: psh_nat_trans_im ⟹ B.
Proof.
use make_nat_trans.
- exact (λ x xx, pr1 xx).
- abstract
(intros x y f ;
apply idpath).
Defined.
Proposition isMonic_psh_nat_trans_im_incl
: isMonic (C := PreShv C) psh_nat_trans_im_incl.
Proof.
intros Z θ₁ θ₂ p.
use nat_trans_eq.
{
apply homset_property.
}
intro x.
use funextsec.
intro xx.
use subtypePath_prop.
exact (eqtohomot (nat_trans_eq_pointwise p x) xx).
Qed.
Definition psh_nat_trans_im_incl_monic
: Monic (PreShv C) psh_nat_trans_im B.
Proof.
use make_Monic.
- exact psh_nat_trans_im_incl.
- exact isMonic_psh_nat_trans_im_incl.
Defined.
Proposition psh_nat_trans_im_comm
: nat_trans_comp
_ _ _
psh_nat_trans_to_im
psh_nat_trans_im_incl
=
τ.
Proof.
use nat_trans_eq.
{
apply homset_property.
}
intro x.
cbn.
apply idpath.
Qed.
Section MapFromImage.
Context {Z : C^op ⟶ HSET}
(θ : A ⟹ Z)
(p : ∏ (x : C)
(a₁ a₂ : (A x : hSet)),
τ x a₁ = τ x a₂ → θ x a₁ = θ x a₂).
Proposition map_from_psh_nat_trans_im_unique
{x : C}
(b : (psh_nat_trans_im x : hSet))
: ∃! (z : (Z x : hSet)),
∏ (y : C)
(g : y --> x)
(a : (A y : hSet)),
τ y a = #B g (pr1 b)
→ θ y a = #Z g z.
Proof.
induction b as [ b q ].
revert q.
cbn -[hProp_to_hSet].
use factor_through_squash.
- apply isapropiscontr.
- intros (a & q).
use make_iscontr.
+ refine (θ x a ,, _).
intros y g a' r.
refine (_ @ eqtohomot (nat_trans_ax θ _ _ g) a).
cbn.
use p.
refine (r @ _).
refine (_ @ eqtohomot (!(nat_trans_ax τ _ _ g)) a).
cbn.
apply maponpaths.
exact (!q).
+ intros z.
use subtypePath.
{
intro.
do 4 (use impred ; intro).
apply setproperty.
}
cbn.
refine (_ @ !(pr2 z _ (identity _) _ _)).
* refine (!_).
exact (eqtohomot (functor_id Z _) _).
* refine (_ @ !(eqtohomot (functor_id B _) _)).
exact q.
Qed.
Definition map_from_psh_nat_trans_im_el
{x : C}
(b : (psh_nat_trans_im x : hSet))
: (Z x : hSet)
:= pr11 (map_from_psh_nat_trans_im_unique b).
Proposition map_from_psh_nat_trans_im_el_eq
{x : C}
(b : (psh_nat_trans_im x : hSet))
{y : C}
(g : y --> x)
(a : (A y : hSet))
(q : τ y a = #B g (pr1 b))
: θ y a = #Z g (map_from_psh_nat_trans_im_el b).
Proof.
exact (pr21 (map_from_psh_nat_trans_im_unique b) y g a q).
Qed.
Proposition map_from_psh_nat_trans_im_unique_eq
{x : C}
(b : (psh_nat_trans_im x : hSet))
{z₁ z₂ : (Z x : hSet)}
(q₁ : ∏ (y : C)
(g : y --> x)
(a : (A y : hSet)),
τ y a = #B g (pr1 b)
→ θ y a = #Z g z₁)
(q₂ : ∏ (y : C)
(g : y --> x)
(a : (A y : hSet)),
τ y a = #B g (pr1 b)
→ θ y a = #Z g z₂)
: z₁ = z₂.
Proof.
exact (maponpaths
pr1
(proofirrelevance
_
(isapropifcontr
(map_from_psh_nat_trans_im_unique b))
(z₁ ,, q₁)
(z₂ ,, q₂))).
Qed.
Definition map_from_psh_nat_trans_im_data
: nat_trans_data psh_nat_trans_im Z
:= λ x b, map_from_psh_nat_trans_im_el b.
Arguments map_from_psh_nat_trans_im_data /.
Proposition map_from_psh_nat_trans_im_laws
: is_nat_trans _ _ map_from_psh_nat_trans_im_data.
Proof.
intros x y f.
use funextsec.
intro b.
induction b as [ b q ].
use map_from_psh_nat_trans_im_unique_eq.
- refine (#B f b ,, _).
abstract
(revert q ;
use factor_through_squash_hProp ;
intros (a & r) ;
use hinhpr ;
refine (#A f a ,, _) ;
refine (eqtohomot (nat_trans_ax τ _ _ f) a @ _) ;
cbn ;
apply maponpaths ;
exact r).
- cbn.
intros z g a r.
refine (map_from_psh_nat_trans_im_el_eq _ _ _ _).
cbn.
exact r.
- cbn.
intros z g a r.
refine (map_from_psh_nat_trans_im_el_eq (b,, q) (g · f) a _ @ _).
+ refine (r @ !_).
cbn.
exact (eqtohomot (functor_comp B f g) b).
+ exact (eqtohomot (functor_comp Z f g) _).
Qed.
Definition map_from_psh_nat_trans_im
: psh_nat_trans_im ⟹ Z.
Proof.
use make_nat_trans.
- exact map_from_psh_nat_trans_im_data.
- exact map_from_psh_nat_trans_im_laws.
Defined.
Proposition map_from_psh_nat_trans_im_comm_pt
{x : C}
(a : (A x : hSet))
: map_from_psh_nat_trans_im x (psh_nat_trans_to_im x a) = θ x a.
Proof.
cbn.
refine (!_).
refine (_ @ eqtohomot (functor_id Z _) _).
use map_from_psh_nat_trans_im_el_eq.
refine (_ @ !(eqtohomot (functor_id B _) _)).
cbn.
apply idpath.
Qed.
Proposition map_from_psh_nat_trans_im_comm
: nat_trans_comp
_ _ _
psh_nat_trans_to_im
map_from_psh_nat_trans_im
=
θ.
Proof.
use nat_trans_eq.
{
apply homset_property.
}
intros x.
use funextsec.
intro a.
exact (map_from_psh_nat_trans_im_comm_pt a).
Qed.
Proposition map_from_psh_nat_trans_im_unique_mor
{ζ₁ ζ₂ : psh_nat_trans_im ⟹ Z}
(q₁ : nat_trans_comp
_ _ _
psh_nat_trans_to_im
ζ₁
=
θ)
(q₂ : nat_trans_comp
_ _ _
psh_nat_trans_to_im
ζ₂
=
θ)
: ζ₁ = ζ₂.
Proof.
use nat_trans_eq.
{
apply homset_property.
}
intro x.
use funextsec.
intro b.
use map_from_psh_nat_trans_im_unique_eq.
- exact b.
- intros y g a r.
refine (_ @ eqtohomot (nat_trans_ax ζ₁ _ _ g) b).
cbn.
refine (!_).
refine (_ @ eqtohomot (nat_trans_eq_pointwise q₁ y) a).
cbn.
apply maponpaths.
use subtypePath_prop.
cbn.
exact (!r).
- intros y g a r.
refine (_ @ eqtohomot (nat_trans_ax ζ₂ _ _ g) b).
cbn.
refine (!_).
refine (_ @ eqtohomot (nat_trans_eq_pointwise q₂ y) a).
cbn.
apply maponpaths.
use subtypePath_prop.
cbn.
exact (!r).
Qed.
End MapFromImage.
End Image.
End ExamplesDepPsh.
Context {A B : C^op ⟶ HSET}
(τ : A ⟹ B).
Definition psh_nat_trans_im_data
: functor_data C^op SET.
Proof.
use make_functor_data.
- exact (λ x,
∑ (yy : (B x : hSet)),
hProp_to_hSet (∃ (xx : (A x : hSet)), τ x xx = yy))%set%logic.
- intros x y f yy.
refine (#B f (pr1 yy) ,, _).
abstract
(induction yy as [ yy p ] ;
revert p ;
cbn -[hProp_to_hSet] ;
use factor_through_squash_hProp ;
intros (xx & p) ;
use hinhpr ;
refine (#A f xx ,, _) ;
rewrite <- p ;
exact (eqtohomot (nat_trans_ax τ _ _ f) xx)).
Defined.
Proposition psh_nat_trans_im_laws
: is_functor psh_nat_trans_im_data.
Proof.
split.
- intros x.
use funextsec.
intros xx.
use subtypePath_prop.
cbn.
exact (eqtohomot (functor_id B x) (pr1 xx)).
- intros x y z f g.
use funextsec.
intros xx.
use subtypePath_prop.
cbn.
exact (eqtohomot (functor_comp B f g) (pr1 xx)).
Qed.
Definition psh_nat_trans_im
: C^op ⟶ HSET.
Proof.
use make_functor.
- exact psh_nat_trans_im_data.
- exact psh_nat_trans_im_laws.
Defined.
Definition psh_nat_trans_to_im
: A ⟹ psh_nat_trans_im.
Proof.
use make_nat_trans.
- refine (λ x xx, τ x xx ,, _).
abstract
(use hinhpr ;
refine (xx ,, _) ;
apply idpath).
- abstract
(intros x y f ;
use funextsec ;
intro xx ;
use subtypePath_prop ;
cbn ;
exact (eqtohomot (nat_trans_ax τ _ _ f) xx)).
Defined.
Definition psh_nat_trans_im_incl
: psh_nat_trans_im ⟹ B.
Proof.
use make_nat_trans.
- exact (λ x xx, pr1 xx).
- abstract
(intros x y f ;
apply idpath).
Defined.
Proposition isMonic_psh_nat_trans_im_incl
: isMonic (C := PreShv C) psh_nat_trans_im_incl.
Proof.
intros Z θ₁ θ₂ p.
use nat_trans_eq.
{
apply homset_property.
}
intro x.
use funextsec.
intro xx.
use subtypePath_prop.
exact (eqtohomot (nat_trans_eq_pointwise p x) xx).
Qed.
Definition psh_nat_trans_im_incl_monic
: Monic (PreShv C) psh_nat_trans_im B.
Proof.
use make_Monic.
- exact psh_nat_trans_im_incl.
- exact isMonic_psh_nat_trans_im_incl.
Defined.
Proposition psh_nat_trans_im_comm
: nat_trans_comp
_ _ _
psh_nat_trans_to_im
psh_nat_trans_im_incl
=
τ.
Proof.
use nat_trans_eq.
{
apply homset_property.
}
intro x.
cbn.
apply idpath.
Qed.
Section MapFromImage.
Context {Z : C^op ⟶ HSET}
(θ : A ⟹ Z)
(p : ∏ (x : C)
(a₁ a₂ : (A x : hSet)),
τ x a₁ = τ x a₂ → θ x a₁ = θ x a₂).
Proposition map_from_psh_nat_trans_im_unique
{x : C}
(b : (psh_nat_trans_im x : hSet))
: ∃! (z : (Z x : hSet)),
∏ (y : C)
(g : y --> x)
(a : (A y : hSet)),
τ y a = #B g (pr1 b)
→ θ y a = #Z g z.
Proof.
induction b as [ b q ].
revert q.
cbn -[hProp_to_hSet].
use factor_through_squash.
- apply isapropiscontr.
- intros (a & q).
use make_iscontr.
+ refine (θ x a ,, _).
intros y g a' r.
refine (_ @ eqtohomot (nat_trans_ax θ _ _ g) a).
cbn.
use p.
refine (r @ _).
refine (_ @ eqtohomot (!(nat_trans_ax τ _ _ g)) a).
cbn.
apply maponpaths.
exact (!q).
+ intros z.
use subtypePath.
{
intro.
do 4 (use impred ; intro).
apply setproperty.
}
cbn.
refine (_ @ !(pr2 z _ (identity _) _ _)).
* refine (!_).
exact (eqtohomot (functor_id Z _) _).
* refine (_ @ !(eqtohomot (functor_id B _) _)).
exact q.
Qed.
Definition map_from_psh_nat_trans_im_el
{x : C}
(b : (psh_nat_trans_im x : hSet))
: (Z x : hSet)
:= pr11 (map_from_psh_nat_trans_im_unique b).
Proposition map_from_psh_nat_trans_im_el_eq
{x : C}
(b : (psh_nat_trans_im x : hSet))
{y : C}
(g : y --> x)
(a : (A y : hSet))
(q : τ y a = #B g (pr1 b))
: θ y a = #Z g (map_from_psh_nat_trans_im_el b).
Proof.
exact (pr21 (map_from_psh_nat_trans_im_unique b) y g a q).
Qed.
Proposition map_from_psh_nat_trans_im_unique_eq
{x : C}
(b : (psh_nat_trans_im x : hSet))
{z₁ z₂ : (Z x : hSet)}
(q₁ : ∏ (y : C)
(g : y --> x)
(a : (A y : hSet)),
τ y a = #B g (pr1 b)
→ θ y a = #Z g z₁)
(q₂ : ∏ (y : C)
(g : y --> x)
(a : (A y : hSet)),
τ y a = #B g (pr1 b)
→ θ y a = #Z g z₂)
: z₁ = z₂.
Proof.
exact (maponpaths
pr1
(proofirrelevance
_
(isapropifcontr
(map_from_psh_nat_trans_im_unique b))
(z₁ ,, q₁)
(z₂ ,, q₂))).
Qed.
Definition map_from_psh_nat_trans_im_data
: nat_trans_data psh_nat_trans_im Z
:= λ x b, map_from_psh_nat_trans_im_el b.
Arguments map_from_psh_nat_trans_im_data /.
Proposition map_from_psh_nat_trans_im_laws
: is_nat_trans _ _ map_from_psh_nat_trans_im_data.
Proof.
intros x y f.
use funextsec.
intro b.
induction b as [ b q ].
use map_from_psh_nat_trans_im_unique_eq.
- refine (#B f b ,, _).
abstract
(revert q ;
use factor_through_squash_hProp ;
intros (a & r) ;
use hinhpr ;
refine (#A f a ,, _) ;
refine (eqtohomot (nat_trans_ax τ _ _ f) a @ _) ;
cbn ;
apply maponpaths ;
exact r).
- cbn.
intros z g a r.
refine (map_from_psh_nat_trans_im_el_eq _ _ _ _).
cbn.
exact r.
- cbn.
intros z g a r.
refine (map_from_psh_nat_trans_im_el_eq (b,, q) (g · f) a _ @ _).
+ refine (r @ !_).
cbn.
exact (eqtohomot (functor_comp B f g) b).
+ exact (eqtohomot (functor_comp Z f g) _).
Qed.
Definition map_from_psh_nat_trans_im
: psh_nat_trans_im ⟹ Z.
Proof.
use make_nat_trans.
- exact map_from_psh_nat_trans_im_data.
- exact map_from_psh_nat_trans_im_laws.
Defined.
Proposition map_from_psh_nat_trans_im_comm_pt
{x : C}
(a : (A x : hSet))
: map_from_psh_nat_trans_im x (psh_nat_trans_to_im x a) = θ x a.
Proof.
cbn.
refine (!_).
refine (_ @ eqtohomot (functor_id Z _) _).
use map_from_psh_nat_trans_im_el_eq.
refine (_ @ !(eqtohomot (functor_id B _) _)).
cbn.
apply idpath.
Qed.
Proposition map_from_psh_nat_trans_im_comm
: nat_trans_comp
_ _ _
psh_nat_trans_to_im
map_from_psh_nat_trans_im
=
θ.
Proof.
use nat_trans_eq.
{
apply homset_property.
}
intros x.
use funextsec.
intro a.
exact (map_from_psh_nat_trans_im_comm_pt a).
Qed.
Proposition map_from_psh_nat_trans_im_unique_mor
{ζ₁ ζ₂ : psh_nat_trans_im ⟹ Z}
(q₁ : nat_trans_comp
_ _ _
psh_nat_trans_to_im
ζ₁
=
θ)
(q₂ : nat_trans_comp
_ _ _
psh_nat_trans_to_im
ζ₂
=
θ)
: ζ₁ = ζ₂.
Proof.
use nat_trans_eq.
{
apply homset_property.
}
intro x.
use funextsec.
intro b.
use map_from_psh_nat_trans_im_unique_eq.
- exact b.
- intros y g a r.
refine (_ @ eqtohomot (nat_trans_ax ζ₁ _ _ g) b).
cbn.
refine (!_).
refine (_ @ eqtohomot (nat_trans_eq_pointwise q₁ y) a).
cbn.
apply maponpaths.
use subtypePath_prop.
cbn.
exact (!r).
- intros y g a r.
refine (_ @ eqtohomot (nat_trans_ax ζ₂ _ _ g) b).
cbn.
refine (!_).
refine (_ @ eqtohomot (nat_trans_eq_pointwise q₂ y) a).
cbn.
apply maponpaths.
use subtypePath_prop.
cbn.
exact (!r).
Qed.
End MapFromImage.
End Image.
End ExamplesDepPsh.
Definition dep_psh_fiberwise_terminal
(C : category)
: fiberwise_terminal (cleaving_disp_cat_dep_psh C).
Proof.
split.
- exact dep_psh_fiber_terminal.
- intros Γ₁ Γ₂ s.
exact (dep_psh_preserves_terminal s).
Defined.
Definition dep_psh_fiberwise_initial
(C : category)
: fiberwise_initial (cleaving_disp_cat_dep_psh C).
Proof.
split.
- exact dep_psh_fiber_initial.
- intros Γ₁ Γ₂ s.
exact (dep_psh_preserves_initial s).
Defined.
Definition dep_psh_fiberwise_binproducts
(C : category)
: fiberwise_binproducts (cleaving_disp_cat_dep_psh C).
Proof.
split.
- exact dep_psh_fiber_binproducts.
- intros Γ₁ Γ₂ s.
exact (dep_psh_preserves_binproduct s).
Defined.
Definition dep_psh_fiberwise_bincoproducts
(C : category)
: fiberwise_bincoproducts (cleaving_disp_cat_dep_psh C).
Proof.
split.
- exact dep_psh_fiber_bincoproducts.
- intros Γ₁ Γ₂ s.
exact (dep_psh_preserves_bincoproduct s).
Defined.
Definition dep_psh_fiberwise_equalizers
(C : category)
: fiberwise_equalizers (cleaving_disp_cat_dep_psh C).
Proof.
split.
- exact dep_psh_fiber_equalizers.
- intros Γ₁ Γ₂ s.
exact (dep_psh_preserves_equalizer s).
Defined.
(C : category)
: fiberwise_terminal (cleaving_disp_cat_dep_psh C).
Proof.
split.
- exact dep_psh_fiber_terminal.
- intros Γ₁ Γ₂ s.
exact (dep_psh_preserves_terminal s).
Defined.
Definition dep_psh_fiberwise_initial
(C : category)
: fiberwise_initial (cleaving_disp_cat_dep_psh C).
Proof.
split.
- exact dep_psh_fiber_initial.
- intros Γ₁ Γ₂ s.
exact (dep_psh_preserves_initial s).
Defined.
Definition dep_psh_fiberwise_binproducts
(C : category)
: fiberwise_binproducts (cleaving_disp_cat_dep_psh C).
Proof.
split.
- exact dep_psh_fiber_binproducts.
- intros Γ₁ Γ₂ s.
exact (dep_psh_preserves_binproduct s).
Defined.
Definition dep_psh_fiberwise_bincoproducts
(C : category)
: fiberwise_bincoproducts (cleaving_disp_cat_dep_psh C).
Proof.
split.
- exact dep_psh_fiber_bincoproducts.
- intros Γ₁ Γ₂ s.
exact (dep_psh_preserves_bincoproduct s).
Defined.
Definition dep_psh_fiberwise_equalizers
(C : category)
: fiberwise_equalizers (cleaving_disp_cat_dep_psh C).
Proof.
split.
- exact dep_psh_fiber_equalizers.
- intros Γ₁ Γ₂ s.
exact (dep_psh_preserves_equalizer s).
Defined.