Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
* [HoTT] Injective types
@ 2019-04-30 23:05 escardo.martin
  2019-05-01  2:50 ` Michael Shulman
  0 siblings, 1 reply; 11+ messages in thread
From: escardo.martin @ 2019-04-30 23:05 UTC (permalink / raw)
  To: Homotopy Type Theory


[-- 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 --]

^ permalink raw reply	[flat|nested] 11+ messages in thread

end of thread, other threads:[~2019-05-07 22:06 UTC | newest]

Thread overview: 11+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2019-04-30 23:05 [HoTT] Injective types escardo.martin
2019-05-01  2:50 ` Michael Shulman
2019-05-01  6:25   ` escardo.martin
2019-05-01 16:55     ` Michael Shulman
2019-05-02 20:46       ` escardo.martin
2019-05-03 11:45         ` Michael Shulman
2019-05-03 13:25           ` Kenji Maillard
2019-05-03 18:23             ` Thierry Coquand
2019-05-07 12:42         ` Nils Anders Danielsson
2019-05-07 13:51           ` Andreas Nuyts
2019-05-07 22:06             ` Martín Hötzel Escardó

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).