Make pointed-set categories and schemas actually pointed

src/categorical_algebra/FinCats.jl

@@ -25,8 +25,8 @@
 using ACSets
 using ...GATs
 import ...GATs: equations
-using ...Theories: ThCategory, ThSchema, ThPointedSetCategory, ThPointedSetSchema,
-  ObExpr, HomExpr, AttrExpr, AttrTypeExpr, FreeSchema, FreePointedSetCategory, zeromap
+using ...Theories: ThCategory, ThSchema, ThPointedCategory, ThPointedSchema,
+  ObExpr, HomExpr, AttrExpr, AttrTypeExpr, FreeSchema, FreePointedCategory, zeromap
 import ...Theories: dom, codom, id, compose, ⋅, ∘
 using ...Graphs
 import ...Graphs: edges, src, tgt, enumerate_paths
@@ -312,11 +312,11 @@
   FinCatPresentation{ThSchema,Ob,Hom}(pres)
 end
 
-function FinCatPresentation(pres::Presentation{ThPointedSetSchema})
+function FinCatPresentation(pres::Presentation{ThPointedSchema})
   S = pres.syntax
   Ob = Union{S.Ob, S.AttrType}
   Hom = Union{S.Hom, S.Attr, S.AttrType}
-  FinCatPresentation{ThPointedSetSchema,Ob,Hom}(pres)
+  FinCatPresentation{ThPointedSchema,Ob,Hom}(pres)
 end
 """
 Computes the graph generating a finitely
@@ -328,12 +328,12 @@
 presentation(C::FinCatPresentation) = C.presentation
 
 ob_generators(C::FinCatPresentation) = generators(presentation(C), :Ob)
-ob_generators(C::Union{FinCatPresentation{ThSchema},FinCatPresentation{ThPointedSetSchema}}) = let P = presentation(C)
+ob_generators(C::Union{FinCatPresentation{ThSchema},FinCatPresentation{ThPointedSchema}}) = let P = presentation(C)
   vcat(generators(P, :Ob), generators(P, :AttrType))
 end
 
 hom_generators(C::FinCatPresentation) = generators(presentation(C), :Hom)
-hom_generators(C::Union{FinCatPresentation{ThSchema},FinCatPresentation{ThPointedSetSchema}}) = let P = presentation(C)
+hom_generators(C::Union{FinCatPresentation{ThSchema},FinCatPresentation{ThPointedSchema}}) = let P = presentation(C)
   vcat(generators(P, :Hom), generators(P, :Attr))
 end
 equations(C::FinCatPresentation) = equations(presentation(C))
@@ -348,7 +348,7 @@
 
 ob(C::FinCatPresentation, x::GATExpr) =
   gat_typeof(x) == :Ob ? x : error("Expression $x is not an object")
-ob(C::Union{FinCatPresentation{ThSchema},FinCatPresentation{ThPointedSetSchema}}, x::GATExpr) =
+ob(C::Union{FinCatPresentation{ThSchema},FinCatPresentation{ThPointedSchema}}, x::GATExpr) =
   gat_typeof(x) ∈ (:Ob, :AttrType) ? x :
     error("Expression $x is not an object or attribute type")
 
@@ -357,7 +357,7 @@
   mapreduce(f -> hom(C, f), compose, fs)
 hom(C::FinCatPresentation, f::GATExpr) =
   gat_typeof(f) == :Hom ? f : error("Expression $f is not a morphism")
-hom(::Union{FinCatPresentation{ThSchema},FinCatPresentation{ThPointedSetSchema}}, f::GATExpr) =
+hom(::Union{FinCatPresentation{ThSchema},FinCatPresentation{ThPointedSchema}}, f::GATExpr) =
   gat_typeof(f) ∈ (:Hom, :Attr, :AttrType) ? f :
     error("Expression $f is not a morphism or attribute")
 

src/theories/Category.jl

@@ -3,7 +3,7 @@ export ThCategory, FreeCategory, Ob, Hom, dom, codom, id, compose, ⋅,
   ThCopresheaf, FreeCopresheaf, El, ElExpr, ob, act,
   ThPresheaf, FreePresheaf, coact,
   ThMCategory, FreeMCategory, Tight, reflexive, transitive,
-  ThPointedSetCategory, FreePointedSetCategory, zeromap
+  ThPointedCategory, FreePointedCategory, zeromap, ZeroOb
 
 import Base: inv, show
 
@@ -200,21 +200,27 @@ abstract type TightExpr{T} <: GATExpr{T} end
 end
 
 """
-Theory of a pointed set-enriched category.
-We axiomatize a category equipped with zero morphisms.
+Theory of a pointed category.
+We axiomatize a category equipped with a zero object and zero morphisms.
+At the moment, the zero object is technically only required to be 
+a weak zero object; we don't ban nonzero maps to and from it.
 
 A functor from an ordinary category into a freely generated
-pointed-set enriched category, 
-equivalently, a pointed-set enriched category in which no two nonzero maps 
+pointed category, 
+equivalently, a pointed category in which no two nonzero maps 
 compose to a zero map, is a good notion
