[HoTT] Preprint - Cubical informal type theory: the higher groupoid structure

[HoTT] Preprint - Cubical informal type theory: the higher groupoid structure

[Bruno Bentzen]

[-- Attachment #1.1: Type: text/plain, Size: 1461 bytes --]

Dear All,

I have recently posted my new preprint on arxiv whose link is attached in 
the following.

https://arxiv.org/abs/1806.08490

Title: Cubical informal type theory: the higher groupoid structure

Abstract: 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 constructive type theory with 
axioms governing higher-dimensional constructions via Voevodsky's 
univalance axiom and higher-inductive types, this paper proposes a way of 
doing informal type theory with a cubical type theory as the underlying 
foundation instead. To that end, we adopt a cubical type theory recently 
proposed by Angiuli, Hou (Favonia) and Harper, a framework with a 
cumulative hierarchy of univalent Kan universes, full univalence and 
instances of higher-inductive types. In the present paper we confine 
ourselves to some elementary theorems concerning the higher groupoid 
structure of types.

Any corrections, comments and suggestions are most welcome and appreciated.

Best,
Bruno

--
Bruno Bentzen
https://sites.google.com/site/bbentzena/

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1.2: Type: text/html, Size: 1965 bytes --]