Library UniMath.OrderTheory.Lattice.CompleteHeyting

Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.

Require Import UniMath.OrderTheory.Lattice.Lattice.
Require Import UniMath.OrderTheory.Lattice.Bounded.
Require Import UniMath.OrderTheory.Lattice.Heyting.

Declare Scope heyting.
Delimit Scope heyting with heyting.
Local Open Scope heyting.

1. Complete Heyting algebra

Definition is_upperbound_lattice
           {X : hSet}
           (L : lattice X)
           {I : UU}
           (f : I → X)
           (x : X)
  : UU
  := ∏ (i : I), Lle L (f i) x.

Definition is_least_upperbound_lattice
           {X : hSet}
           (L : lattice X)
           {I : UU}
           (f : I → X)
           (x : X)
  : UU
  := is_upperbound_lattice L f x
     ×
     ∏ (y : X), is_upperbound_lattice L f y → Lle L x y.

Definition is_complete_lattice
           {X : hSet}
           (L : lattice X)
  : UU
  := ∏ (I : UU)
       (f : I → X),
     ∑ (x : X),
     is_least_upperbound_lattice L f x.

Definition complete_heyting_algebra
  : UU
  := ∑ (X : hSet)
       (L : bounded_lattice X),
     is_complete_lattice L
     ×
     exponential L.

Definition make_complete_heyting_algebra
           (X : hSet)
           (L : bounded_lattice X)
           (CL : is_complete_lattice L)
           (EL : exponential L)
  : complete_heyting_algebra
  := X ,, L ,, CL ,, EL.

Coercion complete_heyting_algebra_to_carrier
         (H : complete_heyting_algebra)
  : hSet.
Show proof.
  exact (pr1 H).

Coercion lattice_of_complete_heyting_algebra
         (H : complete_heyting_algebra)
  : bounded_lattice H.
Show proof.
  exact (pr12 H).

2. Operations of complete Heyting algebras

Definition complete_heyting_algebra_top
           (H : complete_heyting_algebra)
  : H
  := Ltop H.

Notation "⊤" := (complete_heyting_algebra_top _) : heyting.

Definition complete_heyting_algebra_bot
           (H : complete_heyting_algebra)
  : H
  := Lbot H.

Notation "⊥" := (complete_heyting_algebra_bot _) : heyting.

Definition complete_heyting_algebra_le
           {H : complete_heyting_algebra}
           (x y : H)
  : hProp
  := Lle H x y.

Notation "x ≤ y" := (complete_heyting_algebra_le x y) : heyting.

Definition complete_heyting_algebra_min
           {H : complete_heyting_algebra}
           (x y : H)
  : H
  := Lmin H x y.

Notation "x ∧ y" := (complete_heyting_algebra_min x y) : heyting.

Definition complete_heyting_algebra_max
           {H : complete_heyting_algebra}
           (x y : H)
  : H
  := Lmax H x y.

Notation "x ∨ y" := (complete_heyting_algebra_max x y) : heyting.

Definition complete_heyting_algebra_lub
           {H : complete_heyting_algebra}
           {I : UU}
           (f : I → H)
  : H
  := pr1 (pr122 H I f).

Notation "\/_{ i } f" := (complete_heyting_algebra_lub (λ i, f)) (at level 20, i binder)
    : heyting.

Note that one can also write `\/_{ i : I } f`

Definition complete_heyting_algebra_exp
           {H : complete_heyting_algebra}
           (x y : H)
  : H
  := pr222 H x y.

Notation "x ⇒ y" := (complete_heyting_algebra_exp x y) : heyting.

Definition complete_heyting_algebra_neg
           {H : complete_heyting_algebra}
           (x : H)
  : H
  := x ⇒ ⊥.

Notation "¬ x" := (complete_heyting_algebra_neg x) : heyting.

Definition h_valued_pred_comp
           {H : complete_heyting_algebra}
           {X : hSet}
           (p : X → H)
  : hSet.
