Cubical informal type theory: the higher groupoid structure

Bruno Bentzen

Following a project of developing conventions and notations for informal type theory carried out in the homotopy type theory book for a framework built out of an augmentation of co…