Library UniMath.CategoryTheory.DisplayedCats.Examples.HValuedPredicates

Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.OrderTheory.Lattice.CompleteHeyting.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Categories.HSET.All.
Require Import UniMath.CategoryTheory.Limits.Terminal.
Require Import UniMath.CategoryTheory.Limits.BinProducts.
Require Import UniMath.CategoryTheory.Limits.Pullbacks.
Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.CategoryTheory.DisplayedCats.Isos.
Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.
Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations.
Require Import UniMath.CategoryTheory.DisplayedCats.Fiber.
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.Hyperdoctrines.FirstOrderHyperdoctrine.
Require Import UniMath.CategoryTheory.Hyperdoctrines.Tripos.

Local Open Scope cat.
Local Open Scope heyting.

Section HValuedSets.
  Context (H : complete_heyting_algebra).

1. The displayed category of H-valued predicates

  Definition disp_cat_ob_mor_h_valued_sets
    : disp_cat_ob_mor SET.
  Show proof.
    simple refine (_ ,, _).
    - exact (λ (X : hSet), X → H).
    - exact (λ (X Y : hSet)
               (P : X → H)
               (Q : Y → H)
               (f : X → Y),
             ∏ (x : X), P x ≤ Q(f x)).

  Proposition disp_cat_id_comp_h_valued_sets
    : disp_cat_id_comp SET disp_cat_ob_mor_h_valued_sets.
  Show proof.
    split.
    - intros X P x ; cbn in *.
      apply cha_le_refl.
    - intros X Y Z f g P Q R p q x ; cbn in *.
      refine (cha_le_trans (p x) _).
      apply q.

  Definition disp_cat_data_h_valued_sets
    : disp_cat_data SET.
  Show proof.
    simple refine (_ ,, _).
    - exact disp_cat_ob_mor_h_valued_sets.
    - exact disp_cat_id_comp_h_valued_sets.

  Proposition locally_propositional_h_valued_sets
    : locally_propositional
        disp_cat_data_h_valued_sets.
  Show proof.
    intro ; intros.
    use impred ; intro.
    apply propproperty.

  Proposition disp_cat_axioms_h_valued_sets
    : disp_cat_axioms SET disp_cat_data_h_valued_sets.
  Show proof.
    repeat split ; intros.
    - apply locally_propositional_h_valued_sets.
    - apply locally_propositional_h_valued_sets.
    - apply locally_propositional_h_valued_sets.
    - apply isasetaprop.
      apply locally_propositional_h_valued_sets.

  Definition disp_cat_h_valued_sets
    : disp_cat SET.
  Show proof.
    simple refine (_ ,, _).
    - exact disp_cat_data_h_valued_sets.
    - exact disp_cat_axioms_h_valued_sets.

2. Properties of this displayed category

  Proposition is_univalent_disp_h_valued_sets
    : is_univalent_disp disp_cat_h_valued_sets.
  Show proof.
    use is_univalent_disp_from_fibers.
    intros X P Q.
    use isweqimplimpl.
    - cbn in *.
      intro p.
      use funextsec ; intro x.
      use cha_le_antisymm.
      + exact (pr1 p x).
      + exact (pr12 p x).
    - use funspace_isaset.
      apply setproperty.
    - use isaproptotal2.
      + intro.
        apply isaprop_is_z_iso_disp.
      + intros.
        apply locally_propositional_h_valued_sets.

  Definition cleaving_h_valued_sets
    : cleaving disp_cat_h_valued_sets.
  Show proof.
    intros Y X f Q.
    simple refine ((λ x, Q(f x)) ,, _ ,, _).
    - abstract
        (intro ;
         apply cha_le_refl).
    - intros W g R p.
      use iscontraprop1.
      + abstract
          (use isaproptotal2 ; [ | intros ; apply locally_propositional_h_valued_sets ] ;
           intro ;
           apply disp_cat_h_valued_sets).
      + abstract
          (refine (p ,, _) ;
           apply locally_propositional_h_valued_sets).