Show proof.
  use make_hSet.
  - exact (∑ (x : X), ⊤%heyting ≤ p x).
  - abstract
      (use isaset_total2 ; [ apply setproperty | ] ;
       intro x ;
       apply isasetaprop ;
       apply propproperty).

Notation "{{ p }}" := (h_valued_pred_comp p) : heyting.

3. Laws for complete Heyting algebras

For the laws, we use `cha` as an abbreviation for 'complete Heyting algebra'. We did not do so for the operations, because there one can use the notation.
Proposition cha_min_assoc
            {H : complete_heyting_algebra}
            (x y z : H)
  : ((x ∧ y) ∧ z) = (x ∧ (y ∧ z)).
Show proof.
  exact (isassoc_Lmin H x y z).

Proposition cha_min_comm
            {H : complete_heyting_algebra}
            (x y : H)
  : (x ∧ y) = (y ∧ x).
Show proof.
  exact (iscomm_Lmin H x y).

Proposition cha_max_assoc
            {H : complete_heyting_algebra}
            (x y z : H)
  : ((x ∨ y) ∨ z) = (x ∨ (y ∨ z)).
Show proof.
  exact (isassoc_Lmax H x y z).

Proposition cha_max_comm
            {H : complete_heyting_algebra}
            (x y : H)
  : (x ∨ y) = (y ∨ x).
Show proof.
  exact (iscomm_Lmax H x y).

Proposition cha_min_absorb
            {H : complete_heyting_algebra}
            (x y : H)
  : (x ∧ (x ∨ y)) = x.
Show proof.
  exact (Lmin_absorb H x y).

Proposition cha_max_absorb
            {H : complete_heyting_algebra}
            (x y : H)
  : (x ∨ (x ∧ y)) = x.
Show proof.
  exact (Lmax_absorb H x y).

Proposition cha_min_id
            {H : complete_heyting_algebra}
            (x : H)
  : (x ∧ x) = x.
Show proof.
  exact (Lmin_id H x).

Proposition cha_max_id
            {H : complete_heyting_algebra}
            (x : H)
  : (x ∨ x) = x.
Show proof.
  exact (Lmax_id H x).

Proposition cha_le_refl
            {H : complete_heyting_algebra}
            (x : H)
  : x ≤ x.
Show proof.
  exact (isrefl_Lle H x).

Proposition cha_le_antisymm
            {H : complete_heyting_algebra}
            {x y : H}
            (p : x ≤ y)
            (q : y ≤ x)
  : x = y.
Show proof.
  exact (isantisymm_Lle H x y p q).

Proposition cha_le_trans
            {H : complete_heyting_algebra}
            {x y z : H}
            (p : x ≤ y)
            (q : y ≤ z)
  : x ≤ z.
Show proof.
  exact (istrans_Lle H x y z p q).

Proposition cha_min_le_l
            {H : complete_heyting_algebra}
            (x y : H)
  : (x ∧ y) ≤ x.
Show proof.
  exact (Lmin_le_l H x y).

Proposition cha_min_le_r
            {H : complete_heyting_algebra}
            (x y : H)
  : (x ∧ y) ≤ y.
Show proof.
  exact (Lmin_le_r H x y).

Proposition cha_min_le_case
            {H : complete_heyting_algebra}
            {x y z : H}
            (p : z ≤ x)
            (q : z ≤ y)
  : z ≤ (x ∧ y).
Show proof.
  exact (Lmin_le_case H x y z p q).

Proposition cha_max_le_l
            {H : complete_heyting_algebra}
            (x y : H)
  : x ≤ (x ∨ y).
Show proof.
  exact (Lmax_le_l H x y).

Proposition cha_max_le_r
            {H : complete_heyting_algebra}
            (x y : H)
  : y ≤ (x ∨ y).
Show proof.
  exact (Lmax_le_r H x y).

Proposition cha_max_le_case
            {H : complete_heyting_algebra}
            {x y z : H}
            (p : x ≤ z)
            (q : y ≤ z)
  : (x ∨ y) ≤ z.
