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

Generalizable Variables A B C K L f.

Global Instance bounded_sl_is_sl `{IsBoundedSemiLattice L} : IsSemiLattice L.
L: Type
Aop: SgOp L
Aunit: MonUnit L
H: IsBoundedSemiLattice L
IsSemiLattice L
Proof.
L: Type
Aop: SgOp L
Aunit: MonUnit L
H: IsBoundedSemiLattice L
IsSemiLattice L
repeat (split; try apply _).
Qed.

Global Instance bounded_join_sl_is_join_sl `{IsBoundedJoinSemiLattice L} : IsJoinSemiLattice L.
L: Type
Ajoin: Join L
Abottom: Bottom L
H: IsBoundedJoinSemiLattice L
IsJoinSemiLattice L
Proof.
L: Type
Ajoin: Join L
Abottom: Bottom L
H: IsBoundedJoinSemiLattice L
IsJoinSemiLattice L
repeat (split; try apply _).
Qed.

Global Instance bounded_meet_sl_is_meet_sl `{IsBoundedMeetSemiLattice L} : IsMeetSemiLattice L.
L: Type
Ameet: Meet L
Atop: Top L
H: IsBoundedMeetSemiLattice L
IsMeetSemiLattice L
Proof.
L: Type
Ameet: Meet L
Atop: Top L
H: IsBoundedMeetSemiLattice L
IsMeetSemiLattice L
repeat (split; try apply _).
Qed.

Global Instance bounded_lattice_is_lattice `{IsBoundedLattice L} : IsLattice L.
L: Type
Ajoin: Join L
Ameet: Meet L
Abottom: Bottom L
Atop: Top L
H: IsBoundedLattice L
IsLattice L
Proof.
L: Type
Ajoin: Join L
Ameet: Meet L
Abottom: Bottom L
Atop: Top L
H: IsBoundedLattice L
IsLattice L
repeat split; apply _.
Qed.

Global Instance bounded_sl_mor_is_sl_mor `{H : IsBoundedJoinPreserving A B f}
  : IsJoinPreserving f.
A, B: Type
Ajoin: Join A
Bjoin: Join B
Abottom: Bottom A
Bbottom: Bottom B
f: A -> B
H: IsBoundedJoinPreserving f
IsJoinPreserving f
Proof.
A, B: Type
Ajoin: Join A
Bjoin: Join B
Abottom: Bottom A
Bbottom: Bottom B
f: A -> B
H: IsBoundedJoinPreserving f
IsJoinPreserving f
red;apply _.
Qed.

Lemma preserves_join `{IsJoinPreserving L K f} x y
  : f (x ⊔ y) = f x ⊔ f y.
L, K: Type
Ajoin: Join L
Bjoin: Join K
f: L -> K
H: IsJoinPreserving f
x, y: L
f (x ⊔ y) = f x ⊔ f y
Proof.
L, K: Type
Ajoin: Join L
Bjoin: Join K
f: L -> K
H: IsJoinPreserving f
x, y: L
f (x ⊔ y) = f x ⊔ f y apply preserves_sg_op. Qed.

Lemma preserves_bottom `{IsBoundedJoinPreserving L K f}
  : f ⊥ = ⊥.
L, K: Type
Ajoin: Join L
Bjoin: Join K
Abottom: Bottom L
Bbottom: Bottom K
f: L -> K
H: IsBoundedJoinPreserving f
f ⊥ = ⊥
Proof.
L, K: Type
Ajoin: Join L
Bjoin: Join K
Abottom: Bottom L
Bbottom: Bottom K
f: L -> K
H: IsBoundedJoinPreserving f
f ⊥ = ⊥ apply preserves_mon_unit. Qed.

Lemma preserves_meet `{IsMeetPreserving L K f} x y :
  f (x ⊓ y) = f x ⊓ f y.
L, K: Type
Ameet: Meet L
Bmeet: Meet K
f: L -> K
H: IsMeetPreserving f
x, y: L
f (x ⊓ y) = f x ⊓ f y
Proof.
L, K: Type
Ameet: Meet L
Bmeet: Meet K
f: L -> K
H: IsMeetPreserving f
x, y: L
f (x ⊓ y) = f x ⊓ f y apply preserves_sg_op. Qed.

