Library UniMath.OrderTheory.Prebilattice.Prebilattice
Pre-bilattice Georgios V. Pitsiladis, Aug. 2024 -
Pre-bilattices are structures
comprising two lattice structures over the same set.
Usually, the first lattice is called the 'truth' lattice
(hence tlattice below) with operators 'meet' and 'join',
while the second lattice is called the 'knowledge' lattce
(hence klattice below) with operators 'conensus' and 'gulliblity'.
Require Import UniMath.Algebra.BinaryOperations.
Require Import UniMath.OrderTheory.Lattice.Lattice.
Require Import UniMath.OrderTheory.Lattice.Bounded.
Section Def .
Definition prebilattice (X : hSet) := lattice X × lattice X .
Definition prebilattice_carrier {X : hSet} (b : prebilattice X) := X.
Coercion prebilattice_carrier : prebilattice >-> hSet.
Definition make_prebilattice {X : hSet} (tLattice kLattice: lattice X) : prebilattice X := tLattice,, kLattice.
Definition tlattice {X : hSet} (b : prebilattice X) : lattice X := pr1 b .
Definition klattice {X : hSet} (b : prebilattice X) : lattice X := pr2 b .
Definition dual_prebilattice {X : hSet} (b : prebilattice X) := make_prebilattice (klattice b) (tlattice b) .
Definition t_opp_prebilattice {X : hSet} (b : prebilattice X) := make_prebilattice (dual_lattice (tlattice b)) (klattice b) .
Definition k_opp_prebilattice {X : hSet} (b : prebilattice X) := dual_prebilattice (t_opp_prebilattice (dual_prebilattice b)).
Definition opp_prebilattice {X : hSet} (b : prebilattice X) := make_prebilattice (dual_lattice (tlattice b)) (dual_lattice (klattice b)) .
Definition meet {X : hSet} (b : prebilattice X) : binop X := Lmin (tlattice b) .
Definition join {X: hSet} (b : prebilattice X) : binop X := Lmax (tlattice b) .
Definition consensus {X : hSet} (b : prebilattice X) : binop X := Lmin (klattice b) .
Definition gullibility {X : hSet} (b : prebilattice X) : binop X := Lmax (klattice b) .
Lemma isaset_prebilattice (X : hSet) : isaset (prebilattice X) .
Show proof.
Definition prebilattice_transportf {X1 X2 : hSet} (b1 : prebilattice X1) (b2 : prebilattice X2) (p : X1 = X2)
(m : meet (transportf prebilattice p b1) ~ meet b2)
(j : join (transportf prebilattice p b1) ~ join b2)
(c : consensus (transportf prebilattice p b1) ~ consensus b2)
(g : gullibility (transportf prebilattice p b1) ~ gullibility b2)
: transportf prebilattice p b1 = b2.
Show proof.
Definition prebilattice_eq {X : hSet} (b1 : prebilattice X) (b2 : prebilattice X) (m : meet b1 ~ meet b2) (j : join b1 ~ join b2) (c : consensus b1 ~ consensus b2) (g : gullibility b1 ~ gullibility b2): b1 = b2.
Show proof.
End Def.
Section Properties.
Lemma isassoc_consensus {X : hSet} (b : prebilattice X) : isassoc (consensus b).
Show proof.
Lemma isassoc_join {X : hSet} (b : prebilattice X) : isassoc (join b) .
Show proof.
Lemma isassoc_meet {X : hSet} (b : prebilattice X) : isassoc (meet b) .
Show proof.
Lemma iscomm_consensus {X : hSet} (b : prebilattice X) : iscomm (consensus b) .
Show proof.
Lemma iscomm_gullibility {X : hSet} (b : prebilattice X) : iscomm (gullibility b) .
Show proof.
Lemma iscomm_meet {X : hSet} (b : prebilattice X) : iscomm (meet b) .
Show proof.
Lemma iscomm_join {X : hSet} (b : prebilattice X) : iscomm (join b) .
Show proof.
Lemma join_id {X : hSet} (b : prebilattice X) (x : X) : join b x x = x .
Show proof.
Lemma meet_id {X : hSet} (b : prebilattice X) (x : X) : meet b x x = x .
Show proof.
Lemma consensus_gullibility_absorb {X : hSet} (b : prebilattice X) (x y : X) : consensus b x (gullibility b x y) = x .
Show proof.
Lemma gullibility_consensus_absorb {X : hSet} (b : prebilattice X) (x y : X) : gullibility b x (consensus b x y) = x .
Show proof.
Lemma meet_join_absorb {X : hSet} (b : prebilattice X) (x y : X) : meet b x (join b x y) = x .
Show proof.
Lemma join_meet_absorb {X : hSet} (b : prebilattice X) (x y : X) : join b x (meet b x y) = x .
Show proof.
Definition tle {X : hSet} (b : prebilattice X) : hrel X := Lle (tlattice b).
Definition kle {X : hSet} (b : prebilattice X) : hrel X := Lle (klattice b).
Definition tge {X : hSet} (b : prebilattice X) : hrel X := Lge (tlattice b).
Definition kge {X : hSet} (b : prebilattice X) : hrel X := Lge (klattice b).
Lemma istrans_tle {X : hSet} (b : prebilattice X) : istrans (tle b) .
Show proof.
Lemma istrans_kle {X : hSet} (b : prebilattice X) : istrans (kle b) .
Show proof.
End Properties .
Section Bounded .
Definition bounded_prebilattice (X : hSet) :=
bounded_lattice X × bounded_lattice X.
Definition make_bounded_prebilattice {X : hSet} (tLattice kLattice : bounded_lattice X) : bounded_prebilattice X := tLattice,, kLattice.
Definition bounded_prebilattice_to_prebilattice X (b : bounded_prebilattice X) : prebilattice X := make_prebilattice (pr1 b) (pr2 b) .
Coercion bounded_prebilattice_to_prebilattice : bounded_prebilattice >-> prebilattice.
Definition fls {X : hSet} (b : bounded_prebilattice X) : X := Lbot (pr1 b).
Definition tru {X : hSet} (b : bounded_prebilattice X) : X := Ltop (pr1 b).
Definition bot {X: hSet} (b : bounded_prebilattice X) : X := Lbot (pr2 b) .
Definition top {X: hSet} (b : bounded_prebilattice X) : X := Ltop (pr2 b) .
End Bounded .
Require Import UniMath.OrderTheory.Lattice.Lattice.
Require Import UniMath.OrderTheory.Lattice.Bounded.
Section Def .
Definition prebilattice (X : hSet) := lattice X × lattice X .
Definition prebilattice_carrier {X : hSet} (b : prebilattice X) := X.
Coercion prebilattice_carrier : prebilattice >-> hSet.
Definition make_prebilattice {X : hSet} (tLattice kLattice: lattice X) : prebilattice X := tLattice,, kLattice.
Definition tlattice {X : hSet} (b : prebilattice X) : lattice X := pr1 b .
Definition klattice {X : hSet} (b : prebilattice X) : lattice X := pr2 b .
Definition dual_prebilattice {X : hSet} (b : prebilattice X) := make_prebilattice (klattice b) (tlattice b) .
Definition t_opp_prebilattice {X : hSet} (b : prebilattice X) := make_prebilattice (dual_lattice (tlattice b)) (klattice b) .
Definition k_opp_prebilattice {X : hSet} (b : prebilattice X) := dual_prebilattice (t_opp_prebilattice (dual_prebilattice b)).
Definition opp_prebilattice {X : hSet} (b : prebilattice X) := make_prebilattice (dual_lattice (tlattice b)) (dual_lattice (klattice b)) .
Definition meet {X : hSet} (b : prebilattice X) : binop X := Lmin (tlattice b) .
Definition join {X: hSet} (b : prebilattice X) : binop X := Lmax (tlattice b) .
Definition consensus {X : hSet} (b : prebilattice X) : binop X := Lmin (klattice b) .
Definition gullibility {X : hSet} (b : prebilattice X) : binop X := Lmax (klattice b) .
Lemma isaset_prebilattice (X : hSet) : isaset (prebilattice X) .
Show proof.
Definition prebilattice_transportf {X1 X2 : hSet} (b1 : prebilattice X1) (b2 : prebilattice X2) (p : X1 = X2)
(m : meet (transportf prebilattice p b1) ~ meet b2)
(j : join (transportf prebilattice p b1) ~ join b2)
(c : consensus (transportf prebilattice p b1) ~ consensus b2)
(g : gullibility (transportf prebilattice p b1) ~ gullibility b2)
: transportf prebilattice p b1 = b2.
Show proof.
use dirprodeq.
- use total2_paths_f.
-- use weqfunextsec. use m.
-- use total2_paths_f.
--- use weqfunextsec.
rewrite transportf_total2_const.
use j.
--- apply isaprop_islatticeop.
- use total2_paths_f.
-- use weqfunextsec. use c.
-- use total2_paths_f.
--- use weqfunextsec.
rewrite transportf_total2_const.
use g.
--- apply isaprop_islatticeop.
- use total2_paths_f.
-- use weqfunextsec. use m.
-- use total2_paths_f.
--- use weqfunextsec.
rewrite transportf_total2_const.
use j.
--- apply isaprop_islatticeop.
- use total2_paths_f.
-- use weqfunextsec. use c.
-- use total2_paths_f.
--- use weqfunextsec.
rewrite transportf_total2_const.
use g.
--- apply isaprop_islatticeop.
Definition prebilattice_eq {X : hSet} (b1 : prebilattice X) (b2 : prebilattice X) (m : meet b1 ~ meet b2) (j : join b1 ~ join b2) (c : consensus b1 ~ consensus b2) (g : gullibility b1 ~ gullibility b2): b1 = b2.
Show proof.
End Def.
Section Properties.
Lemma isassoc_consensus {X : hSet} (b : prebilattice X) : isassoc (consensus b).
Show proof.
Lemma isassoc_join {X : hSet} (b : prebilattice X) : isassoc (join b) .
Show proof.
Lemma isassoc_meet {X : hSet} (b : prebilattice X) : isassoc (meet b) .
Show proof.
Lemma iscomm_consensus {X : hSet} (b : prebilattice X) : iscomm (consensus b) .
Show proof.
Lemma iscomm_gullibility {X : hSet} (b : prebilattice X) : iscomm (gullibility b) .
Show proof.
Lemma iscomm_meet {X : hSet} (b : prebilattice X) : iscomm (meet b) .
Show proof.
Lemma iscomm_join {X : hSet} (b : prebilattice X) : iscomm (join b) .
Show proof.
Lemma join_id {X : hSet} (b : prebilattice X) (x : X) : join b x x = x .
Show proof.
Lemma meet_id {X : hSet} (b : prebilattice X) (x : X) : meet b x x = x .
Show proof.
Lemma consensus_gullibility_absorb {X : hSet} (b : prebilattice X) (x y : X) : consensus b x (gullibility b x y) = x .
Show proof.
Lemma gullibility_consensus_absorb {X : hSet} (b : prebilattice X) (x y : X) : gullibility b x (consensus b x y) = x .
Show proof.
Lemma meet_join_absorb {X : hSet} (b : prebilattice X) (x y : X) : meet b x (join b x y) = x .
Show proof.
Lemma join_meet_absorb {X : hSet} (b : prebilattice X) (x y : X) : join b x (meet b x y) = x .
Show proof.
Definition tle {X : hSet} (b : prebilattice X) : hrel X := Lle (tlattice b).
Definition kle {X : hSet} (b : prebilattice X) : hrel X := Lle (klattice b).
Definition tge {X : hSet} (b : prebilattice X) : hrel X := Lge (tlattice b).
Definition kge {X : hSet} (b : prebilattice X) : hrel X := Lge (klattice b).
Lemma istrans_tle {X : hSet} (b : prebilattice X) : istrans (tle b) .
Show proof.
Lemma istrans_kle {X : hSet} (b : prebilattice X) : istrans (kle b) .
Show proof.
End Properties .
Section Bounded .
Definition bounded_prebilattice (X : hSet) :=
bounded_lattice X × bounded_lattice X.
Definition make_bounded_prebilattice {X : hSet} (tLattice kLattice : bounded_lattice X) : bounded_prebilattice X := tLattice,, kLattice.
Definition bounded_prebilattice_to_prebilattice X (b : bounded_prebilattice X) : prebilattice X := make_prebilattice (pr1 b) (pr2 b) .
Coercion bounded_prebilattice_to_prebilattice : bounded_prebilattice >-> prebilattice.
Definition fls {X : hSet} (b : bounded_prebilattice X) : X := Lbot (pr1 b).
Definition tru {X : hSet} (b : bounded_prebilattice X) : X := Ltop (pr1 b).
Definition bot {X: hSet} (b : bounded_prebilattice X) : X := Lbot (pr2 b) .
Definition top {X: hSet} (b : bounded_prebilattice X) : X := Ltop (pr2 b) .
End Bounded .