# Examples for CaTT

Here are some examples to get used to the syntax and understand how the system works

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

# Composition
coh comp (x : *) (y : *) (f : x -> y) (z : *) (g : y -> z) : x -> z
```
Redundant arguments must be kept implicit when using previously defined coherence
```# Left unit
coh unit-l (x : *) (y : *) (f : x -> y) : comp (id x) f -> f
# instead of "comp x x (id x) y f", one only writes "comp (id x) f"

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

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

# Associativity
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)
```
The system also supports terms that are not immediately coherence
```# Identity over an identity
let id2 (x : *) = id (id x)

# Square of an endomorphism
let sq (x : *) (f : x -> x) = comp f f
```
Operations are polymorphic with respect to the type of object
```# 2-composition
let comp2 (x : *) (y : *) (f : x -> y) (f' : x -> y) (a : f -> f') (f'' : x -> y) (b : f' -> f'') = comp a b
## Even though a and b are 2-cells, one can still use comp to compose like the as usual 1-cells
```
More examples are available on my GitHub project page