Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Prelude.
Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Isos.
Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.
Require Import UniMath.CategoryTheory.DisplayedCats.Functors.
Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations.
Require Import UniMath.CategoryTheory.DisplayedCats.Fiber.
Require Import UniMath.CategoryTheory.DisplayedCats.Projection.
Require Import UniMath.CategoryTheory.Limits.Terminal.
Require Import UniMath.CategoryTheory.Limits.BinProducts.
Require Import UniMath.CategoryTheory.Limits.Preservation.

Local Open Scope cat.

Declare Scope hyperdoctrine.
Delimit Scope hyperdoctrine with hd.

Local Open Scope hd.

Definition preorder_hyperdoctrine
  : UU
  := ∑ (C : category)
       (D : disp_cat C),
     Terminal C
     ×
     BinProducts C
     ×
     cleaving D
     ×
     locally_propositional D.

Definition make_preorder_hyperdoctrine
           (C : category)
           (D : disp_cat C)
           (T : Terminal C)
           (BP : BinProducts C)
           (HD : cleaving D)
           (HD' : locally_propositional D)
  : preorder_hyperdoctrine
  := C ,, D ,, T ,, BP ,, HD ,, HD'.

Definition hyperdoctrine
  : UU
  := ∑ (C : category)
       (D : disp_cat C),
     Terminal C
     ×
     BinProducts C
     ×
     cleaving D
     ×
     locally_propositional D
     ×
     is_univalent_disp D.

Definition make_hyperdoctrine
           (C : category)
           (D : disp_cat C)
           (T : Terminal C)
           (BP : BinProducts C)
           (HD : cleaving D)
           (HD' : locally_propositional D)
           (HD'' : is_univalent_disp D)
  : hyperdoctrine
  := C ,, D ,, T ,, BP ,, HD ,, HD' ,, HD''.

Definition univalent_hyperdoctrine
  : UU
  := ∑ (C : category)
       (D : disp_cat C),
     Terminal C
     ×
     BinProducts C
     ×
     cleaving D
     ×
     locally_propositional D
     ×
     is_univalent_disp D
     ×
     is_univalent C.

Definition make_univalent_hyperdoctrine
           (C : category)
           (D : disp_cat C)
           (T : Terminal C)
           (BP : BinProducts C)
           (HD : cleaving D)
           (HD' : locally_propositional D)
           (HD'' : is_univalent_disp D)
           (HC : is_univalent C)
  : univalent_hyperdoctrine
  := C ,, D ,, T ,, BP ,, HD ,, HD' ,, HD'' ,, HC.

Coercion hyperdoctrine_to_preorder_hyperdoctrine
         (H : hyperdoctrine)
  : preorder_hyperdoctrine.
Show proof.

Coercion univalent_hyperdoctrine_to_hyperdoctrine
         (H : univalent_hyperdoctrine)
  : hyperdoctrine.
Show proof.

Definition hyperdoctrine_type_category
           (H : preorder_hyperdoctrine)
  : category
  := pr1 H.

Definition hyperdoctrine_type
           (H : preorder_hyperdoctrine)
  : UU
  := ob (hyperdoctrine_type_category H).

Notation "'ty'" := hyperdoctrine_type : hyperdoctrine.

Definition hyperdoctrine_terminal_type
           (H : preorder_hyperdoctrine)
  : Terminal (hyperdoctrine_type_category H)
  := pr122 H.

Definition hyperdoctrine_unit_type
           {H : preorder_hyperdoctrine}
  : ty H
  := TerminalObject (hyperdoctrine_terminal_type H).

Notation "'𝟙'" := hyperdoctrine_unit_type : hyperdoctrine.

Definition hyperdoctrine_binproducts
           (H : preorder_hyperdoctrine)
  : BinProducts (hyperdoctrine_type_category H)
  := pr1 (pr222 H).

Definition hyperdoctrine_product
           {H : preorder_hyperdoctrine}
           (A B : ty H)
  : ty H
  := BinProductObject _ (hyperdoctrine_binproducts H A B).

Notation "A ×h B" := (hyperdoctrine_product A B) (at level 75, right associativity)
    : hyperdoctrine.

Definition hyperdoctrine_term
           {H : preorder_hyperdoctrine}
           (Γ A : ty H)
  : UU
  := Γ --> A.

Notation "'tm'" := hyperdoctrine_term : hyperdoctrine.

Definition tm_var
           {H : preorder_hyperdoctrine}
           (A : ty H)
  : tm A A
  := identity _.

Definition tm_subst
           {H : preorder_hyperdoctrine}
           {Γ₁ Γ₂ A : ty H}
           (t : tm Γ₂ A)
           (s : tm Γ₁ Γ₂)
  : tm Γ₁ A
  := s · t.

Notation "t [ s ]tm" := (tm_subst t s) (at level 10) : hyperdoctrine.

Proposition tm_subst_var
            {H : preorder_hyperdoctrine}
            {Γ A : ty H}
            (t : tm Γ A)
  : t [ tm_var Γ ]tm = t.
Show proof.

Proposition var_tm_subst
            {H : preorder_hyperdoctrine}
            {Γ A : ty H}
            (t : tm Γ A)
  : (tm_var A) [ t ]tm = t.
Show proof.

Proposition tm_subst_comp
            {H : preorder_hyperdoctrine}
            {Γ₁ Γ₂ Γ₃ A : ty H}
            (s₁ : tm Γ₁ Γ₂)
            (s₂ : tm Γ₂ Γ₃)
            (t : tm Γ₃ A)
  : (t [ s₂ ]tm) [ s₁ ]tm = t [ s₂ [ s₁ ]tm ]tm.
Show proof.

Definition hyperdoctrine_unit_term
           {H : preorder_hyperdoctrine}
           {Γ : ty H}
  : tm Γ 𝟙
  := TerminalArrow _ _.

Notation "'!!'" := hyperdoctrine_unit_term : hyperdoctrine.

Proposition hyperdoctrine_unit_eq
            {H : preorder_hyperdoctrine}
            {Γ : ty H}
            (t₁ t₂ : tm Γ 𝟙)
  : t₁ = t₂.
Show proof.

Proposition hyperdoctrine_unit_eta
            {H : preorder_hyperdoctrine}
            {Γ : ty H}
            (t : tm Γ 𝟙)
  : t = !!.
Show proof.

Proposition hyperdoctrine_unit_tm_subst
            {H : preorder_hyperdoctrine}
            {Γ Γ' : ty H}
            (s : tm Γ Γ')
  : !! [ s ]tm = !!.
Show proof.

Definition hyperdoctrine_pr1
           {H : preorder_hyperdoctrine}
           {Γ A B : ty H}
           (t : tm Γ (A ×h B))
  : tm Γ A
  := t · BinProductPr1 _ _.

Notation "'π₁'" := hyperdoctrine_pr1 : hyperdoctrine.

Definition hyperdoctrine_pr2
           {H : preorder_hyperdoctrine}
           {Γ A B : ty H}
           (t : tm Γ (A ×h B))
  : tm Γ B
  := t · BinProductPr2 _ _.

Notation "'π₂'" := hyperdoctrine_pr2 : hyperdoctrine.

Definition hyperdoctrine_pair
           {H : preorder_hyperdoctrine}
           {Γ A B : ty H}
           (t₁ : tm Γ A)
           (t₂ : tm Γ B)
  : tm Γ (A ×h B)
  := BinProductArrow _ _ t₁ t₂.

Notation "⟨ t₁ , t₂ ⟩" := (hyperdoctrine_pair t₁ t₂) : hyperdoctrine.

Definition hyperdoctrine_diag
           {H : preorder_hyperdoctrine}
           (A : ty H)
  : tm A (A ×h A)
  := ⟨ tm_var _ , tm_var _ ⟩.

Notation "Δ_{ A }" := (hyperdoctrine_diag A) : hyperdoctrine.

Proposition hyperdoctrine_pair_pr1
            {H : preorder_hyperdoctrine}
            {Γ A B : ty H}
            (t₁ : tm Γ A)
            (t₂ : tm Γ B)
  : π₁ ⟨ t₁ , t₂ ⟩ = t₁.
Show proof.

Proposition hyperdoctrine_pair_pr2
            {H : preorder_hyperdoctrine}
            {Γ A B : ty H}
            (t₁ : tm Γ A)
            (t₂ : tm Γ B)
  : π₂ ⟨ t₁ , t₂ ⟩ = t₂.
Show proof.

Proposition hyperdoctrine_pr1_subst
            {H : preorder_hyperdoctrine}
            {Γ Γ' A B : ty H}
            (s : tm Γ Γ')
            (t : tm Γ' (A ×h B))
  : (π₁ t) [ s ]tm = π₁ (t [ s ]tm).
Show proof.

Proposition hyperdoctrine_pr1_comp
            {H : preorder_hyperdoctrine}
            {Γ Γ' A B : ty H}
            (s : tm Γ Γ')
            (t : tm Γ' (A ×h B))
  : s · π₁ t = π₁ (s · t).
Show proof.

Proposition hyperdoctrine_pair_comp_pr1
            {H : preorder_hyperdoctrine}
            {Γ A B : ty H}
            (t₁ : tm Γ A)
            (t₂ : tm Γ B)
  : (π₁ (tm_var _)) [ ⟨ t₁ , t₂ ⟩ ]tm = t₁.
Show proof.

Proposition hyperdoctrine_pair_comp_pr1'
            {H : preorder_hyperdoctrine}
            {Γ A B : ty H}
            (t₁ : tm Γ A)
            (t₂ : tm Γ B)
  : ⟨ t₁, t₂ ⟩ · π₁ (tm_var (A ×h B)) = t₁.
Show proof.

Proposition hyperdoctrine_pr2_subst
            {H : preorder_hyperdoctrine}
            {Γ Γ' A B : ty H}
            (s : tm Γ Γ')
            (t : tm Γ' (A ×h B))
  : (π₂ t) [ s ]tm = π₂ (t [ s ]tm).
Show proof.

Proposition hyperdoctrine_pr2_comp
            {H : preorder_hyperdoctrine}
            {Γ Γ' A B : ty H}
            (s : tm Γ Γ')
            (t : tm Γ' (A ×h B))
  : s · π₂ t = π₂ (s · t).
Show proof.

Proposition hyperdoctrine_pair_comp_pr2
            {H : preorder_hyperdoctrine}
            {Γ A B : ty H}
            (t₁ : tm Γ A)
            (t₂ : tm Γ B)
  : (π₂ (tm_var _)) [ ⟨ t₁ , t₂ ⟩ ]tm = t₂.
Show proof.

Proposition hyperdoctrine_pair_comp_pr2'
            {H : preorder_hyperdoctrine}
            {Γ A B : ty H}
            (t₁ : tm Γ A)
            (t₂ : tm Γ B)
  : ⟨ t₁, t₂ ⟩ · π₂ (tm_var (A ×h B)) = t₂.
Show proof.

Proposition hyperdoctrine_pair_subst
            {H : preorder_hyperdoctrine}
            {Γ Γ' A B : ty H}
            (s : tm Γ Γ')
            (t₁ : tm Γ' A)
            (t₂ : tm Γ' B)
  : ⟨ t₁ , t₂ ⟩ [ s ]tm = ⟨ t₁ [ s ]tm , t₂ [ s ]tm ⟩.
Show proof.

Proposition hyperdoctrine_pair_comp
            {H : preorder_hyperdoctrine}
            {Γ Γ' A B : ty H}
            (s : tm Γ Γ')
            (t₁ : tm Γ' A)
            (t₂ : tm Γ' B)
  : s · ⟨ t₁, t₂ ⟩ = ⟨ s · t₁, s · t₂ ⟩.
Show proof.

Proposition hyperdoctrine_pair_eta
            {H : preorder_hyperdoctrine}
            {Γ A B : ty H}
            (t : tm Γ (A ×h B))
  : t = ⟨ π₁ t , π₂ t ⟩.
Show proof.

Proposition hyperdoctrine_diag_subst
            {H : preorder_hyperdoctrine}
            {Γ A : ty H}
            (t : tm Γ A)
  : Δ_{ A } [ t ]tm = ⟨ t , t ⟩.
Show proof.

Definition hyperdoctrine_formula_disp_cat
           (H : preorder_hyperdoctrine)
  : disp_cat (hyperdoctrine_type_category H)
  := pr12 H.

Definition hyperdoctrine_formula
           {H : preorder_hyperdoctrine}
           (A : ty H)
  : UU
  := ob_disp (hyperdoctrine_formula_disp_cat H) A.

Notation "'form'" := hyperdoctrine_formula : hyperdoctrine.

Definition is_univalent_disp_hyperdoctrine
           (H : hyperdoctrine)
  : is_univalent_disp _
  := pr222 (pr222 H).

Proposition isaset_hyperdoctrine_formula
            {H : hyperdoctrine}
            (A : ty H)
  : isaset (form A).
Show proof.

Definition hyperdoctrine_proof
           {H : preorder_hyperdoctrine}
           {A : ty H}
           (Δ ψ : form A)
  : UU
  := Δ -->[ identity _ ] ψ.

Notation "Δ ⊢ ψ" := (hyperdoctrine_proof Δ ψ) (at level 100) : hyperdoctrine.

Proposition hyperdoctrine_proof_eq
            {H : preorder_hyperdoctrine}
            {A : ty H}
            {Δ ψ : form A}
            (p q : Δ ⊢ ψ)
  : p = q.
Show proof.

Proposition hyperdoctrine_hyp
            {H : preorder_hyperdoctrine}
            {A : ty H}
            (φ : form A)
  : φ ⊢ φ.
Show proof.

Proposition hyperdoctrine_cut
            {H : preorder_hyperdoctrine}
            {A : ty H}
            {Δ ψ χ : form A}
            (p : Δ ⊢ ψ)
            (q : ψ ⊢ χ)
  : Δ ⊢ χ.
Show proof.

Proposition hyperdoctrine_formula_eq
            {H : hyperdoctrine}
            {A : ty H}
            {φ ψ : form A}
            (p : φ ⊢ ψ)
            (q : ψ ⊢ φ)
  : φ = ψ.
Show proof.

Proposition hyperdoctrine_formula_eq_f
            {H : hyperdoctrine}
            {A : ty H}
            {φ ψ : form A}
            (p : φ = ψ)
  : φ ⊢ ψ.
Show proof.

Proposition hyperdoctrine_formula_eq_b
            {H : hyperdoctrine}
            {A : ty H}
            {φ ψ : form A}
            (p : φ = ψ)
  : ψ ⊢ φ.
Show proof.

Definition hyperdoctrine_cleaving
           (H : preorder_hyperdoctrine)
  : cleaving _
  := pr12 (pr222 H).

Definition hyperdoctrine_subst
           {H : preorder_hyperdoctrine}
           {Γ₁ Γ₂ : ty H}
           (φ : form Γ₂)
           (s : tm Γ₁ Γ₂)
  : form Γ₁
  := cleaving_ob (hyperdoctrine_cleaving H) s φ.

Notation "φ [ s ]" := (hyperdoctrine_subst φ s) (at level 10) : hyperdoctrine.

Proposition hyperdoctrine_id_subst
            {H : hyperdoctrine}
            {Γ : ty H}
            (φ : form Γ)
  : φ [ tm_var _ ] = φ.
Show proof.

Proposition hyperdoctrine_comp_subst
            {H : hyperdoctrine}
            {Γ₁ Γ₂ Γ₃ : ty H}
            (s₁ : Γ₁ --> Γ₂)
            (s₂ : Γ₂ --> Γ₃)
            (φ : form Γ₃)
  : φ [ s₂ ] [ s₁ ] = φ [ s₂ [ s₁ ]tm ].
Show proof.

Proposition hyperdoctrine_proof_subst
            {H : preorder_hyperdoctrine}
            {Γ₁ Γ₂ : ty H}
            {Δ φ : form Γ₂}
            (s : tm Γ₁ Γ₂)
            (p : Δ ⊢ φ)
  : Δ [ s ] ⊢ φ [ s ].
Show proof.

Proposition from_disp_mor_hyperdoctrine
            {H : preorder_hyperdoctrine}
            {Γ₁ Γ₂ : ty H}
            {Δ : form Γ₁}
            {φ : form Γ₂}
            (s : tm Γ₁ Γ₂)
            (p : Δ -->[ s ] φ)
  : Δ ⊢ φ [ s ].
Show proof.

Proposition to_disp_mor_hyperdoctrine
            {H : preorder_hyperdoctrine}
            {Γ₁ Γ₂ : ty H}
            {Δ : form Γ₁}
            {φ : form Γ₂}
            (s : tm Γ₁ Γ₂)
            (p : Δ ⊢ φ [ s ])
  : Δ -->[ s ] φ.
Show proof.

Proposition disp_mor_eq_hyperdoctrine
            {H : preorder_hyperdoctrine}
            {Γ₁ Γ₂ : ty H}
            {Δ : form Γ₁}
            {φ : form Γ₂}
            (s : tm Γ₁ Γ₂)
            (p q : Δ -->[ s ] φ)
  : p = q.
Show proof.