Repository: AlgebraicJulia/Catlab.jl
Pull request #616 (2022-04-14 06:29:01)

GAT for M-categories
This PR adds a GAT for [M-categories](https://ncatlab.org/nlab/show/M-category), a simple but underappreciated concept already used when distinguishing tight and loose acset transformations.

It has minor fixes/improvements to the `@present` macro encountered along the way.


Patch:
diff --git a/src/categorical_algebra/CSets.jl b/src/categorical_algebra/CSets.jl
index 9748bb7ed..881eb3f93 100644
--- a/src/categorical_algebra/CSets.jl
+++ b/src/categorical_algebra/CSets.jl
@@ -192,25 +192,24 @@ end
 """ Transformation between attributed C-sets.
 
 Homomorphisms of attributed C-sets generalize homomorphisms of C-sets
-([`CSetTransformation`](@ref)), which the user should understand before reading
+([`CSetTransformation`](@ref)), which you should understand before reading
 further.
 
-A homomorphism of attributed C-sets with schema S: C ↛ A (a profunctor) is a
+A *homomorphism* of attributed C-sets with schema S: C ↛ A (a profunctor) is a
 natural transformation between the corresponding functors col(S) → Set, where
 col(S) is the collage of S. When the components on attribute types, indexed by
 objects of A, are all identity functions, the morphism is called *tight*; in
-general, it is called *loose*. The terms "tight" and "loose" come from what the
-nLab calls an ["M-category"](https://ncatlab.org/nlab/show/M-category). The
-category of acsets on a fixed schema S is an M-category. Calling
+general, it is called *loose*. With this terminology, acsets on a fixed schema
+are the objects of an ℳ-category (see `Catlab.Theories.MCategory`). Calling
 `ACSetTransformation` will construct a tight or loose morphism as appropriate,
 depending on which components are specified.
 
 Since every tight morphism can be considered a loose one, the distinction
-between tight and loose may seem an unimportant technicality, but it can have
+between tight and loose may seem like a small technicality, but it has have
 important consequences because choosing one or the other greatly affects limits
-and colimits of acsets. In practice, the tight morphisms suffice for most
-purposes, including computing colimits. However, when computing limits of
-acsets, the loose morphism are usually preferable.
+and colimits of acsets. In practice, tight morphisms suffice for many purposes,
+including computing colimits. However, when computing limits of acsets, the
+loose morphism are usually preferable.
 """
 abstract type ACSetTransformation{S<:SchemaDescType,Comp,
                                   Dom<:StructACSet{S},Codom<:StructACSet{S}} end
diff --git a/src/core/Present.jl b/src/core/Present.jl
index 926f664d3..efc96b1db 100644
--- a/src/core/Present.jl
+++ b/src/core/Present.jl
@@ -9,7 +9,8 @@ in applications like knowledge representation.
 """
 module Present
 export @present, Presentation, generator, generators, generator_index,
-  has_generator, equations, add_generator!, add_generators!, add_definition!, add_equation!
+  has_generator, equations, add_generator!, add_generators!, add_definition!,
+  add_equation!
 
 using Base.Meta: ParseError
 using MLStyle: @match
@@ -116,26 +117,31 @@ function add_definition!(pres::Presentation, name::Symbol, rhs::GATExpr)
   generator
 end
 
-""" Get the index of a generator
+""" Get the index of a generator, relative to generators of same GAT type.
 """
-generator_index(pres::Presentation, x::Symbol) = pres.generator_name_index[x].second
+function generator_index(pres::Presentation{T,Name}, name::Name) where {T,Name}
+  last(pres.generator_name_index[name])
+end
+function generator_index(pres::Presentation, expr::GATExpr{:generator})
+  name = first(expr)
+  !isnothing(name) || error("Cannot lookup unnamed generator by name")
+  generator_index(pres, name)
+end
 
 """ Shorthand for contructing a term in the presentation
 """
-function make_term(pres::Presentation, e::Symbol)
-  pres[e]
-end
-function make_term(pres::Presentation, e::Expr)
-  @match e begin
+function make_term(pres::Presentation, expr)
+  @match expr begin
+    ::Symbol => pres[expr]
     Expr(:call, term_constructor, args...) =>
       invoke_term(pres.syntax, term_constructor,
-                  map(e -> make_term(pres, e), args)...)
+                  map(arg -> make_term(pres, arg), args)...)
   end
 end
 
 """ Create a new generator in a presentation of a given type
 """
