Library HoTT.Classes.implementations.pointwise

If B is a (bounded) lattice, then so is A → B, pointwise. This relies on functional extensionality.

Section contents.
  Context `{Funext}.

  Context {A B : Type}.
  Context `{BJoin : Join B}.
  Context `{BMeet : Meet B}.
  Context `{BBottom : Bottom B}.
  Context `{BTop : Top B}.

  Global Instance bot_fun : Bottom (A → B)
    := fun _ ⇒ ⊥.

  Global Instance top_fun : Top (A → B)
    := fun _ ⇒ ⊤.

  Global Instance join_fun : Join (A → B) :=
    fun (f g : A → B) (a : A) ⇒ (f a ) ⊔ (g a ).

  Global Instance meet_fun : Meet (A → B) :=
    fun (f g : A → B) (a : A) ⇒ (f a ) ⊓ (g a ).

Try to solve some of the lattice obligations automatically

  Create HintDb lattice_hints.
  #[local]
  Hint Resolve
       associativity
       absorption
       commutativity | 1 : lattice_hints.
  Local Ltac reduce_fun := compute; intros; apply path_forall; intro.

  Global Instance lattice_fun `{!IsLattice B} : IsLattice (A → B).
  Proof.
    repeat split; try apply _; reduce_fun.
    1,4: apply associativity.
    1,3: apply commutativity.
    1,2: apply binary_idempotent.
    1,2: apply absorption.
  Defined.

  Instance boundedjoinsemilattice_fun
   `{!IsBoundedJoinSemiLattice B} :
    IsBoundedJoinSemiLattice (A → B).
  Proof.
    repeat split; try apply _; reduce_fun.
    × apply associativity.
    × apply left_identity.
    × apply right_identity.
    × apply commutativity.
    × apply binary_idempotent.
  Defined.

  Instance boundedmeetsemilattice_fun
   `{!IsBoundedMeetSemiLattice B} :
    IsBoundedMeetSemiLattice (A → B).
  Proof.
    repeat split; try apply _; reduce_fun.
    × apply associativity.
    × apply left_identity.
    × apply right_identity.
    × apply commutativity.
    × apply binary_idempotent.
  Defined.

  Global Instance boundedlattice_fun
   `{!IsBoundedLattice B} : IsBoundedLattice (A → B).
  Proof.
    repeat split; try apply _; reduce_fun; apply absorption.
  Defined.
End contents.

#[export]
  Hint Resolve
       associativity
       absorption
       commutativity | 1 : lattice_hints.