Homomorphisms of frames

module order-theory.homomorphisms-frames where
Imports
open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.functions
open import foundation.universe-levels

open import order-theory.frames
open import order-theory.homomorphisms-meet-semilattices
open import order-theory.homomorphisms-meet-sup-lattices
open import order-theory.homomorphisms-sup-lattices
open import order-theory.order-preserving-maps-posets

Idea

A frame homomorphism is an order preserving map between posets that additionally preserves binary meets and arbitrary joins.

Definitions

module _
  {l1 l2 l3 l4 : Level} (A : Frame l1 l2) (B : Frame l3 l4)
  where

  hom-Frame : UU (l1  lsuc l2  l3)
  hom-Frame = Σ (type-Frame A  type-Frame B)
     f  preserves-order-Poset (poset-Frame A) (poset-Frame B) f ×
      preserves-meets-sups
        ( meet-suplattice-Frame A)
        ( meet-suplattice-Frame B)
        ( f))

  map-hom-Frame : hom-Frame  type-Frame A  type-Frame B
  map-hom-Frame = pr1

  preserves-order-hom-Frame :
    (H : hom-Frame) 
    preserves-order-Poset (poset-Frame A) (poset-Frame B) (map-hom-Frame H)
  preserves-order-hom-Frame = pr1  pr2

  preserves-meets-sups-hom-Frame :
    (H : hom-Frame) 
    preserves-meets-sups
      ( meet-suplattice-Frame A)
      ( meet-suplattice-Frame B)
      ( map-hom-Frame H)
  preserves-meets-sups-hom-Frame = pr2  pr2

  preserves-meets-hom-Frame :
    (H : hom-Frame) 
    preserves-meet
      ( meet-semilattice-Frame A)
      ( meet-semilattice-Frame B)
      ( map-hom-Frame H)
  preserves-meets-hom-Frame = pr1  preserves-meets-sups-hom-Frame

  preserves-sups-hom-Frame :
    (H : hom-Frame) 
    preserves-sups
      ( suplattice-Frame A)
      ( suplattice-Frame B)
      ( map-hom-Frame H)
  preserves-sups-hom-Frame = pr2  preserves-meets-sups-hom-Frame