CATT
=^.^=

Coherences for weak ω-categories.

Examples

If you don't feel inspired, here is a sample session: 

# Identity
coh id (x : *) : x -> x

# Composition
coh comp (x : *) (y : *) (f : x -> y) (z : *) (g : y -> z) : x -> z

# Left unit
coh unit-l (x : *) (y : *) (f : x -> y) : comp x x (id x) y f -> f

# Right unit
coh unit-r (x : *) (y : *) (f : x -> y) : comp x y f y (id y) -> f

# Unitor
coh unit-lr (x : *) : unit-l x x (id x) -> unit-r x x (id x)

# Associativity
coh assoc (x : *) (y : *) (f : x -> y) (z : *) (g : y -> z) (w : *) (h : z -> w) : comp x z (comp x y f z g) w h -> comp x y f w (comp y z g w h)
Implicit arguments are available in order to shorten the coherences: 
# Composition
coh comp (x : *) (y : *) (f : x -> y) (z : *) (g : y -> z) : x -> z
let comp f g = comp _ _ f _ g

# Associativiy
coh assoc (x : *) (y : *) (f : x -> y) (z : *) (g : y -> z) (w : *) (h : z -> w) : comp (comp f g) h -> comp f (comp g h)
let assoc f g h = assoc _ _ f _ g _ h
Operations can be polymorphic wrt the type of objects: 
# Composition
let comp (X : Hom) = coh (x : X) (y : X) (f : x -> y) (z : X) (g : y -> z) : (x -> z)

# 1-composition
let comp1 (x : *) (y : *) (f : x -> y) (z : *) (g : y -> z) = comp * x y f z g

# 2-composition
let comp2 (x : *) (y : *) (f : x -> y) (f' : x -> y) (a : f -> f') (f'' : x -> y) (b : f' -> f'') = comp (x -> y) f f' a f'' b
For a more involved example, have a look at the definition of the Eckmann-Hilton morphism.

More details