Section bounded_join_sl_props.
  Context `{IsBoundedJoinSemiLattice L}.

  Instance join_bottom_l: LeftIdentity (⊔) ⊥ := _.
  Instance join_bottom_r: RightIdentity (⊔) ⊥ := _.
End bounded_join_sl_props.

Section lattice_props.
  Context `{IsLattice L}.

  Definition meet_join_absorption x y : x ⊓ (x ⊔ y) = x := absorption x y.
  Definition join_meet_absorption x y : x ⊔ (x ⊓ y) = x := absorption x y.
End lattice_props.

Section distributive_lattice_props.
  Context `{IsDistributiveLattice L}.

  Instance join_meet_distr_l: LeftDistribute (⊔) (⊓).
L: Type
Ajoin: Join L
Ameet: Meet L
H: IsDistributiveLattice L
LeftDistribute join meet
  Proof.
L: Type
Ajoin: Join L
Ameet: Meet L
H: IsDistributiveLattice L
LeftDistribute join meet exact (join_meet_distr_l _). Qed.

  Global Instance join_meet_distr_r: RightDistribute (⊔) (⊓).
L: Type
Ajoin: Join L
Ameet: Meet L
H: IsDistributiveLattice L
RightDistribute join meet
  Proof.
L: Type
Ajoin: Join L
Ameet: Meet L
H: IsDistributiveLattice L
RightDistribute join meet
  intros x y z.
L: Type
Ajoin: Join L
Ameet: Meet L
H: IsDistributiveLattice L
x, y, z: L
(x ⊓ y) ⊔ z = (x ⊔ z) ⊓ (y ⊔ z) rewrite !(commutativity _ z).
L: Type
Ajoin: Join L
Ameet: Meet L
H: IsDistributiveLattice L
x, y, z: L
z ⊔ (x ⊓ y) = (z ⊔ x) ⊓ (z ⊔ y)
  apply distribute_l.
  Qed.

  Global Instance meet_join_distr_l: LeftDistribute (⊓) (⊔).
L: Type
Ajoin: Join L
Ameet: Meet L
H: IsDistributiveLattice L
LeftDistribute meet join
  Proof.
L: Type
Ajoin: Join L
Ameet: Meet L
H: IsDistributiveLattice L
LeftDistribute meet join
  intros x y z.
L: Type
Ajoin: Join L
Ameet: Meet L
H: IsDistributiveLattice L
x, y, z: L
x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z)
  rewrite (simple_distribute_l (f:=join)).
L: Type
Ajoin: Join L
Ameet: Meet L
H: IsDistributiveLattice L
x, y, z: L
x ⊓ (y ⊔ z) = ((x ⊓ y) ⊔ x) ⊓ ((x ⊓ y) ⊔ z)
  rewrite (simple_distribute_r (f:=join)).
L: Type
Ajoin: Join L
Ameet: Meet L
H: IsDistributiveLattice L
x, y, z: L
x ⊓ (y ⊔ z) = ((x ⊔ x) ⊓ (y ⊔ x)) ⊓ ((x ⊓ y) ⊔ z)
  rewrite (idempotency (⊔) x).
L: Type
Ajoin: Join L
Ameet: Meet L
H: IsDistributiveLattice L
x, y, z: L
x ⊓ (y ⊔ z) = (x ⊓ (y ⊔ x)) ⊓ ((x ⊓ y) ⊔ z)
  rewrite (commutativity (f:=join) y x), meet_join_absorption.
L: Type
Ajoin: Join L
Ameet: Meet L
H: IsDistributiveLattice L
x, y, z: L
x ⊓ (y ⊔ z) = x ⊓ ((x ⊓ y) ⊔ z)
  path_via ((x ⊓ (x ⊔ z)) ⊓ (y ⊔ z)).
L: Type
Ajoin: Join L
Ameet: Meet L
H: IsDistributiveLattice L
x, y, z: L
x ⊓ (y ⊔ z) = (x ⊓ (x ⊔ z)) ⊓ (y ⊔ z)
L: Type
Ajoin: Join L
Ameet: Meet L
H: IsDistributiveLattice L
x, y, z: L
(x ⊓ (x ⊔ z)) ⊓ (y ⊔ z) = x ⊓ ((x ⊓ y) ⊔ z)
  -
L: Type
Ajoin: Join L
Ameet: Meet L
H: IsDistributiveLattice L
x, y, z: L
x ⊓ (y ⊔ z) = (x ⊓ (x ⊔ z)) ⊓ (y ⊔ z) rewrite (meet_join_absorption x z).
L: Type
Ajoin: Join L
Ameet: Meet L
H: IsDistributiveLattice L
x, y, z: L
x ⊓ (y ⊔ z) = x ⊓ (y ⊔ z) reflexivity.
  -
L: Type
Ajoin: Join L
Ameet: Meet L
H: IsDistributiveLattice L
x, y, z: L
(x ⊓ (x ⊔ z)) ⊓ (y ⊔ z) = x ⊓ ((x ⊓ y) ⊔ z) rewrite <-simple_associativity.
L: Type
Ajoin: Join L
Ameet: Meet L
H: IsDistributiveLattice L
x, y, z: L
x ⊓ ((x ⊔ z) ⊓ (y ⊔ z)) = x ⊓ ((x ⊓ y) ⊔ z)
    rewrite <-distribute_r.
L: Type
Ajoin: Join L
Ameet: Meet L
H: IsDistributiveLattice L
x, y, z: L
x ⊓ ((x ⊓ y) ⊔ z) = x ⊓ ((x ⊓ y) ⊔ z)
    reflexivity.
  Qed.

  Global Instance meet_join_distr_r: RightDistribute (⊓) (⊔).
L: Type
Ajoin: Join L
Ameet: Meet L
H: IsDistributiveLattice L
RightDistribute meet join
  Proof.
L: Type
Ajoin: Join L
Ameet: Meet L
H: IsDistributiveLattice L
RightDistribute meet join
  intros x y z.
L: Type
Ajoin: Join L
Ameet: Meet L
H: IsDistributiveLattice L
x, y, z: L
(x ⊔ y) ⊓ z = (x ⊓ z) ⊔ (y ⊓ z) rewrite !(commutativity _ z).
L: Type
Ajoin: Join L
Ameet: Meet L
H: IsDistributiveLattice L
x, y, z: L
z ⊓ (x ⊔ y) = (z ⊓ x) ⊔ (z ⊓ y)
  apply distribute_l.
  Qed.

  Lemma distribute_alt x y z
    : (x ⊓ y) ⊔ (x ⊓ z) ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z) ⊓ (y ⊔ z).
L: Type
Ajoin: Join L
Ameet: Meet L
H: IsDistributiveLattice L
x, y, z: L
((x ⊓ y) ⊔ (x ⊓ z)) ⊔ (y ⊓ z) =
((x ⊔ y) ⊓ (x ⊔ z)) ⊓ (y ⊔ z)
  Proof.
L: Type
Ajoin: Join L
Ameet: Meet L
H: IsDistributiveLattice L
x, y, z: L
((x ⊓ y) ⊔ (x ⊓ z)) ⊔ (y ⊓ z) =
((x ⊔ y) ⊓ (x ⊔ z)) ⊓ (y ⊔ z)
  rewrite (distribute_r x y (x ⊓ z)), join_meet_absorption.
L: Type
Ajoin: Join L
Ameet: Meet L
H: IsDistributiveLattice L
x, y, z: L
(x ⊓ (y ⊔ (x ⊓ z))) ⊔ (y ⊓ z) =
((x ⊔ y) ⊓ (x ⊔ z)) ⊓ (y ⊔ z)
  rewrite (distribute_r _ _ (y ⊓ z)).
L: Type
Ajoin: Join L
Ameet: Meet L
H: IsDistributiveLattice L
x, y, z: L
(x ⊔ (y ⊓ z)) ⊓ ((y ⊔ (x ⊓ z)) ⊔ (y ⊓ z)) =
((x ⊔ y) ⊓ (x ⊔ z)) ⊓ (y ⊔ z)
  rewrite (distribute_l x y z).
L: Type
Ajoin: Join L
Ameet: Meet L
H: IsDistributiveLattice L
x, y, z: L
((x ⊔ y) ⊓ (x ⊔ z)) ⊓ ((y ⊔ (x ⊓ z)) ⊔ (y ⊓ z)) =
((x ⊔ y) ⊓ (x ⊔ z)) ⊓ (y ⊔ z)
  rewrite (commutativity y (x ⊓ z)), <-(simple_associativity _ y).
L: Type
Ajoin: Join L
Ameet: Meet L
H: IsDistributiveLattice L
x, y, z: L
((x ⊔ y) ⊓ (x ⊔ z)) ⊓ ((x ⊓ z) ⊔ (y ⊔ (y ⊓ z))) =
((x ⊔ y) ⊓ (x ⊔ z)) ⊓ (y ⊔ z)
  rewrite join_meet_absorption.
L: Type
Ajoin: Join L
Ameet: Meet L
H: IsDistributiveLattice L
x, y, z: L
((x ⊔ y) ⊓ (x ⊔ z)) ⊓ ((x ⊓ z) ⊔ y) =
((x ⊔ y) ⊓ (x ⊔ z)) ⊓ (y ⊔ z)
  rewrite (distribute_r x z y).
L: Type
Ajoin: Join L
Ameet: Meet L
H: IsDistributiveLattice L
x, y, z: L
((x ⊔ y) ⊓ (x ⊔ z)) ⊓ ((x ⊔ y) ⊓ (z ⊔ y)) =
((x ⊔ y) ⊓ (x ⊔ z)) ⊓ (y ⊔ z)
  rewrite (commutativity (f:=join) z y).
L: Type
Ajoin: Join L
Ameet: Meet L
H: IsDistributiveLattice L
x, y, z: L
((x ⊔ y) ⊓ (x ⊔ z)) ⊓ ((x ⊔ y) ⊓ (y ⊔ z)) =
((x ⊔ y) ⊓ (x ⊔ z)) ⊓ (y ⊔ z)
  rewrite (commutativity (x ⊔ y) (x ⊔ z)).
L: Type
Ajoin: Join L
Ameet: Meet L
H: IsDistributiveLattice L
x, y, z: L
((x ⊔ z) ⊓ (x ⊔ y)) ⊓ ((x ⊔ y) ⊓ (y ⊔ z)) =
((x ⊔ z) ⊓ (x ⊔ y)) ⊓ (y ⊔ z)
  rewrite simple_associativity, <-(simple_associativity (x ⊔ z)).
L: Type
Ajoin: Join L
Ameet: Meet L
H: IsDistributiveLattice L
x, y, z: L
((x ⊔ z) ⊓ ((x ⊔ y) ⊓ (x ⊔ y))) ⊓ (y ⊔ z) =
((x ⊔ z) ⊓ (x ⊔ y)) ⊓ (y ⊔ z)
  rewrite (idempotency _ _).
L: Type
Ajoin: Join L
Ameet: Meet L
H: IsDistributiveLattice L
x, y, z: L
((x ⊔ z) ⊓ (x ⊔ y)) ⊓ (y ⊔ z) =
((x ⊔ z) ⊓ (x ⊔ y)) ⊓ (y ⊔ z)
  rewrite (commutativity (x ⊔ z) (x ⊔ y)).
L: Type
Ajoin: Join L
Ameet: Meet L
H: IsDistributiveLattice L
x, y, z: L
((x ⊔ y) ⊓ (x ⊔ z)) ⊓ (y ⊔ z) =
((x ⊔ y) ⊓ (x ⊔ z)) ⊓ (y ⊔ z)
  reflexivity.
  Qed.
End distributive_lattice_props.

Section lower_bounded_lattice.
  Context `{IsLattice L} `{Bottom L} `{!IsBoundedJoinSemiLattice L}.

  Global Instance meet_bottom_l: LeftAbsorb (⊓) ⊥.
