Repository: AlgebraicJulia/Catlab.jl
Pull request #786 (2023-05-24 18:39:26)

Subobject classifier + Internal hom for C-Sets
Combines subacset search with computation of representables.

Tested on DDS (with equations to make the repr finite), Grph, and ReflGrph.

A change to SigmaMigration was needed because the previous implementation threw away the diagram map data (*how* the input CSet is related to the output CSet). Maybe should return a proper DiagramHom, but for now it's just the result ACSet + a dictionary of the diagram map components.

Shoutout to @KevinArlin for helping me work out where the homs go in the subobject classifier + internal hom constructions!


Patch:
diff --git a/Project.toml b/Project.toml
index b169dff70..d55337e41 100644
--- a/Project.toml
+++ b/Project.toml
@@ -2,7 +2,7 @@ name = "Catlab"
 uuid = "134e5e36-593f-5add-ad60-77f754baafbe"
 license = "MIT"
 authors = ["Evan Patterson <evan@epatters.org>"]
-version = "0.15.3"
+version = "0.15.2"
 
 [deps]
 ACSets = "227ef7b5-1206-438b-ac65-934d6da304b8"
@@ -44,7 +44,7 @@ CatlabSCSExt = "SCS"
 CatlabTikzPicturesExt = "TikzPictures"
 
 [compat]
-ACSets = "0.2.3"
+ACSets = "0.2.5"
 Colors = "0.12"
 CompTime = "0.1"
 Compose = "0.7, 0.8, 0.9"
diff --git a/src/categorical_algebra/CSets.jl b/src/categorical_algebra/CSets.jl
index 497026603..d66b67c59 100644
--- a/src/categorical_algebra/CSets.jl
+++ b/src/categorical_algebra/CSets.jl
@@ -36,6 +36,8 @@ using ..FinSets: VarFunction, LooseVarFunction, IdentityFunction, VarSet
 import ..Limits: limit, colimit, universal
 import ..Subobjects: Subobject, implies, ⟹, subtract, \, negate, ¬, non, ~
 import ..Sets: SetOb, SetFunction, TypeSet
+using ..Sets
+using ..Diagrams: Diagram, diagram
 import ..FinSets: FinSet, FinFunction, FinDomFunction, force, predicate, 
                   is_monic, is_epic, preimage
 import ..FinCats: FinDomFunctor, components, is_natural
@@ -197,14 +199,26 @@ const ACSetDomCat = FinCats.FinCatPresentation{
             TypeCat{Union{FinSet,VarSet},
                     Union{VarFunction,FinDomFunction{Int}}}}
   acset::ACS
+  # FIXME: The equations should not be here. They should be in the acset, which
+  # is not yet supported for struct acsets.
+  equations::Vector{Pair}
 end
-FinDomFunctor(X::ACSet) = ACSetFunctor(X)
+FinDomFunctor(X::ACSet; equations=Pair[]) = ACSetFunctor(X, equations)
+ACSet(X::ACSetFunctor) = X.acset
 
 hasvar(X::ACSet) = any(o->nparts(X,o) > 0, attrtypes(acset_schema(X)))
 hasvar(X::ACSetFunctor) = hasvar(X.acset)
 
-dom(F::ACSetFunctor) = FinCat(Presentation(F.acset))
-codom(F::ACSetFunctor) = hasvar(F) ? TypeCat{VarSet,VarFunction}() : TypeCat{SetOb,FinDomFunction{Int}}()
+function dom(F::ACSetFunctor)
+  pres = Presentation(F.acset)
+  add_equations!(pres, F.equations)
+  FinCat(pres)
+end
+
+function codom(F::ACSetFunctor)
+  hasvar(F) ? TypeCat{VarSet,VarFunction}() :
+    TypeCat{SetOb,FinDomFunction{Int}}()
+end
 
 Categories.do_ob_map(F::ACSetFunctor, x) = 
   (hasvar(F) ? VarSet : SetOb)(F.acset, functor_key(x))
@@ -215,7 +229,7 @@ functor_key(x) = x
 functor_key(expr::GATExpr{:generator}) = first(expr)
 
 # Set-valued FinDomFunctors as ACSets.
