exn-arrow.agda

A `→? B = A `→ Bit `× B

{-
    id?
   +---+
   |  0|- Bit
A ≡|≡≡≡|≡ A
   +---+
-}
id? : A `→? A
id? = {!< zero × id >!}

{-
           f ;? g
   +---------------------+
   |       +--------(OR)-|- Bit
   |   f   |     g    |  |
   | +---+ |   +---+  |  |
   | |  ?|-+   |  ?|--+  |
A ≡|≡|≡≡≡|≡≡B≡≡|≡≡≡|≡≡≡≡≡|≡ C
   | +---+     +---+     |
   +---------------------+
-}
_⁏?_ : A `→? B → B `→? C → A `→? C

{-
    fail!
    +---+
    | 1-|- Bit
 A ≡|  ≡|≡ B
    +---+

-}
fail! : A `→? B

{-
     lift f
   +--------+
   |   f  0-|- Bit
   | +--+   |
A ≡|≡|  |≡≡≡|≡ B
   | +--+   |
   +--------+
-}
lift : A `→ B → A `→? B