1. Cubical Agda: A dependently typed programming language with univalence and higher inductive types. (6th April 2021) Authors: VEZZOSI, ANDREA; MÖRTBERG, ANDERS; ABEL, ANDREAS Journal: Journal of functional programming Issue: Volume 31(2021) Page Start: Record Type: Journal Article View Content: Available online (eLD content is only available in our Reading Rooms) ↗