-
+(T::Type{ACS})(F::Diagram) where ACS <: ACSet = F |> diagram |> T
 function (::Type{ACS})(F::FinDomFunctor) where ACS <: ACSet
   X = if ACS isa UnionAll
     pres = presentation(dom(F))
@@ -1685,6 +1699,16 @@ function Base.push!(S::SubobjectIteratorState,h::ACSetTransformation)
   push!(S.seen, h); push!(S.to_recurse, h); push!(S.to_yield, h)
 end
 
+"""This would be much more efficient with canonical isomorph"""
+function is_seen(S::SubobjectIteratorState, f::ACSetTransformation)
+  for h in S.seen 
+    if any(σ -> force(σ⋅h) == force(f), isomorphisms(dom(f),dom(h)))
+      return true 
+    end
+  end
+  return false
+end
+
 """
 We recurse only if there is nothing to yield or we have something to recurse on 
 that is bigger than the biggest thing in our to-yield set.
@@ -1716,7 +1740,7 @@ function Base.iterate(Sub::SubobjectIterator, state=SubobjectIteratorState())
       rem = copy(dX)
       comps = delete_subobj!(rem, Dict([o => [p]]))
       h = ACSetTransformation(rem, dX; comps...) ⋅ X
-      if h ∉ state.seen
+      if !is_seen(state, h)
         push!(state, h)
       end
     end
diff --git a/src/categorical_algebra/CategoricalAlgebra.jl b/src/categorical_algebra/CategoricalAlgebra.jl
index 5af0e404b..72b5b7570 100644
--- a/src/categorical_algebra/CategoricalAlgebra.jl
+++ b/src/categorical_algebra/CategoricalAlgebra.jl
@@ -12,9 +12,9 @@ include("FinSets.jl")
 include("Permutations.jl")
 include("Matrices.jl")
 include("FinRelations.jl")
+include("Diagrams.jl")
 include("CSets.jl")
 include("GraphCategories.jl")
-include("Diagrams.jl")
 include("CommutativeDiagrams.jl")
 include("CatElements.jl")
 include("Chase.jl")
diff --git a/src/categorical_algebra/DataMigrations.jl b/src/categorical_algebra/DataMigrations.jl
index 51576ee59..268345e1e 100644
--- a/src/categorical_algebra/DataMigrations.jl
+++ b/src/categorical_algebra/DataMigrations.jl
@@ -1,13 +1,15 @@
 """ Functorial data migration for attributed C-sets.
 """
 module DataMigrations
-export DataMigration, SigmaMigration, DeltaMigration, SigmaMigrationFunctor, 
-  DeltaMigrationFunctor, DataMigrationFunctor, functor, migrate, migrate!,  representable, yoneda, colimit_representables
+export DataMigration, SigmaMigration, DeltaMigration, migrate, migrate!,
+  representable, yoneda, colimit_representables, subobject_classifier, 
+  internal_hom, SigmaMigrationFunctor, DeltaMigrationFunctor, 
+  DataMigrationFunctor, functor
 
 using ACSets
 using ACSets.DenseACSets: constructor, datatypes
 using ...GATs
-using ...Theories: ob, hom, dom, codom, attr, AttrTypeExpr
+using ...Theories: ob, hom, dom, codom, attr, AttrTypeExpr, ⋅
 using ..Categories, ..FinCats, ..Limits, ..Diagrams, ..FinSets, ..CSets
 using ...Graphs, ..FreeDiagrams
 import ..Categories: ob_map, hom_map
@@ -279,6 +281,7 @@ const GlucMigrationFunctor{Dom,Codom} = DataMigrationFunctor{Dom,Codom,<:GlucSch
 
 # Sigma migration
 #################
+
 struct SigmaMigrationFunctor{Dom,Codom,M<:SigmaSchemaMigration} <: AbstractMigrationFunctor{Dom,Codom}
   migration::M
   dom_constructor
@@ -292,14 +295,18 @@ functor(F::SigmaMigrationFunctor) = functor(migration(F))
 SigmaMigrationFunctor(f,::Type{T},c::ACSet) where T<:StructACSet = SigmaMigrationFunctor(f,T(),constructor(c))
 SigmaMigrationFunctor(f,d::ACSet,::Type{T}) where T<:StructACSet = SigmaMigrationFunctor(f,d,T())
 SigmaMigrationFunctor(f,d::Type{T′},::Type{T}) where {T<:StructACSet, T′<:StructACSet} = SigmaMigrationFunctor(f,d,T())
+
 """
 Create a C-Set for the collage of the functor. Initialize data in the domain 
 portion of the collage, then run the chase.
