A canonical normal form theorem for the type theory of regular categories

In this thesis is shown a proof of canonical normal form theorem for the type theory of regular categories. The theorem states that any closed typed term, whose derivation has no open assumption, can be reduced by a sequence of reductions into an equivalent one in canonical form and that the proof of any provable judgement can be transformed into an equivalent one in introductory form.