Cateq

Cateq is an implementation of the procedure given by Makkai to decide whether two cells of an omega-category induced by a polygraph are equal. You can give it a try directly in your browser. Some explanations on the syntax follow.

Some explanations on the syntax:

% A comment start with '%' and stops at the end of the line
% A 0-cell is defined like this:
x := gen *

% Several 0-cells can be defined using commas
y,z := gen *

% An (n+1)-cell between two n-cells is defined as follows
f := gen x -> y

% As before, we can define several such (n+1)-cells at the same time
g,h := gen x -> y
f',g',h' := gen y -> z

% Cells can be composed with *0, *1, etc.
% Identities are obtained by applying id1, id2, etc.
% Variables containing a cell can be defined using ':='
u := f *0 f'
v := f *0 g'
v' := id1 x *0 f *0 f'

% We ask whether two n-cells are equal with '='
u = u  % prints: true
u = v  % prints: false
u = v' % prints: true

% Let's add 2-cells
al := gen f -> g
be := gen g -> h
al' := gen f' -> g'
be' := gen g' -> h'

% Writing formulas with higher cells become quickly tiresome
(f *0 al') *1 ((al *1 be) *0 g') *1 (h *0 be') = (al *1 be) *0 (al' *1 be')

% cateq understands pasting diagrams
% pasting diagrams represent cells by the set of the generators "involved" in them
% cateq deduces how to compose the generators to build the cell
% pasting diagrams are introduced with '{ ... }'
{ f, f' } = f *0 f' % prints: true

% Of course, cateq checks that your pasting diagram is correct
% It fails otherwise
X := { f , g } % fails
Y := { x , g' } % fails
        

A complete example:

% LICS19 Example
x,y,z := gen *
a,b,c := gen x -> y
d,e,f := gen y -> z
al,al' := gen a -> b
be,be' := gen b -> c
ga,ga' := gen d -> e
de,de' := gen e -> f
A := gen al *0 de -> al' *0 de'
B := gen be *0 ga -> be' *0 ga'
Aext := ( a *0 ga ) *1 A *1 ( be *0 f )
Aext' := ( a *0 ga' ) *1 A *1 ( be' *0 f )
Bext := ( al *0 d ) *1 B *1 ( c *0 de )
Bext' := ( al' *0 d ) *1 B *1 ( c *0 de' )
Aext *2 Bext' = Bext *2 Aext' % prints: false

% The same request can be expressed with pasting diagrams
{ be, A, ga } *2 { al', B, de'} = { al, B, de } *2 { be', A, ga' } % prints: false