+
+When `return_unit` is true, returns the diagram morphism given by the unit of
+the adjunction between Σ and Δ migration functors.
 """
 #This should be deprecated in terms of a new migrate function if anybody works on sigma migrations sometime.
 #Also, we probably don't want to construct the collage every time we migrate using M, at least it should
 #be possible to cache.
-function (M::SigmaMigrationFunctor)(d::ACSet; n=100)
+function (M::SigmaMigrationFunctor)(d::ACSet; n=100, return_unit::Bool=false)
   D,CD = M.dom_constructor(), M.codom_constructor()
   F = functor(M)
   S = acset_schema(d)
@@ -313,9 +320,8 @@ function (M::SigmaMigrationFunctor)(d::ACSet; n=100)
   for (k,v) in datatypes(D)  atypes[Symbol(ob_map(i1,k))] = v end
   for (k,v) in datatypes(CD) atypes[Symbol(ob_map(i2,k))] = v end
   col_type = crel_type(presentation(apex(col)); types=atypes, name="Sigma")()
-  for o in ob(S)
+  for o in types(S)
     add_parts!(col_type, Symbol(ob_map(i1,o)), nparts(d,o))
-    #add parts for attrvars?
   end
   for h in arrows(S; just_names=true)
     s,t = add_srctgt(hom_map(i1,h))
@@ -340,7 +346,7 @@ function (M::SigmaMigrationFunctor)(d::ACSet; n=100)
       res[domval,h] = codomval
     end
   end
-  #Go back and make sure attributes that ought to have 
+  #Go back and make sure attributes that ought to have
   #specific values because of d do have those values.
   for (k,kdom,kcod) in attrs(S)
     f = hom_map(F,k)
@@ -363,13 +369,27 @@ function (M::SigmaMigrationFunctor)(d::ACSet; n=100)
       res[f1j,nameof(f2)] = oldval
     end
   end
-  return res
-end 
+  rem_free_vars!(res)
+  return_unit || return res
+
+  # Return result as DiagramHom{id}.
+  diagram_map = Dict(map(types(S)) do o
+    s, t= add_srctgt("α_$o")
+    m = last.(sort(collect(zip([rel_res[x] for x in [s,t]]...))))
+    ff = o ∈ ob(S) ? FinFunction : VarFunction{attrtype_type(D,o)}
+    o => ff(m, nparts(rel_res, nameof(ob_map(functor(M)⋅i2,o))))
+  end)
+  ddom = FinDomFunctor(d; equations=equations(dom(functor(M))))
+  dcodom = FinDomFunctor(res; equations=equations(codom(functor(M))))
+  DiagramHom{id}(functor(M), diagram_map, ddom, dcodom)
+end
+
 """
 Split an n-fold composite (n may be 1) 
 Hom or Attr into its left n-1 and rightmost 1 components
 """
-split_r(f) = head(f) == :compose ? (compose(args(f)[1:end-1]),last(f)) : (id(dom(f)),f)
+split_r(f) = head(f) == :compose ?
+  (compose(args(f)[1:end-1]),last(f)) : (id(dom(f)),f)
 
 # Yoneda embedding
 #-----------------
@@ -386,13 +406,19 @@ which works because left Kan extensions take representables to representables
 representables (they can be infinite), this function thus inherits any
 limitations of our implementation of left pushforward data migrations.
 """
-function representable(T, C::Presentation{ThSchema}, ob::Symbol)
+function representable(T, C::Presentation{ThSchema}, ob::Symbol;
+                       return_unit_id::Bool=false)
   C₀ = Presentation{Symbol}(FreeSchema)
   add_generator!(C₀, C[ob])
   X = AnonACSet(C₀); add_part!(X, ob)
   F = FinFunctor(Dict(ob => ob), Dict(), C₀, C)
   ΣF = SigmaMigrationFunctor(F, X, T)
