@theory ThCategory begin
@op begin
(→) := Hom
(⋅) := compose
end
Ob::TYPE
Hom(dom::Ob, codom::Ob)::TYPE
id(A::Ob)::(A → A)
compose(f::(A → B), g::(B → C))::(A → C) ⊣ [A::Ob, B::Ob, C::Ob]
(f ⋅ g) ⋅ h == f ⋅ (g ⋅ h) ⊣ [A::Ob, B::Ob, C::Ob, D::Ob,
f::(A → B), g::(B → C), h::(C → D)]
f ⋅ id(B) == f ⊣ [A::Ob, B::Ob, f::(A → B)]
id(A) ⋅ f == f ⊣ [A::Ob, B::Ob, f::(A → B)]
end
two type constructors, Ob (object) and Hom (morphism)
type Hom is a dependent type
depending on two objects, named dom (domain) and codom (codomain)
two term constructors, id (identity) and compose (composition).
return types depend on the argument values, eg id(A) has type Hom(A,A)
compose also uses context variables, listed to the right of the ⊣ symbol
@op call allows us to create method aliases that can then be used throughout the rest of the theory and outside of definition
result of the @theory macro: a module with the following members
for each declaration in the theory, a function named with the name of the declaration
declaration: includes term constructors, type constructors, arguments to type constructors (i.e. accessors like dom and codom), and aliases of the above)
in the above example, module ThCategory has functions Ob, Hom, dom, codom, compose, id, ⋅, →
a submodule called Meta with members
T: a zero-field struct that serves as a type-level signifier for the theory.
theory: a constant of type GAT which stores the data of the theory.
@theory: a macro which expands directly to theory, which is used to pass around the data of the theory at macro-expand time.
@present (Gatlab.models.Presentations.jl)
two methods for defining models of a GAT
as julia objects using @instance macro
useful for casting generic data structures, such as matrices, abstract tensor systems, and wiring diagrams, in categorical language
as syntactic objects using @present macro
define small categories by generators and relations
useful in applications like knowledge representation