Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
* [HoTT] Propositional Truncation
@ 2019-03-05 22:31 Jean Joseph
  2019-03-05 22:47 ` Nicolai Kraus
  0 siblings, 1 reply; 14+ messages in thread
From: Jean Joseph @ 2019-03-05 22:31 UTC (permalink / raw)
  To: Homotopy Type Theory


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

Hi,

From the HoTT book, the truncation of any type A has two constructors:

1) for any a : A, there is |a| : ||A||
2) for any x,y : ||A||, x = y. 

I get that if A is inhabited, then ||A|| is inhabited by (1). But is it 
true that, if ||A|| is inhabited, then A is inhabited? 

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

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

end of thread, other threads:[~2019-03-08 22:29 UTC | newest]

Thread overview: 14+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2019-03-05 22:31 [HoTT] Propositional Truncation Jean Joseph
2019-03-05 22:47 ` Nicolai Kraus
2019-03-05 23:07   ` Martín Hötzel Escardó
2019-03-07 14:10     ` Licata, Dan
2019-03-07 16:16       ` Martín Hötzel Escardó
2019-03-07 16:35         ` Ben Sherman
2019-03-07 21:52         ` Anders Mörtberg
2019-03-07 22:41           ` Martín Hötzel Escardó
2019-03-07 22:51             ` Licata, Dan
2019-03-07 23:01               ` Martín Hötzel Escardó
2019-03-07 23:23                 ` Martín Hötzel Escardó
2019-03-08 14:59                   ` Anders Mortberg
2019-03-08 15:13                     ` Licata, Dan
2019-03-08 22:28                       ` 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).