-function make_generator(pres::Presentation, name::Symbol,
+function make_generator(pres::Presentation, name::Union{Symbol,Nothing},
                         type::Symbol, type_args::Vector)
   invoke_term(pres.syntax, type, name,
               map(e -> make_term(pres, e), type_args)...)
@@ -143,19 +149,17 @@ end
 
 """ Create and add a new generator
 """
-function construct_generator!(pres::Presentation, name::Symbol,
-                              type::Symbol, type_args::Vector=[]; idem=true)
-  if !(name ∈ keys(pres.generator_name_index)) || !idem
-    add_generator!(pres, make_generator(pres,name,type,type_args))
-  end
+function construct_generator!(pres::Presentation, name::Union{Symbol,Nothing},
+                              type::Symbol, type_args::Vector=[])
+  add_generator!(pres, make_generator(pres, name, type, type_args))
 end
 
 """ Create and add multiple generators
 """
-function construct_generators!(pres::Presentation, names::Vector,
-                               type::Symbol, type_args::Vector=[]; idem=true)
+function construct_generators!(pres::Presentation, names::AbstractVector,
+                               type::Symbol, type_args::Vector=[])
   for name in names
-    construct_generator!(pres, name, type, type_args, idem=idem)
+    construct_generator!(pres, name, type, type_args)
   end
 end
 
diff --git a/src/theories/Category.jl b/src/theories/Category.jl
index e379df11d..6dae40563 100644
--- a/src/theories/Category.jl
+++ b/src/theories/Category.jl
@@ -1,12 +1,11 @@
 export Category, FreeCategory, Ob, Hom, dom, codom, id, compose, ⋅,
   Copresheaf, FreeCopresheaf, El, ElExpr, ob, act,
   Presheaf, FreePresheaf, coact,
-  DisplayedCategory, Act, hom
+  DisplayedCategory, Act, hom,
+  MCategory, FreeMCategory, Tight, reflexive, transitive
 
 import Base: show
 
-abstract type ElExpr{T} <: GATExpr{T} end
-
 # Category
 ##########
 
@@ -100,6 +99,8 @@ Axiomatized as a covariant category action.
   act(x, id(A)) == x ⊣ (A::Ob, x::El(A))
 end
 
+abstract type ElExpr{T} <: GATExpr{T} end
+
 @syntax FreeCopresheaf{ObExpr,HomExpr,ElExpr} Copresheaf begin
   compose(f::Hom, g::Hom) = associate_unit(new(f,g; strict=true), id)
 end
@@ -175,3 +176,38 @@ Reference: Ahrens & Lumsdaine 2019, "Displayed categories", Definition 3.1.
   f̄ ⋅ id(y) == f̄ ⊣ (A::Ob, B::Ob, f::(A → B), x::El(A), y::El(B), f̄::Act(f,x,y))
   id(x) ⋅ f̄ == f̄ ⊣ (A::Ob, B::Ob, f::(A → B), x::El(A), y::El(B), f̄::Act(f,x,y))
 end
+
+# ℳ-category
+############
+
+""" Theory of an *ℳ-category*.
+
+The term "ℳ-category", used on the
+[nLab](https://ncatlab.org/nlab/show/M-category) is not very common, but the
+concept itself shows up commonly. An *ℳ-category* is a category with a
+distinguished wide subcategory, whose morphisms are suggestively called *tight*;
+for contrast, a generic morphism is called *loose*. Equivalently, an ℳ-category
+is a category enriched in the category ℳ of injections, the full subcategory of
+the arrow category of Set spanned by injections.
+
+In the following GAT, tightness is axiomatized as a property of morphisms: a
+dependent family of sets over the hom-sets, each having at most one inhabitant.
+"""
+@theory MCategory{Ob,Hom,Tight} <: Category{Ob,Hom} begin
+  Tight(hom::Hom(A,B))::TYPE ⊣ (A::Ob, B::Ob)
+
+  # Tightness is a property.
+  t == t′ ⊣ (A::Ob, B::Ob, f::Hom(A,B), t::Tight(f), t′::Tight(f))
+
+  # Tight morphisms form a subcategory.
+  reflexive(A::Ob)::Tight(id(A))
+  transitive(t::Tight(f), u::Tight(g))::Tight(compose(f,g)) ⊣
+    (A::Ob, B::Ob, C::Ob, f::Hom(A,B), g::Hom(B,C), t::Tight(f), u::Tight(g))
+end
+
+abstract type TightExpr{T} <: GATExpr{T} end
+
+@syntax FreeMCategory{ObExpr,HomExpr,TightExpr} MCategory begin
+  compose(f::Hom, g::Hom) = associate_unit(new(f,g; strict=true), id)
+  transitive(t::Tight, u::Tight) = associate_unit(new(t,u; strict=true), reflexive)
+end


Test patch:
diff --git a/test/core/Present.jl b/test/core/Present.jl
index 762545012..9e2706332 100644
--- a/test/core/Present.jl
+++ b/test/core/Present.jl
@@ -25,6 +25,8 @@ add_generator!(pres, B)
 @test_throws Exception add_generator!(pres, A)
 @test pres[:A] == A
 @test pres[[:A,:B]] == [A, B]
+@test generator_index(pres, :B) == 2
+@test generator_index(pres, B) == 2
 
 add_generators!(pres, (f,g))
 @test generators(pres) == [A, B, f, g]