Library UniMath.CategoryTheory.TwoSidedDisplayedCats.Total

Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Isos.
Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.
Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat.
Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos.
Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence.

Local Open Scope cat.

Definition transportb_total2
           {X Y : UU}
           (Z : X → Y → UU)
           {x₁ x₂ : X}
           (p : x₁ = x₂)
           (yz : ∑ (y : Y), Z x₂ y)
  : transportb
      (λ (x : X), ∑ (y : Y), Z x y)
      p
      yz
    =
    pr1 yz
    ,,
    transportb
      (λ x, Z x (pr1 yz))
      p
      (pr2 yz).
Show proof.
  induction p ; cbn.
  apply idpath.

Section TotalOfTwoSidedDispCat.
  Context {C₁ C₂ : category}
          (D : twosided_disp_cat C₁ C₂).

1. Total category
1.1. Definition
 Definition total_twosided_disp_precategory_ob_mor
    : precategory_ob_mor.
  Show proof.
    use make_precategory_ob_mor.
    - exact (∑ (x : C₁) (y : C₂), D x y).
    - exact (λ xy₁ xy₂,
             ∑ (f : pr1 xy₁ --> pr1 xy₂)
               (g : pr12 xy₁ --> pr12 xy₂),
             pr22 xy₁ -->[ f ][ g ] pr22 xy₂).

  Definition total_twosided_disp_precategory_data
    : precategory_data.
  Show proof.
    use make_precategory_data.
    - exact total_twosided_disp_precategory_ob_mor.
    - exact (λ xy,
             identity (pr1 xy)
             ,,
             identity (pr12 xy)
             ,,
             id_two_disp (pr22 xy)).
    - exact (λ xy₁ xy₂ xy₃ fg₁ fg₂,
             pr1 fg₁ · pr1 fg₂
             ,,
             pr12 fg₁ · pr12 fg₂
             ,,
             pr22 fg₁ ;;2 pr22 fg₂).

  Definition total_twosided_disp_is_precategory
    : is_precategory total_twosided_disp_precategory_data.
  Show proof.
    use make_is_precategory_one_assoc.
    - intros xy₁ xy₂ fg.
      use total2_paths_2_b.
      + apply id_left.
      + apply id_left.
      + apply id_two_disp_left.
    - intros xy₁ xy₂ fg.
      use total2_paths_2_b.
      + apply id_right.
      + apply id_right.
      + apply id_two_disp_right.
    - intros xy₁ xy₂ xy₃ xy₄ fg₁ fg₂ fg₃.
      use total2_paths_2_b.
      + apply assoc.
      + apply assoc.
      + apply assoc_two_disp.

  Definition total_twosided_disp_precategory
    : precategory.
  Show proof.
    use make_precategory.
    - exact total_twosided_disp_precategory_data.
    - exact total_twosided_disp_is_precategory.

  Definition has_homsets_total_twosided_disp_category
    : has_homsets total_twosided_disp_precategory_ob_mor.
  Show proof.
    intros xy₁ xy₂.
    apply isaset_total2.
    - apply homset_property.
    - intro.
      apply isaset_total2.
      + apply homset_property.
      + intro.
        apply isaset_disp_mor.

  Definition total_twosided_disp_category
    : category.
  Show proof.
    use make_category.
    - exact total_twosided_disp_precategory.
    - exact has_homsets_total_twosided_disp_category.

  Definition from_eq_total
             {x₁ x₂ : total_twosided_disp_category}
             {f g : x₁ --> x₂}
             (p : f = g)
    : pr22 f
      =
      transportb
        (λ z, _ -->[ z ][ _ ] _)
        (maponpaths (λ z, pr1 z) p)
        (transportb
           (λ z, _ -->[ _ ][ z ] _)
           (maponpaths (λ z, pr12 z) p)
           (pr22 g)).
  Show proof.
    induction p.
    apply idpath.