3. The hyperdoctrine of H-valued predicates

  Definition h_valued_sets_hyperdoctrine
    : hyperdoctrine.
  Show proof.
    use make_hyperdoctrine.
    - exact SET.
    - exact disp_cat_h_valued_sets.
    - exact TerminalHSET.
    - exact BinProductsHSET.
    - exact cleaving_h_valued_sets.
    - exact locally_propositional_h_valued_sets.
    - exact is_univalent_disp_h_valued_sets.

4. Logic of H-valued predicates

4.1. Fiberwise terminal object

  Definition fiberwise_terminal_h_valued_sets
    : fiberwise_terminal cleaving_h_valued_sets.
  Show proof.
    use make_fiberwise_terminal_locally_propositional.
    - exact locally_propositional_h_valued_sets.
    - exact (λ (X : hSet) (x : X), ⊤).
    - abstract
        (cbn ;
         intros X P x ;
         apply cha_le_top).
    - abstract
        (cbn ;
         intros X Y f x ;
         apply cha_le_refl).

4.2. Fiberwise initial object

  Definition fiberwise_initial_h_valued_sets
    : fiberwise_initial cleaving_h_valued_sets.
  Show proof.
    use make_fiberwise_initial_locally_propositional.
    - exact locally_propositional_h_valued_sets.
    - exact (λ (X : hSet) (x : X), ⊥).
    - abstract
        (cbn ;
         intros X P x ;
         apply cha_bot_le).
    - abstract
        (cbn ;
         intros X Y f x ;
         apply cha_le_refl).

4.3. Fiberwise binary products

  Definition fiberwise_binproducts_h_valued_sets
    : fiberwise_binproducts cleaving_h_valued_sets.
  Show proof.
    use make_fiberwise_binproducts_locally_propositional.
    - exact locally_propositional_h_valued_sets.
    - exact (λ (X : hSet) (P Q : X → H) (x : X), P x ∧ Q x).
    - abstract
        (intros X P Q x ; apply cha_min_le_l).
    - abstract
        (intros X P Q x ; apply cha_min_le_r).
    - abstract
        (intros X P Q R p q x ;
         exact (cha_min_le_case (p x) (q x))).
    - abstract
        (intros X Y f P Q x ;
         apply cha_le_refl).

4.4. Fiberwise binary coproducts

  Definition fiberwise_bincoproducts_h_valued_sets
    : fiberwise_bincoproducts cleaving_h_valued_sets.
  Show proof.
    use make_fiberwise_bincoproducts_locally_propositional.
    - exact locally_propositional_h_valued_sets.
    - exact (λ (X : hSet) (P Q : X → H) (x : X), P x ∨ Q x).
    - abstract
        (intros X P Q x ; apply cha_max_le_l).
    - abstract
        (intros X P Q x ; apply cha_max_le_r).
    - abstract
        (intros X P Q R p q x ;
         exact (cha_max_le_case (p x) (q x))).
    - abstract
        (intros X Y f P Q x ;
         apply cha_le_refl).

4.5. Fiberwise exponentials

  Definition fiberwise_exponentials_h_valued_sets
    : fiberwise_exponentials fiberwise_binproducts_h_valued_sets.
  Show proof.
    use make_fiberwise_exponentials_locally_propositional.
    - exact locally_propositional_h_valued_sets.
    - exact (λ (X : hSet) (P Q : X → H) (x : X), P x ⇒ Q x).
    - abstract
        (intros X P Q x ; cbn ;
         rewrite cha_min_comm ;
         apply cha_exp_eval).
    - abstract
        (intros X P Q R p x ; cbn in * ;
         use cha_to_le_exp ;
         rewrite cha_min_comm ;
         exact (p x)).
    - abstract
        (intros X Y f P Q x ; cbn ;
         apply cha_le_refl).

