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.DisplayedCats.Fiberwise.FiberwiseTerminal.
Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseInitial.
Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseProducts.
Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseCoproducts.
Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseCartesianClosed.
Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.DependentProducts.
Require Import UniMath.CategoryTheory.DisplayedCats.Fiberwise.DependentSums.
Require Import UniMath.CategoryTheory.Hyperdoctrines.Hyperdoctrine.
Require Import UniMath.CategoryTheory.Limits.Initial.
Require Import UniMath.CategoryTheory.Limits.Terminal.
Require Import UniMath.CategoryTheory.Limits.BinProducts.
Require Import UniMath.CategoryTheory.Limits.BinCoproducts.
Require Import UniMath.CategoryTheory.Limits.Pullbacks.
Require Import UniMath.CategoryTheory.Limits.Preservation.

Require Import UniMath.Tactics.Simplify.
Require Import UniMath.Tactics.Utilities.
Require Import Ltac2.Ltac2.
Require Import Ltac2.Notations.

Local Open Scope cat.
Local Open Scope hd.

Set Default Show proof.

Definition first_order_hyperdoctrine
  : UU
  := ∑ (H : hyperdoctrine),
     fiberwise_terminal (hyperdoctrine_cleaving H)
     ×
     fiberwise_initial (hyperdoctrine_cleaving H)
     ×
     ∑ (P : fiberwise_binproducts (hyperdoctrine_cleaving H)),
     fiberwise_bincoproducts (hyperdoctrine_cleaving H)
     ×
     fiberwise_exponentials P
     ×
     has_dependent_products (hyperdoctrine_cleaving H)
     ×
     has_dependent_sums (hyperdoctrine_cleaving H).

Coercion first_order_hyperdoctrine_to_hyperdoctrine
         (H : first_order_hyperdoctrine)
  : hyperdoctrine.
Show proof.

Coercion first_order_hyperdoctrine_to_preorder_hyperdoctrine
         (H : first_order_hyperdoctrine)
  : first_order_preorder_hyperdoctrine.
Show proof.

Definition univalent_first_order_hyperdoctrine
  : UU
  := ∑ (H : univalent_hyperdoctrine),
     fiberwise_terminal (hyperdoctrine_cleaving H)
     ×
     fiberwise_initial (hyperdoctrine_cleaving H)
     ×
     ∑ (P : fiberwise_binproducts (hyperdoctrine_cleaving H)),
     fiberwise_bincoproducts (hyperdoctrine_cleaving H)
     ×
     fiberwise_exponentials P
     ×
     has_dependent_products (hyperdoctrine_cleaving H)
     ×
     has_dependent_sums (hyperdoctrine_cleaving H).

Coercion univalent_first_order_hyperdoctrine_to_hyperdoctrine
         (H : univalent_first_order_hyperdoctrine)
  : univalent_hyperdoctrine.
Show proof.

Coercion univalent_first_order_hyperdoctrine_to_first_order
         (H : univalent_first_order_hyperdoctrine)
  : first_order_hyperdoctrine.
Show proof.

Definition make_first_order_preorder_hyperdoctrine
           (H : preorder_hyperdoctrine)
           (TH : fiberwise_terminal (hyperdoctrine_cleaving H))
           (IH : fiberwise_initial (hyperdoctrine_cleaving H))
           (PH : fiberwise_binproducts (hyperdoctrine_cleaving H))
           (CH : fiberwise_bincoproducts (hyperdoctrine_cleaving H))
           (IMPH : fiberwise_exponentials PH)
           (DPH : has_dependent_products (hyperdoctrine_cleaving H))
           (DSH : has_dependent_sums (hyperdoctrine_cleaving H))
  : first_order_preorder_hyperdoctrine
  := H
     ,,
     TH
     ,,
     IH
     ,,
     PH
     ,,
     CH
     ,,
     IMPH
     ,,
     DPH
     ,,
     DSH.