-  return ΣF(X)
+  if return_unit_id
+    η = ΣF(X; return_unit=true)
+    (ACSet(diagram(codom(η))), only(collect(diagram_map(η)[ob])))
+  else
+    ΣF(X)
+  end
 end
 
 """
@@ -400,38 +426,116 @@ ACSet types do not store info about equations, so this info is lost when we try
 to recover the presentation from the datatype. Thus, this method for 
 `representable` should only be used for free schemas
 """ 
-representable(::Type{T}, ob::Symbol) where T <: StructACSet =
-  representable(T, Presentation(T), ob)
+representable(::Type{T}, ob::Symbol; kw...) where T <: StructACSet =
+  representable(T, Presentation(T), ob; kw...)
 
-""" Yoneda embedding of category C in category of C-sets.
 
-Because Catlab privileges copresheaves (C-sets) over presheaves, this is the
-*contravariant* Yoneda embedding, i.e., the embedding C^op → C-Set.
+"""
+The subobject classifier Ω in a presheaf topos is the presheaf that sends each 
+object A to the set of sieves on it (equivalently, the set of subobjects of the 
+representable presheaf for A). Counting subobjects gives us the *number* of A 
+parts; the hom data for f:A->B for subobject Aᵢ is determined via:
+
+Aᵢ ↪ A 
+↑    ↑ f*  
+PB⌝↪ B          (PB picks out a subobject of B, up to isomorphism.)
 
-If representables have already been computed (which can be expensive) they can
-be provided via the `cache` keyword argument.
+(where A and B are the representables for objects A and B and f* is the unique 
+map from B into the A which sends the point of B to f applied to the point of A)
 
