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.

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.

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.

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.