Definition make_first_order_hyperdoctrine
           (H : hyperdoctrine)
           (TH : fiberwise_terminal (hyperdoctrine_cleaving H))
           (IH : fiberwise_initial (hyperdoctrine_cleaving H))
           (PH : fiberwise_binproducts (hyperdoctrine_cleaving H))
           (CH : fiberwise_bincoproducts (hyperdoctrine_cleaving H))
           (IMPH : fiberwise_exponentials PH)
           (DPH : has_dependent_products (hyperdoctrine_cleaving H))
           (DSH : has_dependent_sums (hyperdoctrine_cleaving H))
  : first_order_hyperdoctrine
  := H
     ,,
     TH
     ,,
     IH
     ,,
     PH
     ,,
     CH
     ,,
     IMPH
     ,,
     DPH
     ,,
     DSH.

Definition make_univalent_first_order_hyperdoctrine
           (H : univalent_hyperdoctrine)
           (TH : fiberwise_terminal (hyperdoctrine_cleaving H))
           (IH : fiberwise_initial (hyperdoctrine_cleaving H))
           (PH : fiberwise_binproducts (hyperdoctrine_cleaving H))
           (CH : fiberwise_bincoproducts (hyperdoctrine_cleaving H))
           (IMPH : fiberwise_exponentials PH)
           (DPH : has_dependent_products (hyperdoctrine_cleaving H))
           (DSH : has_dependent_sums (hyperdoctrine_cleaving H))
  : univalent_first_order_hyperdoctrine
  := H
     ,,
     TH
     ,,
     IH
     ,,
     PH
     ,,
     CH
     ,,
     IMPH
     ,,
     DPH
     ,,
     DSH.

Definition first_order_hyperdoctrine_truth
           {H : first_order_hyperdoctrine}
           {Γ : ty H}
  : form Γ
  := terminal_obj_in_fib (pr12 H) Γ.

Notation "'⊤'" := first_order_hyperdoctrine_truth : hyperdoctrine.

Proposition truth_intro
            {H : first_order_hyperdoctrine}
            {Γ : ty H}
            (Δ : form Γ)
  : Δ ⊢ ⊤.
Show proof.

Proposition truth_subst
            {H : first_order_hyperdoctrine}
            {Γ₁ Γ₂ : ty H}
            (s : tm Γ₁ Γ₂)
  : ⊤ [ s ] = ⊤.
Show proof.

Definition first_order_hyperdoctrine_false
           {H : first_order_hyperdoctrine}
           {Γ : ty H}
  : form Γ
  := initial_obj_in_fib (pr122 H) Γ.

Notation "'⊥'" := first_order_hyperdoctrine_false : hyperdoctrine.

Proposition false_elim
            {H : first_order_hyperdoctrine}
            {Γ : ty H}
            (Δ φ : form Γ)
            (p : Δ ⊢ ⊥)
  : Δ ⊢ φ.
Show proof.

Proposition false_subst
            {H : first_order_hyperdoctrine}
            {Γ₁ Γ₂ : ty H}
            (s : Γ₁ --> Γ₂)
  : ⊥ [ s ] = ⊥.
Show proof.

Definition first_order_hyperdoctrine_conj
           {H : first_order_hyperdoctrine}
           {Γ : ty H}
           (φ ψ : form Γ)
  : form Γ
  := BinProductObject _ (binprod_in_fib (pr1 (pr222 H)) φ ψ).

Notation "φ ∧ ψ" := (first_order_hyperdoctrine_conj φ ψ) : hyperdoctrine.

Proposition conj_intro
            {H : first_order_hyperdoctrine}
            {Γ : ty H}
            {Δ φ ψ : form Γ}
            (p : Δ ⊢ φ)
            (q : Δ ⊢ ψ)
  : Δ ⊢ φ ∧ ψ.
Show proof.

Proposition conj_elim_left
            {H : first_order_hyperdoctrine}
            {Γ : ty H}
            {Δ φ ψ : form Γ}
            (p : Δ ⊢ φ ∧ ψ)
  : Δ ⊢ φ.
Show proof.