-Input `cons` is a constructor for the ACSet
+Returns the classifier as well as a dictionary of subobjects corresponding to 
+the parts of the classifier.
+"""
+function subobject_classifier(T::Type, S::Presentation{ThSchema}; kw...)
+  isempty(generators(S, :AttrType)) ||
+    error("Cannot compute Ω for schema with attributes")
+  y = yoneda(T, S; kw...)
+  obs = nameof.(generators(S, :Ob))
+  subobs = Dict(ob => subobject_graph(ob_map(y, ob))[2] for ob in obs)
+  Ω = T()
+  for ob in obs
+    add_parts!(Ω, ob, length(subobs[ob]))
+  end
+  for (f, a, b) in homs(acset_schema(Ω))
+    BA = hom_map(y, f)
+    Ω[f] = map(parts(Ω, a)) do pᵢ
+      Aᵢ = hom(subobs[a][pᵢ])
+      _, PB = force.(pullback(Aᵢ, BA))
+      return only(filter(parts(Ω, b)) do pⱼ
+        Bⱼ = hom(subobs[b][pⱼ])
+        any(σ ->  force(σ ⋅ Bⱼ) == PB, isomorphisms(dom(PB),dom(Bⱼ)))
+      end)
+    end
+  end
+  return Ω, subobs
+end
+
+"""
+Objects: Fᴳ(c) = C-Set(C × G, F)    where C is the representable c
+
+Given a map f: a->b, we compute that f(Aᵢ) = Bⱼ by constructing the following:
+          Aᵢ
+    A × G → F
+  f*↑ ↑ ↑ ↗ Bⱼ       find the hom Bⱼ that makes this commute
+    B × G 
+
+where f* is given by `yoneda`.
+"""
+function internal_hom(G::T, F::T, S::Presentation{ThSchema}; kw...) where T<:ACSet
+  y = yoneda(T, S; kw...)
+  obs = nameof.(generators(S, :Ob))
+  prods = Dict(ob => product(ob_map(y, ob),G) for ob in obs)
+  maps = Dict(ob => homomorphisms(apex(prods[ob]),F) for ob in obs)
+  Fᴳ = T()
+  for ob in obs
+    add_parts!(Fᴳ, ob, length(maps[ob]))
+  end
+  for (f, a, b) in homs(acset_schema(G))
+    BA = hom_map(y, f)
+    π₁, π₂ = prods[b]
+    Fᴳ[f] = map(parts(Fᴳ, a)) do pᵢ
+      composite = force(universal(prods[a], Span(π₁⋅BA, π₂)) ⋅ maps[a][pᵢ])
+      findfirst(==(composite), maps[b])
+    end
+  end
+  return Fᴳ, homs
+end
+
+""" Compute the Yoneda embedding of a category C in the category of C-sets.
+
+Because Catlab privileges copresheaves (C-sets) over presheaves, this is the
+*contravariant* Yoneda embedding, i.e., the embedding functor C^op → C-Set.
+
+The first argument `cons` is a constructor for the ACSet, such as a struct acset
+type. If representables have already been computed (which can be expensive),
+they can be supplied via the `cache` keyword argument.
 
 Returns a `FinDomFunctor` with domain `op(C)`.
 """
-function yoneda(cons, C::Presentation{ThSchema}; cache=nothing)
-  cache = isnothing(cache) ? Dict() : cache
-  y_ob = Dict(map(nameof.(generators(C, :Ob))) do c 
-    @debug "Computing representable $c"
-    c => haskey(cache, c) ? cache[c] : representable(cons, C, c)
-  end)
-  y_ob = merge(y_ob, Dict(map(nameof.(generators(C,:AttrType))) do c 
+function yoneda(cons, C::Presentation{ThSchema};
+                cache::AbstractDict=Dict{Symbol,Any}())
+  # Compute any representables that have not already been computed.
+  for c in nameof.(generators(C, :Ob))
+    haskey(cache, c) && continue
+    cache[c] = representable(cons, C, c, return_unit_id=true)
+  end
+  for c in nameof.(generators(C, :AttrType))
+    haskey(cache, c) && continue
     rep = cons()
-    add_part!(rep, c)
-    c => rep
-  end))
+    cache[c] = (rep, add_part!(rep, c))
+  end
+
+  # Object map of Yoneda embedding.
+  y_ob = Dict(c => yc for (c, (yc, _)) in pairs(cache))
+
+  # Morphism map of Yoneda embedding.
   y_hom = Dict(Iterators.map(generators(C, :Hom) ∪ generators(C, :Attr)) do f
-    c, d = nameof.([dom(f), codom(f)])
-    yc, yd = y_ob[c], y_ob[d]
-    initial = Dict(d => Dict(1 => yc[1,f]))
+    c, d = nameof(dom(f)), nameof(codom(f))
+    (yc, rootc), (yd, rootd) = cache[c], cache[d]
+    initial = Dict(d => Dict(rootd => yc[rootc,f]))
     f => homomorphism(yd, yc, initial=initial) # Unique homomorphism.
   end)
+
   FinDomFunctor(y_ob, y_hom, op(FinCat(C)))
 end
 yoneda(::Type{T}; kw...) where T <: StructACSet = yoneda(T, Presentation(T); kw...)
diff --git a/src/categorical_algebra/Diagrams.jl b/src/categorical_algebra/Diagrams.jl
index d8e043c69..e46ba55f6 100644
--- a/src/categorical_algebra/Diagrams.jl
+++ b/src/categorical_algebra/Diagrams.jl
@@ -105,9 +105,9 @@ type `DiagramHom{id}` and `DiagramHom{op}` induce morphisms between colimits and
 between limits of the diagrams, respectively, whereas morphisms of type
 `DiagramHom{co}` generalize morphisms of polynomial functors.
 """
-struct DiagramHom{T,C<:Cat,F<:FinFunctor,Φ<:FinTransformation,D<:Functor{<:FinCat,C}}
+struct DiagramHom{T,C<:Cat,F<:FinFunctor,Φ,D<:Functor{<:FinCat,C}}
   shape_map::F
-  diagram_map::Φ
+  diagram_map::Φ # bug: Φ should be type constrained to be a FinTransformation  
   precomposed_diagram::D
 end
 DiagramHom{T}(shape_map::F, diagram_map::Φ, precomposed_diagram::D) where
diff --git a/src/categorical_algebra/FinSets.jl b/src/categorical_algebra/FinSets.jl
index 8a958879f..9c46957e5 100644
--- a/src/categorical_algebra/FinSets.jl
+++ b/src/categorical_algebra/FinSets.jl
@@ -327,6 +327,9 @@ symbolic attributes. (Likewise, AttrVars will have to wrap Any rather than Int)
 end
 VarFunction(f::AbstractVector{Int},cod::Int) = VarFunction(FinFunction(f,cod))
 VarFunction(f::FinDomFunction) = VarFunction{Union{}}(AttrVar.(collect(f)),codom(f))