1.2. First and second projection
  Definition twosided_disp_category_pr1_data
    : functor_data total_twosided_disp_category C₁.
  Show proof.
    use make_functor_data.
    - exact (λ xy, pr1 xy).
    - exact (λ xy₁ xy₂ fg, pr1 fg).

  Definition twosided_disp_category_pr1_is_functor
    : is_functor twosided_disp_category_pr1_data.
  Show proof.
    refine (_ ,, _) ; intro ; intros ; cbn.
    - apply idpath.
    - apply idpath.

  Definition twosided_disp_category_pr1
    : total_twosided_disp_category ⟶ C₁.
  Show proof.
    use make_functor.
    - exact twosided_disp_category_pr1_data.
    - exact twosided_disp_category_pr1_is_functor.

  Definition twosided_disp_category_pr2_data
    : functor_data total_twosided_disp_category C₂.
  Show proof.
    use make_functor_data.
    - exact (λ xy, pr12 xy).
    - exact (λ xy₁ xy₂ fg, pr12 fg).

  Definition twosided_disp_category_pr2_is_functor
    : is_functor twosided_disp_category_pr2_data.
  Show proof.
    refine (_ ,, _) ; intro ; intros ; cbn.
    - apply idpath.
    - apply idpath.

  Definition twosided_disp_category_pr2
    : total_twosided_disp_category ⟶ C₂.
  Show proof.
    use make_functor.
    - exact twosided_disp_category_pr2_data.
    - exact twosided_disp_category_pr2_is_functor.