-of a functor that's total on objects and partial on morphisms.
+of a partial functor.
 """
-@theory ThPointedSetCategory{Ob,Hom} <: ThCategory{Ob,Hom} begin
+@theory ThPointedCategory{Ob,Hom} <: ThCategory{Ob,Hom} begin
+  ZeroOb()::Ob
   zeromap(A,B)::Hom(A,B)⊣(A::Ob,B::Ob)
   compose(zeromap(A,B),f::(B→C))==zeromap(A,C)⊣(A::Ob,B::Ob,C::Ob)
   compose(g::(A→B),zeromap(A,B))==zeromap(A,C)⊣(A::Ob,B::Ob,C::Ob)
+
+  #f == g ⊣ (A::Ob,f::Hom(A,ZeroOb()),g::Hom(A,ZeroOb()))
+  #f == g ⊣ (B::Ob,f::Hom(ZeroOb(),B),g::Hom(ZeroOb(),B))
 end
 
-@syntax FreePointedSetCategory{ObExpr,HomExpr} ThPointedSetCategory begin
+@syntax FreePointedCategory{ObExpr,HomExpr} ThPointedCategory begin
   compose(f::Hom,g::Hom) = associate_unit(normalize_zero(new(f,g; strict=true)), id)
 end

src/theories/Schema.jl

@@ -1,4 +1,4 @@
-export ThSchema, FreeSchema, AttrType, Attr, SchemaExpr, AttrTypeExpr, AttrExpr, ThPointedSetSchema, FreePointedSetSchema,zeromap
+export ThSchema, FreeSchema, AttrType, Attr, SchemaExpr, AttrTypeExpr, AttrExpr, ThPointedSchema, FreePointedSchema,zeromap, ZeroAttr
 
 # Schema
 
@@ -33,9 +33,14 @@ abstract type AttrExpr{T} <: SchemaExpr{T} end
   compose(f::Hom, x::Attr) = associate_unit(new(f,x; strict=true), id)
 end
 
-@theory ThPointedSetSchema{Ob,Hom,AttrType,Attr} <: ThPointedSetCategory{Ob,Hom} begin
+"""
+A pointed schema is a schema which is pointed on both sides.
+"""
+@theory ThPointedSchema{Ob,Hom,AttrType,Attr} <: ThPointedCategory{Ob,Hom} begin
   AttrType::TYPE
   Attr(dom::Ob,codom::AttrType)::TYPE
+
+  ZeroAttr()::AttrType
   zeromap(A::Ob,X::AttrType)::Attr(A,X)
 
   compose(f::Hom(A,B), g::Attr(B,X))::Attr(A,X) ⊣ (A::Ob, B::Ob, X::AttrType)
@@ -46,9 +51,10 @@ end
   (compose(f, compose(g, a)) == compose(compose(f, g), a)
     ⊣ (A::Ob, B::Ob, C::Ob, X::AttrType, f::Hom(A,B), g::Hom(B,C), a::Attr(C, X)))
   compose(id(A), a) == a ⊣ (A::Ob, X::AttrType, a::Attr(A,X))
+  #a == b ⊣(A::Ob,a::Attr(A,ZeroAttr()),b::Attr(A,ZeroAttr()))
 end
 
-@syntax FreePointedSetSchema{ObExpr,HomExpr,AttrTypeExpr,AttrExpr} ThPointedSetSchema begin
+@syntax FreePointedSchema{ObExpr,HomExpr,AttrTypeExpr,AttrExpr} ThPointedSchema begin
   compose(f::Hom,g::Hom) = associate_unit(normalize_zero(new(f,g; strict=true)), id)
   compose(f::Hom,a::Attr) = associate_unit(normalize_zero(new(f,a; strict=true)), id)
 end

test/theories/Category.jl

@@ -125,8 +125,13 @@ x = El(:x, A)
 # Pointed category
 ##################
 
-A,B,C,D = map(x->Ob(FreePointedSetCategory,x),[:A,:B,:C,:D])
+A,B,C,D = map(x->Ob(FreePointedCategory,x),[:A,:B,:C,:D])
+Z = ZeroOb(FreePointedCategory.Ob)
 f,g,h = Hom(:f,A,B),Hom(:g,B,C),Hom(:h,C,D)
 zAB,zBC,zAC = zeromap(A,B),zeromap(B,C),zeromap(A,C)
+k,l = Hom(:k,A,Z), Hom(:l,Z,A)
+zAZ,zZA = zeromap(A,Z),zeromap(Z,A)
 @test zAC == compose(f,zBC) == compose(zAB,g)
 @test compose(f,zBC,h) == zeromap(A,D)
+#@test k == zAZ
+#@test l == zZA

test/theories/Schema.jl

@@ -21,8 +21,8 @@ x, y = Attr(:x, A, C), Attr(:y, B, C)
 # Pointed schema
 ##################
 
-A,B,C = map(x->Ob(FreePointedSetSchema,x),[:A,:B,:C])
-X = AttrType(FreePointedSetSchema.AttrType,:X)
+A,B,C = map(x->Ob(FreePointedSchema,x),[:A,:B,:C])
+X = AttrType(FreePointedSchema.AttrType,:X)
 f,g = Hom(:f,A,B),Hom(:g,B,C)
 a = Attr(:a,C,X)
 zAB,zBC,zAC,zAX,zBX,zCX = zeromap(A,B),zeromap(B,C),zeromap(A,C),zeromap(A,X),zeromap(B,X),zeromap(C,X)