Beylin, Ilya; Dybjer, Peter Extracting a proof of coherence for monoidal categories from a proof of normalization for monoids. (English) Zbl 1407.68432 Berardi, Stefano (ed.) et al., Types for proofs and programs. International workshop TYPES ’95, Torino, Italy, June 5–8, 1995. Selected papers. Berlin: Springer. Lect. Notes Comput. Sci. 1158, 47-61 (1996). MSC: 68T15 18D10 PDFBibTeX XMLCite \textit{I. Beylin} and \textit{P. Dybjer}, Lect. Notes Comput. Sci. 1158, 47--61 (1996; Zbl 1407.68432) Full Text: DOI
Dybjer, Peter Inductive families. (English) Zbl 0808.03044 Formal Asp. Comput. 6, No. 4, 440-465 (1994). MSC: 03F35 03B70 PDFBibTeX XMLCite \textit{P. Dybjer}, Formal Asp. Comput. 6, No. 4, 440--465 (1994; Zbl 0808.03044) Full Text: DOI