1.3. Isos in the total category
  Section IsoTotal.
    Context {x₁ x₂ : C₁}
            {y₁ y₂ : C₂}
            {xy₁ : D x₁ y₁}
            {xy₂ : D x₂ y₂}
            {f : x₁ --> x₂}
            {Hf : is_z_isomorphism f}
            {g : y₁ --> y₂}
            {Hg : is_z_isomorphism g}
            (fg : xy₁ -->[ f ][ g ] xy₂)
            (Hfg : is_iso_twosided_disp Hf Hg fg).

    Let total_fg : total_twosided_disp_category ⟦ (x₁ ,, y₁ ,, xy₁) , (x₂ ,, y₂ ,, xy₂) ⟧
        := f ,, g ,, fg.
    Let f_z_iso : z_iso x₁ x₂ := f ,, Hf.
    Let g_z_iso : z_iso y₁ y₂ := g ,, Hg.

    Definition is_z_iso_total_twosided_disp_cat_inv
      : total_twosided_disp_category ⟦ (x₂ ,, y₂ ,, xy₂) , (x₁ ,, y₁ ,, xy₁) ⟧
      := inv_from_z_iso f_z_iso
         ,,
         inv_from_z_iso g_z_iso
         ,,
         iso_inv_twosided_disp Hfg.

    Definition is_z_iso_total_twosided_disp_cat_inv_right
      : total_fg · is_z_iso_total_twosided_disp_cat_inv = identity _.
    Show proof.
      use total2_paths_2_b ; cbn.
      - apply (z_iso_inv_after_z_iso f_z_iso).
      - apply (z_iso_inv_after_z_iso g_z_iso).
      - apply inv_after_iso_twosided_disp.

    Definition is_z_iso_total_twosided_disp_cat_inv_left
      : is_z_iso_total_twosided_disp_cat_inv · total_fg = identity _.
    Show proof.
      use total2_paths_2_b ; cbn.
      - apply (z_iso_after_z_iso_inv f_z_iso).
      - apply (z_iso_after_z_iso_inv g_z_iso).
      - apply iso_after_inv_twosided_disp.

    Definition is_z_iso_total_twosided_disp_cat
      : is_z_isomorphism total_fg.
    Show proof.
      simple refine (is_z_iso_total_twosided_disp_cat_inv ,, _ ,, _).
      - apply is_z_iso_total_twosided_disp_cat_inv_right.
      - apply is_z_iso_total_twosided_disp_cat_inv_left.
  End IsoTotal.

  Definition make_z_iso_total_twosided_disp_cat
             {x₁ x₂ : C₁}
             {y₁ y₂ : C₂}
             {xy₁ : D x₁ y₁}
             {xy₂ : D x₂ y₂}
             {f : z_iso x₁ x₂}
             {g : z_iso y₁ y₂}
             (fg : iso_twosided_disp f g xy₁ xy₂)
    : @z_iso
        total_twosided_disp_category
        (x₁ ,, y₁ ,, xy₁)
        (x₂ ,, y₂ ,, xy₂).
  Show proof.
    simple refine (_ ,, _).
    - exact (pr1 f ,, pr1 g ,, pr1 fg).
    - use is_z_iso_total_twosided_disp_cat.
      + exact (pr2 f).
      + exact (pr2 g).
      + exact (pr2 fg).

  Section FromIsoTotal.
      Context {x₁ x₂ : C₁}
              {y₁ y₂ : C₂}
              {xy₁ : D x₁ y₁}
              {xy₂ : D x₂ y₂}
              (f : @z_iso
                     total_twosided_disp_category
                     (x₁ ,, y₁ ,, xy₁)
                     (x₂ ,, y₂ ,, xy₂)).

      Definition from_iso_total_twosided_disp_cat_pr1
        : z_iso x₁ x₂.
      Show proof.
        use make_z_iso.
        - exact (pr11 f).
        - exact (pr1 (inv_from_z_iso f)).
        - split.
          + exact (maponpaths pr1 (z_iso_inv_after_z_iso f)).
          + exact (maponpaths pr1 (z_iso_after_z_iso_inv f)).

      Definition from_iso_total_twosided_disp_cat_pr12
        : z_iso y₁ y₂.
      Show proof.
        use make_z_iso.
        - exact (pr121 f).
        - exact (pr12 (inv_from_z_iso f)).
        - split.
          + exact (maponpaths (λ z, pr12 z) (z_iso_inv_after_z_iso f)).
          + exact (maponpaths (λ z, pr12 z) (z_iso_after_z_iso_inv f)).

      Definition from_iso_total_twosided_disp_cat_pr22
        : iso_twosided_disp
            from_iso_total_twosided_disp_cat_pr1
            from_iso_total_twosided_disp_cat_pr12
            xy₁ xy₂.
      Show proof.
        simple refine (_ ,, _ ,, _ ,, _).
        - exact (pr221 f).
        - exact (pr22 (inv_from_z_iso f)).
        - exact (from_eq_total (z_iso_inv_after_z_iso f)).
        - exact (from_eq_total (z_iso_after_z_iso_inv f)).

      Definition from_iso_total_twosided_disp_cat
        : ∑ (f : z_iso x₁ x₂)
            (g : z_iso y₁ y₂),
          iso_twosided_disp f g xy₁ xy₂.
      Show proof.
        simple refine (_ ,, _ ,, _).
        - exact from_iso_total_twosided_disp_cat_pr1.
        - exact from_iso_total_twosided_disp_cat_pr12.
        - exact from_iso_total_twosided_disp_cat_pr22.
  End FromIsoTotal.

  Definition weq_z_iso_total_twosided_disp_cat_help_eq
             {x₁ x₂ : C₁}
             {y₁ y₂ : C₂}
             {xy₁ : D x₁ y₁}
             {xy₂ : D x₂ y₂}
             {fg₁ fg₂ : ∑ (f : z_iso x₁ x₂)
                          (g : z_iso y₁ y₂),
                        iso_twosided_disp f g xy₁ xy₂}
             (p : pr11 fg₁ = pr11 fg₂)
             (q : pr112 fg₁ = pr112 fg₂)
             (r : pr122 fg₁
                  =
                  transportb
                    (λ z, _ -->[ z ][ _ ] _)
                    p
                    (transportb
                       (λ z, _ -->[ _ ][ z ] _)
                       q
                       (pr122 fg₂)))
    : fg₁ = fg₂.
  Show proof.
    induction fg₁ as [ f₁ fg₁ ].
    induction fg₁ as [ g₁ fg₁ ].
    induction f₁ as [ f₁ Hf₁ ].
    induction g₁ as [ g₁ Hg₁ ].
    induction fg₁ as [ fg₁ Hfg₁ ].
    induction fg₂ as [ f₂ fg₂ ].
    induction fg₂ as [ g₂ fg₂ ].
    induction f₂ as [ f₂ Hf₂ ].
    induction g₂ as [ g₂ Hg₂ ].
    induction fg₂ as [ fg₂ Hfg₂ ].
    cbn in *.
    induction p ; induction q ; cbn in *.
    induction r.
    assert (p : Hf₁ = Hf₂) by apply isaprop_is_z_isomorphism.
    induction p.
    apply maponpaths.
    assert (p : Hg₁ = Hg₂) by apply isaprop_is_z_isomorphism.
    induction p.
    do 2 apply maponpaths.
    apply isaprop_is_iso_twosided_disp.

  Definition weq_z_iso_total_twosided_disp_cat
             {x₁ x₂ : C₁}
             {y₁ y₂ : C₂}
             (xy₁ : D x₁ y₁)
             (xy₂ : D x₂ y₂)
    : (∑ (f : z_iso x₁ x₂)
         (g : z_iso y₁ y₂),
       iso_twosided_disp f g xy₁ xy₂)
      ≃
      (@z_iso
          total_twosided_disp_category
          (x₁ ,, y₁ ,, xy₁)
          (x₂ ,, y₂ ,, xy₂)).
  Show proof.
    use weq_iso.
    - exact (λ fg, make_z_iso_total_twosided_disp_cat (pr22 fg)).
    - exact from_iso_total_twosided_disp_cat.
    - abstract
        (intros f ;
         use weq_z_iso_total_twosided_disp_cat_help_eq ; apply idpath).
    - abstract
        (intros f ;
         use subtypePath ; [ intro ; apply isaprop_is_z_isomorphism | ] ;
         apply idpath).

