{-# OPTIONS --without-K #-}
module Composition.Forkable where

open import Type  hiding ()
open import Level using (_⊔_)

record Forkable {s t} {S :  s}
                (1+ : S  S)
                (_↝_ : S  S   t) :  (s  t) where
  constructor mk
  field
    fork :  {i o} (f g : i  o)  (1+ i)  o

open import Data.Product
open import Data.Bool

funFork :  {s}  Forkable (_×_ Bool)  (A B :  s)  A  B)
funFork {s} = mk fork where
  fork :  {A B :  s}  (f g : A  B)  Bool × A  B
  fork f g (b , x) = (if b then f else g) x

open import Data.Nat using (suc)
open import Data.Bits

bitsFunFork : Forkable suc _→ᵇ_
bitsFunFork = mk fork where
  fork :  {i o}  (f g : i →ᵇ o)  suc i →ᵇ o
  fork f g (b  x) = (if b then f else g) x