L: Type
Ajoin: Join L
Ameet: Meet L
H: IsLattice L
H0: Bottom L
IsBoundedJoinSemiLattice0: IsBoundedJoinSemiLattice L
LeftAbsorb meet ⊥
  Proof.
L: Type
Ajoin: Join L
Ameet: Meet L
H: IsLattice L
H0: Bottom L
IsBoundedJoinSemiLattice0: IsBoundedJoinSemiLattice L
LeftAbsorb meet ⊥
  intros x.
L: Type
Ajoin: Join L
Ameet: Meet L
H: IsLattice L
H0: Bottom L
IsBoundedJoinSemiLattice0: IsBoundedJoinSemiLattice L
x: L
⊥ ⊓ x = ⊥ rewrite <-(join_bottom_l x), absorption.
L: Type
Ajoin: Join L
Ameet: Meet L
H: IsLattice L
H0: Bottom L
IsBoundedJoinSemiLattice0: IsBoundedJoinSemiLattice L
x: L
⊥ = ⊥
  trivial.
  Qed.

  Global Instance meet_bottom_r: RightAbsorb (⊓) ⊥.
L: Type
Ajoin: Join L
Ameet: Meet L
H: IsLattice L
H0: Bottom L
IsBoundedJoinSemiLattice0: IsBoundedJoinSemiLattice L
RightAbsorb meet ⊥
  Proof.