1.4. Univalence of the total category
  Definition is_univalent_total_twosided_disp_category
             (HC₁ : is_univalent C₁)
             (HC₂ : is_univalent C₂)
             (HD : is_univalent_twosided_disp_cat D)
    : is_univalent total_twosided_disp_category.
  Show proof.
    intros x y.
    use weqhomot.
    - refine (weq_z_iso_total_twosided_disp_cat _ _
              ∘ weqtotal2
                  (_ ,, HC₁ _ _)
                  (λ p,
                  weqtotal2
                    (_ ,, HC₂ _ _)
                    (λ q, (_ ,, HD _ _ _ _ p q _ _))
              ∘ _
              ∘ total2_paths_equiv _ _ _)
              ∘ total2_paths_equiv _ _ _)%weq ; cbn.
      induction x, y.
      cbn in *.
      induction p.
      exact (idweq _).
    - abstract
        (intro p ;
         induction p ;
         use subtypePath ; [ intro ; apply isaprop_is_z_isomorphism | ] ;
         apply idpath).

2. Left total displayed category
2.1. Definition
  Definition left_total_of_twosided_disp_cat_ob_mor
    : disp_cat_ob_mor C₂.
  Show proof.
    simple refine (_ ,, _).
    - exact (λ y, ∑ (x : C₁), D x y).
    - exact (λ y₁ y₂ xy₁ xy₂ g,
             ∑ (f : pr1 xy₁ --> pr1 xy₂),
             pr2 xy₁ -->[ f ][ g ] pr2 xy₂).

  Definition left_total_of_twosided_disp_cat_id_comp
    : disp_cat_id_comp C₂ left_total_of_twosided_disp_cat_ob_mor.
  Show proof.
    split.
    - exact (λ y xy, identity (pr1 xy) ,, id_two_disp (pr2 xy)).
    - exact (λ y₁ y₂ y₃ g₁ g₂ xy₁ xy₂ xy₃ fg₁ fg₂,
             pr1 fg₁ · pr1 fg₂
             ,,
             (pr2 fg₁ ;;2 pr2 fg₂)).

  Definition left_total_of_twosided_disp_cat_data
    : disp_cat_data C₂.
  Show proof.
    simple refine (_ ,, _).
    - exact left_total_of_twosided_disp_cat_ob_mor.
    - exact left_total_of_twosided_disp_cat_id_comp.

  Definition left_total_of_twosided_disp_cat_axioms
    : disp_cat_axioms C₂ left_total_of_twosided_disp_cat_data.
  Show proof.
    repeat split.
    - intro ; intros.
      unfold mor_disp ; cbn.
      rewrite transportb_total2.
      use total2_paths_f.
      + apply id_left.
      + cbn.
        rewrite id_two_disp_left.
        unfold transportb_disp_mor2, transportf_disp_mor2.
        apply (transportfbinv (λ z, _ -->[ z ][ _ ] _) _ _).
    - intro ; intros.
      unfold mor_disp ; cbn.
      rewrite transportb_total2.
      use total2_paths_f.
      + apply id_right.
      + cbn.
        rewrite id_two_disp_right.
        apply (transportfbinv (λ z, _ -->[ z ][ _ ] _) _ _).
    - intro ; intros.
      unfold mor_disp ; cbn.
      rewrite transportb_total2.
      use total2_paths_f.
      + apply assoc.
      + cbn.
        rewrite assoc_two_disp.
        apply (transportfbinv (λ z, _ -->[ z ][ _ ] _) _ _).
    - intros.
      apply isaset_total2.
      + apply homset_property.
      + intro.
        apply isaset_disp_mor.

  Definition left_total_of_twosided_disp_cat
    : disp_cat C₂.
  Show proof.
    simple refine (_ ,, _).
    - exact left_total_of_twosided_disp_cat_data.
    - exact left_total_of_twosided_disp_cat_axioms.

