```module Algebra.Heyting.Layered
( Layered (..)
, layer
) where

import           Prelude

import           Algebra.Lattice ( BoundedJoinSemiLattice (..)
, JoinSemiLattice (..)
, BoundedMeetSemiLattice (..)
, MeetSemiLattice (..)
, BoundedLattice
, Lattice
)

import           Algebra.Heyting (HeytingAlgebra (..))

-- |
-- Layer one Heyting algebra on top of the other.  Note: this is not
-- a categorical sum.
data Layered a b
= Lower a
| Upper b
deriving (Show, Eq, Ord)

instance (JoinSemiLattice a, JoinSemiLattice b) => JoinSemiLattice (Layered a b) where
Lower _   \/ u@Upper{} = u
u@Upper{} \/ Lower _   = u
Lower l   \/ Lower l'  = Lower \$ l \/ l'
Upper u   \/ Upper u'  = Upper \$ u \/ u'

instance (BoundedJoinSemiLattice a, JoinSemiLattice b) => BoundedJoinSemiLattice (Layered a b) where
bottom = Lower bottom

instance (MeetSemiLattice a, MeetSemiLattice b) => MeetSemiLattice (Layered a b) where
l@Lower{} /\ Upper _   = l
Upper _   /\ l@Lower{} = l
Lower l   /\ Lower l'  = Lower \$ l /\ l'
Upper u   /\ Upper u'  = Upper \$ u /\ u'

instance (MeetSemiLattice a, BoundedMeetSemiLattice b) => BoundedMeetSemiLattice (Layered a b) where
top = Upper top

instance ( Lattice a
, Lattice b
) => Lattice (Layered a b)

instance ( Lattice a
, Lattice b
, BoundedJoinSemiLattice a
, BoundedMeetSemiLattice b
) => BoundedLattice (Layered a b)

instance ( HeytingAlgebra a
, HeytingAlgebra b
, Eq a
) => HeytingAlgebra (Layered a b) where
Lower _   ==> Upper _      = Upper top
Upper _   ==> l@Lower{}    = l
Upper u   ==> Upper u'     = Upper \$ u ==> u'
Lower l   ==> Lower l'     = case l ==> l' of
ll' | ll' == top -> Upper top
| otherwise  -> Lower ll'

layer :: (a -> c) -> (b -> c) -> Layered a b -> c
layer f _ (Lower a) = f a
layer _ g (Upper b) = g b
```