namespace latin:/❚
import diagops scala://diagops.latin2❚
/T Declare operator constants
Use an empty meta theory! E.g. if we used LF as a meta theory the notation
would be parsed as LF-y.
❚
theory TypeTheoryDiagramOperatorsSyntax =
single_typeindexifier # SINGLE TYPEINDEXIFY 1 prec -2000000 ❙
multi_typeindexifier # MULTI TYPEINDEXIFY 1 prec -2000000 ❙
❚
theory TypeTheoryDiagramOperatorsSemantics : ur:?LF =
include ☞http://cds.omdoc.org/urtheories?ModExp ❙
rule diagops?ComputeSingleTypeIndexed ❙
rule diagops?ComputeMultiTypeIndexed ❙
❚
theory TypeTheoryDiagramOperators =
include ?TypeTheoryDiagramOperatorsSyntax ❙
include ?TypeTheoryDiagramOperatorsSemantics ❙
❚
// theory TestMagma2 : ?TestMagmaMeta2 =
U: tp ❙
op: tm U ⟶ tm U ⟶ tm U ❘ # 1 ∘ 2 ❙
❚
// diagram TestEndoMagmaSingle : ?TypeTheoryDiagramOperators := SINGLE TYPEINDEXIFY ?TestMagma2 ❚
// diagram TestEndoMagmaMulti : ?TypeTheoryDiagramOperators := MULTI TYPEINDEXIFY ?TestMagma2 ❚