Database
BASIC CATEGORY THEORY
Categorical constructions
Functor evaluation
cdiag
Next ⟩
df-evlf
Metamath Proof Explorer
Unicode
Structured
Syntax definition
cdiag
Description:
Extend class notation to include the diagonal functor.
Ref
Expression
Assertion
cdiag
class DiagFunc