Library TypeTheory.ALV2.CwF_SplitTypeCat_Equiv_Cats
TypeTheory.ALV2.CwF_SplitTypeCat_Equiv_Cats
Part of the TypeTheory library (Ahrens, Lumsdaine, Voevodsky, 2015–present).
Require Import UniMath.Foundations.Sets.
Require Import TypeTheory.Auxiliary.CategoryTheoryImports.
Require Import TypeTheory.Auxiliary.Auxiliary.
Require Import TypeTheory.Auxiliary.UnicodeNotations.
Require Import TypeTheory.Displayed_Cats.Auxiliary.
Require Import TypeTheory.Displayed_Cats.Core.
Require Import TypeTheory.Displayed_Cats.Constructions.
Require Import TypeTheory.Displayed_Cats.Equivalences.
Require Import TypeTheory.ALV1.CwF_SplitTypeCat_Defs.
Require Import TypeTheory.ALV1.CwF_SplitTypeCat_Maps.
Require Import TypeTheory.ALV2.CwF_SplitTypeCat_Cats.
Require Import TypeTheory.ALV1.CwF_SplitTypeCat_Equivalence.
Local Set Automatic Introduction.
Notation "# F" := (disp_functor_on_morphisms F)
(at level 3) : mor_disp_scope.
Section Auxiliary.
Definition disp_functor_id_composite
{C : category}
{CC DD EE : disp_cat C}
(FF : disp_functor (functor_identity _) CC DD)
(GG : disp_functor (functor_identity _) DD EE)
: disp_functor (functor_identity _) CC EE
:= disp_functor_composite FF GG.
End Auxiliary.
Section Fix_Context.
Context {C : category}.
Local Notation "Γ ◂ A" := (comp_ext _ Γ A) (at level 30).
Local Notation "'Ty'" := (fun X Γ => (TY X : functor _ _) Γ : hSet) (at level 10).
Local Notation Δ := comp_ext_compare.
Local Notation φ := obj_ext_mor_φ.
Section Compatible_Disp_Cat.
Definition strucs_compat_ob_mor
: disp_cat_ob_mor (total_category
(term_fun_disp_cat C × qq_structure_disp_cat C)).
Proof.
use tpair.
- intros XYZ. exact (iscompatible_term_qq (pr1 (pr2 XYZ)) (pr2 (pr2 XYZ))).
- simpl; intros; exact unit.
Defined.
Definition strucs_compat_id_comp
: disp_cat_id_comp _ strucs_compat_ob_mor.
Proof.
split; intros; exact tt.
Qed.
Definition strucs_compat_data : disp_cat_data _
:= ( _ ,, strucs_compat_id_comp).
Definition strucs_compat_axioms : disp_cat_axioms _ strucs_compat_data.
Proof.
repeat apply tpair; intros; try apply isasetaprop; apply isapropunit.
Qed.
Definition strucs_compat_disp_cat
: disp_cat (total_category
(term_fun_disp_cat C × qq_structure_disp_cat C))
:= ( _ ,, strucs_compat_axioms).
Definition compat_structures_disp_cat
:= sigma_disp_cat strucs_compat_disp_cat.
Definition compat_structures_pr1_disp_functor
: disp_functor (functor_identity _)
compat_structures_disp_cat (term_fun_disp_cat C)
:= disp_functor_id_composite
(sigmapr1_disp_functor _) (dirprodpr1_disp_functor _ _).
Definition compat_structures_pr2_disp_functor
: disp_functor (functor_identity _)
compat_structures_disp_cat (qq_structure_disp_cat C)
:= disp_functor_id_composite
(sigmapr1_disp_functor _) (dirprodpr2_disp_functor _ _).
Definition compat_structures_precat
:= total_category (strucs_compat_disp_cat).
Definition compat_structures_pr1_functor
: functor compat_structures_precat (term_fun_structure_precat C)
:= functor_composite
(pr1_category _)
(total_functor (dirprodpr1_disp_functor _ _)).
Definition compat_structures_pr2_functor
: functor compat_structures_precat (qq_structure_precat C)
:= functor_composite
(pr1_category _)
(total_functor (dirprodpr2_disp_functor _ _)).
End Compatible_Disp_Cat.
Lemmas towards an equivalence
Section Unique_QQ_From_Term.
Lemma qq_from_term_ob {X : obj_ext_precat} (Y : term_fun_disp_cat C X)
: ∑ (Z : qq_structure_disp_cat C X), strucs_compat_disp_cat (X ,, (Y ,, Z)).
Proof.
exists (qq_from_term Y).
apply iscompatible_qq_from_term.
Defined.
Lemma comp_ext_compare_te
{X : obj_ext_structure C}
{Y : term_fun_structure C X}
{Γ:C} {A A' : Ty X Γ} (e : A = A')
: # (TM Y : functor _ _) (Δ e) (te Y A') = te Y A.
Proof.
destruct e; cbn.
exact (toforallpaths _ _ _ (functor_id (TM _) _) _).
Qed.
Lemma qq_from_term_mor {X X' : obj_ext_precat} {F : X --> X'}
{Y : term_fun_disp_cat C X} {Y'} (FY : Y -->[F] Y')
{Z : qq_structure_disp_cat C X} {Z'}
(W : strucs_compat_disp_cat (X,,(Y,,Z)))
(W' : strucs_compat_disp_cat (X',,(Y',,Z')))
: ∑ (FZ : Z -->[F] Z'), W -->[(F,,(FY,,FZ))] W'.
Proof.
refine (_,, tt).
intros Γ' Γ f A.
cbn in W, W', FY. unfold iscompatible_term_qq in *.
unfold term_fun_mor in FY.
apply (Q_pp_Pb_unique Y'); simpl; unfold yoneda_morphisms_data.
- etrans. apply @pathsinv0, assoc.
etrans. apply maponpaths, obj_ext_mor_ax.
etrans. apply qq_π.
apply pathsinv0.
etrans. apply @pathsinv0, assoc.
etrans. apply maponpaths, qq_π.
etrans. apply assoc. apply cancel_postcomposition.
etrans. apply @pathsinv0, assoc.
etrans. apply maponpaths. apply comp_ext_compare_π.
apply obj_ext_mor_ax.
- etrans. exact (toforallpaths _ _ _ (functor_comp (TM _) _ _) _).
etrans. cbn. apply maponpaths, @pathsinv0, (term_fun_mor_te FY).
etrans. refine (toforallpaths _ _ _
(!nat_trans_ax (term_fun_mor_TM _) _ _ _) _).
etrans. cbn. apply maponpaths, @pathsinv0, W.
etrans. apply term_fun_mor_te.
apply pathsinv0.
etrans. exact (toforallpaths _ _ _ (functor_comp (TM _) _ _) _).
etrans. cbn. apply maponpaths, @pathsinv0, W'.
etrans. exact (toforallpaths _ _ _ (functor_comp (TM _) _ _) _).
cbn. apply maponpaths.
apply comp_ext_compare_te.
Time Qed.
Lemma qq_from_term_mor_unique {X X' : obj_ext_precat} {F : X --> X'}
{Y : term_fun_disp_cat C X} {Y'} (FY : Y -->[F] Y')
{Z : qq_structure_disp_cat C X} {Z'}
(W : strucs_compat_disp_cat (X,,(Y,,Z)))
(W' : strucs_compat_disp_cat (X',,(Y',,Z')))
: isaprop (∑ (FZ : Z -->[F] Z'), W -->[(F,,(FY,,FZ))] W').
Proof.
apply isofhleveltotal2.
- simpl. repeat (apply impred_isaprop; intro). apply homset_property.
- intros; simpl. apply isapropunit.
Qed.
End Unique_QQ_From_Term.
Section Unique_Term_From_QQ.
Lemma term_from_qq_ob {X : obj_ext_precat} (Z : qq_structure_disp_cat C X)
: ∑ (Y : term_fun_disp_cat C X), strucs_compat_disp_cat (X ,, (Y ,, Z)).
Proof.
exists (term_from_qq Z).
apply iscompatible_term_from_qq.
Defined.
The next main goal is the following statement. However, the construction of the morphism of term structures is rather large; so we factor the first component (the map of term presheaves) into several steps, going explicitly via the canonical term-structure constructed from sections term_fun_from_qq, before returning to this in term_from_qq_mor below.
Lemma term_from_qq_mor {X X' : obj_ext_precat} {F : X --> X'}
{Z : qq_structure_disp_cat C X} {Z'} (FZ : Z -->[F] Z')
{Y : term_fun_disp_cat C X} {Y'}
(W : strucs_compat_disp_cat (X,,(Y,,Z)))
(W' : strucs_compat_disp_cat (X',,(Y',,Z')))
: ∑ (FY : Y -->[F] Y'), W -->[(F,,(FY,,FZ))] W'.
Abort.
Section Rename_me.
Lemma tm_from_qq_mor_data {X X' : obj_ext_precat} {F : X --> X'}
{Z : qq_structure_disp_cat C X} {Z'} (FZ : Z -->[F] Z')
: forall Γ : C, (tm_from_qq Z Γ) --> (tm_from_qq Z' Γ).
Proof.
intros Γ Ase.
exists ((obj_ext_mor_TY F : nat_trans _ _) _ (pr1 Ase)).
exists (pr1 (pr2 Ase) ;; φ F _).
etrans. apply @pathsinv0, assoc.
etrans. apply maponpaths, obj_ext_mor_ax.
apply (pr2 (pr2 Ase)).
Defined.
Lemma tm_from_qq_mor_naturality {X X' : obj_ext_precat} {F : X --> X'}
{Z : qq_structure_disp_cat C X} {Z'} (FZ : Z -->[F] Z')
: is_nat_trans (tm_from_qq Z) (tm_from_qq Z') (tm_from_qq_mor_data FZ).
Proof.
intros Γ Γ' f; cbn in Γ, Γ', f.
apply funextsec; intros [A [s e]].
use tm_from_qq_eq.
- cbn. exact (toforallpaths _ _ _
(nat_trans_ax (obj_ext_mor_TY _) _ _ _) _).
- cbn. apply PullbackArrowUnique.
+ etrans. cbn. apply @pathsinv0, assoc.
etrans. apply maponpaths, comp_ext_compare_π.
etrans. apply @pathsinv0, assoc.
etrans. apply maponpaths, obj_ext_mor_ax.
refine (PullbackArrow_PullbackPr1
(mk_Pullback _ _ _ _ _ _ (qq_π_Pb _ f A)) _ _ _ _).
+ cbn in FZ; cbn.
etrans. apply maponpaths_2, @pathsinv0, assoc.
etrans. apply @pathsinv0, assoc.
etrans. apply maponpaths, @pathsinv0, FZ.
etrans. apply assoc.
etrans. apply maponpaths_2.
apply (PullbackArrow_PullbackPr2 (mk_Pullback _ _ _ _ _ _ _)).
apply pathsinv0, assoc.
Time Qed.
Lemma tm_from_qq_mor_TM {X X' : obj_ext_precat} {F : X --> X'}
{Z : qq_structure_disp_cat C X} {Z'} (FZ : Z -->[F] Z')
: nat_trans (tm_from_qq Z) (tm_from_qq Z').
Proof.
exists (tm_from_qq_mor_data FZ).
apply tm_from_qq_mor_naturality.
Defined.
Lemma tm_from_qq_mor_pp {X X' : obj_ext_precat} {F : X --> X'}
{Z : qq_structure_disp_cat C X} {Z'} (FZ : Z -->[F] Z')
: (tm_from_qq_mor_TM FZ : preShv C ⟦ _ , _ ⟧) ;; pp_from_qq Z'
= pp_from_qq Z;; obj_ext_mor_TY F.
Proof.
apply nat_trans_eq. apply homset_property.
intros Γ. apply idpath.
Qed.
Lemma tm_from_qq_mor_te {X X' : obj_ext_precat} {F : X --> X'}
{Z : qq_structure_disp_cat C X} {Z'} (FZ : Z -->[F] Z')
{Γ} (A : Ty X Γ)
: tm_from_qq_mor_TM FZ _ (te_from_qq Z A)
= # (tm_from_qq Z') (φ F A)
(te_from_qq Z' ((obj_ext_mor_TY F : nat_trans _ _) _ A)).
Proof.
cbn.
use tm_from_qq_eq_reindex.
- cbn.
etrans. Focus 2. exact (toforallpaths _ _ _ (functor_comp (TY _) _ _) _).
etrans. Focus 2. cbn. apply maponpaths_2, @pathsinv0, obj_ext_mor_ax.
exact (toforallpaths _ _ _ (nat_trans_ax (obj_ext_mor_TY F) _ _ _) _).
- etrans. Focus 2. apply @pathsinv0,
(postCompWithPullbackArrow _ _ _ (mk_Pullback _ _ _ _ _ _ _)).
apply PullbackArrowUnique.
+ cbn.
etrans. apply @pathsinv0, assoc.
etrans. apply maponpaths, qq_π.
etrans. apply assoc.
etrans. Focus 2. apply @pathsinv0, id_right.
etrans. Focus 2. apply id_left.
apply maponpaths_2.
etrans. apply @pathsinv0, assoc.
etrans. apply maponpaths, comp_ext_compare_π.
etrans. apply @pathsinv0, assoc.
etrans. apply maponpaths, obj_ext_mor_ax.
apply (PullbackArrow_PullbackPr1 (mk_Pullback _ _ _ _ _ _ _)).
+ etrans. Focus 2. apply @pathsinv0, id_right.
etrans. cbn. apply maponpaths_2, maponpaths_2, maponpaths.
etrans. apply comp_ext_compare_comp.
apply maponpaths_2, comp_ext_compare_comp.
etrans. apply @pathsinv0, assoc.
etrans. apply maponpaths_2, assoc.
etrans. apply @pathsinv0, assoc.
etrans. apply maponpaths.
etrans. apply assoc.
apply @pathsinv0, @qq_comp.
etrans. apply maponpaths_2, assoc.
etrans. apply @pathsinv0, assoc.
etrans. apply maponpaths, comp_ext_compare_qq.
etrans. apply maponpaths_2, @pathsinv0, assoc.
etrans. apply @pathsinv0, assoc.
etrans. apply maponpaths, @pathsinv0. use FZ.
etrans. apply assoc.
etrans. apply maponpaths_2.
apply (PullbackArrow_PullbackPr2 (mk_Pullback _ _ _ _ _ _ _)).
apply id_left.
Time Qed.
End Rename_me.
Definition term_from_qq_mor_TM {X X' : obj_ext_precat} {F : X --> X'}
{Z : qq_structure_disp_cat C X} {Z'} (FZ : Z -->[F] Z')
{Y : term_fun_disp_cat C X} {Y'}
(W : strucs_compat_disp_cat (X,,(Y,,Z)))
(W' : strucs_compat_disp_cat (X',,(Y',,Z')))
: TM (Y : term_fun_structure _ _) --> TM (Y' : term_fun_structure _ _).
Proof.
refine ( _ ;; (tm_from_qq_mor_TM FZ : preShv C ⟦ _ , _ ⟧) ;; _).
- refine (given_TM_to_canonical _ _ (Y,,W)).
- refine (canonical_TM_to_given _ _ (Y',,W')).
Defined.
Lemma term_from_qq_mor {X X' : obj_ext_precat} {F : X --> X'}
{Z : qq_structure_disp_cat C X} {Z'} (FZ : Z -->[F] Z')
{Y : term_fun_disp_cat C X} {Y'}
(W : strucs_compat_disp_cat (X,,(Y,,Z)))
(W' : strucs_compat_disp_cat (X',,(Y',,Z')))
: ∑ (FY : Y -->[F] Y'), W -->[(F,,(FY,,FZ))] W'.
Proof.
simpl in W, W'; unfold iscompatible_term_qq in W, W'. simpl in Y, Y'. refine (_,,tt). simpl; unfold term_fun_mor.
exists (term_from_qq_mor_TM FZ W W').
apply dirprodpair; try intros Γ A.
- etrans. apply @pathsinv0, assoc.
etrans. apply maponpaths, (pp_canonical_TM_to_given _ _ (_,,_)).
etrans. apply @pathsinv0, assoc.
etrans. apply maponpaths, tm_from_qq_mor_pp.
etrans. apply assoc.
apply maponpaths_2, (pp_given_TM_to_canonical _ _ (_,,_)).
- unfold term_from_qq_mor_TM.
cbn.
etrans. apply maponpaths, maponpaths, given_TM_to_canonical_te.
etrans. apply maponpaths, (tm_from_qq_mor_te FZ).
etrans. apply (toforallpaths _ _ _
(nat_trans_ax (canonical_TM_to_given _ _ (_,,_)) _ _ _) _).
cbn. apply maponpaths. apply (canonical_TM_to_given_te _ _ (_,,_)).
Defined.
Lemma term_from_qq_mor_unique {X X' : obj_ext_precat} {F : X --> X'}
{Z : qq_structure_disp_cat C X} {Z'} (FZ : Z -->[F] Z')
{Y : term_fun_disp_cat C X} {Y'}
(W : strucs_compat_disp_cat (X,,(Y,,Z)))
(W' : strucs_compat_disp_cat (X',,(Y',,Z')))
: isaprop (∑ (FY : Y -->[F] Y'), W -->[(F,,(FY,,FZ))] W').
Proof.
apply isofhleveltotal2.
- simpl. apply isaprop_term_fun_mor.
- intros; simpl. apply isapropunit.
Defined.
End Unique_Term_From_QQ.
{Z : qq_structure_disp_cat C X} {Z'} (FZ : Z -->[F] Z')
{Y : term_fun_disp_cat C X} {Y'}
(W : strucs_compat_disp_cat (X,,(Y,,Z)))
(W' : strucs_compat_disp_cat (X',,(Y',,Z')))
: ∑ (FY : Y -->[F] Y'), W -->[(F,,(FY,,FZ))] W'.
Abort.
Section Rename_me.
Lemma tm_from_qq_mor_data {X X' : obj_ext_precat} {F : X --> X'}
{Z : qq_structure_disp_cat C X} {Z'} (FZ : Z -->[F] Z')
: forall Γ : C, (tm_from_qq Z Γ) --> (tm_from_qq Z' Γ).
Proof.
intros Γ Ase.
exists ((obj_ext_mor_TY F : nat_trans _ _) _ (pr1 Ase)).
exists (pr1 (pr2 Ase) ;; φ F _).
etrans. apply @pathsinv0, assoc.
etrans. apply maponpaths, obj_ext_mor_ax.
apply (pr2 (pr2 Ase)).
Defined.
Lemma tm_from_qq_mor_naturality {X X' : obj_ext_precat} {F : X --> X'}
{Z : qq_structure_disp_cat C X} {Z'} (FZ : Z -->[F] Z')
: is_nat_trans (tm_from_qq Z) (tm_from_qq Z') (tm_from_qq_mor_data FZ).
Proof.
intros Γ Γ' f; cbn in Γ, Γ', f.
apply funextsec; intros [A [s e]].
use tm_from_qq_eq.
- cbn. exact (toforallpaths _ _ _
(nat_trans_ax (obj_ext_mor_TY _) _ _ _) _).
- cbn. apply PullbackArrowUnique.
+ etrans. cbn. apply @pathsinv0, assoc.
etrans. apply maponpaths, comp_ext_compare_π.
etrans. apply @pathsinv0, assoc.
etrans. apply maponpaths, obj_ext_mor_ax.
refine (PullbackArrow_PullbackPr1
(mk_Pullback _ _ _ _ _ _ (qq_π_Pb _ f A)) _ _ _ _).
+ cbn in FZ; cbn.
etrans. apply maponpaths_2, @pathsinv0, assoc.
etrans. apply @pathsinv0, assoc.
etrans. apply maponpaths, @pathsinv0, FZ.
etrans. apply assoc.
etrans. apply maponpaths_2.
apply (PullbackArrow_PullbackPr2 (mk_Pullback _ _ _ _ _ _ _)).
apply pathsinv0, assoc.
Time Qed.
Lemma tm_from_qq_mor_TM {X X' : obj_ext_precat} {F : X --> X'}
{Z : qq_structure_disp_cat C X} {Z'} (FZ : Z -->[F] Z')
: nat_trans (tm_from_qq Z) (tm_from_qq Z').
Proof.
exists (tm_from_qq_mor_data FZ).
apply tm_from_qq_mor_naturality.
Defined.
Lemma tm_from_qq_mor_pp {X X' : obj_ext_precat} {F : X --> X'}
{Z : qq_structure_disp_cat C X} {Z'} (FZ : Z -->[F] Z')
: (tm_from_qq_mor_TM FZ : preShv C ⟦ _ , _ ⟧) ;; pp_from_qq Z'
= pp_from_qq Z;; obj_ext_mor_TY F.
Proof.
apply nat_trans_eq. apply homset_property.
intros Γ. apply idpath.
Qed.
Lemma tm_from_qq_mor_te {X X' : obj_ext_precat} {F : X --> X'}
{Z : qq_structure_disp_cat C X} {Z'} (FZ : Z -->[F] Z')
{Γ} (A : Ty X Γ)
: tm_from_qq_mor_TM FZ _ (te_from_qq Z A)
= # (tm_from_qq Z') (φ F A)
(te_from_qq Z' ((obj_ext_mor_TY F : nat_trans _ _) _ A)).
Proof.
cbn.
use tm_from_qq_eq_reindex.
- cbn.
etrans. Focus 2. exact (toforallpaths _ _ _ (functor_comp (TY _) _ _) _).
etrans. Focus 2. cbn. apply maponpaths_2, @pathsinv0, obj_ext_mor_ax.
exact (toforallpaths _ _ _ (nat_trans_ax (obj_ext_mor_TY F) _ _ _) _).
- etrans. Focus 2. apply @pathsinv0,
(postCompWithPullbackArrow _ _ _ (mk_Pullback _ _ _ _ _ _ _)).
apply PullbackArrowUnique.
+ cbn.
etrans. apply @pathsinv0, assoc.
etrans. apply maponpaths, qq_π.
etrans. apply assoc.
etrans. Focus 2. apply @pathsinv0, id_right.
etrans. Focus 2. apply id_left.
apply maponpaths_2.
etrans. apply @pathsinv0, assoc.
etrans. apply maponpaths, comp_ext_compare_π.
etrans. apply @pathsinv0, assoc.
etrans. apply maponpaths, obj_ext_mor_ax.
apply (PullbackArrow_PullbackPr1 (mk_Pullback _ _ _ _ _ _ _)).
+ etrans. Focus 2. apply @pathsinv0, id_right.
etrans. cbn. apply maponpaths_2, maponpaths_2, maponpaths.
etrans. apply comp_ext_compare_comp.
apply maponpaths_2, comp_ext_compare_comp.
etrans. apply @pathsinv0, assoc.
etrans. apply maponpaths_2, assoc.
etrans. apply @pathsinv0, assoc.
etrans. apply maponpaths.
etrans. apply assoc.
apply @pathsinv0, @qq_comp.
etrans. apply maponpaths_2, assoc.
etrans. apply @pathsinv0, assoc.
etrans. apply maponpaths, comp_ext_compare_qq.
etrans. apply maponpaths_2, @pathsinv0, assoc.
etrans. apply @pathsinv0, assoc.
etrans. apply maponpaths, @pathsinv0. use FZ.
etrans. apply assoc.
etrans. apply maponpaths_2.
apply (PullbackArrow_PullbackPr2 (mk_Pullback _ _ _ _ _ _ _)).
apply id_left.
Time Qed.
End Rename_me.
Definition term_from_qq_mor_TM {X X' : obj_ext_precat} {F : X --> X'}
{Z : qq_structure_disp_cat C X} {Z'} (FZ : Z -->[F] Z')
{Y : term_fun_disp_cat C X} {Y'}
(W : strucs_compat_disp_cat (X,,(Y,,Z)))
(W' : strucs_compat_disp_cat (X',,(Y',,Z')))
: TM (Y : term_fun_structure _ _) --> TM (Y' : term_fun_structure _ _).
Proof.
refine ( _ ;; (tm_from_qq_mor_TM FZ : preShv C ⟦ _ , _ ⟧) ;; _).
- refine (given_TM_to_canonical _ _ (Y,,W)).
- refine (canonical_TM_to_given _ _ (Y',,W')).
Defined.
Lemma term_from_qq_mor {X X' : obj_ext_precat} {F : X --> X'}
{Z : qq_structure_disp_cat C X} {Z'} (FZ : Z -->[F] Z')
{Y : term_fun_disp_cat C X} {Y'}
(W : strucs_compat_disp_cat (X,,(Y,,Z)))
(W' : strucs_compat_disp_cat (X',,(Y',,Z')))
: ∑ (FY : Y -->[F] Y'), W -->[(F,,(FY,,FZ))] W'.
Proof.
simpl in W, W'; unfold iscompatible_term_qq in W, W'. simpl in Y, Y'. refine (_,,tt). simpl; unfold term_fun_mor.
exists (term_from_qq_mor_TM FZ W W').
apply dirprodpair; try intros Γ A.
- etrans. apply @pathsinv0, assoc.
etrans. apply maponpaths, (pp_canonical_TM_to_given _ _ (_,,_)).
etrans. apply @pathsinv0, assoc.
etrans. apply maponpaths, tm_from_qq_mor_pp.
etrans. apply assoc.
apply maponpaths_2, (pp_given_TM_to_canonical _ _ (_,,_)).
- unfold term_from_qq_mor_TM.
cbn.
etrans. apply maponpaths, maponpaths, given_TM_to_canonical_te.
etrans. apply maponpaths, (tm_from_qq_mor_te FZ).
etrans. apply (toforallpaths _ _ _
(nat_trans_ax (canonical_TM_to_given _ _ (_,,_)) _ _ _) _).
cbn. apply maponpaths. apply (canonical_TM_to_given_te _ _ (_,,_)).
Defined.
Lemma term_from_qq_mor_unique {X X' : obj_ext_precat} {F : X --> X'}
{Z : qq_structure_disp_cat C X} {Z'} (FZ : Z -->[F] Z')
{Y : term_fun_disp_cat C X} {Y'}
(W : strucs_compat_disp_cat (X,,(Y,,Z)))
(W' : strucs_compat_disp_cat (X',,(Y',,Z')))
: isaprop (∑ (FY : Y -->[F] Y'), W -->[(F,,(FY,,FZ))] W').
Proof.
apply isofhleveltotal2.
- simpl. apply isaprop_term_fun_mor.
- intros; simpl. apply isapropunit.
Defined.
End Unique_Term_From_QQ.
We show, in this section, that the (non-displayed) projection functors from the (total) precategory of compatible-pairs-of-structures on C to the precategories of q-morphism structures and of term-structures are each equivalences.
TODO: scrap this section, and recover it from the displayed version.
Section Strucs_Equiv_Precats.
Lemma compat_structures_pr1_ess_surj
: essentially_surjective (compat_structures_pr1_functor).
Proof.
unfold essentially_surjective.
intros XY; destruct XY as [X Y]; apply hinhpr.
exists ((X,,(Y,, qq_from_term Y)),,iscompatible_qq_from_term Y).
apply identity_iso.
Qed.
Lemma compat_structures_pr1_fully_faithful
: fully_faithful (compat_structures_pr1_functor).
Proof.
intros XYZW XYZW'.
destruct XYZW as [ [X [Y Z] ] W].
destruct XYZW' as [ [X' [Y' Z'] ] W'].
unfold compat_structures_pr1_functor; simpl.
assert (structural_lemma :
∏ (A : UU) (B C : A -> UU) (D : ∏ a, B a -> C a -> UU)
(H : ∏ a b, iscontr (∑ c, D a b c)),
isweq (fun abcd : ∑ (abc : ∑ a, (B a × C a)),
D (pr1 abc) (pr1 (pr2 abc)) (pr2 (pr2 abc))
=> (pr1 (pr1 abcd),, pr1 (pr2 (pr1 abcd))))).
{ clear C X Y Z W X' Y' Z' W'.
intros A B C D H.
use gradth.
+ intros ab.
set (cd := iscontrpr1 (H (pr1 ab) (pr2 ab))).
exact ((pr1 ab,, (pr2 ab,, pr1 cd)),, pr2 cd).
+ intros abcd; destruct abcd as [ [a [b c] ] d]; simpl.
refine (@maponpaths _ _
(fun cd : ∑ c' : C a, (D a b c') => (a,, b,, (pr1 cd)),, (pr2 cd))
_ (_,, _) _).
apply proofirrelevancecontr, H.
+ intros ab; destruct ab as [a b]. apply idpath. }
use (structural_lemma _ _ _ (fun _ _ _ => unit) _ ).
intros FX FY. apply iscontraprop1.
- exact (qq_from_term_mor_unique FY W W').
- exact (qq_from_term_mor FY W W').
Qed.
Lemma compat_structures_pr2_ess_surj
: essentially_surjective (compat_structures_pr2_functor).
Proof.
unfold essentially_surjective.
intros XZ; destruct XZ as [X Z]; apply hinhpr.
exists ((X,,(term_from_qq Z,, Z)),,iscompatible_term_from_qq Z).
apply identity_iso.
Qed.
Lemma compat_structures_pr2_fully_faithful
: fully_faithful (compat_structures_pr2_functor).
Proof.
intros XYZW XYZW';
destruct XYZW as [ [X [Y Z] ] W];
destruct XYZW' as [ [X' [Y' Z'] ] W'].
unfold compat_structures_pr2_functor; simpl.
assert (structural_lemma :
∏ A (B C : A -> UU) (D : ∏ a, B a -> C a -> UU)
(H : ∏ a c, iscontr (∑ b, D a b c)),
isweq (fun abcd : ∑ (abc : ∑ a, (B a × C a)),
D (pr1 abc) (pr1 (pr2 abc)) (pr2 (pr2 abc))
=> (pr1 (pr1 abcd),, pr2 (pr2 (pr1 abcd))))).
{ clear C X Y Z W X' Y' Z' W'.
intros A B C D H.
use gradth.
+ intros ac.
set (bd := iscontrpr1 (H (pr1 ac) (pr2 ac))).
exact ((pr1 ac,, (pr1 bd,, pr2 ac)),, pr2 bd).
+ intros abcd; destruct abcd as [ [a [b c] ] d]; simpl.
refine (@maponpaths _ _
(fun bd : ∑ b' : B a, (D a b' c) => (a,, (pr1 bd),, c),, (pr2 bd))
_ (_,, _) _).
apply proofirrelevancecontr, H.
+ intros ac; destruct ac as [a c]. apply idpath. }
simple refine (structural_lemma _ _ _ (fun _ _ _ => unit) _).
intros FX FY. apply iscontraprop1.
- exact (term_from_qq_mor_unique FY W W').
- exact (term_from_qq_mor FY W W').
Qed.
End Strucs_Equiv_Precats.
Section Strucs_Disp_Equiv.
Lemma compat_structures_pr1_ess_split
: disp_functor_disp_ess_split_surj (compat_structures_pr1_disp_functor).
Proof.
unfold disp_functor_disp_ess_split_surj.
intros X Y.
exists ((Y,, qq_from_term Y),,iscompatible_qq_from_term Y).
apply identity_iso_disp.
Defined.
Lemma compat_structures_pr1_ff
: disp_functor_ff (compat_structures_pr1_disp_functor).
Proof.
intros X X' YZW YZW'.
destruct YZW as [ [Y Z] W].
destruct YZW' as [ [Y' Z'] W'].
unfold compat_structures_pr1_functor; simpl.
intros FX.
assert (structural_lemma :
∏ (B C : UU) (D : B -> C -> UU)
(H : ∏ b, iscontr (∑ c, D b c)),
isweq (fun bcd : ∑ (bc : B × C), D (pr1 bc) (pr2 bc)
=> pr1 (pr1 bcd))).
clear C X Y Z W X' Y' Z' W' FX.
{ intros B C D H.
use gradth.
+ intros b.
set (cd := iscontrpr1 (H b)).
exact ((b,,pr1 cd),, pr2 cd).
+ intros bcd; destruct bcd as [ [b c] d]; simpl.
refine (@maponpaths _ _
(fun cd : ∑ c', (D b c') => (b,, (pr1 cd)),, (pr2 cd))
_ (_,, _) _).
apply proofirrelevancecontr, H.
+ intros b; apply idpath. }
simple refine (structural_lemma _ _ (fun _ _ => unit) _).
intros FY. apply iscontraprop1.
- exact (qq_from_term_mor_unique FY W W').
- exact (qq_from_term_mor FY W W').
Qed.
Lemma compat_structures_pr1_is_equiv_over_id
: is_equiv_over_id (compat_structures_pr1_disp_functor).
Proof.
apply is_equiv_from_ff_ess_over_id.
- apply compat_structures_pr1_ess_split.
- apply compat_structures_pr1_ff.
Defined.
Definition compat_structures_pr1_equiv_over_id
: equiv_over_id _ _
:= compat_structures_pr1_is_equiv_over_id.
Definition compat_structures_pr1_inverse_over_id
: equiv_over_id
(term_fun_disp_cat C) compat_structures_disp_cat.
Proof.
exact (equiv_inv _ (compat_structures_pr1_is_equiv_over_id)).
Defined.
Lemma compat_structures_pr2_ess_split
: disp_functor_disp_ess_split_surj (compat_structures_pr2_disp_functor).
Proof.
unfold disp_functor_disp_ess_split_surj.
intros X Z.
exists ((term_from_qq Z,, Z),,iscompatible_term_from_qq Z).
apply identity_iso_disp.
Defined.
Lemma compat_structures_pr2_ff
: disp_functor_ff (compat_structures_pr2_disp_functor).
Proof.
intros X X' YZW YZW'.
destruct YZW as [ [Y Z] W].
destruct YZW' as [ [Y' Z'] W'].
unfold compat_structures_pr1_functor; simpl.
intros FX.
assert (structural_lemma :
∏ (B C : UU) (D : B -> C -> UU)
(H : ∏ c, iscontr (∑ b, D b c)),
isweq (fun bcd : ∑ (bc : B × C), D (pr1 bc) (pr2 bc)
=> pr2 (pr1 bcd))).
clear C X Y Z W X' Y' Z' W' FX.
{ intros B C D H.
use gradth.
+ intros c.
set (bd := iscontrpr1 (H c)).
exact ((pr1 bd,,c),, pr2 bd).
+ intros bcd; destruct bcd as [ [b c] d]; simpl.
refine (@maponpaths _ _
(fun bd : ∑ b', (D b' c) => ((pr1 bd),, c),, (pr2 bd))
_ (_,, _) _).
apply proofirrelevancecontr, H.
+ intros c; apply idpath. }
simple refine (structural_lemma _ _ (fun _ _ => unit) _).
intros FY. apply iscontraprop1.
- exact (term_from_qq_mor_unique FY W W').
- exact (term_from_qq_mor FY W W').
Qed.
Lemma compat_structures_pr2_is_equiv_over_id
: is_equiv_over_id (compat_structures_pr2_disp_functor).
Proof.
apply is_equiv_from_ff_ess_over_id.
- apply compat_structures_pr2_ess_split.
- apply compat_structures_pr2_ff.
Defined.
Definition compat_structures_pr2_equiv_over_id
: equiv_over_id _ _
:= compat_structures_pr2_is_equiv_over_id.
Definition compat_structures_pr2_inverse_over_id
: equiv_over_id
(qq_structure_disp_cat C) compat_structures_disp_cat.
Proof.
exact (equiv_inv _ (compat_structures_pr2_is_equiv_over_id)).
Defined.
End Strucs_Disp_Equiv.
Section Strucs_Fiber_Equiv.
Context (X : obj_ext_Precat C).
Definition term_struc_to_qq_struc_fiber_functor
: functor
(fiber_category (term_fun_disp_cat C) X)
(fiber_category (qq_structure_disp_cat C) X).
Proof.
eapply functor_composite.
- eapply fiber_functor.
exact compat_structures_pr1_inverse_over_id.
- exact (fiber_functor compat_structures_pr2_equiv_over_id X).
Defined.
Definition term_struc_to_qq_struc_is_equiv
: adj_equivalence_of_precats
term_struc_to_qq_struc_fiber_functor.
Proof.
use comp_adj_equivalence_of_precats.
- apply homset_property.
- apply homset_property.
- apply homset_property.
- apply fiber_equiv.
apply is_equiv_of_equiv_over_id.
- apply fiber_equiv.
apply is_equiv_of_equiv_over_id.
Defined.
End Strucs_Fiber_Equiv.
End Fix_Context.
Lemma compat_structures_pr1_ess_surj
: essentially_surjective (compat_structures_pr1_functor).
Proof.
unfold essentially_surjective.
intros XY; destruct XY as [X Y]; apply hinhpr.
exists ((X,,(Y,, qq_from_term Y)),,iscompatible_qq_from_term Y).
apply identity_iso.
Qed.
Lemma compat_structures_pr1_fully_faithful
: fully_faithful (compat_structures_pr1_functor).
Proof.
intros XYZW XYZW'.
destruct XYZW as [ [X [Y Z] ] W].
destruct XYZW' as [ [X' [Y' Z'] ] W'].
unfold compat_structures_pr1_functor; simpl.
assert (structural_lemma :
∏ (A : UU) (B C : A -> UU) (D : ∏ a, B a -> C a -> UU)
(H : ∏ a b, iscontr (∑ c, D a b c)),
isweq (fun abcd : ∑ (abc : ∑ a, (B a × C a)),
D (pr1 abc) (pr1 (pr2 abc)) (pr2 (pr2 abc))
=> (pr1 (pr1 abcd),, pr1 (pr2 (pr1 abcd))))).
{ clear C X Y Z W X' Y' Z' W'.
intros A B C D H.
use gradth.
+ intros ab.
set (cd := iscontrpr1 (H (pr1 ab) (pr2 ab))).
exact ((pr1 ab,, (pr2 ab,, pr1 cd)),, pr2 cd).
+ intros abcd; destruct abcd as [ [a [b c] ] d]; simpl.
refine (@maponpaths _ _
(fun cd : ∑ c' : C a, (D a b c') => (a,, b,, (pr1 cd)),, (pr2 cd))
_ (_,, _) _).
apply proofirrelevancecontr, H.
+ intros ab; destruct ab as [a b]. apply idpath. }
use (structural_lemma _ _ _ (fun _ _ _ => unit) _ ).
intros FX FY. apply iscontraprop1.
- exact (qq_from_term_mor_unique FY W W').
- exact (qq_from_term_mor FY W W').
Qed.
Lemma compat_structures_pr2_ess_surj
: essentially_surjective (compat_structures_pr2_functor).
Proof.
unfold essentially_surjective.
intros XZ; destruct XZ as [X Z]; apply hinhpr.
exists ((X,,(term_from_qq Z,, Z)),,iscompatible_term_from_qq Z).
apply identity_iso.
Qed.
Lemma compat_structures_pr2_fully_faithful
: fully_faithful (compat_structures_pr2_functor).
Proof.
intros XYZW XYZW';
destruct XYZW as [ [X [Y Z] ] W];
destruct XYZW' as [ [X' [Y' Z'] ] W'].
unfold compat_structures_pr2_functor; simpl.
assert (structural_lemma :
∏ A (B C : A -> UU) (D : ∏ a, B a -> C a -> UU)
(H : ∏ a c, iscontr (∑ b, D a b c)),
isweq (fun abcd : ∑ (abc : ∑ a, (B a × C a)),
D (pr1 abc) (pr1 (pr2 abc)) (pr2 (pr2 abc))
=> (pr1 (pr1 abcd),, pr2 (pr2 (pr1 abcd))))).
{ clear C X Y Z W X' Y' Z' W'.
intros A B C D H.
use gradth.
+ intros ac.
set (bd := iscontrpr1 (H (pr1 ac) (pr2 ac))).
exact ((pr1 ac,, (pr1 bd,, pr2 ac)),, pr2 bd).
+ intros abcd; destruct abcd as [ [a [b c] ] d]; simpl.
refine (@maponpaths _ _
(fun bd : ∑ b' : B a, (D a b' c) => (a,, (pr1 bd),, c),, (pr2 bd))
_ (_,, _) _).
apply proofirrelevancecontr, H.
+ intros ac; destruct ac as [a c]. apply idpath. }
simple refine (structural_lemma _ _ _ (fun _ _ _ => unit) _).
intros FX FY. apply iscontraprop1.
- exact (term_from_qq_mor_unique FY W W').
- exact (term_from_qq_mor FY W W').
Qed.
End Strucs_Equiv_Precats.
Section Strucs_Disp_Equiv.
Lemma compat_structures_pr1_ess_split
: disp_functor_disp_ess_split_surj (compat_structures_pr1_disp_functor).
Proof.
unfold disp_functor_disp_ess_split_surj.
intros X Y.
exists ((Y,, qq_from_term Y),,iscompatible_qq_from_term Y).
apply identity_iso_disp.
Defined.
Lemma compat_structures_pr1_ff
: disp_functor_ff (compat_structures_pr1_disp_functor).
Proof.
intros X X' YZW YZW'.
destruct YZW as [ [Y Z] W].
destruct YZW' as [ [Y' Z'] W'].
unfold compat_structures_pr1_functor; simpl.
intros FX.
assert (structural_lemma :
∏ (B C : UU) (D : B -> C -> UU)
(H : ∏ b, iscontr (∑ c, D b c)),
isweq (fun bcd : ∑ (bc : B × C), D (pr1 bc) (pr2 bc)
=> pr1 (pr1 bcd))).
clear C X Y Z W X' Y' Z' W' FX.
{ intros B C D H.
use gradth.
+ intros b.
set (cd := iscontrpr1 (H b)).
exact ((b,,pr1 cd),, pr2 cd).
+ intros bcd; destruct bcd as [ [b c] d]; simpl.
refine (@maponpaths _ _
(fun cd : ∑ c', (D b c') => (b,, (pr1 cd)),, (pr2 cd))
_ (_,, _) _).
apply proofirrelevancecontr, H.
+ intros b; apply idpath. }
simple refine (structural_lemma _ _ (fun _ _ => unit) _).
intros FY. apply iscontraprop1.
- exact (qq_from_term_mor_unique FY W W').
- exact (qq_from_term_mor FY W W').
Qed.
Lemma compat_structures_pr1_is_equiv_over_id
: is_equiv_over_id (compat_structures_pr1_disp_functor).
Proof.
apply is_equiv_from_ff_ess_over_id.
- apply compat_structures_pr1_ess_split.
- apply compat_structures_pr1_ff.
Defined.
Definition compat_structures_pr1_equiv_over_id
: equiv_over_id _ _
:= compat_structures_pr1_is_equiv_over_id.
Definition compat_structures_pr1_inverse_over_id
: equiv_over_id
(term_fun_disp_cat C) compat_structures_disp_cat.
Proof.
exact (equiv_inv _ (compat_structures_pr1_is_equiv_over_id)).
Defined.
Lemma compat_structures_pr2_ess_split
: disp_functor_disp_ess_split_surj (compat_structures_pr2_disp_functor).
Proof.
unfold disp_functor_disp_ess_split_surj.
intros X Z.
exists ((term_from_qq Z,, Z),,iscompatible_term_from_qq Z).
apply identity_iso_disp.
Defined.
Lemma compat_structures_pr2_ff
: disp_functor_ff (compat_structures_pr2_disp_functor).
Proof.
intros X X' YZW YZW'.
destruct YZW as [ [Y Z] W].
destruct YZW' as [ [Y' Z'] W'].
unfold compat_structures_pr1_functor; simpl.
intros FX.
assert (structural_lemma :
∏ (B C : UU) (D : B -> C -> UU)
(H : ∏ c, iscontr (∑ b, D b c)),
isweq (fun bcd : ∑ (bc : B × C), D (pr1 bc) (pr2 bc)
=> pr2 (pr1 bcd))).
clear C X Y Z W X' Y' Z' W' FX.
{ intros B C D H.
use gradth.
+ intros c.
set (bd := iscontrpr1 (H c)).
exact ((pr1 bd,,c),, pr2 bd).
+ intros bcd; destruct bcd as [ [b c] d]; simpl.
refine (@maponpaths _ _
(fun bd : ∑ b', (D b' c) => ((pr1 bd),, c),, (pr2 bd))
_ (_,, _) _).
apply proofirrelevancecontr, H.
+ intros c; apply idpath. }
simple refine (structural_lemma _ _ (fun _ _ => unit) _).
intros FY. apply iscontraprop1.
- exact (term_from_qq_mor_unique FY W W').
- exact (term_from_qq_mor FY W W').
Qed.
Lemma compat_structures_pr2_is_equiv_over_id
: is_equiv_over_id (compat_structures_pr2_disp_functor).
Proof.
apply is_equiv_from_ff_ess_over_id.
- apply compat_structures_pr2_ess_split.
- apply compat_structures_pr2_ff.
Defined.
Definition compat_structures_pr2_equiv_over_id
: equiv_over_id _ _
:= compat_structures_pr2_is_equiv_over_id.
Definition compat_structures_pr2_inverse_over_id
: equiv_over_id
(qq_structure_disp_cat C) compat_structures_disp_cat.
Proof.
exact (equiv_inv _ (compat_structures_pr2_is_equiv_over_id)).
Defined.
End Strucs_Disp_Equiv.
Section Strucs_Fiber_Equiv.
Context (X : obj_ext_Precat C).
Definition term_struc_to_qq_struc_fiber_functor
: functor
(fiber_category (term_fun_disp_cat C) X)
(fiber_category (qq_structure_disp_cat C) X).
Proof.
eapply functor_composite.
- eapply fiber_functor.
exact compat_structures_pr1_inverse_over_id.
- exact (fiber_functor compat_structures_pr2_equiv_over_id X).
Defined.
Definition term_struc_to_qq_struc_is_equiv
: adj_equivalence_of_precats
term_struc_to_qq_struc_fiber_functor.
Proof.
use comp_adj_equivalence_of_precats.
- apply homset_property.
- apply homset_property.
- apply homset_property.
- apply fiber_equiv.
apply is_equiv_of_equiv_over_id.
- apply fiber_equiv.
apply is_equiv_of_equiv_over_id.
Defined.
End Strucs_Fiber_Equiv.
End Fix_Context.