L: Type
Ajoin: Join L
Ameet: Meet L
H: IsLattice L
H0: Bottom L
IsBoundedJoinSemiLattice0: IsBoundedJoinSemiLattice L
RightAbsorb meet ⊥
  intros x.
L: Type
Ajoin: Join L
Ameet: Meet L
H: IsLattice L
H0: Bottom L
IsBoundedJoinSemiLattice0: IsBoundedJoinSemiLattice L
x: L
x ⊓ ⊥ = ⊥
  rewrite (commutativity (f:=meet)), left_absorb.
L: Type
Ajoin: Join L
Ameet: Meet L
H: IsLattice L
H0: Bottom L
IsBoundedJoinSemiLattice0: IsBoundedJoinSemiLattice L
x: L
⊥ = ⊥
  trivial.
  Qed.
End lower_bounded_lattice.

Section from_another_sl.
  Local Open Scope mc_add_scope.
  Context `{IsSemiLattice A} `{IsHSet B}
   `{Bop : SgOp B} (f : B -> A) `{!IsInjective f}
   (op_correct : forall x y, f (x + y) = f x + f y).

  Lemma projected_sl: IsSemiLattice B.
A: Type
Aop: SgOp A
H: IsSemiLattice A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x + y) = f x + f y
IsSemiLattice B
  Proof.