2.2. Isomorphisms
  Definition make_iso_left_total_of_twosided_disp_cat
             {y : C₂}
             {xy₁ xy₂ : left_total_of_twosided_disp_cat y}
             (f : z_iso (pr1 xy₁) (pr1 xy₂))
             (fg : iso_twosided_disp f (identity_z_iso _) (pr2 xy₁) (pr2 xy₂))
    : z_iso_disp (identity_z_iso _) xy₁ xy₂.
  Show proof.
    simple refine (_ ,, _ ,, _ ,, _).
    - exact (pr1 f ,, pr1 fg).
    - exact (pr12 f ,, pr12 fg).
    - abstract
        (unfold mor_disp ; cbn ;
         rewrite transportb_total2 ; cbn ;
         use total2_paths_f ; [ apply z_iso_after_z_iso_inv | ] ;
         cbn ;
         etrans ; [ apply maponpaths ; apply (iso_after_inv_twosided_disp (pr2 fg)) | ] ;
         apply (transportfbinv (λ z, _ -->[ z ][ _ ] _) _ _)).
    - abstract
        (unfold mor_disp ; cbn ;
         rewrite transportb_total2 ; cbn ;
         use total2_paths_f ; [ apply z_iso_inv_after_z_iso | ] ;
         cbn ;
         etrans ; [ apply maponpaths ; apply (inv_after_iso_twosided_disp (pr2 fg)) | ] ;
         apply (transportfbinv (λ z, _ -->[ z ][ _ ] _) _ _)).

  Definition from_iso_left_total_of_twosided_disp_cat_pr1
             {y : C₂}
             {xy₁ xy₂ : left_total_of_twosided_disp_cat y}
             (f : z_iso_disp (identity_z_iso _) xy₁ xy₂)
    : z_iso (pr1 xy₁) (pr1 xy₂).
  Show proof.
    simple refine (_ ,, _ ,, _ ,, _).
    - exact (pr11 f).
    - exact (pr112 f).
    - abstract
        (refine (maponpaths pr1 (inv_mor_after_z_iso_disp f) @ _) ;
         unfold mor_disp ; cbn ;
         rewrite transportb_total2 ;
         apply idpath).
    - abstract
        (refine (maponpaths pr1 (z_iso_disp_after_inv_mor f) @ _) ;
         unfold mor_disp ; cbn ;
         rewrite transportb_total2 ;
         apply idpath).

  Definition from_iso_left_total_of_twosided_disp_cat_pr2
             {y : C₂}
             {xy₁ xy₂ : left_total_of_twosided_disp_cat y}
             (f : z_iso_disp (identity_z_iso _) xy₁ xy₂)
    : iso_twosided_disp
        (from_iso_left_total_of_twosided_disp_cat_pr1 f)
        (identity_z_iso _) (pr2 xy₁) (pr2 xy₂).
  Show proof.
    simple refine (_ ,, _ ,, _ ,, _).
    - exact (pr21 f).
    - exact (pr212 f).
    - abstract
        (pose (p := inv_mor_after_z_iso_disp f) ; unfold mor_disp in p ; cbn in p ;
         rewrite transportb_total2 in p ;
         refine (!(fiber_paths (!p)) @ _) ; cbn ;
         unfold transportb, transportb_disp_mor2, transportf_disp_mor2 ;
         rewrite !twosided_prod_transport ;
         apply maponpaths_2 ;
         apply isaset_dirprod ; apply homset_property).
    - abstract
        (pose (p := z_iso_disp_after_inv_mor f) ; unfold mor_disp in p ; cbn in p ;
         rewrite transportb_total2 in p ;
         refine (!(fiber_paths (!p)) @ _) ; cbn ;
         unfold transportb, transportb_disp_mor2, transportf_disp_mor2 ;
         rewrite !twosided_prod_transport ;
         apply maponpaths_2 ;
         apply isaset_dirprod ; apply homset_property).

  Definition weq_iso_left_total_of_twosided_disp_cat_eq_help
             {y : C₂}
             {xy₁ xy₂ : left_total_of_twosided_disp_cat y}
             {fg₁ fg₂ : ∑ (f : z_iso (pr1 xy₁) (pr1 xy₂)),
                        iso_twosided_disp
                          f (identity_z_iso _)
                          (pr2 xy₁) (pr2 xy₂)}
             (p : pr11 fg₁ = pr11 fg₂)
             (q : pr12 fg₁
                  =
                  transportb
                    (λ z, _ -->[ z ][ _ ] _)
                    p
                    (pr12 fg₂))
    : fg₁ = fg₂.
  Show proof.
    induction fg₁ as [ f₁ fg₁ ].
    induction f₁ as [ f₁ Hf₁ ].
    induction fg₁ as [ fg₁ Hfg₁ ].
    induction fg₂ as [ f₂ fg₂ ].
    induction f₂ as [ f₂ Hf₂ ].
    induction fg₂ as [ fg₂ Hfg₂ ].
    cbn in *.
    induction p ; cbn in *.
    induction q.
    assert (Hf₁ = Hf₂) as p by apply isaprop_is_z_isomorphism.
    induction p.
    do 2 apply maponpaths.
    apply isaprop_is_iso_twosided_disp.

  Definition weq_iso_left_total_of_twosided_disp_cat
             {y : C₂}
             (xy₁ xy₂ : left_total_of_twosided_disp_cat y)
    : (∑ (f : z_iso (pr1 xy₁) (pr1 xy₂)),
       iso_twosided_disp f (identity_z_iso _) (pr2 xy₁) (pr2 xy₂))
      ≃
      z_iso_disp (identity_z_iso _) xy₁ xy₂.
  Show proof.
    use weq_iso.
    - exact (λ f, make_iso_left_total_of_twosided_disp_cat (pr1 f) (pr2 f)).
    - exact (λ f,
             from_iso_left_total_of_twosided_disp_cat_pr1 f
             ,,
             from_iso_left_total_of_twosided_disp_cat_pr2 f).
    - abstract
        (intro f ;
         cbn ;
         use weq_iso_left_total_of_twosided_disp_cat_eq_help ;
         apply idpath).
    - abstract
        (intro f ;
         use subtypePath ; [ intro ; apply isaprop_is_z_iso_disp | ] ;
         apply idpath).

