concats.idr

import Data.List

interface Cat obj (0 hom: obj -> obj -> Type) where
  id : {a: obj} -> hom a a
  seq: {a, b, c: obj} -> hom a b -> hom b c -> hom a c

interface Cat (List obj) hom => Concat obj hom where
  para: {Γ₁, Γ₂, Δ₁, Δ₂ : List obj}
     -> hom Γ₁ Δ₁ -> hom Γ₂ Δ₂ 
     -> hom (Γ₁ ++ Γ₂) (Δ₁ ++ Δ₂)
     
interface Concat obj hom => Cartesian obj hom where
  product: List obj -> obj
  rename: {Γ: List obj}
       -> (ρ: forall a. List a -> List a)
       -> hom Γ (ρ Γ)
  merge: {Γ: List obj} -> hom Γ [product Γ]
  split: {Γ: List obj} -> hom [product Γ] Γ
  fork: {Γ, Δ₁, Δ₂: List obj} 
     -> hom Γ Δ₁ -> hom Γ Δ₂
     -> hom Γ (Δ₁ ++ Δ₂)
  fork f g = seq {a=Γ} (rename {Γ} (\l => l ++ l)) (para {Γ₁=Γ} f g)