A: Type
Aop: SgOp A
H: IsSemiLattice A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x + y) = f x + f y
IsSemiLattice B
  split.
A: Type
Aop: SgOp A
H: IsSemiLattice A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x + y) = f x + f y
IsCommutativeSemiGroup B
A: Type
Aop: SgOp A
H: IsSemiLattice A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x + y) = f x + f y
BinaryIdempotent sg_op
  -
A: Type
Aop: SgOp A
H: IsSemiLattice A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x + y) = f x + f y
IsCommutativeSemiGroup B apply (projected_com_sg f).
A: Type
Aop: SgOp A
H: IsSemiLattice A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x + y) = f x + f y
forall x y : B, f (x + y) = f x + f y assumption.
  -
A: Type
Aop: SgOp A
H: IsSemiLattice A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x + y) = f x + f y
BinaryIdempotent sg_op repeat intro; apply (injective f).
A: Type
Aop: SgOp A
H: IsSemiLattice A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x + y) = f x + f y
x: B
f (x + x) = f x rewrite !op_correct, (idempotency (+) _).
A: Type
Aop: SgOp A
H: IsSemiLattice A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x + y) = f x + f y
x: B
f x = f x
    reflexivity.
  Qed.
End from_another_sl.

Section from_another_bounded_sl.
  Local Open Scope mc_add_scope.
  Context `{IsBoundedSemiLattice A} `{IsHSet B}
   `{Bop : SgOp B} `{Bunit : MonUnit B} (f : B -> A) `{!IsInjective f}
   (op_correct : forall x y, f (x + y) = f x + f y)
   (unit_correct : f mon_unit = mon_unit).

  Lemma projected_bounded_sl: IsBoundedSemiLattice B.
A: Type
Aop: SgOp A
Aunit: MonUnit A
H: IsBoundedSemiLattice A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
Bunit: MonUnit B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x + y) = f x + f y
unit_correct: f mon_unit = mon_unit
IsBoundedSemiLattice B
  Proof.
A: Type
Aop: SgOp A
Aunit: MonUnit A
H: IsBoundedSemiLattice A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
Bunit: MonUnit B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x + y) = f x + f y
unit_correct: f mon_unit = mon_unit
IsBoundedSemiLattice B
  split.
A: Type
Aop: SgOp A
Aunit: MonUnit A
H: IsBoundedSemiLattice A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
Bunit: MonUnit B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x + y) = f x + f y
unit_correct: f mon_unit = mon_unit
IsCommutativeMonoid B
A: Type
Aop: SgOp A
Aunit: MonUnit A
H: IsBoundedSemiLattice A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
Bunit: MonUnit B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x + y) = f x + f y
unit_correct: f mon_unit = mon_unit
BinaryIdempotent sg_op
  -
A: Type
Aop: SgOp A
Aunit: MonUnit A
H: IsBoundedSemiLattice A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
Bunit: MonUnit B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x + y) = f x + f y
unit_correct: f mon_unit = mon_unit
IsCommutativeMonoid B apply (projected_com_monoid f);trivial.
  -
A: Type
Aop: SgOp A
Aunit: MonUnit A
H: IsBoundedSemiLattice A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
Bunit: MonUnit B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x + y) = f x + f y
unit_correct: f mon_unit = mon_unit
BinaryIdempotent sg_op repeat intro; apply (injective f).
A: Type
Aop: SgOp A
Aunit: MonUnit A
H: IsBoundedSemiLattice A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
Bunit: MonUnit B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x + y) = f x + f y
unit_correct: f mon_unit = mon_unit
x: B
f (x + x) = f x
    rewrite op_correct, (idempotency (+) _).
A: Type
Aop: SgOp A
Aunit: MonUnit A
H: IsBoundedSemiLattice A
B: Type
IsHSet0: IsHSet B
Bop: SgOp B
Bunit: MonUnit B
f: B -> A
IsInjective0: IsInjective f
op_correct: forall x y : B, f (x + y) = f x + f y
unit_correct: f mon_unit = mon_unit
x: B
f x = f x
    trivial.
  Qed.
End from_another_bounded_sl.

Global Instance id_join_sl_morphism `{IsJoinSemiLattice A} : IsJoinPreserving (@id A)
  := {}.

