diff --git a/src/models/GATExprUtils.jl b/src/models/GATExprUtils.jl
index 81672bed..91d713c0 100644
--- a/src/models/GATExprUtils.jl
+++ b/src/models/GATExprUtils.jl
@@ -84,6 +84,7 @@ function involute(expr::GATExpr)
   arg = first(expr)
   head(expr) == head(arg) ? first(arg) : expr
 end
+
 """
 If given GATExpr contains a zero morphism,
 collapse the expression to a single zero morphism.
@@ -95,7 +96,9 @@ function normalize_zero(expr::E;zname=:zeromap) where E <: GATExpr
       ztype = typeof(subexpr)
       s,t = gat_type_args(expr)
       return ztype([s,t],[s,t])
-    end end
+    end
+  end
   expr
 end
+
 end
diff --git a/test/models/SymbolicModels.jl b/test/models/SymbolicModels.jl
index 37740e92..00867257 100644
--- a/test/models/SymbolicModels.jl
+++ b/test/models/SymbolicModels.jl
@@ -365,4 +365,34 @@ f, g, h, k = Hom(:f, A, B), Hom(:g, B, C), Hom(:h, B, A), Hom(:k, C, B)
 # Involution
 @test invert(invert(f)) == f
 
+# PointedSetCategory
+
+"""
+Theory of a pointed set-enriched category.
+We axiomatize a category equipped with zero morphisms.
+
+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
+compose to a zero map, is a good notion
+of a functor that's total on objects and partial on morphisms.
+"""
+@theory ThPointedSetCategory <: ThCategory begin
+  zeromap(A::Ob,B::Ob)::Hom(A,B)
+  (compose(zeromap(A,B),f::(B→C))==zeromap(A,C)) :: Hom(A, C) ⊣ [A::Ob,B::Ob,C::Ob]
+  (compose(g::(A→B),zeromap(A,B))==zeromap(A,C)) :: Hom(A, C) ⊣ [A::Ob,B::Ob,C::Ob]
+end
+
+@symbolic_model FreePointedSetCategory{ObExpr,HomExpr} ThPointedSetCategory begin
+  compose(f::Hom,g::Hom) = associate_unit(normalize_zero(new(f,g; strict=true)), id)
+end
+
+using .ThPointedSetCategory
+
+A,B,C,D = map(x->Ob(FreePointedSetCategory,x),[:A,:B,:C,:D])
+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)
+@test zAC == compose(f,zBC) == compose(zAB,g)
+@test compose(f,zBC,h) == zeromap(A,D)
+
 end
diff --git a/test/syntax/Scopes.jl b/test/syntax/Scopes.jl
index 6e751cc6..f55f00bd 100644
--- a/test/syntax/Scopes.jl
+++ b/test/syntax/Scopes.jl
@@ -54,6 +54,7 @@ nameless = Ident(tag1, LID(1), nothing)
 
 @test gettag(retag(Dict(tag1 => tag2), x)) == tag2
 @test nameof(rename(tag1, Dict(:x => :y), x)) == :y
+@test rename(tag1, Dict{Symbol, Symbol}(), x) == x
 
 # Bindings
 ##########
@@ -118,6 +119,8 @@ xy_scope′ = Scope([bind_x]; tag=tag1)
 @test hasident(xy_scope, x)
 @test !hasident(xy_scope; tag=tag1)
 
+value_scope = Scope{Union{Int, String}}(:x => 1, :y => 1) isa Scope{Union{Int, String}}
+
 s = Scope{String, Int}()
 
 bind_x_typed = Binding{String, Int}(:x, Set([:x]), "ex", 2)