Require Import
  HoTT.Classes.interfaces.abstract_algebra
  HoTT.TruncType.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

(** Demonstrate the [HProp] is a (bounded) lattice w.r.t. the logical
operations. This requires Univalence. *)
Global Instance join_hor : Join HProp := hor.
Definition hand (X Y : HProp) : HProp := Build_HProp (X * Y).
Global Instance meet_hprop : Meet HProp := hand.
Global Instance bottom_hprop : Bottom HProp := False_hp.
Global Instance top_hprop : Top HProp := Unit_hp.

Section contents.
  Context `{Univalence}.

  (* We use this notation because [hor] can accept arguments of type [Type], which leads to minor confusion in the instances below *)
  Notation lor := (hor : HProp -> HProp -> HProp).

  (* This tactic attempts to destruct a truncated sum (disjunction) *)
  Local Ltac hor_intros :=
    let x := fresh in
    intro x; repeat (strip_truncations; destruct x as [x | x]).

  Instance commutative_hor : Commutative lor.
H: Univalence
Commutative
  ((fun P Q : HProp => hor P Q)
   :
   HProp -> HProp -> HProp)
  Proof.
H: Univalence
Commutative
  ((fun P Q : HProp => hor P Q)
   :
   HProp -> HProp -> HProp)
    intros ??.
H: Univalence
x, y: HProp
hor x y = hor y x
    apply path_iff_hprop; hor_intros; apply tr; auto.
  Defined.

  Instance commutative_hand : Commutative hand.
H: Univalence
Commutative hand
  Proof.
H: Univalence
Commutative hand
    intros ??.
H: Univalence
x, y: HProp
hand x y = hand y x
    apply path_hprop.
H: Univalence
x, y: HProp
hand x y <~> hand y x
    apply equiv_prod_symm.
  Defined.

  Instance associative_hor : Associative lor.
H: Univalence
Associative
  ((fun P Q : HProp => hor P Q)
   :
   HProp -> HProp -> HProp)
  Proof.
H: Univalence
Associative
  ((fun P Q : HProp => hor P Q)
   :
   HProp -> HProp -> HProp)
    intros ???.
H: Univalence
x, y, z: HProp
hor x (hor y z) = hor (hor x y) z
    apply path_iff_hprop;
    hor_intros; apply tr;
    ((by auto) || (left; apply tr) || (right; apply tr));
    auto.
  Defined.

  Instance associative_hand : Associative hand.
H: Univalence
Associative hand
  Proof.
H: Univalence
Associative hand
    intros ???.
H: Univalence
x, y, z: HProp
hand x (hand y z) = hand (hand x y) z
    apply path_hprop.
H: Univalence
x, y, z: HProp
hand x (hand y z) <~> hand (hand x y) z
    apply equiv_prod_assoc.
  Defined.

  Instance idempotent_hor : BinaryIdempotent lor.
H: Univalence
BinaryIdempotent
  ((fun P Q : HProp => hor P Q)
   :
   HProp -> HProp -> HProp)
  Proof.
H: Univalence
BinaryIdempotent
  ((fun P Q : HProp => hor P Q)
   :
   HProp -> HProp -> HProp)
    intros ?.
H: Univalence
x: HProp
Idempotent (fun P Q : HProp => hor P Q) x compute.
H: Univalence
x: HProp
Build_HProp (Trunc (-1) (x + x)) = x
    apply path_iff_hprop; hor_intros; auto.
H: Univalence
x: HProp
H0: x
Build_HProp (Trunc (-1) (x + x))
    by apply tr, inl.
  Defined.

  Instance idempotent_hand : BinaryIdempotent hand.
H: Univalence
BinaryIdempotent hand
  Proof.
H: Univalence
BinaryIdempotent hand
    intros ?.
H: Univalence
x: HProp
Idempotent hand x
    apply path_iff_hprop.
H: Univalence
x: HProp
hand x x -> x
H: Univalence
x: HProp
x -> hand x x
    -
H: Univalence
x: HProp
hand x x -> x intros [a _] ; apply a.
    -
H: Univalence
x: HProp
x -> hand x x intros a; apply (pair a a).
  Defined.

  Instance leftidentity_hor : LeftIdentity lor False_hp.
H: Univalence
LeftIdentity
  ((fun P Q : HProp => hor P Q)
   :
   HProp -> HProp -> HProp) False_hp
  Proof.
H: Univalence
LeftIdentity
  ((fun P Q : HProp => hor P Q)
   :
   HProp -> HProp -> HProp) False_hp
    intros ?.
H: Univalence
y: HProp
hor False_hp y = y
    apply path_iff_hprop; hor_intros; try contradiction || assumption.
H: Univalence
y: HProp
H0: y
hor False_hp y
    by apply tr, inr.
  Defined.

  Instance rightidentity_hor : RightIdentity lor False_hp.
H: Univalence
RightIdentity
  ((fun P Q : HProp => hor P Q)
   :
   HProp -> HProp -> HProp) False_hp
  Proof.
H: Univalence
RightIdentity
  ((fun P Q : HProp => hor P Q)
   :
   HProp -> HProp -> HProp) False_hp
    intros ?.
H: Univalence
x: HProp
hor x False_hp = x
    apply path_iff_hprop; hor_intros; try contradiction || assumption.
H: Univalence
x: HProp
H0: x
hor x False_hp
    by apply tr, inl.
  Defined.

  Instance leftidentity_hand : LeftIdentity hand Unit_hp.
H: Univalence
LeftIdentity hand Unit_hp
  Proof.
H: Univalence
LeftIdentity hand Unit_hp
    intros ?.
H: Univalence
y: HProp
hand Unit_hp y = y
    apply path_trunctype, prod_unit_l.
  Defined.

  Instance rightidentity_hand : RightIdentity hand Unit_hp.
H: Univalence
RightIdentity hand Unit_hp
  Proof.
H: Univalence
RightIdentity hand Unit_hp
    intros ?.
H: Univalence
x: HProp
hand x Unit_hp = x
    apply path_trunctype, prod_unit_r.
  Defined.

  Instance absorption_hor_hand : Absorption lor hand.
H: Univalence
Absorption
  ((fun P Q : HProp => hor P Q)
   :
   HProp -> HProp -> HProp) hand
  Proof.
H: Univalence
Absorption
  ((fun P Q : HProp => hor P Q)
   :
   HProp -> HProp -> HProp) hand
    intros ??.
H: Univalence
x, y: HProp
hor x (hand x y) = x
    apply path_iff_hprop.
H: Univalence
x, y: HProp
hor x (hand x y) -> x
H: Univalence
x, y: HProp
x -> hor x (hand x y)
    -
H: Univalence
x, y: HProp
hor x (hand x y) -> x intros X; strip_truncations.
H: Univalence
x, y: HProp
X: (x + hand x y)%type
x
      destruct X as [? | [? _]]; assumption.
    -
H: Univalence
x, y: HProp
x -> hor x (hand x y) intros ?.
H: Univalence
x, y: HProp
X: x
hor x (hand x y) by apply tr, inl.
  Defined.

  Instance absorption_hand_hor : Absorption hand lor.
H: Univalence
Absorption hand
  ((fun P Q : HProp => hor P Q)
   :
   HProp -> HProp -> HProp)
  Proof.
H: Univalence
Absorption hand
  ((fun P Q : HProp => hor P Q)
   :
   HProp -> HProp -> HProp)
    intros ??.
H: Univalence
x, y: HProp
hand x (hor x y) = x
    apply path_iff_hprop.
H: Univalence
x, y: HProp
hand x (hor x y) -> x
H: Univalence
x, y: HProp
x -> hand x (hor x y)
    -
H: Univalence
x, y: HProp
hand x (hor x y) -> x intros [? _]; assumption.
    -
H: Univalence
x, y: HProp
x -> hand x (hor x y) intros ?.
H: Univalence
x, y: HProp
X: x
hand x (hor x y)
      split.
H: Univalence
x, y: HProp
X: x
x
H: Univalence
x, y: HProp
X: x
hor x y
      *
H: Univalence
x, y: HProp
X: x
x assumption.
      *
H: Univalence
x, y: HProp
X: x
hor x y by apply tr, inl.
  Defined.

  Global Instance boundedlattice_hprop : IsBoundedLattice HProp.
H: Univalence
IsBoundedLattice HProp
  Proof.
H: Univalence
IsBoundedLattice HProp repeat split; apply _. Defined.
End contents.