Global Instance id_meet_sl_morphism `{IsMeetSemiLattice A} : IsMeetPreserving (@id A)
  := {}.

Global Instance id_bounded_join_sl_morphism `{IsBoundedJoinSemiLattice A}
  : IsBoundedJoinPreserving (@id A)
  := {}.

Global Instance id_lattice_morphism `{IsLattice A} : IsLatticePreserving (@id A)
  := {}.

Section morphism_composition.
  Context `{Join A} `{Meet A} `{Bottom A}
    `{Join B} `{Meet B} `{Bottom B}
    `{Join C} `{Meet C} `{Bottom C}
    (f : A -> B) (g : B -> C).

  Instance compose_join_sl_morphism:
    IsJoinPreserving f -> IsJoinPreserving g ->
    IsJoinPreserving (g ∘ f).
A: Type
H: Join A
H0: Meet A
H1: Bottom A
B: Type
H2: Join B
H3: Meet B
H4: Bottom B
C: Type
H5: Join C
H6: Meet C
H7: Bottom C
f: A -> B
g: B -> C
IsJoinPreserving f ->
IsJoinPreserving g -> IsJoinPreserving (g ∘ f)
  Proof.
A: Type
H: Join A
H0: Meet A
H1: Bottom A
B: Type
H2: Join B
H3: Meet B
H4: Bottom B
C: Type
H5: Join C
H6: Meet C
H7: Bottom C
f: A -> B
g: B -> C
IsJoinPreserving f ->
IsJoinPreserving g -> IsJoinPreserving (g ∘ f)
  red; apply _.
  Qed.

  Instance compose_meet_sl_morphism:
    IsMeetPreserving f -> IsMeetPreserving g ->
    IsMeetPreserving (g ∘ f).