Proposition conj_elim_right
            {H : first_order_hyperdoctrine}
            {Γ : ty H}
            {Δ φ ψ : form Γ}
            (p : Δ ⊢ φ ∧ ψ)
  : Δ ⊢ ψ.
Show proof.

Proposition conj_subst
            {H : first_order_hyperdoctrine}
            {Γ₁ Γ₂ : ty H}
            (s : Γ₁ --> Γ₂)
            (φ ψ : form Γ₂)
  : (φ ∧ ψ) [ s ] = (φ [ s ] ∧ ψ [ s ]).
Show proof.

Proposition weaken_left
            {H : first_order_hyperdoctrine}
            {Γ : ty H}
            {Δ₁ φ : form Γ}
            (p : Δ₁ ⊢ φ)
            (Δ₂ : form Γ)
  : Δ₁ ∧ Δ₂ ⊢ φ.
Show proof.

Proposition weaken_right
            {H : first_order_hyperdoctrine}
            {Γ : ty H}
            {Δ₂ φ : form Γ}
            (p : Δ₂ ⊢ φ)
            (Δ₁ : form Γ)
  : Δ₁ ∧ Δ₂ ⊢ φ.
Show proof.

Proposition weaken_cut
            {H : first_order_hyperdoctrine}
            {Γ : ty H}
            {Δ φ ψ : form Γ}
            (p : Δ ⊢ φ)
            (q : Δ ∧ φ ⊢ ψ)
  : Δ ⊢ ψ.
Show proof.

Proposition weaken_to_empty
            {H : first_order_hyperdoctrine}
            {Γ : ty H}
            {Δ φ : form Γ}
            (p : ⊤ ⊢ φ)
  : Δ ⊢ φ.
Show proof.

