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 ❚