2.3. The univalence
  Definition is_univalent_left_total_of_twosided_disp_cat
             (HC₁ : is_univalent C₁)
             (HD : is_univalent_twosided_disp_cat D)
    : is_univalent_disp left_total_of_twosided_disp_cat.
  Show proof.
    intros y₁ y₂ p xy₁ xy₂.
    induction p.
    use weqhomot.
    - exact (weq_iso_left_total_of_twosided_disp_cat xy₁ xy₂
             ∘ weqtotal2
                 (_ ,, HC₁ _ _)
                 (λ p, (_ ,, HD _ _ _ _ p (idpath _) (pr2 xy₁) (pr2 xy₂)))
             ∘ total2_paths_equiv _ _ _)%weq.
    - abstract
        (intro p ;
         induction p ;
         use subtypePath ; [ intro ; apply isaprop_is_z_iso_disp | ] ;
         cbn ;
         apply idpath).

3. Right total displayed category
3.1. Definition
  Definition right_total_of_twosided_disp_cat_ob_mor
    : disp_cat_ob_mor C₁.
  Show proof.
    simple refine (_ ,, _).
    - exact (λ x, ∑ (y : C₂), D x y).
    - exact (λ x₁ x₂ xy₁ xy₂ f,
             ∑ (g : pr1 xy₁ --> pr1 xy₂),
             pr2 xy₁ -->[ f ][ g ] pr2 xy₂).

  Definition right_total_of_twosided_disp_cat_id_comp
    : disp_cat_id_comp C₁ right_total_of_twosided_disp_cat_ob_mor.
  Show proof.
    split.
    - exact (λ x xy, identity (pr1 xy) ,, id_two_disp (pr2 xy)).
    - exact (λ x₁ x₂ x₃ f₁ f₂ xy₁ xy₂ xy₃ fg₁ fg₂,
             pr1 fg₁ · pr1 fg₂
             ,,
             (pr2 fg₁ ;;2 pr2 fg₂)).

  Definition right_total_of_twosided_disp_cat_data
    : disp_cat_data C₁.
  Show proof.
    simple refine (_ ,, _).
    - exact right_total_of_twosided_disp_cat_ob_mor.
    - exact right_total_of_twosided_disp_cat_id_comp.

  Definition right_total_of_twosided_disp_cat_axioms
    : disp_cat_axioms C₁ right_total_of_twosided_disp_cat_data.
  Show proof.
    repeat split.
    - intro ; intros.
      unfold mor_disp ; cbn.
      rewrite transportb_total2.
      use total2_paths_f.
      + apply id_left.
      + cbn.
        rewrite id_two_disp_left.
        unfold transportb, transportb_disp_mor2, transportf_disp_mor2.
        rewrite <- twosided_swap_transport.
        apply transportfbinv.
    - intro ; intros.
      unfold mor_disp ; cbn.
      rewrite transportb_total2.
      use total2_paths_f.
      + apply id_right.
      + cbn.
        rewrite id_two_disp_right.
        unfold transportb, transportb_disp_mor2, transportf_disp_mor2.
        rewrite <- twosided_swap_transport.
        apply transportfbinv.
    - intro ; intros.
      unfold mor_disp ; cbn.
      rewrite transportb_total2.
      use total2_paths_f.
      + apply assoc.
      + cbn.
        rewrite assoc_two_disp.
        unfold transportb, transportb_disp_mor2, transportf_disp_mor2.
        rewrite <- twosided_swap_transport.
        apply transportfbinv.
    - intros.
      apply isaset_total2.
      + apply homset_property.
      + intro.
        apply isaset_disp_mor.

  Definition right_total_of_twosided_disp_cat
    : disp_cat C₁.
  Show proof.
    simple refine (_ ,, _).
    - exact right_total_of_twosided_disp_cat_data.
    - exact right_total_of_twosided_disp_cat_axioms.

