Browse Source

ENH: Enforce unitality of composition in default syntax systems.

pull/424/head
Evan Patterson 6 months ago
parent
commit
4176bf3343
  1. 2
      experiments/CompAlgebra/src/AlgebraicNets.jl
  2. 2
      experiments/Markov/src/MarkovCategories.jl
  3. 6
      src/theories/Category.jl
  4. 20
      src/theories/HigherCategory.jl
  5. 22
      src/theories/Monoidal.jl
  6. 4
      src/theories/MonoidalAdditive.jl
  7. 4
      src/theories/Preorders.jl
  8. 4
      src/theories/Relations.jl
  9. 4
      test/theories/Category.jl

2
experiments/CompAlgebra/src/AlgebraicNets.jl

@ -40,7 +40,7 @@ end
@syntax AlgebraicNet{ObExpr,HomExpr} AlgebraicNetTheory begin
# FIXME: `compose` and `otimes` should delegate to wiring layer when possible.
compose(f::Hom, g::Hom) = associate(new(f,g; strict=true))
compose(f::Hom, g::Hom) = associate_unit(new(f,g; strict=true), id)
otimes(A::Ob, B::Ob) = associate_unit(new(A,B), munit)
otimes(f::Hom, g::Hom) = associate(new(f,g))

2
experiments/Markov/src/MarkovCategories.jl

@ -21,7 +21,7 @@ end
@syntax FreeMarkovCategory{ObExpr,HomExpr} MarkovCategory begin
otimes(A::Ob, B::Ob) = associate_unit(new(A,B), munit)
otimes(f::Hom, g::Hom) = associate(new(f,g))
compose(f::Hom, g::Hom) = associate(new(f,g; strict=true))
compose(f::Hom, g::Hom) = associate_unit(new(f,g; strict=true), id)
end
function show_latex(io::IO, expr::HomExpr{:expectation}; kw...)

6
src/theories/Category.jl

