Fixpoints of indexed functors, graphs, multi-graphs, poly-graphs

Fix.idr

infixr 5 ~> -- Morphism of indexed functors
infixr 5 ~~> -- Morphism of graphs/doubly-indexed functors
infixr 5 :~> -- Morphism of multi-graphs
infixr 5 :~:> -- Morphism of poly-graphs 

namespace Fix1 
  -- Objects are Types

  -- Morphisms are functions between types (->)

  -- Fixpoints of endofunctors over type
  data Mu : (pattern : Type -> Type) -> Type where
    In : {f: Type -> Type} -> f (Mu f) -> Mu f
  
  Algebra : (Type -> Type) -> Type -> Type  
  Algebra f a = f a -> a

  data Coyoneda : (Type -> Type) -> Type -> Type  where
    Coyo : (a -> b) -> f a -> Coyoneda f b

  mcata : Algebra (Coyoneda f) c -> Mu f -> c
  mcata alg (In op) = alg $ Coyo (mcata alg) op

namespace IxFix 
  -- Objects are indexed functors

  -- Morphisms are natural transformations between indexed functors 
  (~>) : {k : Type} -> (k -> Type) -> (k -> Type) -> Type  
  (~>) f g = {a : k} -> f a -> g a 

  -- Fixpoints of higher-order functors over indexed functors
  data Mu : ((k -> Type) -> (l -> Type)) -> k -> Type where
    In : f (Mu f) ~> Mu f

  Algebra : {k : Type} -> (h : (k -> Type) -> k -> Type) -> (f : k -> Type) -> Type
  Algebra h f = h f ~> f 

  data Coyoneda : (pattern: (k -> Type) -> l -> Type) -> (f : k -> Type) -> l -> Type  where
    Coyo : (f ~> g) -> h f ~> Coyoneda h g

  mcata : Algebra (Coyoneda f) c -> Mu f ~> c
  mcata alg (In op) = alg $ Coyo (mcata alg) op

namespace CatFix 
  -- Objects are graphs 
  Graph : Type -> Type 
  Graph o = o -> o -> Type 

  -- Morphisms are vertex-preserving transformations between graphs
  (~~>) : {o : Type} -> (o -> o -> Type) -> (o -> o -> Type) -> Type  
  (~~>) f g = {s, t : o} -> f s t -> g s t 

   -- Fixpoints of functors over graphs 
  data Mu : (Graph o -> Graph o) -> Graph o where
    In : f (Mu f) ~~> Mu f

  Algebra : {o : Type} -> (Graph o -> Graph o) -> Graph o -> Type
  Algebra f a = f a ~~> a 
    
  data Coyoneda : {o : Type} -> (pattern: (Graph o -> Graph o)) -> Graph o -> Graph o  where
    Coyo : f ~~> g -> h f ~~> Coyoneda h g

  mcata : Algebra (Coyoneda f) c -> Mu f ~~> c
  mcata alg (In op) = alg $ Coyo (mcata alg) op
    
namespace MultiFix 
  -- Objects are multi-graphs
  Multigraph : Type -> Type 
  Multigraph o = List o -> o -> Type
  
  -- Morphisms are vertex preserving transformations between multi-graphs
  (:~>) : {o : Type} -> Multigraph o -> Multigraph o -> Type  
  (:~>) f g = {s : List o} -> {t : o} -> f s t -> g s t 

  -- Fixpoints of functors over multi-graphs
  data Mu : (Multigraph o -> Multigraph o) -> Multigraph o where
    In : f (Mu f) :~> Mu f

  Algebra : {o : Type} -> (Multigraph o -> Multigraph o) -> Multigraph o -> Type
  Algebra f a = f a :~> a 

  data Coyoneda : {o : Type} -> (Multigraph o -> Multigraph o) -> Multigraph o -> Multigraph o where
    Coyo : f :~> g -> h f :~> Coyoneda h g

  mcata : Algebra (Coyoneda f) c -> Mu f :~> c
  mcata alg (In op) = alg $ Coyo (mcata alg) op

namespace PolyFix 
  -- Objects are poly-graphs
  Polygraph : Type -> Type 
  Polygraph o = List o -> List o -> Type 

  -- Morphisms are vertex preserving transformations between poly-graphs
  (:~:>) : {o : Type} -> Polygraph o -> Polygraph o -> Type  
  (:~:>) f g = {s, t : List o} -> f s t -> g s t 

  -- Fixpoints of functors over poly-graphs
  data Mu : (Polygraph o -> Polygraph o) -> Polygraph o where
    In : f (Mu f) :~:> Mu f

  Algebra : {o : Type} -> (Polygraph o -> Polygraph o) -> Polygraph o -> Type
  Algebra f a = f a :~:> a 

  data Coyoneda : {o : Type} -> (Polygraph o -> Polygraph o) -> Polygraph o -> Polygraph o where
    Coyo : f :~:> g -> h f :~:> Coyoneda h g

  mcata : Algebra (Coyoneda f) c -> Mu f :~:> c
  mcata alg (In op) = alg $ Coyo (mcata alg) op