Proposition hyp_sym
            {H : first_order_hyperdoctrine}
            {Γ : ty H}
            {Δ Δ' φ : form Γ}
            (p : Δ ∧ Δ' ⊢ φ)
  : Δ' ∧ Δ ⊢ φ.
Show proof.

Proposition hyp_ltrans
            {H : first_order_hyperdoctrine}
            {Γ : ty H}
            {Δ Δ' Δ'' φ : form Γ}
            (p : Δ ∧ (Δ' ∧ Δ'') ⊢ φ)
  : (Δ ∧ Δ') ∧ Δ'' ⊢ φ.
Show proof.

Proposition hyp_rtrans
            {H : first_order_hyperdoctrine}
            {Γ : ty H}
            {Δ Δ' Δ'' φ : form Γ}
            (p : (Δ ∧ Δ') ∧ Δ'' ⊢ φ)
  : Δ ∧ (Δ' ∧ Δ'') ⊢ φ.
Show proof.

Proposition conj_assoc
            {H : first_order_hyperdoctrine}
            {Γ : ty H}
            (φ₁ φ₂ φ₃ : form Γ)
  : ((φ₁ ∧ φ₂) ∧ φ₃) = (φ₁ ∧ (φ₂ ∧ φ₃)).
Show proof.

Definition first_order_hyperdoctrine_disj
           {H : first_order_hyperdoctrine}
           {Γ : ty H}
           (φ ψ : form Γ)
  : form Γ
  := BinCoproductObject (bincoprod_in_fib (pr12 (pr222 H)) φ ψ).

Notation "φ ∨ ψ" := (first_order_hyperdoctrine_disj φ ψ) : hyperdoctrine.

Proposition disj_intro_left
            {H : first_order_hyperdoctrine}
            {Γ : ty H}
            {Δ φ ψ : form Γ}
            (p : Δ ⊢ φ)
  : Δ ⊢ φ ∨ ψ.
Show proof.

Proposition disj_intro_right
            {H : first_order_hyperdoctrine}
            {Γ : ty H}
            {Δ φ ψ : form Γ}
            (p : Δ ⊢ ψ)
  : Δ ⊢ φ ∨ ψ.
Show proof.

Proposition distributivity
            {H : first_order_hyperdoctrine}
            {Γ : ty H}
            (φ ψ χ : form Γ)
  : φ ∧ (ψ ∨ χ) ⊢ (φ ∧ ψ) ∨ (φ ∧ χ).
Show proof.

Proposition disj_elim
            {H : first_order_hyperdoctrine}
            {Γ : ty H}
            {Δ φ ψ χ : form Γ}
            (p : Δ ⊢ φ ∨ ψ)
            (q : Δ ∧ φ ⊢ χ)
            (r : Δ ∧ ψ ⊢ χ)
  : Δ ⊢ χ.
Show proof.

Proposition disj_subst
            {H : first_order_hyperdoctrine}
            {Γ₁ Γ₂ : ty H}
            (s : Γ₁ --> Γ₂)
            (φ ψ : form Γ₂)
  : (φ ∨ ψ) [ s ] = (φ [ s ] ∨ ψ [ s ]).
Show proof.

Definition first_order_hyperdoctrine_impl
           {H : first_order_hyperdoctrine}
           {Γ : ty H}
           (φ ψ : form Γ)
  : form Γ
  := exp_in_fib (pr122 (pr222 H)) φ ψ.

Notation "φ ⇒ ψ" := (first_order_hyperdoctrine_impl φ ψ) : hyperdoctrine.

Proposition impl_intro
            {H : first_order_hyperdoctrine}
            {Γ : ty H}
            {Δ φ ψ : form Γ}
            (p : Δ ∧ φ ⊢ ψ)
  : Δ ⊢ φ ⇒ ψ.
Show proof.

Proposition impl_elim
            {H : first_order_hyperdoctrine}
            {Γ : ty H}
            {Δ φ ψ : form Γ}
            (p : Δ ⊢ φ)
            (q : Δ ⊢ φ ⇒ ψ)
  : Δ ⊢ ψ.
Show proof.

Proposition impl_subst
            {H : first_order_hyperdoctrine}
            {Γ₁ Γ₂ : ty H}
            (s : Γ₁ --> Γ₂)
            (φ ψ : form Γ₂)
  : (φ ⇒ ψ) [ s ] = (φ [ s ] ⇒ ψ [ s ]).
Show proof.

Proposition impl_id
            {H : first_order_hyperdoctrine}
            {Γ : ty H}
            (φ : form Γ)
  : ⊤ ⊢ φ ⇒ φ.
Show proof.

Definition first_order_hyperdoctrine_forall
           {H : first_order_hyperdoctrine}
           {Γ A : ty H}
           (φ : form (Γ ×h A))
  : form Γ
  := dep_prod (pr1 (pr222 (pr222 H))) (π₁ (identity (Γ ×h A))) φ.

Notation "'∀h' φ" := (first_order_hyperdoctrine_forall φ) (at level 10)
    : hyperdoctrine.

Proposition forall_intro
            {H : first_order_hyperdoctrine}
            {Γ A : ty H}
            {Δ : form Γ}
            {φ : form (Γ ×h A)}
            (p : Δ [ π₁ (tm_var _) ] ⊢ φ)
  : Δ ⊢ ∀h φ.
Show proof.

Proposition forall_elim
            {H : first_order_hyperdoctrine}
            {Γ A : ty H}
            {Δ : form Γ}
            {φ : form (Γ ×h A)}
            (p : Δ ⊢ ∀h φ)
            (t : tm Γ A)
  : Δ ⊢ φ [ ⟨ tm_var _ , t ⟩ ].
Show proof.

Proposition quantifier_subst_pb_eq
            {H : first_order_hyperdoctrine}
            {Γ₁ Γ₂ : ty H}
            (A : ty H)
            (s : tm Γ₁ Γ₂)
  : s [ π₁ (tm_var (Γ₁ ×h A)) ]tm
    =
    (π₁ (tm_var _)) [ ⟨ s [ π₁ (tm_var _) ]tm , π₂ (tm_var _) ⟩ ]tm.
Show proof.

Definition quantifier_subst_pb
           {H : first_order_hyperdoctrine}
           {Γ₁ Γ₂ : ty H}
           (A : ty H)
           (s : tm Γ₁ Γ₂)
  : isPullback (!(quantifier_subst_pb_eq A s)).
Show proof.

Proposition forall_subst
            {H : first_order_hyperdoctrine}
            {Γ₁ Γ₂ A : ty H}
            (s : tm Γ₁ Γ₂)
            (φ : form (Γ₂ ×h A))
  : (∀h φ) [ s ]
    =
    (∀h (φ [ ⟨ s [ π₁ (tm_var _) ]tm , π₂ (tm_var _) ⟩ ])).
Show proof.

Definition first_order_hyperdoctrine_exists
           {H : first_order_hyperdoctrine}
           {Γ A : ty H}
           (φ : form (Γ ×h A))
  : form Γ
  := dep_sum (pr2 (pr222 (pr222 H))) (π₁ (identity (Γ ×h A))) φ.

Notation "'∃h' φ" := (first_order_hyperdoctrine_exists φ) (at level 10)
    : hyperdoctrine.

Proposition exists_subst
            {H : first_order_hyperdoctrine}
            {Γ₁ Γ₂ A : ty H}
            (s : tm Γ₁ Γ₂)
            (φ : form (Γ₂ ×h A))
  : (∃h φ) [ s ]
    =
    ∃h (φ [ ⟨ s [ π₁ (tm_var _) ]tm , π₂ (tm_var _) ⟩ ]).
Show proof.

Proposition exists_intro
            {H : first_order_hyperdoctrine}
            {Γ A : ty H}
            {Δ : form Γ}
            {φ : form (Γ ×h A)}
            {t : tm Γ A}
            (p : Δ ⊢ φ [ ⟨ tm_var _ , t ⟩ ])
  : Δ ⊢ ∃h φ.
Show proof.

Proposition exists_elim_empty
            {H : first_order_hyperdoctrine}
            {Γ A : ty H}
            {Δ ψ : form Γ}
            {φ : form (Γ ×h A)}
            (p : Δ ⊢ ∃h φ)
            (q : φ ⊢ ψ [ π₁ (tm_var (Γ ×h A)) ])
  : Δ ⊢ ψ.
Show proof.

Proposition frobenius_reciprocity
            {H : first_order_hyperdoctrine}
            {Γ A : ty H}
            (φ : form (Γ ×h A))
            (Δ : form Γ)
  : Δ ∧ (∃h φ) ⊢ (∃h (Δ [ π₁ (tm_var (Γ ×h A)) ] ∧ φ)).
Show proof.

Proposition exists_elim
            {H : first_order_hyperdoctrine}
            {Γ A : ty H}
            {Δ ψ : form Γ}
            {φ : form (Γ ×h A)}
            (p : Δ ⊢ ∃h φ)
            (q : Δ [ π₁ (tm_var (Γ ×h A)) ] ∧ φ ⊢ ψ [ π₁ (tm_var (Γ ×h A)) ])
  : Δ ⊢ ψ.
Show proof.

Definition first_order_hyperdoctrine_equal
           {H : first_order_hyperdoctrine}
           {Γ A : ty H}
           (t₁ t₂ : tm Γ A)
  : form Γ
  := (dep_sum (pr2 (pr222 (pr222 H))) (Δ_{A}) ⊤) [ ⟨ t₁ , t₂ ⟩ ].

Notation "t₁ ≡ t₂" := (first_order_hyperdoctrine_equal t₁ t₂)
    : hyperdoctrine.

Proposition equal_subst
            {H : first_order_hyperdoctrine}
            {Γ₁ Γ₂ A : ty H}
            (s : Γ₁ --> Γ₂)
            (t₁ t₂ : tm Γ₂ A)
  : (t₁ ≡ t₂) [ s ] = (t₁ [ s ]tm ≡ t₂ [ s ]tm).
Show proof.

Proposition hyperdoctrine_refl'
            {H : first_order_hyperdoctrine}
            {Γ A : ty H}
            (t : tm Γ A)
  : ⊤ ⊢ t ≡ t.
Show proof.

Proposition hyperdoctrine_refl
            {H : first_order_hyperdoctrine}
            {Γ A : ty H}
            (Δ : form Γ)
            (t : tm Γ A)
  : Δ ⊢ t ≡ t.
Show proof.

Proposition hyperdoctrine_refl_eq
            {H : first_order_hyperdoctrine}
            {Γ A : ty H}
            (Δ : form Γ)
            {t₁ t₂ : tm Γ A}
            (p : t₁ = t₂)
  : Δ ⊢ t₁ ≡ t₂.
Show proof.

Proposition hyperdoctrine_eq_elim_help
            {H : first_order_hyperdoctrine}
            {Γ A : ty H}
            (φ : form (A ×h A))
            (p : ⊤ ⊢ φ [ Δ_{A} ])
            (t₁ t₂ : tm Γ A)
  : t₁ ≡ t₂ ⊢ φ [ ⟨ t₁ , t₂ ⟩ ].
Show proof.

Proposition hyperdoctrine_eq_elim_help_con'
            {H : first_order_hyperdoctrine}
            {Γ A : ty H}
            (φ : form ((A ×h A) ×h Γ))
            (p : ⊤ ⊢ φ [ ⟨ Δ_{A} [ π₁ (tm_var _) ]tm , π₂ (tm_var _) ⟩ ])
            (t₁ t₂ : tm Γ A)
  : t₁ ≡ t₂ ⊢ φ [ ⟨ ⟨ t₁ , t₂ ⟩ , tm_var _ ⟩ ].
Show proof.

Definition hyperdoctrine_eq_elim_help_con_sub
           {H : first_order_hyperdoctrine}
           (Γ A : ty H)
  : tm ((A ×h A) ×h Γ) (Γ ×h (A ×h A)).
Show proof.

Proposition hyperdoctrine_eq_elim_help_con
            {H : first_order_hyperdoctrine}
            {Γ A : ty H}
            (φ : form (Γ ×h (A ×h A)))
            (p : ⊤ ⊢ φ [ ⟨ π₁ (tm_var _) , Δ_{A} [ π₂ (tm_var _) ]tm ⟩ ])
            (t₁ t₂ : tm Γ A)
  : t₁ ≡ t₂ ⊢ φ [ ⟨ tm_var _ , ⟨ t₁ , t₂ ⟩ ⟩ ].
Show proof.

Proposition hyperdoctrine_eq_elim
            {H : first_order_hyperdoctrine}
            {Γ A : ty H}
            {Δ : form Γ}
            (φ : form (Γ ×h A))
            {t₁ t₂ : tm Γ A}
            (p : Δ ⊢ t₁ ≡ t₂)
            (q : Δ ⊢ φ [ ⟨ tm_var _ , t₁ ⟩ ])
  : Δ ⊢ φ [ ⟨ tm_var _ , t₂ ⟩ ].
Show proof.

Proposition hyperdoctrine_eq_sym
            {H : first_order_hyperdoctrine}
            {Γ A : ty H}
            {Δ : form Γ}
            {t₁ t₂ : tm Γ A}
            (p : Δ ⊢ t₁ ≡ t₂)
  : Δ ⊢ t₂ ≡ t₁.
Show proof.

Proposition hyperdoctrine_eq_trans
            {H : first_order_hyperdoctrine}
            {Γ A : ty H}
            {Δ : form Γ}
            {t₁ t₂ t₃ : tm Γ A}
            (p : Δ ⊢ t₁ ≡ t₂)
            (p' : Δ ⊢ t₂ ≡ t₃)
  : Δ ⊢ t₁ ≡ t₃.
Show proof.

Proposition hyperdoctrine_eq_transportf
            {H : first_order_hyperdoctrine}
            {Γ A : ty H}
            {Δ : form Γ}
            {t₁ t₂ : tm Γ A}
            (φ : form A)
            (p : Δ ⊢ t₁ ≡ t₂)
            (q : Δ ⊢ φ [ t₁ ])
  : Δ ⊢ φ [ t₂ ].
Show proof.

Proposition hyperdoctrine_eq_transportb
            {H : first_order_hyperdoctrine}
            {Γ A : ty H}
            {Δ : form Γ}
            {t₁ t₂ : tm Γ A}
            (φ : form A)
            (p : Δ ⊢ t₁ ≡ t₂)
            (q : Δ ⊢ φ [ t₂ ])
  : Δ ⊢ φ [ t₁ ].
Show proof.

Proposition hyperdoctrine_unit_eq_prf
            {H : first_order_hyperdoctrine}
            {Γ : ty H}
            (t : tm Γ 𝟙)
            (Δ : form Γ)
  : Δ ⊢ t ≡ !!.
Show proof.

Proposition hyperdoctrine_unit_tm_eq
            {H : first_order_hyperdoctrine}
            {Γ : ty H}
            (t t' : tm Γ 𝟙)
            (Δ : form Γ)
  : Δ ⊢ t ≡ t'.
Show proof.

Proposition hyperdoctrine_eq_pr1
            {H : first_order_hyperdoctrine}
            {Γ A B : ty H}
            {Δ : form Γ}
            {t t' : tm Γ (A ×h B)}
            (p : Δ ⊢ t ≡ t')
  : Δ ⊢ π₁ t ≡ π₁ t'.
Show proof.

Proposition hyperdoctrine_eq_pr2
            {H : first_order_hyperdoctrine}
            {Γ A B : ty H}
            {Δ : form Γ}
            {t t' : tm Γ (A ×h B)}
            (p : Δ ⊢ t ≡ t')
  : Δ ⊢ π₂ t ≡ π₂ t'.
Show proof.

Proposition hyperdoctrine_eq_pair_left
            {H : first_order_hyperdoctrine}
            {Γ A B : ty H}
            {Δ : form Γ}
            {s₁ s₂ : tm Γ A}
            (p : Δ ⊢ s₁ ≡ s₂)
            (t : tm Γ B)
  : Δ ⊢ ⟨ s₁ , t ⟩ ≡ ⟨ s₂ , t ⟩.
Show proof.

Proposition hyperdoctrine_eq_pair_right
            {H : first_order_hyperdoctrine}
            {Γ A B : ty H}
            {Δ : form Γ}
            (s : tm Γ A)
            {t₁ t₂ : tm Γ B}
            (p : Δ ⊢ t₁ ≡ t₂)
  : Δ ⊢ ⟨ s , t₁ ⟩ ≡ ⟨ s , t₂ ⟩.
Show proof.

Proposition hyperdoctrine_eq_pair_eq
            {H : first_order_hyperdoctrine}
            {Γ A B : ty H}
            {Δ : form Γ}
            {s₁ s₂ : tm Γ A}
            (p : Δ ⊢ s₁ ≡ s₂)
            {t₁ t₂ : tm Γ B}
            (q : Δ ⊢ t₁ ≡ t₂)
  : Δ ⊢ ⟨ s₁ , t₁ ⟩ ≡ ⟨ s₂ , t₂ ⟩.
Show proof.

Proposition hyperdoctrine_eq_prod_eq
            {H : first_order_hyperdoctrine}
            {Γ A B : ty H}
            {Δ : form Γ}
            {t₁ t₂ : tm Γ (A ×h B)}
            (p : Δ ⊢ π₁ t₁ ≡ π₁ t₂)
            (q : Δ ⊢ π₂ t₁ ≡ π₂ t₂)
  : Δ ⊢ t₁ ≡ t₂.
Show proof.

Proposition hyperdoctrine_subst_eq
            {H : first_order_hyperdoctrine}
            {Γ Γ' B : ty H}
            {Δ : form _}
            {s₁ s₂ : tm Γ Γ'}
            (p : Δ ⊢ s₁ ≡ s₂)
            (t : tm Γ' B)
  : Δ ⊢ t [ s₁ ]tm ≡ t [ s₂ ]tm.
Show proof.