Restricted monads are relative monads

Restricted.idr

-- 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
record Functor {s, t : Type} (c1 : s -> s -> Type) (c2 : t -> t -> Type) (f : s -> t) where
  constructor MkFun 
  mapf : {a, b : s} -> c1 a b -> c2 (f a) (f b)

-- Types equipped with Equality
record Eqs where 
  constructor MkEqs
  carrier : Type 
  eq : carrier -> carrier -> Bool 

-- Example, Natural numbers 
eqNat : Eqs 
eqNat = MkEqs Nat (==)

-- Morphisms in the category of types with equality
EqArr : Eqs -> Eqs -> Type 
EqArr a b  = a.carrier -> b.carrier 

-- Set, implemented as List for simplicity
Set : Type -> Type 
Set a = List a 

-- setMap is a functor from the category of Eqs to Type
setMap : EqArr a b -> Set (a.carrier) -> Set (b.carrier)
setMap = map

-- embedding of the subcategory Eqs into Type
Embed : Eqs -> Type 
Embed a = a.carrier 

-- category of types
Idr : Type -> Type -> Type 
Idr a b = a -> b 

-- Set . Embed is a functor from the category of Eq to Type
setFunctor : Functor EqArr Idr (Set . Embed)
setFunctor = MkFun map

-- Set is the relative monad w.r.t this embedding  
setEx : Freest Embed (Set . Embed) (MkEqs Nat (==)) 
setEx = Var 5