src/SOAS/Theory.idr


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
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48

module SOAS.Theory

import SOAS.Algebra
import SOAS.Context
import SOAS.Family
import SOAS.Strength
import SOAS.Structure
import SOAS.Var

public export
record (.Initial)
         (signature : type.SortedFunctor)
         (meta : type.SortedFamily)
         (a : type.SortedFamily) where
  constructor MkInitial
  metalg : signature.MetaAlg meta a
  sem :
    (0 b : type.SortedFamily) ->
    (metalg : signature.MetaAlg meta b) =>
    a -|> b

%hint
public export
(.pointedCoalgStruct) :
  (str : Strength signature) =>
  signature.Initial meta a -> type.PointedCoalgStruct a
init.pointedCoalgStruct = MkPointedCoalgStruct
  { ren = init.sem ([] a) @{traverse init.metalg.alg init.metalg.var init.metalg.mvar}
  , var = init.metalg.var
  }


%hint
public export
(.monStruct) :
  (str : Strength signature) =>
  signature.Initial meta a -> type.MonStruct a
init.monStruct = MkSubstMonoidStruct
  { var = init.metalg.var
  , mult = init.sem (a ^ a) @{traverse init.metalg.alg id init.metalg.mvar}
  }

%hint
public export
(.monoidStruct) :
  (str : Strength signature) =>
  signature.Initial meta a -> signature.MonoidStruct a
init.monoidStruct = MkSignatureMonoid { mon = init.monStruct , alg = init.metalg.alg }