A: Type
H: Join A
H0: Meet A
H1: Bottom A
B: Type
H2: Join B
H3: Meet B
H4: Bottom B
C: Type
H5: Join C
H6: Meet C
H7: Bottom C
f: A -> B
g: B -> C
IsMeetPreserving f ->
IsMeetPreserving g -> IsMeetPreserving (g ∘ f)
  Proof.
A: Type
H: Join A
H0: Meet A
H1: Bottom A
B: Type
H2: Join B
H3: Meet B
H4: Bottom B
C: Type
H5: Join C
H6: Meet C
H7: Bottom C
f: A -> B
g: B -> C
IsMeetPreserving f ->
IsMeetPreserving g -> IsMeetPreserving (g ∘ f)
  red;apply _.
  Qed.

  Instance compose_bounded_join_sl_morphism:
    IsBoundedJoinPreserving f -> IsBoundedJoinPreserving g ->
    IsBoundedJoinPreserving (g ∘ f).
A: Type
H: Join A
H0: Meet A
H1: Bottom A
B: Type
H2: Join B
H3: Meet B
H4: Bottom B
C: Type
H5: Join C
H6: Meet C
H7: Bottom C
f: A -> B
g: B -> C
IsBoundedJoinPreserving f ->
IsBoundedJoinPreserving g ->
IsBoundedJoinPreserving (g ∘ f)
  Proof.
A: Type
H: Join A
H0: Meet A
H1: Bottom A
B: Type
H2: Join B
H3: Meet B
H4: Bottom B
C: Type
H5: Join C
H6: Meet C
H7: Bottom C
f: A -> B
g: B -> C
IsBoundedJoinPreserving f ->
IsBoundedJoinPreserving g ->
IsBoundedJoinPreserving (g ∘ f)
  red; apply _.
  Qed.

  Instance compose_lattice_morphism:
    IsLatticePreserving f -> IsLatticePreserving g -> IsLatticePreserving (g ∘ f).
A: Type
H: Join A
H0: Meet A
H1: Bottom A
B: Type
H2: Join B
H3: Meet B
H4: Bottom B
C: Type
H5: Join C
H6: Meet C
H7: Bottom C
f: A -> B
g: B -> C
IsLatticePreserving f ->
IsLatticePreserving g -> IsLatticePreserving (g ∘ f)
  Proof.
A: Type
H: Join A
H0: Meet A
H1: Bottom A
B: Type
H2: Join B
H3: Meet B
H4: Bottom B
C: Type
H5: Join C
H6: Meet C
H7: Bottom C
f: A -> B
g: B -> C
IsLatticePreserving f ->
IsLatticePreserving g -> IsLatticePreserving (g ∘ f)
  split; apply _.
  Qed.

  Instance invert_join_sl_morphism:
    forall `{!IsEquiv f}, IsJoinPreserving f ->
    IsJoinPreserving (f^-1).
A: Type
H: Join A
H0: Meet A
H1: Bottom A
B: Type
H2: Join B
H3: Meet B
H4: Bottom B
C: Type
H5: Join C
H6: Meet C
H7: Bottom C
f: A -> B
g: B -> C
forall IsEquiv0 : IsEquiv f,
IsJoinPreserving f -> IsJoinPreserving f^-1
  Proof.
A: Type
H: Join A
H0: Meet A
H1: Bottom A
B: Type
H2: Join B
H3: Meet B
H4: Bottom B
C: Type
H5: Join C
H6: Meet C
H7: Bottom C
f: A -> B
g: B -> C
forall IsEquiv0 : IsEquiv f,
IsJoinPreserving f -> IsJoinPreserving f^-1
  red; apply _.
  Qed.

  Instance invert_meet_sl_morphism:
    forall `{!IsEquiv f}, IsMeetPreserving f ->
    IsMeetPreserving (f^-1).
