A \otimes B

tensor of types

Ty.tensor, printed A ⊗ B

from source

\bigcirc A

the lax modality

Ty.circ, printed ◯A

unbridged

f \mathbin{;} g

composition of morphisms, in diagrammatic order

Mor.comp, printed f ≫ g

from source

f \otimes g

tensor of morphisms

Mor.tens, printed f ⊗ g

from source

f \equiv g

derivable equality of morphisms

MEq, printed f ≡ g

from source

\llbracket f \rrbracket_I

the meaning of f under the interpretation I

eval, printed ⟦f⟧[I]

new