cleanup

src/nonstdlib/models/Pushouts.jl

@@ -23,19 +23,19 @@ using .ThPushout
     rootindex = sort(collect(Set(values(roots))))
     toindex = [findfirst(==(r),rootindex) for r in roots]
     PushoutInt(DataStructures.num_groups(d), 
-     [toindex[roots[b]] for b in 1:B], 
+     [toindex[roots[b]] for b in 1:B],
      [toindex[roots[c+B]] for c in 1:C]
     )
   end
   cospan(p::PushoutInt) = Cospan(p.ob, p.i1, p.i2)
-  function universal(p::PushoutInt, csp::Cospan; context)
+  function universal(p::PushoutInt, csp::Cospan)
     map(1:p.ob) do i
       for (proj, csp_map) in [(p.i1, csp.left), (p.i2, csp.right)]
         for (j, i′) in enumerate(proj)
           if i′ == i return csp_map[j] end
         end
       end
-      error("Pushout is jointly surjective")
+      error("Pushout $p is not jointly surjective")
     end
   end
 end

src/syntax/gats/ast.jl

@@ -16,6 +16,11 @@ A *sort*, which is essentially a type constructor without arguments
   method::Ident
 end
 
+"""
+`AlgSort`
+
+A sort for equality judgments of terms for a particular sort
+"""
 @struct_hash_equal struct AlgEqSort <: AbstractAlgSort
   head::Ident
   method::Ident
@@ -213,9 +218,8 @@ end
 Accessing a name from a term of tuple type
 """
 @struct_hash_equal struct AlgDot <: AbstractDot
-  head::Ident #Symbol
+  head::Ident
   body::AlgTerm
-  # sort::AlgSort
 end
 headof(a::AlgDot) = a.head 
 bodyof(a::AlgDot) = a.body

src/syntax/gats/judgments.jl

@@ -158,6 +158,10 @@ Is tantamount to (in a vanilla GAT):
       ⊣ [(dom, codom, apex)::Ob, i_1::dom->apex, i_2::codom->apex]
     i2(cospan(a, i_1, i_2)) == i_2
       ⊣ [(dom, codom, apex)::Ob, i_1::dom->apex, i_2::codom->apex]
+
+    cospan(apex(csp), i1(csp), i2(csp)) == csp
+      ⊣ [(dom, codom)::Ob, csp::Cospan(dom, codom)]
+
 """
 @struct_hash_equal struct AlgStruct <: TrmTypConstructor
   declaration::Ident