4.6. Dependent products

  Definition has_dependent_products_h_valued_sets
    : has_dependent_products cleaving_h_valued_sets.
  Show proof.
    use make_has_dependent_products_poset.
    - exact locally_propositional_h_valued_sets.
    - exact (λ (X Y : hSet)
               (f : X → Y)
               (P : X → H)
               (y : Y),
             /\_{ z : ∑ (x : X), f x = y } P (pr1 z)).
    - abstract
        (intros X Y f P x ; cbn in * ;
         use cha_glb_le ; [ exact (x ,, idpath _) | ] ;
         cbn ;
         apply cha_le_refl).
    - abstract
        (intros X Y f P Q p y ; cbn in * ;
         use cha_le_glb ;
         intros z ;
         induction z as [ x q ] ;
         induction q ; cbn ;
         apply p).
    - abstract
        (intros Y₂ Y₁ X₂ X₁ f₁ f₂ g₁ g₂ p Hp P y ; cbn in * ;
         use cha_le_glb ;
         intros z ;
         induction z as [ z zp ] ;
         use cha_glb_le ;
         [ exact (el_pullback_set Hp z y zp ,, el_pullback_set_pr2 Hp z y zp)
         | ] ;
         cbn ;
         rewrite el_pullback_set_pr1 ;
         apply cha_le_refl).

4.7. Dependent sums

  Definition has_dependent_sums_h_valued_sets
    : has_dependent_sums cleaving_h_valued_sets.
  Show proof.
    use make_has_dependent_sums_poset.
    - exact locally_propositional_h_valued_sets.
    - exact (λ (X Y : hSet)
               (f : X → Y)
               (P : X → H)
               (y : Y),
             \/_{ z : ∑ (x : X), f x = y } P (pr1 z)).
    - abstract
        (intros X Y f P x ; cbn in * ;
         use cha_le_lub ; [ exact (x ,, idpath _) | ] ;
         cbn ;
         apply cha_le_refl).
    - abstract
        (intros X Y f P Q p y ; cbn in * ;
         use cha_lub_le ;
         intros z ;
         induction z as [ x q ] ;
         induction q ; cbn ;
         apply p).
    - abstract
        (intros Y₂ Y₁ X₂ X₁ f₁ f₂ g₁ g₂ p Hp P y ; cbn in * ;
         use cha_lub_le ;
         intros z ;
         induction z as [ z zp ] ;
         use cha_le_lub ;
         [ exact (el_pullback_set Hp z y zp ,, el_pullback_set_pr2 Hp z y zp)
         | ] ;
         cbn ;
         rewrite el_pullback_set_pr1 ;
         apply cha_le_refl).

5. The first-order hyperdoctrine of H-valued predicates

  Definition h_valued_sets_first_order_hyperdoctrine
    : first_order_hyperdoctrine.
  Show proof.
    use make_first_order_hyperdoctrine.
    - exact h_valued_sets_hyperdoctrine.
    - exact fiberwise_terminal_h_valued_sets.
    - exact fiberwise_initial_h_valued_sets.
    - exact fiberwise_binproducts_h_valued_sets.
    - exact fiberwise_bincoproducts_h_valued_sets.
    - exact fiberwise_exponentials_h_valued_sets.
    - exact has_dependent_products_h_valued_sets.
    - exact has_dependent_sums_h_valued_sets.

6. The tripos of H-valued predicates

  Local Open Scope hd.

  Section TriposOfHValuedSets.
    Context (X : hSet).

    Definition power_h_valued_set
      : hSet
      := funset X H.

    Definition in_power_h_valued_set
      : X × power_h_valued_set → H
      := λ xf, pr2 xf (pr1 xf).
  End TriposOfHValuedSets.

  Definition is_tripos_h_valued_sets
    : is_tripos h_valued_sets_first_order_hyperdoctrine.
  Show proof.
    intro X ; cbn in * ; unfold prodtofuntoprod ; cbn.
    refine (power_h_valued_set X ,, in_power_h_valued_set X ,, _).
    intros Γ R ; cbn in *.
    simple refine (_ ,, _).
    - exact (λ Γ x, R (x ,, Γ)).
    - abstract
        (apply idpath).

  Definition tripos_h_valued_sets
    : tripos.
  Show proof.
    use make_tripos.
    - exact h_valued_sets_first_order_hyperdoctrine.
    - exact is_tripos_h_valued_sets.
End HValuedSets.