Library HoTT.Classes.implementations.hprop_lattice

Require Import
  HoTT.Classes.interfaces.abstract_algebra
  HoTT.Universes.TruncType.

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.
  Proof.
    intros ??.
    apply path_iff_hprop; hor_intros; apply tr; auto.
  Defined.

  Instance commutative_hand : Commutative hand.
  Proof.
    intros ??.
    apply path_hprop.
    apply equiv_prod_symm.
  Defined.

  Instance associative_hor : Associative lor.
  Proof.
    intros ???.
    apply path_iff_hprop;
    hor_intros; apply tr;
    ((by auto) || (left; apply tr) || (right; apply tr));
    auto.
  Defined.

  Instance associative_hand : Associative hand.
  Proof.
    intros ???.
    apply path_hprop.
    apply equiv_prod_assoc.
  Defined.

  Instance idempotent_hor : BinaryIdempotent lor.
  Proof.
    intros ?. compute.
    apply path_iff_hprop; hor_intros; auto.
    by apply tr, inl.
  Defined.

  Instance idempotent_hand : BinaryIdempotent hand.
  Proof.
    intros ?.
    apply path_iff_hprop.
    - intros [a _] ; apply a.
    - intros a; apply (pair a a).
  Defined.

  Instance leftidentity_hor : LeftIdentity lor False_hp.
  Proof.
    intros ?.
    apply path_iff_hprop; hor_intros; try contradiction || assumption.
    by apply tr, inr.
  Defined.

  Instance rightidentity_hor : RightIdentity lor False_hp.
  Proof.
    intros ?.
    apply path_iff_hprop; hor_intros; try contradiction || assumption.
    by apply tr, inl.
  Defined.

  Instance leftidentity_hand : LeftIdentity hand Unit_hp.
  Proof.
    intros ?.
    apply path_trunctype, prod_unit_l.
  Defined.

  Instance rightidentity_hand : RightIdentity hand Unit_hp.
  Proof.
    intros ?.
    apply path_trunctype, prod_unit_r.
  Defined.

  Instance absorption_hor_hand : Absorption lor hand.
  Proof.
    intros ??.
    apply path_iff_hprop.
    - intros X; strip_truncations.
      destruct X as [? | [? _]]; assumption.
    - intros ?. by apply tr, inl.
  Defined.

  Instance absorption_hand_hor : Absorption hand lor.
  Proof.
    intros ??.
    apply path_iff_hprop.
    - intros [? _]; assumption.
    - intros ?.
      split.
      × assumption.
      × by apply tr, inl.
  Defined.

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