A: Type
H: Join A
H0: Meet A
H1: Bottom A
B: Type
H2: Join B
H3: Meet B
H4: Bottom B
C: Type
H5: Join C
H6: Meet C
H7: Bottom C
f: A -> B
g: B -> C
forall IsEquiv0 : IsEquiv f,
IsMeetPreserving f -> IsMeetPreserving f^-1
  Proof.
A: Type
H: Join A
H0: Meet A
H1: Bottom A
B: Type
H2: Join B
H3: Meet B
H4: Bottom B
C: Type
H5: Join C
H6: Meet C
H7: Bottom C
f: A -> B
g: B -> C
forall IsEquiv0 : IsEquiv f,
IsMeetPreserving f -> IsMeetPreserving f^-1
  red; apply _.
  Qed.

  Instance invert_bounded_join_sl_morphism:
    forall `{!IsEquiv f}, IsBoundedJoinPreserving f ->
    IsBoundedJoinPreserving (f^-1).
A: Type
H: Join A
H0: Meet A
H1: Bottom A
B: Type
H2: Join B
H3: Meet B
H4: Bottom B
C: Type
H5: Join C
H6: Meet C
H7: Bottom C
f: A -> B
g: B -> C
forall IsEquiv0 : IsEquiv f,
IsBoundedJoinPreserving f ->
IsBoundedJoinPreserving f^-1
  Proof.
A: Type
H: Join A
H0: Meet A
H1: Bottom A
B: Type
H2: Join B
H3: Meet B
H4: Bottom B
C: Type
H5: Join C
H6: Meet C
H7: Bottom C
f: A -> B
g: B -> C
forall IsEquiv0 : IsEquiv f,
IsBoundedJoinPreserving f ->
IsBoundedJoinPreserving f^-1
  red; apply _.
  Qed.

  Instance invert_lattice_morphism:
    forall `{!IsEquiv f}, IsLatticePreserving f -> IsLatticePreserving (f^-1).
A: Type
H: Join A
H0: Meet A
H1: Bottom A
B: Type
H2: Join B
H3: Meet B
H4: Bottom B
C: Type
H5: Join C
H6: Meet C
H7: Bottom C
f: A -> B
g: B -> C
forall IsEquiv0 : IsEquiv f,
IsLatticePreserving f -> IsLatticePreserving f^-1
  Proof.
A: Type
H: Join A
H0: Meet A
H1: Bottom A
B: Type
H2: Join B
H3: Meet B
H4: Bottom B
C: Type
H5: Join C
H6: Meet C
H7: Bottom C
f: A -> B
g: B -> C
forall IsEquiv0 : IsEquiv f,
IsLatticePreserving f -> IsLatticePreserving f^-1
  split; apply _.
  Qed.
End morphism_composition.

#[export]
Hint Extern 4 (IsJoinPreserving (_ ∘ _)) =>
  class_apply @compose_join_sl_morphism : typeclass_instances.
#[export]
Hint Extern 4 (IsMeetPreserving (_ ∘ _)) =>
  class_apply @compose_meet_sl_morphism : typeclass_instances.
#[export]
Hint Extern 4 (IsBoundedJoinPreserving (_ ∘ _)) =>
  class_apply @compose_bounded_join_sl_morphism : typeclass_instances.
#[export]
Hint Extern 4 (IsLatticePreserving (_ ∘ _)) =>
  class_apply @compose_lattice_morphism : typeclass_instances.
#[export]
Hint Extern 4 (IsJoinPreserving (_^-1)) =>
  class_apply @invert_join_sl_morphism : typeclass_instances.
#[export]
Hint Extern 4 (IsMeetPreserving (_^-1)) =>
  class_apply @invert_meet_sl_morphism : typeclass_instances.
#[export]
Hint Extern 4 (IsBoundedJoinPreserving (_^-1)) =>
  class_apply @invert_bounded_join_sl_morphism : typeclass_instances.
#[export]
Hint Extern 4 (IsLatticePreserving (_^-1)) =>
  class_apply @invert_lattice_morphism : typeclass_instances.