3.2. Isomorphisms
  Definition make_iso_right_total_of_twosided_disp_cat
             {x : C₁}
             {xy₁ xy₂ : right_total_of_twosided_disp_cat x}
             (g : z_iso (pr1 xy₁) (pr1 xy₂))
             (fg : iso_twosided_disp (identity_z_iso _) g (pr2 xy₁) (pr2 xy₂))
    : z_iso_disp (identity_z_iso _) xy₁ xy₂.
  Show proof.
    simple refine (_ ,, _ ,, _ ,, _).
    - exact (pr1 g ,, pr1 fg).
    - exact (pr12 g ,, pr12 fg).
    - abstract
        (unfold mor_disp ; cbn ;
         rewrite transportb_total2 ; cbn ;
         use total2_paths_f ; [ apply z_iso_after_z_iso_inv | ] ;
         cbn ;
         etrans ; [ apply maponpaths ; apply (iso_after_inv_twosided_disp (pr2 fg)) | ] ;
         unfold transportb, transportb_disp_mor2, transportf_disp_mor2 ;
         rewrite <- twosided_swap_transport ;
         apply transportfbinv).
    - abstract
        (unfold mor_disp ; cbn ;
         rewrite transportb_total2 ; cbn ;
         use total2_paths_f ; [ apply z_iso_inv_after_z_iso | ] ;
         cbn ;
         etrans ; [ apply maponpaths ; apply (inv_after_iso_twosided_disp (pr2 fg)) | ] ;
         unfold transportb, transportb_disp_mor2, transportf_disp_mor2 ;
         rewrite <- twosided_swap_transport ;
         apply transportfbinv).

  Definition from_iso_right_total_of_twosided_disp_cat_pr1
             {x : C₁}
             {xy₁ xy₂ : right_total_of_twosided_disp_cat x}
             (g : z_iso_disp (identity_z_iso _) xy₁ xy₂)
    : z_iso (pr1 xy₁) (pr1 xy₂).
  Show proof.
    simple refine (_ ,, _ ,, _ ,, _).
    - exact (pr11 g).
    - exact (pr112 g).
    - abstract
        (refine (maponpaths pr1 (inv_mor_after_z_iso_disp g) @ _) ;
         unfold mor_disp ; cbn ;
         rewrite transportb_total2 ;
         apply idpath).
    - abstract
        (refine (maponpaths pr1 (z_iso_disp_after_inv_mor g) @ _) ;
         unfold mor_disp ; cbn ;
         rewrite transportb_total2 ;
         apply idpath).

  Definition from_iso_right_total_of_twosided_disp_cat_pr2
             {x : C₁}
             {xy₁ xy₂ : right_total_of_twosided_disp_cat x}
             (g : z_iso_disp (identity_z_iso _) xy₁ xy₂)
    : iso_twosided_disp
        (identity_z_iso _)
        (from_iso_right_total_of_twosided_disp_cat_pr1 g)
        (pr2 xy₁) (pr2 xy₂).
  Show proof.
    simple refine (_ ,, _ ,, _ ,, _).
    - exact (pr21 g).
    - exact (pr212 g).
    - abstract
        (pose (p := inv_mor_after_z_iso_disp g) ; unfold mor_disp in p ; cbn in p ;
         rewrite transportb_total2 in p ;
         refine (!(fiber_paths (!p)) @ _) ; cbn ;
         unfold transportb, transportb_disp_mor2, transportf_disp_mor2 ;
         rewrite twosided_swap_transport ;
         rewrite !twosided_prod_transport ;
         apply maponpaths_2 ;
         apply isaset_dirprod ; apply homset_property).
    - abstract
        (pose (p := z_iso_disp_after_inv_mor g) ; unfold mor_disp in p ; cbn in p ;
         rewrite transportb_total2 in p ;
         refine (!(fiber_paths (!p)) @ _) ; cbn ;
         unfold transportb, transportb_disp_mor2, transportf_disp_mor2 ;
         rewrite twosided_swap_transport ;
         rewrite !twosided_prod_transport ;
         apply maponpaths_2 ;
         apply isaset_dirprod ; apply homset_property).

  Definition weq_iso_right_total_of_twosided_disp_cat_eq_help
             {x : C₁}
             {xy₁ xy₂ : right_total_of_twosided_disp_cat x}
             {fg₁ fg₂ : ∑ (g : z_iso (pr1 xy₁) (pr1 xy₂)),
                        iso_twosided_disp
                          (identity_z_iso _)
                          g
                          (pr2 xy₁) (pr2 xy₂)}
             (p : pr11 fg₁ = pr11 fg₂)
             (q : pr12 fg₁
                  =
                  transportb
                    (λ z, _ -->[ _ ][ z ] _)
                    p
                    (pr12 fg₂))
    : fg₁ = fg₂.
  Show proof.
    induction fg₁ as [ f₁ fg₁ ].
    induction f₁ as [ f₁ Hf₁ ].
    induction fg₁ as [ fg₁ Hfg₁ ].
    induction fg₂ as [ f₂ fg₂ ].
    induction f₂ as [ f₂ Hf₂ ].
    induction fg₂ as [ fg₂ Hfg₂ ].
    cbn in *.
    induction p ; cbn in *.
    induction q.
    assert (Hf₁ = Hf₂) as p by apply isaprop_is_z_isomorphism.
    induction p.
    do 2 apply maponpaths.
    apply isaprop_is_iso_twosided_disp.

  Definition weq_iso_right_total_of_twosided_disp_cat
             {x : C₁}
             (xy₁ xy₂ : right_total_of_twosided_disp_cat x)
    : (∑ (g : z_iso (pr1 xy₁) (pr1 xy₂)),
       iso_twosided_disp (identity_z_iso _) g (pr2 xy₁) (pr2 xy₂))
      ≃
      z_iso_disp (identity_z_iso _) xy₁ xy₂.
  Show proof.
    use weq_iso.
    - exact (λ f, make_iso_right_total_of_twosided_disp_cat (pr1 f) (pr2 f)).
    - exact (λ f,
             from_iso_right_total_of_twosided_disp_cat_pr1 f
             ,,
             from_iso_right_total_of_twosided_disp_cat_pr2 f).
    - abstract
        (intro f ;
         cbn ;
         use weq_iso_right_total_of_twosided_disp_cat_eq_help ;
         apply idpath).
    - abstract
        (intro f ;
         use subtypePath ; [ intro ; apply isaprop_is_z_iso_disp | ] ;
         apply idpath).

3.3. The univalence
  Definition is_univalent_right_total_of_twosided_disp_cat
             (HC₂ : is_univalent C₂)
             (HD : is_univalent_twosided_disp_cat D)
    : is_univalent_disp right_total_of_twosided_disp_cat.
  Show proof.
    intros y₁ y₂ p xy₁ xy₂.
    induction p.
    use weqhomot.
    - exact (weq_iso_right_total_of_twosided_disp_cat xy₁ xy₂
             ∘ weqtotal2
                 (_ ,, HC₂ _ _)
                 (λ q, (_ ,, HD _ _ _ _ (idpath _) q (pr2 xy₁) (pr2 xy₂)))
             ∘ total2_paths_equiv _ _ _)%weq.
    - abstract
        (intro p ;
         induction p ;
         use subtypePath ; [ intro ; apply isaprop_is_z_iso_disp | ] ;
         cbn ;
         apply idpath).
End TotalOfTwoSidedDispCat.