zanzix

-- Left kan extension w.r.t the functor j
data Lan : (j: k -> Type) -> (f : k -> Type) -> Type -> Type where 
  MkLan : {j: k -> Type} -> {a:k} -> (j a -> b) -> f a -> Lan j f b

-- The free relative monad over j
data Freest : {k : Type} -> (k -> Type) -> (k -> Type) -> k -> Type where
  Var  : {j : k -> Type} -> j v -> Freest j f v
  Bind : {j : k -> Type} -> Lan j f (Freest j f v) -> Freest j f v

-- General Functor

zanzix

-- The Bicategory of endofunctors as a 2d indexed algebra

-- Natural transformations between functors (Type -> Type)
infixr 1 :~>
(:~>) : {o : Type} -> (o -> Type) -> (o -> Type) -> Type  
(:~>) f g = {a : o} -> f a -> g a 

-- | Syntax

-- 0-cells are Categories

zanzix

%hide Neg 

-- Base types. Unit, Bool, Monoid
data Ty = Unit | B | M | Ten Ty Ty | Sum Ty Ty | Neg Ty 

Val : Ty -> Type 
Val Unit = Unit 
Val (Sum a b) = Either (Val a) (Val b) 
Val (Ten a b) = (Val a, Val b) 
Val B = Bool 

zanzix

-- Greatest fixpoint of (1 + a * x), "possibly-terminating streams"
data Colist : Type -> Type where 
  Nil : Colist a 
  (::) : a -> Inf (Colist a) -> Colist a 

-- Environment indexed by a colist
data CoAll : (p : k -> Type) -> Colist k -> Type where 
  Empty : CoAll p Nil
  Cons : {p : k -> Type} -> p x -> Inf (CoAll p xs) -> CoAll p (x :: xs)

zanzix

-- | Concategory
data Concat : List o -> List o -> Type where
  -- Identity
  Id : Concat as as
  -- Sequential composition
  Seq : Concat bs cs -> Concat as bs -> Concat as cs
  -- Par
  Par : {as, bs, cs, ds : List o} -> Concat as bs -> Concat cs ds -> Concat (as++cs) (bs++ds)
  -- Symmetry
  Sym : Concat (x ++ y) (y ++ x)

zanzix

import Data.List.Elem 

data Ty = U | Base | Prod Ty Ty | Sum Ty Ty | Imp Ty Ty | Sub Ty Ty | S Ty 

infixr 5 :*: 
(:*:) : Ty -> Ty -> Ty
(:*:) = Prod 

infixr 5 ~> 
(~>) : Ty -> Ty -> Ty

zanzix

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 (->)

zanzix

-- We define uncurried versions of Pair and Either to help with type-checking
data Tuple : (Type, Type) -> Type where 
  MkTuple : a -> b -> Tuple (a, b)

data Sum : (Type, Type) -> Type where 
  Left : a -> Sum (a, b)
  Right : b -> Sum (a, b)

-- These are bifunctor versions of projections/injections
data Fst : (Type, Type) -> Type where 

zanzix

infixr 5 +++
infixr 5 ***

-- A list over a type
-- data List : Type -> Type where 
--   Nil : List a 
--   (::) : a -> List a -> List a 

Graph : Type -> Type 
Graph obj = obj -> obj -> Type 

zanzix

-- Profunctor composition
data CompP : (k1 -> k2 -> Type) -> (k2 -> k3 -> Type) -> k1 -> k3 -> Type where 
InComp : {k1, k2, k3 : Type} -> {a : k1} -> {b : k2} -> {c : k3} -> {p : k1 -> k2 -> Type} -> {q : k2 -> k3 -> Type} 
  -> p a b -> q b c -> CompP p q a c 

-- Natural transformations over profunctors
Nt : {k1, k2 : Type} -> {arr : t -> t -> Type} -> (k1 -> k2 -> t) -> (k1 -> k2 -> t) -> Type  
Nt f g = {a : k1} -> {b : k2} -> arr (f a b) (g a b) 

-- Category of idris functions