@ -48,7 +48,7 @@ compose(fs::Vector) = foldl(compose, fs)
compose(f, g, h, fs...) = compose([f, g, h, fs...])
@syntax FreeCategory{ObExpr,HomExpr} Category begin
compose(f::Hom, g::Hom) = associate(new(f,g; strict=true))
compose(f::Hom, g::Hom) = associate_unit(new(f,g; strict=true), id)
end
function show_unicode(io::IO, expr::HomExpr{:compose}; kw...)
@ -101,7 +101,7 @@ Axiomatized as a covariant category action.
end
@syntax FreeCopresheaf{ObExpr,HomExpr,ElExpr} Copresheaf begin
compose(f::Hom, g::Hom) = associate(new(f,g; strict=true))
compose(f::Hom, g::Hom) = associate_unit(new(f,g; strict=true), id)
end
""" Theory of *presheaves*.
@ -123,7 +123,7 @@ Axiomatized as a contravariant category action.
end
@syntax FreePresheaf{ObExpr,HomExpr,ElExpr} Presheaf begin
compose(f::Hom, g::Hom) = associate(new(f,g; strict=true))
compose(f::Hom, g::Hom) = associate_unit(new(f,g; strict=true), id)
end
function show(io::IO, ::MIME"text/plain", expr::ElExpr)

20
src/theories/HigherCategory.jl

@ -40,8 +40,8 @@ composeH(α, β, γ, αs...) = composeH([α, β, γ, αs...])
Checks domains of morphisms but not 2-morphisms.
"""
@syntax FreeCategory2{ObExpr,HomExpr,Hom2Expr} Category2 begin
compose(f::Hom, g::Hom) = associate(new(f,g; strict=true))
compose(α::Hom2, β::Hom2) = associate(new(α,β))
compose(f::Hom, g::Hom) = associate_unit(new(f,g; strict=true), id)
compose(α::Hom2, β::Hom2) = associate_unit(new(α,β), id)
composeH(α::Hom2, β::Hom2) = associate(new(α,β))
end
@ -127,10 +127,10 @@ composeV(α, β, γ, αs...) = composeV([α, β, γ, αs...])
Checks domains of morphisms but not 2-morphisms.
"""
@syntax FreeDoubleCategory{ObExpr,HomVExpr,HomHExpr,Hom2Expr} DoubleCategory begin
compose(f::HomV, g::HomV) = associate(new(f,g; strict=true))
compose(f::HomH, g::HomH) = associate(new(f,g; strict=true))
composeH(α::Hom2, β::Hom2) = associate(new(α,β))
composeV(α::Hom2, β::Hom2) = associate(new(α,β))
composeV(f::HomV, g::HomV) = associate_unit(new(f,g; strict=true), idV)
composeH(f::HomH, g::HomH) = associate_unit(new(f,g; strict=true), idH)
composeV(α::Hom2, β::Hom2) = associate_unit(new(α,β), id2V)
composeH(α::Hom2, β::Hom2) = associate_unit(new(α,β), id2H)
end
function show_unicode(io::IO, expr::Hom2Expr{:composeV}; kw...)
@ -270,10 +270,10 @@ end
otimes(f::HomV, g::HomV) = associate(new(f,g))
otimes(f::HomH, g::HomH) = associate(new(f,g))
otimes(f::Hom2, g::Hom2) = associate(new(f,g))
compose(f::HomV, g::HomV) = associate(new(f,g; strict=true))
compose(f::HomH, g::HomH) = associate(new(f,g; strict=true))
composeH(α::Hom2, β::Hom2) = associate(new(α,β))
composeV(α::Hom2, β::Hom2) = associate(new(α,β))
composeV(f::HomV, g::HomV) = associate_unit(new(f,g; strict=true), idV)
composeH(f::HomH, g::HomH) = associate_unit(new(f,g; strict=true), idH)
composeV(α::Hom2, β::Hom2) = associate_unit(new(α,β), id2V)
composeH(α::Hom2, β::Hom2) = associate_unit(new(α,β), id2H)
end
function show_unicode(io::IO, expr::HomVExpr{:braidV}; kw...)

22
src/theories/Monoidal.jl

@ -111,7 +111,7 @@ end
@syntax FreeSymmetricMonoidalCategory{ObExpr,HomExpr} SymmetricMonoidalCategory begin
otimes(A::Ob, B::Ob) = associate_unit(new(A,B), munit)
otimes(f::Hom, g::Hom) = associate(new(f,g))
compose(f::Hom, g::Hom) = associate(new(f,g; strict=true))
compose(f::Hom, g::Hom) = associate_unit(new(f,g; strict=true), id)
end
function show_latex(io::IO, expr::HomExpr{:braid}; kw...)
@ -224,7 +224,7 @@ This convention could be dropped or reversed.
@syntax FreeCartesianCategory{ObExpr,HomExpr} CartesianCategory begin
otimes(A::Ob, B::Ob) = associate_unit(new(A,B), munit)
otimes(f::Hom, g::Hom) = associate(new(f,g))
compose(f::Hom, g::Hom) = associate(new(f,g; strict=true))
compose(f::Hom, g::Hom) = associate_unit(new(f,g; strict=true), id)
pair(f::Hom, g::Hom) = compose(mcopy(dom(f)), otimes(f,g))
proj1(A::Ob, B::Ob) = otimes(id(A), delete(B))
@ -284,7 +284,7 @@ end
@syntax FreeBiproductCategory{ObExpr,HomExpr} BiproductCategory begin
otimes(A::Ob, B::Ob) = associate_unit(new(A,B), munit)
otimes(f::Hom, g::Hom) = associate(new(f,g))
compose(f::Hom, g::Hom) = associate(new(f,g; strict=true))
compose(f::Hom, g::Hom) = associate_unit(new(f,g; strict=true), id)
pair(f::Hom, g::Hom) = Δ(dom(f)) (f g)
copair(f::Hom, g::Hom) = (f g) (codom(f))
@ -322,7 +322,7 @@ end
@syntax FreeClosedMonoidalCategory{ObExpr,HomExpr} ClosedMonoidalCategory begin
otimes(A::Ob, B::Ob) = associate_unit(new(A,B), munit)
otimes(f::Hom, g::Hom) = associate(new(f,g))
compose(f::Hom, g::Hom) = associate(new(f,g; strict=true))
compose(f::Hom, g::Hom) = associate_unit(new(f,g; strict=true), id)
end
function show_latex(io::IO, expr::ObExpr{:hom}; kw...)
@ -363,7 +363,7 @@ See also `FreeCartesianCategory`.
@syntax FreeCartesianClosedCategory{ObExpr,HomExpr} CartesianClosedCategory begin
otimes(A::Ob, B::Ob) = associate_unit(new(A,B), munit)
otimes(f::Hom, g::Hom) = associate(new(f,g))
compose(f::Hom, g::Hom) = associate(new(f,g; strict=true))
compose(f::Hom, g::Hom) = associate_unit(new(f,g; strict=true), id)
pair(f::Hom, g::Hom) = Δ(dom(f)) (f g)
proj1(A::Ob, B::Ob) = id(A) (B)
@ -400,7 +400,7 @@ end
unit=munit, contravariant=true)
otimes(A::Ob, B::Ob) = associate_unit(new(A,B), munit)
otimes(f::Hom, g::Hom) = associate(new(f,g))
compose(f::Hom, g::Hom) = associate(new(f,g; strict=true))
compose(f::Hom, g::Hom) = associate_unit(new(f,g; strict=true), id)
mate(f::Hom) = distribute_mate(involute(new(f)))
hom(A::Ob, B::Ob) = B dual(A)
ev(A::Ob, B::Ob) = id(B) (σ(dual(A), A) dcounit(A))
@ -439,7 +439,7 @@ end
end
@syntax FreeDaggerCategory{ObExpr,HomExpr} DaggerCategory begin
compose(f::Hom, g::Hom) = associate(new(f,g; strict=true))
compose(f::Hom, g::Hom) = associate_unit(new(f,g; strict=true), id)
dagger(f::Hom) = distribute_dagger(involute(new(f)))
end
@ -464,7 +464,7 @@ end
@syntax FreeDaggerSymmetricMonoidalCategory{ObExpr,HomExpr} DaggerSymmetricMonoidalCategory begin
otimes(A::Ob, B::Ob) = associate_unit(new(A,B), munit)
otimes(f::Hom, g::Hom) = associate(new(f,g))
compose(f::Hom, g::Hom) = associate(new(f,g; strict=true))
compose(f::Hom, g::Hom) = associate_unit(new(f,g; strict=true), id)
dagger(f::Hom) = distribute_unary(distribute_dagger(involute(new(f))),
dagger, otimes)
end
@ -492,7 +492,7 @@ end
unit=munit, contravariant=true)
otimes(A::Ob, B::Ob) = associate_unit(new(A,B), munit)
otimes(f::Hom, g::Hom) = associate(new(f,g))
compose(f::Hom, g::Hom) = associate(new(f,g; strict=true))
compose(f::Hom, g::Hom) = associate_unit(new(f,g; strict=true), id)
dagger(f::Hom) = distribute_unary(distribute_dagger(involute(new(f))),
dagger, otimes)
mate(f::Hom) = distribute_mate(involute(new(f)))
@ -514,7 +514,7 @@ end
@syntax FreeTracedMonoidalCategory{ObExpr,HomExpr} TracedMonoidalCategory begin
otimes(A::Ob, B::Ob) = associate_unit(new(A,B), munit)
otimes(f::Hom, g::Hom) = associate(new(f,g))
compose(f::Hom, g::Hom) = associate(new(f,g; strict=true))
compose(f::Hom, g::Hom) = associate_unit(new(f,g; strict=true), id)
# FIXME: `GAT.equations` fails to identify the implicit equation.
#trace(X::Ob, A::Ob, B::Ob, f::Hom) = new(X,A,B,f; strict=true)
end
@ -550,7 +550,7 @@ end
@syntax FreeHypergraphCategory{ObExpr,HomExpr} HypergraphCategory begin
otimes(A::Ob, B::Ob) = associate_unit(new(A,B), munit)
otimes(f::Hom, g::Hom) = associate(new(f,g))
compose(f::Hom, g::Hom) = associate(new(f,g; strict=true))
compose(f::Hom, g::Hom) = associate_unit(new(f,g; strict=true), id)
dagger(f::Hom) = distribute_unary(distribute_dagger(involute(new(f))),
dagger, otimes)
end

4
src/theories/MonoidalAdditive.jl

@ -60,7 +60,7 @@ end
@syntax FreeSymmetricMonoidalCategoryAdditive{ObExpr,HomExpr} SymmetricMonoidalCategoryAdditive begin
oplus(A::Ob, B::Ob) = associate_unit(new(A,B), mzero)
oplus(f::Hom, g::Hom) = associate(new(f,g))
compose(f::Hom, g::Hom) = associate(new(f,g; strict=true))
compose(f::Hom, g::Hom) = associate_unit(new(f,g; strict=true), id)
end
function show_latex(io::IO, expr::HomExpr{:swap}; kw...)
@ -125,7 +125,7 @@ could be dropped or reversed.
@syntax FreeCocartesianCategory{ObExpr,HomExpr} CocartesianCategory begin
oplus(A::Ob, B::Ob) = associate_unit(new(A,B), mzero)
oplus(f::Hom, g::Hom) = associate(new(f,g))
compose(f::Hom, g::Hom) = associate(new(f,g; strict=true))
compose(f::Hom, g::Hom) = associate_unit(new(f,g; strict=true), id)
copair(f::Hom, g::Hom) = compose(oplus(f,g), plus(codom(f)))
coproj1(A::Ob, B::Ob) = oplus(id(A), zero(B))

4
src/theories/Preorders.jl

@ -14,7 +14,7 @@ Thin categories have at most one morphism between any two objects.
end
@syntax FreeThinCategory{ObExpr,HomExpr} ThinCategory begin
compose(f::Hom, g::Hom) = associate(new(f,g; strict=true))
compose(f::Hom, g::Hom) = associate_unit(new(f,g; strict=true), id)
end
@theory ThinSymmetricMonoidalCategory{Ob,Hom} <: SymmetricMonoidalCategory{Ob,Hom} begin
@ -22,7 +22,7 @@ end
end
@syntax FreeThinSymmetricMonoidalCategory{ObExpr,HomExpr} ThinSymmetricMonoidalCategory begin
compose(f::Hom, g::Hom) = associate(new(f,g; strict=true))
compose(f::Hom, g::Hom) = associate_unit(new(f,g; strict=true), id)
otimes(A::Ob, B::Ob) = associate_unit(new(A,B), munit)
otimes(f::Hom, g::Hom) = associate(new(f,g))
end

4
src/theories/Relations.jl

@ -27,7 +27,7 @@ end
@syntax FreeBicategoryRelations{ObExpr,HomExpr} BicategoryRelations begin
otimes(A::Ob, B::Ob) = associate_unit(new(A,B), munit)
otimes(R::Hom, S::Hom) = associate(new(R,S))
compose(R::Hom, S::Hom) = associate(new(R,S; strict=true))
compose(R::Hom, S::Hom) = associate_unit(new(R,S; strict=true), id)
dagger(R::Hom) = distribute_unary(distribute_dagger(involute(new(R))),
dagger, otimes)
meet(R::Hom, S::Hom) = compose(mcopy(dom(R)), otimes(R,S), mmerge(codom(R)))
@ -60,7 +60,7 @@ end
@syntax FreeAbelianBicategoryRelations{ObExpr,HomExpr} AbelianBicategoryRelations begin
oplus(A::Ob, B::Ob) = associate_unit(new(A,B), mzero)
oplus(R::Hom, S::Hom) = associate(new(R,S))
compose(R::Hom, S::Hom) = associate(new(R,S; strict=true))
compose(R::Hom, S::Hom) = associate_unit(new(R,S; strict=true), id)
dagger(R::Hom) = distribute_unary(distribute_dagger(involute(new(R))),
dagger, oplus)
meet(R::Hom, S::Hom) = compose(mcopy(dom(R)), oplus(R,S), mmerge(codom(R)))

4
test/theories/Category.jl

@ -18,8 +18,10 @@ f, g = Hom(:f, A, B), Hom(:g, B, A)
@test codom(compose(f,g)) == A
@test_throws SyntaxDomainError compose(f,f)
# Associativity
# Associativity and unitality
@test compose(compose(f,g),f) == compose(f,compose(g,f))
@test compose(id(A), f) == f
@test compose(f, id(B)) == f
# Extra syntax
@test compose(f,g,f) == compose(compose(f,g),f)

Loading…
Cancel
Save