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)