Library UniMath.CategoryTheory.Hyperdoctrines.Tripos

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.

Local Open Scope cat.
Local Open Scope hd.

1. Tripos

Definition is_power_object_tripos
           {H : first_order_preorder_hyperdoctrine}
           (X : ty H)
           (PX : ty H)
           (inX : form (X ×h PX))
  : UU
  := ∏ (Γ : ty H)
       (R : form (X ×h Γ)),
     ∑ (f : tm Γ PX),
     R
     =
     inX [ ⟨ π₁ (tm_var _) , f [ π₂ (tm_var _) ]tm ⟩ ].

Definition is_preorder_tripos
           (H : first_order_preorder_hyperdoctrine)
  : UU
  := ∏ (X : ty H),
     ∑ (PX : ty H)
       (inX : form (X ×h PX)),
     is_power_object_tripos X PX inX.

Definition preorder_tripos
  : UU
  := ∑ (H : first_order_preorder_hyperdoctrine), is_preorder_tripos H.

Coercion preorder_tripos_to_first_order_hyperdoctrine
         (H : preorder_tripos)
  : first_order_preorder_hyperdoctrine.
Show proof.
  exact (pr1 H).

Definition is_tripos
           (H : first_order_hyperdoctrine)
           (H' := first_order_hyperdoctrine_to_preorder_hyperdoctrine H)
  : UU
  := ∏ (X : ty H'),
     ∑ (PX : ty H')
       (inX : form (X ×h PX)),
     is_power_object_tripos X PX inX.

Definition tripos
  : UU
  := ∑ (H : first_order_hyperdoctrine), is_tripos H.

Coercion tripos_to_first_order_hyperdoctrine
         (H : tripos)
  : first_order_hyperdoctrine.
Show proof.
  exact (pr1 H).

Definition tripos_power
           {H : tripos}
           (X : ty H)
  : ty H
  := pr1 (pr2 H X).

Notation "'ℙ'" := tripos_power.
Definition tripos_in
           {H : tripos}
           (X : ty H)
  : form (X ×h ℙ X)
  := pr12 (pr2 H X).

Notation "x ∈ P" := ((tripos_in _) [ ⟨ x , P ⟩ ]).

Proposition tripos_in_subst
            {H : tripos}
            {Γ₁ Γ₂ X : ty H}
            (x : tm Γ₂ X)
            (P : tm Γ₂ (ℙ X))
            (s : tm Γ₁ Γ₂)
  : (x ∈ P) [ s ]
    =
    ((x [ s ]tm) ∈ (P [ s ]tm)).
Show proof.
  unfold tripos_in.
  hypersimplify.
  apply idpath.

Definition tripos_compr
           {H : tripos}
           {X : ty H}
           {Γ : ty H}
           (R : form (X ×h Γ))
  : tm Γ (ℙ X)
  := pr1 (pr22 (pr2 H X) Γ R).

Notation "{{ R }}" := (tripos_compr R).

Proposition mor_to_tripos_power_eq
            {H : tripos}
            (X : ty H)
            (Γ : ty H)
            (R : form (X ×h Γ))
            (x := π₁ (tm_var (X ×h Γ)))
            (γ := π₂ (tm_var (X ×h Γ)))
  : R = (x ∈ ({{ R }} [ γ ]tm)).
Show proof.
  exact (pr2 (pr22 (pr2 H X) Γ R)).

Proposition mor_to_tripos_power_f
            {H : tripos}
            (X : ty H)
            (Γ : ty H)
            (R : form (X ×h Γ))
            (Δ : form (X ×h Γ))
            (x := π₁ (tm_var (X ×h Γ)))
            (γ := π₂ (tm_var (X ×h Γ)))
            (p : Δ ⊢ R)
  : Δ ⊢ x ∈ ({{ R }} [ γ ]tm).
Show proof.
  refine (hyperdoctrine_cut p _).
  exact (hyperdoctrine_formula_eq_f (mor_to_tripos_power_eq X Γ R)).

Proposition mor_to_tripos_power_b
            {H : tripos}
            (X : ty H)
            (Γ : ty H)
            (R : form (X ×h Γ))
            (Δ : form (X ×h Γ))
            (x := π₁ (tm_var (X ×h Γ)))
            (γ := π₂ (tm_var (X ×h Γ)))
            (p : Δ ⊢ x ∈ {{ R }} [ γ ]tm)
  : Δ ⊢ R.
Show proof.
  refine (hyperdoctrine_cut p _).
  exact (hyperdoctrine_formula_eq_b (mor_to_tripos_power_eq X Γ R)).

Definition make_tripos
           (H : first_order_hyperdoctrine)
           (HH : is_tripos H)
  : tripos
  := H ,, HH.

2. Some substitutions necessary to define weak triposes

Definition hyperdoctrine_sub_pr_1_of_4
           {H : first_order_hyperdoctrine}
           {A B C D : ty H}
  : tm (((A ×h B) ×h C) ×h D) A
  := π₁ (π₁ (π₁ (tm_var _))).

Definition hyperdoctrine_sub_pr_2_of_4
           {H : first_order_hyperdoctrine}
           {A B C D : ty H}
  : tm (((A ×h B) ×h C) ×h D) B
  := π₂ (π₁ (π₁ (tm_var _))).

Definition hyperdoctrine_sub_pr_3_of_4
           {H : first_order_hyperdoctrine}
           {A B C D : ty H}
  : tm (((A ×h B) ×h C) ×h D) C
  := π₂ (π₁ (tm_var _)).

Definition hyperdoctrine_sub_pr_4_of_4
           {H : first_order_hyperdoctrine}
           {A B C D : ty H}
  : tm (((A ×h B) ×h C) ×h D) D
  := π₂ (tm_var _).

Definition hyperdoctrine_sub_pr_4_3
           {H : first_order_hyperdoctrine}
           {A B C D : ty H}
  : tm (((A ×h B) ×h C) ×h D) (D ×h C)
  := ⟨ hyperdoctrine_sub_pr_4_of_4 , hyperdoctrine_sub_pr_3_of_4 ⟩.

Definition hyperdoctrine_sub_pr_4_2
           {H : first_order_hyperdoctrine}
           {A B C D : ty H}
  : tm (((A ×h B) ×h C) ×h D) (D ×h B)
  := ⟨ hyperdoctrine_sub_pr_4_of_4 , hyperdoctrine_sub_pr_2_of_4 ⟩.

Arguments hyperdoctrine_sub_pr_1_of_4 {_ _ _ _ _} /.
Arguments hyperdoctrine_sub_pr_2_of_4 {_ _ _ _ _} /.
Arguments hyperdoctrine_sub_pr_3_of_4 {_ _ _ _ _} /.
Arguments hyperdoctrine_sub_pr_4_of_4 {_ _ _ _ _} /.
Arguments hyperdoctrine_sub_pr_4_3 {_ _ _ _ _} /.
Arguments hyperdoctrine_sub_pr_4_2 {_ _ _ _ _} /.

3. The definition of weak triposes

Definition is_weak_tripos_law
           {H : first_order_hyperdoctrine}
           {X : ty H}
           {PX : ty H}
           (inX : form (X ×h PX))
  : UU
  := ∏ (Γ : ty H)
       (R : form (X ×h Γ)),
     let s₁ := (hyperdoctrine_sub_pr_4_3 : tm (((𝟙 ×h Γ) ×h PX) ×h X) _) in
     let s₂ := (hyperdoctrine_sub_pr_4_2 : tm (((𝟙 ×h Γ) ×h PX) ×h X) _) in
     ⊤ ⊢ (∀h ∃h ∀h (inX [ s₁ ] ⇔ R [ s₂ ])).

Definition is_weak_tripos
           (H : first_order_hyperdoctrine)
  : UU
  := ∏ (X : ty H),
     ∑ (PX : ty H)
       (inX : form (X ×h PX)),
     is_weak_tripos_law inX.

Definition weak_tripos
  : UU
  := ∑ (H : first_order_hyperdoctrine), is_weak_tripos H.

Coercion weak_tripos_to_first_order_hyperdoctrine
         (H : weak_tripos)
  : first_order_hyperdoctrine.
Show proof.
  exact (pr1 H).

Definition make_weak_tripos
           (H : first_order_hyperdoctrine)
           (HH : is_weak_tripos H)
  : weak_tripos
  := H ,, HH.

4. Every tripos is a weak tripos

Proposition tripos_to_weak_tripos_law
            {H : tripos}
            (X : ty H)
  : is_weak_tripos_law (tripos_in X).
Show proof.
  intros Γ R.
  use forall_intro.
  use exists_intro.
  - exact ({{ R }} [ π₂ (tm_var _) ]tm).
  - cbn ; hypersimplify.
    use forall_intro.
    pose (x := π₂ (tm_var ((𝟙 ×h Γ) ×h X))).
    pose (γ := π₂ (π₁ (tm_var ((𝟙 ×h Γ) ×h X)))).
    fold x γ.
    use iff_intro.
    + use weaken_right.
      refine (hyperdoctrine_cut
                _
                (hyperdoctrine_proof_subst
                   ⟨ x , γ ⟩
                   (mor_to_tripos_power_b X Γ R _ (hyperdoctrine_hyp _)))).
      rewrite tripos_in_subst.
      hypersimplify.
      apply hyperdoctrine_hyp.
    + use weaken_right.
      refine (hyperdoctrine_cut
                (hyperdoctrine_proof_subst
                   ⟨ x , γ ⟩
                   (mor_to_tripos_power_f X Γ R _ (hyperdoctrine_hyp _)))
                _).
      rewrite tripos_in_subst.
      hypersimplify.
      apply hyperdoctrine_hyp.

Definition tripos_to_weak_tripos
           (H : tripos)
  : is_weak_tripos H.
Show proof.
  intros X.
  simple refine (_ ,, _ ,, _).
  - exact (ℙ X).
  - exact (tripos_in X).
  - exact (tripos_to_weak_tripos_law X).