[HoTT] Injective types

[escardo.martin@gmail.com]

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

I would like to advertise this paper, which investigates injective types 
and algebraically injective types, and their relationship 
(https://arxiv.org/abs/1903.01211).

In this paper, it is important to take universe levels seriously (for the 
reasons explained there). In the HoTT book, and in Coq, the universes are 
taken to be cumulative on the nose, and we pretend, notationally, that 
there is only one universe (this is called typical ambiguity). Based on the 
experience of this paper, I have the feeling that the loss of cumulativity, 
as in Agda, but also as in the infty-topos model of univalent type theory 
by Mike (https://arxiv.org/abs/1904.07004) is a good thing. In particular, 
I am not sure how typical ambiguity with cumulativity would be able to 
handle what is said in the above injectives paper.

When I say "would be able to handle" I don't mean just "accepting the 
constructions", but also present them to the (mathematical) user in such a 
way that is both understandable and usable as a blackbox (by quoting 
published resuls).

Martin

-- 
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: 1654 bytes --]