+FinFunction(f::VarFunction{T}) where T = FinFunction(
+  [f.fun(i) isa AttrVar ? f.fun(i).val : error("Cannot cast to FinFunction") 
+   for i in dom(f)], f.codom)
 Base.length(f::AbsVarFunction{T}) where T = length(collect(f.fun))
 Base.collect(f::AbsVarFunction{T}) where T = collect(f.fun)
 (f::VarFunction{T})(v::T) where T = v 
diff --git a/src/gats/Presentations.jl b/src/gats/Presentations.jl
index e3efb8c5f..92c433535 100644
--- a/src/gats/Presentations.jl
+++ b/src/gats/Presentations.jl
@@ -10,7 +10,7 @@ in applications like knowledge representation.
 module Presentations
 export @present, Presentation, generator, generators, generator_index,
   has_generator, equations, add_generator!, add_generators!, add_definition!,
-  add_equation!
+  add_equation!, add_equations!
 
 using Base.Meta: ParseError
 using MLStyle: @match
@@ -104,9 +104,12 @@ equations(pres::Presentation) = pres.equations
 
 """ Add an equation between terms to a presentation.
 """
-function add_equation!(pres::Presentation, lhs::GATExpr, rhs::GATExpr)
+add_equation!(pres::Presentation, lhs::GATExpr, rhs::GATExpr) =
   push!(pres.equations, lhs => rhs)
-end
+
+""" Add sequence of equations to a presentation.
+"""
+add_equations!(pres::Presentation, eqs) = append!(pres.equations, eqs)
 
 """ Add a generator defined by an equation.
 """


