Some constructions on ?-groupoids
(2014)
Conference Proceeding
Weak ω-groupoids are the higher dimensional generalisation of setoids and are an essential ingredient of the construc- tive semantics of Homotopy Type Theory [10]. Following up on our previous formalisation [3] and Brunerie’s notes [5], we present a... Read More about Some constructions on ?-groupoids.