Wild omega-Categories for the Homotopy Hypothesis in Type Theory

DOI10.4230/LIPICS.TLCA.2015.226zbMath1433.03031OpenAlexW1502741774MaRDI QIDQ5277842

Tom Hirschowitz, Nicolas Tabareau, Andre Hirschowitz

Publication date: 12 July 2017

Full work available at URL: https://hal.archives-ouvertes.fr/hal-01178301

zbMATH Keywords

homotopy type theorycoinductionhomotopy hypothesisomega-categories

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) 2-categories, bicategories, double categories (18N10) Operads (general) (18M60) Type theory (03B38)

Related Items (2)

The construction of set-truncated higher inductive types ⋮ Unnamed Item

Uses Software

• Unnamed Item

This page was built for publication: Wild omega-Categories for the Homotopy Hypothesis in Type Theory