blob: f902ad4a2aad924d0e4411e4afbb00bf326d539c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
|
module SOAS.Strength
import SOAS.Family
import SOAS.Structure
import SOAS.Var
public export
0
(.SortedFunctor) : (type : Type) -> Type
type.SortedFunctor = type.SortedFamily -> type.SortedFamily
public export
record Strength (f : type.SortedFunctor) where
constructor MkStrength
strength :
(0 p,x : type.SortedFamily) ->
(mon : type.PointedCoalgStruct p) ->
(f (x ^ p)) -|> ((f x) ^ p)
export
(.str) :
Strength f ->
{0 p,x : type.SortedFamily} ->
(mon : type.PointedCoalgStruct p) =>
(f (x ^ p)) -|> ((f x) ^ p)
strength.str {p,x,mon} = strength.strength p x mon
public export
record (.Map) (signature : type.SortedFunctor) where
constructor MkMap
map :
{0 a,b : type.SortedFamily} -> (a -|> b) ->
signature a -|> signature b
|