Show proof.
  exact (Lmax_le_case H x y z p q).

Proposition cha_min_le_eq_l
            {H : complete_heyting_algebra}
            {x y : H}
            (p : x ≤ y)
  : (x ∧ y) = x.
Show proof.
  exact (Lmin_le_eq_l H x y p).

Proposition cha_min_le_eq_r
            {H : complete_heyting_algebra}
            {x y : H}
            (p : y ≤ x)
  : (x ∧ y) = y.
Show proof.
  exact (Lmin_le_eq_r H x y p).

Proposition cha_max_le_eq_l
            {H : complete_heyting_algebra}
            {x y : H}
            (p : y ≤ x)
  : (x ∨ y) = x.
Show proof.
  exact (Lmax_le_eq_l H x y p).

Proposition cha_max_le_eq_r
            {H : complete_heyting_algebra}
            {x y : H}
            (p : x ≤ y)
  : (x ∨ y) = y.
Show proof.
  exact (Lmax_le_eq_r H x y p).

Proposition cha_lunit_max_bot
            {H : complete_heyting_algebra}
            (x : H)
  : (⊥ ∨ x) = x.
Show proof.
  exact (islunit_Lmax_Lbot H x).

Proposition cha_runit_max_bot
            {H : complete_heyting_algebra}
            (x : H)
  : (x ∨ ⊥) = x.
Show proof.
  rewrite cha_max_comm.
  apply cha_lunit_max_bot.

Proposition cha_lunit_min_top
            {H : complete_heyting_algebra}
            (x : H)
  : (⊤ ∧ x) = x.
Show proof.
  exact (islunit_Lmin_Ltop H x).

Proposition cha_runit_min_bot
            {H : complete_heyting_algebra}
            (x : H)
  : (x ∧ ⊤) = x.
Show proof.
  rewrite cha_min_comm.
  apply cha_lunit_min_top.

Proposition cha_min_bot_l
            {H : complete_heyting_algebra}
            (x : H)
  : (⊥ ∧ x) = ⊥.
Show proof.
  exact (Lmin_Lbot H x).

Proposition cha_min_bot_r
            {H : complete_heyting_algebra}
            (x : H)
  : (x ∧ ⊥) = ⊥.
Show proof.
  rewrite cha_min_comm.
  apply cha_min_bot_l.

Proposition cha_max_top_l
            {H : complete_heyting_algebra}
            (x : H)
  : (⊤ ∨ x) = ⊤.
Show proof.
  exact (Lmax_Ltop H x).

Proposition cha_max_top_r
            {H : complete_heyting_algebra}
            (x : H)
  : (x ∨ ⊤) = ⊤.
Show proof.
  rewrite cha_max_comm.
  apply cha_max_top_l.

Proposition cha_to_le
            {H : complete_heyting_algebra}
            {x y : H}
            (p : (x ∧ y) = x)
  : x ≤ y.
Show proof.
  exact p.

Proposition cha_from_le
            {H : complete_heyting_algebra}
            {x y : H}
            (p : x ≤ y)
  : (x ∧ y) = x.
Show proof.
  exact p.

Proposition cha_bot_le
            {H : complete_heyting_algebra}
            (x : H)
  : ⊥ ≤ x.
Show proof.
  use cha_to_le.
  apply cha_min_bot_l.

Proposition cha_le_top
            {H : complete_heyting_algebra}
            (x : H)
  : x ≤ ⊤.
Show proof.
  use cha_to_le.
  apply cha_runit_min_bot.

Proposition cha_from_le_exp
            {H : complete_heyting_algebra}
            {x y z : H}
            (p : z ≤ (x ⇒ y))
  : (z ∧ x) ≤ y.
Show proof.
  exact (pr1 (pr2 (pr222 H) x y z) p).

Proposition cha_to_le_exp
            {H : complete_heyting_algebra}
            {x y z : H}
            (p : (z ∧ x) ≤ y)
  : z ≤ (x ⇒ y).
