A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory

Article Details
Title:	A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory
Article URLs:	https://doi.org/10.1145/2933575.2934545 http://ieeexplore.ieee.org/document/8576476
Alternative Article URLs:
Authors:	Kuen-Bang Hou (Favonia)	Carnegie Mellon University
	Eric Finster	École Polytechnique, LIX
	Daniel R. Licata	Wesleyan University
	Peter LeFanu Lumsdaine	Stockholm University
Sharing:	Unknown
Verification:	Authors have not verified information
Artifact Evaluation Badge:	none
Artifact URLs:	https://github.com/HoTT/HoTT-Agda/blob/1.0/Homotopy/BlakersMassey.agda https://github.com/dlicata335/hott-agda/blob/master/homotopy/blakersmassey/ooTopos.agda
Artifact Correspondence Email Addresses:
NSF Award Numbers:	1116703, 1128155
DBLP Key:	conf/lics/FavoniaFLL16
Author Comments:

ACM/IEEE Logic in Computer Science, LICS 2016