module Data.Morphism.Indexed

import Data.Setoid.Indexed

public export
IFunc : {a : Type} -> (x, y : a -> Type) -> Type
IFunc {a} x y = (i : a) -> x i -> y i

public export
record IFunction {a : Type} (x, y : ISetoid a) where
  constructor MkIFunction
  func : IFunc x.U y.U
  cong : (i : a) -> {u, v : x.U i} -> x.relation i u v -> y.relation i (func i u) (func i v)

public export
ifunc : IFunc x y -> IFunction (isetoid x) (isetoid y)
ifunc f = MkIFunction f (\i => cong (f i))

public export
compFunc : IFunction b c -> IFunction a b -> IFunction a c
compFunc f g = MkIFunction (\i => f.func i . g.func i) (\i => f.cong i . g.cong i)