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.Hyperdoctrines.Hyperdoctrine.
Require Import UniMath.CategoryTheory.Hyperdoctrines.FirstOrderHyperdoctrine.
Require Import UniMath.CategoryTheory.Hyperdoctrines.Tripos.

Local Open Scope cat.
Local Open Scope hd.

Definition is_generic_predicate
           {H : first_order_hyperdoctrine}
           (Ω : ty H)
           (prf : form Ω)
  : UU
  := ∏ (Γ : ty H)
       (φ : form Γ),
     ∑ (f : tm Γ Ω),
     φ = prf [ f ].

Definition generic_predicate
           (H : first_order_hyperdoctrine)
  : UU
  := ∑ (Ω : ty H)
       (prf : form Ω),
     is_generic_predicate Ω prf.

Definition make_generic_predicate
           {H : first_order_hyperdoctrine}
           (Ω : ty H)
           (prf : form Ω)
           (HΩ : is_generic_predicate Ω prf)
  : generic_predicate H
  := Ω ,, prf ,, HΩ.

Coercion ty_of_generic_predicate
         {H : first_order_hyperdoctrine}
         (Ω : generic_predicate H)
  : ty H.
Proof.
  exact (pr1 Ω).
Defined.

Definition prf_of_generic_predicate
           {H : first_order_hyperdoctrine}
           (Ω : generic_predicate H)
  : form Ω
  := pr12 Ω.

Definition mor_to_generic_predicate
           {H : first_order_hyperdoctrine}
           (Ω : generic_predicate H)
           {Γ : ty H}
           (φ : form Γ)
  : tm Γ Ω
  := pr1 (pr22 Ω Γ φ).

Proposition mor_to_generic_predicate_eq
            {H : first_order_hyperdoctrine}
            (Ω : generic_predicate H)
            {Γ : ty H}
            (φ : form Γ)
  : φ
    =
    (prf_of_generic_predicate Ω) [ mor_to_generic_predicate Ω φ ].
Proof.
  exact (pr2 (pr22 Ω Γ φ)).
Qed.

Definition tripos_generic_predicate
           (H : tripos)
  : generic_predicate H.
Proof.
  use make_generic_predicate.
  - exact (ℙ 𝟙).
  - exact (let P := tm_var (ℙ 𝟙) in
           !! ∈ P).
  - intros Γ A.
    simple refine (_ ,, _).
    + exact {{ A [ π₂ (tm_var _) ] }}.
    + abstract
        (cbn ;
         rewrite tripos_in_subst ;
         simplify ;
         pose (maponpaths
                 (λ φ, φ [ ⟨ !! , tm_var _ ⟩ ])
                 (mor_to_tripos_power_eq 𝟙 Γ (A [ π₂ (tm_var _) ])))
           as p ;
         cbn in p ;
         rewrite !hyperdoctrine_comp_subst in p ;
         rewrite hyperdoctrine_pr2_subst in p ;
         rewrite var_tm_subst in p ;
         rewrite hyperdoctrine_pair_pr2 in p ;
         rewrite hyperdoctrine_id_subst in p ;
         refine (p @ _) ; clear p ;
         use hyperdoctrine_formula_eq ;
         simplify ;
         apply hyperdoctrine_hyp).
Defined.

Notation "'Ω'" := (ty_of_generic_predicate (tripos_generic_predicate _)).
Notation "'Prf'" := (prf_of_generic_predicate (tripos_generic_predicate _)).

Definition tripos_form_to_tm
           {H : tripos}
           {Γ : ty H}
           (φ : form Γ)
  : tm Γ Ω
  := mor_to_generic_predicate _ φ.

Proposition tripos_form_to_tm_Prf
            {H : tripos}
            {Γ : ty H}
            (φ : form Γ)
  : Prf [ tripos_form_to_tm φ ] = φ.
Proof.
  exact (!(mor_to_generic_predicate_eq (tripos_generic_predicate H) φ)).
Qed.

#[global] Opaque ty_of_generic_predicate.
#[global] Opaque prf_of_generic_predicate.
#[global] Opaque mor_to_generic_predicate.