blob: 67372751c75d6a88dd8c48dbb5ebe54eae6b39c3 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
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)
|