Test patch:
diff --git a/test/categorical_algebra/DataMigrations.jl b/test/categorical_algebra/DataMigrations.jl
index 7d3228366..3d392cdc8 100644
--- a/test/categorical_algebra/DataMigrations.jl
+++ b/test/categorical_algebra/DataMigrations.jl
@@ -73,11 +73,7 @@ F = FinFunctor(
 ΔF = DataMigrationFunctor(F, LabeledDDS{Int}, WeightedGraph{Int})
 @test wg == ΔF(ldds)
 
-idF = FinFunctor(
-  Dict(X => X, Label => Label), 
-  Dict(ϕ => ϕ, label => label), 
-  SchLabeledDDS, SchLabeledDDS
-)
+idF = id(FinCat(SchLabeledDDS))
 @test ldds == migrate(LabeledDDS{Int}, ldds, DataMigration(idF))
 
 # Conjunctive migration
@@ -296,12 +292,7 @@ F = FinFunctor(
   Dict(srcB => srcG, tgtB => tgtG),
   SchUndirectedBipartiteGraph, SchGraph
 )
-
-idF = FinFunctor(
-  Dict(VG => VG, EG => EG),
-  Dict(srcG => srcG, tgtG => tgtG),
-  SchGraph, SchGraph
-)
+idF = id(FinCat(SchGraph))
 
 ΣF = SigmaMigrationFunctor(F, UndirectedBipartiteGraph, Graph)
 X = UndirectedBipartiteGraph()
@@ -318,21 +309,34 @@ X = @acset UndirectedBipartiteGraph begin
   tgt = [1,1,2,3]
 end
 
-Y = ΣF(X)
+Yd = ΣF(X; return_unit=true)
+Y = Graph(codom(Yd))
+α = diagram_map(Yd)
 @test nparts(Y, :V) == 7
 @test nparts(Y, :E) == 4
 @test length(Y[:src] ∩ Y[:tgt]) == 0
+@test isempty(collect(α[:V₁]) ∩ collect(α[:V₂]))
 
 @test SigmaMigrationFunctor(idF, Graph, Graph)(Y) == Y
 
-###Test sigma migrations with attributes
+# Sigma migrations with attributes
+#---------------------------------
+
+# Identity migration on weighted graphs.
+Y = @acset WeightedGraph{Symbol} begin
+  V=2; E=2; Weight=1; src=1; tgt=[1,2]; weight=[AttrVar(1), :X]
+end
+ΣF = SigmaMigrationFunctor(id(FinCat(SchWeightedGraph)),
+                           WeightedGraph{Symbol}, WeightedGraph{Symbol})
+@test is_isomorphic(ΣF(Y),Y)
+
+# Less trivial example.
 @present SchTwoThings(FreeSchema) begin
   Th1::Ob
   Th2::Ob
   Property::AttrType
-  #ID is to keep track of combinatorial objects
-  #as their non-meaningful integer IDs may be modified
-  #by the chase.
+  # The ID attribute keeps track of combinatorial objects as their
+  # non-meaningful integer IDs may be modified by the chase.
   ID::AttrType
   f::Hom(Th1,Th2)
   id::Attr(Th1,ID)
@@ -379,6 +383,7 @@ YY = ΔF(X)
 XX = ΣF(Y)
 @test YY == Y
 @test incident(XX,false,[:f,:prop]) == incident(XX,"ffee cup",:id)
+
 # Terminal map
 #-------------
 @present ThSpan(FreeSchema) begin
@@ -412,21 +417,23 @@ bang = FinFunctor(
 )
 
 Σbang = SigmaMigrationFunctor(bang, Span, Initial)
-Y = Σbang(X)
-
+Yd = Σbang(X; return_unit=true)
+α = diagram_map(Yd)
+@test length(unique([α[:A](1:2)...,α[:L1](1),α[:L2](1:2)...])) == 1
+Y = Initial(codom(Yd))
 @test nparts(Y, :I) == 4
 
 # Map from terminal C 
 #--------------------
 
-vertex = FinFunctor(Dict(I => VG), Dict(), ThInitial, SchGraph)
-edge = FinFunctor(Dict(I => EG), Dict(), ThInitial, SchGraph)
+V = FinFunctor(Dict(I => VG), Dict(), ThInitial, SchGraph)
+E = FinFunctor(Dict(I => EG), Dict(), ThInitial, SchGraph)
 
-Z = SigmaMigrationFunctor(vertex, Initial, Graph)(Y)
+Z = SigmaMigrationFunctor(V, Initial, Graph)(Y)
 @test nparts(Z, :V) == 4
 @test nparts(Z, :E) == 0
 
-Z = SigmaMigrationFunctor(edge, Initial, Graph)(Y)
+Z = SigmaMigrationFunctor(E, Initial, Graph)(Y)
 expected = foldl(⊕,fill(path_graph(Graph,2), 4))  
 @test is_isomorphic(Z,expected)
 
@@ -442,7 +449,7 @@ G = path_graph(Graph,3)
 expected = @acset ReflexiveGraph  begin 
   V=3; E=5; refl=1:3; src=[1,2,3,1,2]; tgt=[1,2,3,2,3] 
 end 
-@test is_isomorphic(Σ(G),expected)
+@test is_isomorphic(Σ(G), expected)
 
 # Sigma with attributes 
 #----------------------
@@ -464,7 +471,7 @@ expected = @acset WG{Float64} begin
 end
 
 @test is_isomorphic(Σ(G), expected)
-
+ 
 # Yoneda embedding
 #-----------------
 
@@ -476,7 +483,8 @@ yV, yE = Graph(1), @acset(Graph, begin V=2;E=1;src=2;tgt=1 end)
 y_Graph = yoneda(Graph)
 @test ob_map(y_Graph, :V) == yV
 @test is_isomorphic(ob_map(y_Graph, :E), yE)
-@test Set(hom_map.(Ref(y_Graph), [:src,:tgt])) == Set(homomorphisms(yV, representable(Graph, :E)))
+@test Set(hom_map.(Ref(y_Graph), [:src,:tgt])) == Set(
+  homomorphisms(yV, representable(Graph, :E)))
 
 F = @migration SchGraph begin
   X => E
@@ -507,13 +515,14 @@ i, o = hom_map(G, :i), hom_map(G, :o)
 @test isempty(outneighbors(X, only(collect(o[:V]))))
 
 # Yoneda embedding for weights graphs (has attributes).
-yV, yE = WeightedGraph{Float64}(1), @acset(WeightedGraph{Float64}, begin 
+WGF = WeightedGraph{Float64}
+yV, yE = WGF(1), @acset(WGF, begin 
   V=2;E=1;Weight=1;src=2;tgt=1; weight=[AttrVar(1)]
 end)
-@test representable(WeightedGraph{Float64}, SchWeightedGraph, :V) == yV
-@test is_isomorphic(representable(WeightedGraph{Float64}, SchWeightedGraph, :E), yE)
+@test representable(WGF, SchWeightedGraph, :V) == yV
+@test is_isomorphic(representable(WGF, SchWeightedGraph, :E), yE)
 
-yWG = yoneda(WeightedGraph{Float64})
+yWG = yoneda(WGF)
 
 F = @migration SchWeightedGraph begin
   X => E
@@ -545,4 +554,43 @@ expected = @acset WeightedGraph{Float64} begin
 end
 @test is_isomorphic(ob_map(colimit_representables(d, yWG), :I), expected)
 
+
+# Subobject classifier
+######################
+# Graph and ReflGraph have 'same' subobject classifier
+ΩG,_ = subobject_classifier(Graph, SchGraph)
+ΩrG,_ = subobject_classifier(ReflexiveGraph, SchReflexiveGraph)
+F = FinFunctor(Dict(:V=>:V, :E=>:E), Dict(:src=>:src, :tgt=>:tgt), 
+               SchGraph, SchReflexiveGraph)
+ΔF = DataMigrationFunctor(F, ReflexiveGraph, Graph)
+@test is_isomorphic(ΩG, ΔF(ΩrG))
+
+# Searching for maps into the subobject classifier is much faster than 
+# enumerating them via `subobject_graph`
+G = (star_graph(Graph, 2)⊗path_graph(Graph, 3))
+@test length(homomorphisms(G, ΩG)) == length(subobject_graph(G)[2])
+
+@present SchDDS42(FreeSchema) begin
+  X::Ob
+  Φ::Hom(X,X)
+  Φ⋅Φ⋅Φ⋅Φ == Φ⋅Φ
 end
+@acset_type DDS42(SchDDS42, index=[:Φ])
+ΩDDs, _ = subobject_classifier(DDS42, SchDDS42)
+@test is_isomorphic(ΩDDs, @acset DDS42 begin X=4; Φ=[1,3,4,4] end)
+
+# Internal Hom
+##############
+G = ReflexiveGraph(2)
+F = path_graph(ReflexiveGraph, 2)
+Fᴳ,_ = internal_hom(G,F, SchReflexiveGraph)
+Z = apex(terminal(ReflexiveGraph)) ⊕ path_graph(ReflexiveGraph, 3)
+@test length(homomorphisms(Z, Fᴳ)) == length(homomorphisms(Z ⊗ G, F)) # 64
+
+G = @acset DDS42 begin X=3; Φ=[2,3,3] end
+F = @acset DDS42 begin X=4; Φ=[2,2,4,4] end
+Fᴳ,_ = internal_hom(G,F, SchDDS42)
+Z = @acset DDS42 begin X=5; Φ=[2,3,4,3,4] end
+@test length(homomorphisms(Z, Fᴳ)) == length(homomorphisms(Z ⊗ G, F)) # 1024
+
+end # module
diff --git a/test/gats/Presentations.jl b/test/gats/Presentations.jl
index 094a7e32f..9c04890f0 100644
--- a/test/gats/Presentations.jl
+++ b/test/gats/Presentations.jl
@@ -9,8 +9,7 @@ presentation_theory(::Presentation{Theory}) where Theory = Theory
 ##############
 
 A, B, C = Ob(FreeCategory, :A, :B, :C)
-f = Hom(:f, A, B)
-g = Hom(:g, B, C)
+f, g, h = Hom(:f, A, B), Hom(:g, B, C), Hom(:h, A, C)
 
 # Generators
 pres = Presentation(FreeCategory)
@@ -35,6 +34,15 @@ add_generators!(pres, (f,g))
 @test generators(pres, FreeCategory.Ob) == [A, B]
 @test generators(pres, FreeCategory.Hom) == [f, g]
 
+# Equations
+add_equation!(pres, compose(f,g), h)
+@test length(equations(pres)) == 1
+
+f′, g′ = Hom(:f′, A, B), Hom(:g′, B, C)
+add_generators!(pres, [f′, g′])
+add_equations!(pres, [f => f′, g => g′])
+@test length(equations(pres)) == 3
+
 # Presentation macro
 ####################