blob: c271c90ca3d6c75f53454076eac0d2c936d1de14 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
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)
|