Show proof.
  exact (pr2 (pr2 (pr222 H) x y z) p).

Proposition cha_exp_eval
            {H : complete_heyting_algebra}
            (x y : H)
  : ((x ⇒ y) ∧ x) ≤ y.
Show proof.
  use cha_from_le_exp.
  apply cha_le_refl.

Proposition cha_le_lub_pt
            {H : complete_heyting_algebra}
            {I : UU}
            (f : I → H)
            (i : I)
  : f i ≤ \/_{ j } f j.
Show proof.
  exact (pr12 (pr122 H I f) i).

Proposition cha_le_lub
            {H : complete_heyting_algebra}
            {I : UU}
            (f : I → H)
            {x : H}
            {i : I}
            (p : x ≤ f i)
  : x ≤ \/_{ j } f j.
Show proof.
  refine (cha_le_trans p _).
  apply cha_le_lub_pt.

Proposition cha_lub_le
            {H : complete_heyting_algebra}
            {I : UU}
            {f : I → H}
            {x : H}
            (p : ∏ (i : I), f i ≤ x)
  : \/_{ j } f j ≤ x.
Show proof.
  exact (pr22 (pr122 H I f) x p).

The following commands prevent that the operations are unfolded by `cbn` or `simpl. Without them, the operations for complete Heyting algebras would be unfolded to the level of lattices, and then it would be more complicated to use the accessors/notation in this file.
#[global] Opaque complete_heyting_algebra_top.
#[global] Opaque complete_heyting_algebra_bot.
#[global] Opaque complete_heyting_algebra_le.
#[global] Opaque complete_heyting_algebra_min.
#[global] Opaque complete_heyting_algebra_max.
#[global] Opaque complete_heyting_algebra_lub.
#[global] Opaque complete_heyting_algebra_exp.

4. Greatest lower bounds for complete Heyting algebras

Definition complete_heyting_algebra_glb
           {H : complete_heyting_algebra}
           {I : UU}
           (f : I → H)
  : H
  := \/_{ i : ∑ (x : H), ∏ (i : I), x ≤ f i } pr1 i.

Notation "/\_{ i } f" := (complete_heyting_algebra_glb (λ i, f)) (at level 20, i binder)
    : heyting.

Proposition cha_glb_le_pt
            {H : complete_heyting_algebra}
            {I : UU}
            (f : I → H)
            (i : I)
  : /\_{ j } f j ≤ f i.
Show proof.
  use cha_lub_le.
  intros x ; cbn.
  exact (pr2 x i).

Proposition cha_glb_le
            {H : complete_heyting_algebra}
            {I : UU}
            (f : I → H)
            {x : H}
            {i : I}
            (p : f i ≤ x)
  : /\_{ j } f j ≤ x.
Show proof.
  refine (cha_le_trans _ p).
  apply cha_glb_le_pt.

Proposition cha_le_glb
            {H : complete_heyting_algebra}
            {I : UU}
            {f : I → H}
            {x : H}
            (p : ∏ (i : I), x ≤ f i)
  : x ≤ /\_{ j } f j.
Show proof.
  unfold complete_heyting_algebra_glb.
  use cha_le_lub.
  - exact (x ,, p).
  - apply cha_le_refl.

#[global] Opaque complete_heyting_algebra_glb.

5. Complete Heyting algebras from greatest upper bounds

Definition is_lowerbound_lattice
           {X : hSet}
           (L : lattice X)
           {I : UU}
           (f : I → X)
           (x : X)
  : UU
  := ∏ (i : I), Lle L x (f i).

Definition is_greatest_lowerbound_lattice
           {X : hSet}
           (L : lattice X)
           {I : UU}
           (f : I → X)
           (x : X)
  : UU
  := is_lowerbound_lattice L f x
     ×
     ∏ (y : X), is_lowerbound_lattice L f y → Lle L y x.

Definition complete_lattice_from_glb
           {X : hSet}
           (L : lattice X)
           (H : ∏ (I : UU)
                  (f : I → X),
                ∑ (x : X),
                is_greatest_lowerbound_lattice L f x)
  : is_complete_lattice L.
Show proof.
  intros I f.
  pose (lub := H (∑ (x : X), ∏ (i : I), Lle L (f i) x) pr1).
  refine (pr1 lub ,, _).
  split.
  - abstract
      (intros i ;
       use (pr22 lub) ;
       intros p ;
       exact (pr2 p i)).
  - abstract
      (intros x Hx ;
       exact (pr12 lub (x ,, Hx))).

6. Bases for complete Heyting algebras

Definition cha_basis_data
           (H : complete_heyting_algebra)
  : UU
  := ∑ (B : UU),
     (B → H)
     ×
     (B → B → hProp).

Definition make_cha_basis_data
           {H : complete_heyting_algebra}
           (B : UU)
           (f : B → H)
           (R : B → B → hProp)
  : cha_basis_data H
  := B ,, f ,, R.

Coercion cha_basis_type
         {H : complete_heyting_algebra}
         (B : cha_basis_data H)
  : UU
  := pr1 B.

Definition cha_basis_incl
           {H : complete_heyting_algebra}
           {B : cha_basis_data H}
           (b : B)
  : H
  := pr12 B b.

Definition cha_basis_rel
           {H : complete_heyting_algebra}
           {B : cha_basis_data H}
           (b₁ b₂ : B)
  : hProp
  := pr22 B b₁ b₂.

Definition cha_basis_laws
           {H : complete_heyting_algebra}
           (B : cha_basis_data H)
  : UU
  := (∏ (b₁ b₂ b₃ : B),
      cha_basis_rel b₁ b₂ → cha_basis_rel b₂ b₃ → cha_basis_rel b₁ b₃)
     ×
     (∏ (x : H),
      x = \/_{ i : ∑ (b : B), cha_basis_incl b ≤ x } cha_basis_incl (pr1 i))
     ×
     (∏ (b₁ b₂ : B),
      cha_basis_rel b₁ b₂ → cha_basis_incl b₂ ≤ cha_basis_incl b₁).

Definition cha_basis
           (H : complete_heyting_algebra)
  : UU
  := ∑ (B : cha_basis_data H), cha_basis_laws B.

Definition make_cha_basis
           {H : complete_heyting_algebra}
           (B : cha_basis_data H)
           (HB : cha_basis_laws B)
  : cha_basis H
  := B ,, HB.

Coercion cha_basis_to_data
         {H : complete_heyting_algebra}
         (B : cha_basis H)
  : cha_basis_data H
  := pr1 B.

Proposition cha_basis_trans
            {H : complete_heyting_algebra}
            (B : cha_basis H)
            {b₁ b₂ b₃ : B}
            (p : cha_basis_rel b₁ b₂)
            (q : cha_basis_rel b₂ b₃)
  : cha_basis_rel b₁ b₃.
Show proof.
  exact (pr12 B b₁ b₂ b₃ p q).

Proposition cha_basis_eq
            {H : complete_heyting_algebra}
            (B : cha_basis H)
            (x : H)
  : x
    =
    \/_{ i : ∑ (b : B), cha_basis_incl b ≤ x } cha_basis_incl (pr1 i).
Show proof.
  exact (pr122 B x).

Proposition cha_basis_antimonotone
            {H : complete_heyting_algebra}
            (B : cha_basis H)
            {b₁ b₂ : B}
            (p : cha_basis_rel b₁ b₂)
  : cha_basis_incl b₂ ≤ cha_basis_incl b₁.
Show proof.
  exact (pr222 B b₁ b₂ p).

7. Complete Boolean algebras

Definition is_boolean_algebra
           (H : complete_heyting_algebra)
  : hProp
  := (∀ (x : H), ((x ∨ ¬ x) = ⊤)%heyting)%logic.