Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
From: Thorsten Altenkirch <Thorsten....@nottingham.ac.uk>
To: Thomas Streicher <stre...@mathematik.tu-darmstadt.de>
Cc: Andrea Vezzosi <sanz...@gmail.com>,
	Kristina Sojakova <sojakova...@gmail.com>,
	Homotopy Type Theory <homotopyt...@googlegroups.com>
Subject: Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent?
Date: Tue, 19 Dec 2017 11:26:52 +0000	[thread overview]
Message-ID: <55AAFF96-F751-4A01-BE3E-280A438A55DC@exmail.nottingham.ac.uk> (raw)
In-Reply-To: <20171218115228.GB29410@mathematik.tu-darmstadt.de>

I don’t understand this: HProps are subobjects of 1 hence they get classified as propositions. Hence there is an element of Omega corresponding to Sigle(a).

Thorsten

On 18/12/2017, 11:52, "homotopyt...@googlegroups.com on behalf of Thomas Streicher" <homotopyt...@googlegroups.com on behalf of stre...@mathematik.tu-darmstadt.de> wrote:

    > >The inconsistency proof you have given is a slightly distorted version
    > >of the following ridiculous argument: {a} and {b} are isomorphic thus
    > >equal for which reason a = b.
    > 
    > Indeed, but we are not in set theory. In set level HoTT Single(True) =
    > Single(False) but True != False.
    
    This is not a question of set theory. In a topos we have propositional
    extensionality in the sense that
    
       \forall p,q:Omega. (p <-> q) -> p = q
    
    but what we don't have is that Single(a) \in \Omega for a \in A.
    
    Thomas
    
    -- 
    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 HomotopyTypeThe...@googlegroups.com.
    For more options, visit https://groups.google.com/d/optout.
    





This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please send it back to me, and immediately delete it. 

Please do not use, copy or disclose the information contained in this
message or in any attachment.  Any views or opinions expressed by the
author of this email do not necessarily reflect the views of the
University of Nottingham.

This message has been checked for viruses but the contents of an
attachment may still contain software viruses which could damage your
computer system, you are advised to perform your own checks. Email
communications with the University of Nottingham may be monitored as
permitted by UK legislation.


  reply	other threads:[~2017-12-19 11:26 UTC|newest]

Thread overview: 54+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2017-12-11  4:22 Kristina Sojakova
2017-12-11 11:42 ` [HoTT] " Jon Sterling
2017-12-11 12:15   ` Kristina Sojakova
2017-12-11 12:43     ` Jon Sterling
2017-12-11 14:28       ` Thomas Streicher
2017-12-11 14:32         ` Kristina Sojakova
2017-12-11 14:23 ` Thorsten Altenkirch
2017-12-12 10:15   ` Andrea Vezzosi
2017-12-12 11:03     ` Thorsten Altenkirch
2017-12-12 12:02       ` Thomas Streicher
2017-12-12 12:21         ` Thorsten Altenkirch
2017-12-12 13:17           ` Jon Sterling
2017-12-12 19:29             ` Thomas Streicher
2017-12-12 19:52               ` Martin Escardo
2017-12-12 23:14           ` Michael Shulman
2017-12-14 12:32             ` Thorsten Altenkirch
2017-12-14 18:52               ` Michael Shulman
2017-12-16 15:21                 ` Thorsten Altenkirch
2017-12-17 12:55                   ` Michael Shulman
2017-12-17 17:08                     ` Ben Sherman
2017-12-17 17:16                       ` Thorsten Altenkirch
2017-12-17 22:43                         ` Floris van Doorn
2017-12-15 17:00           ` Thomas Streicher
2017-12-17  8:47             ` Thorsten Altenkirch
2017-12-17 10:21               ` Thomas Streicher
2017-12-17 11:39                 ` Thorsten Altenkirch
2017-12-18  7:41                   ` Matt Oliveri
2017-12-18 10:00                     ` Michael Shulman
2017-12-18 11:55                       ` Matt Oliveri
2017-12-18 16:24                         ` Michael Shulman
2017-12-18 20:08                           ` Matt Oliveri
2017-12-18 10:10                     ` Thorsten Altenkirch
2017-12-18 11:17                       ` Matt Oliveri
2017-12-18 12:09                       ` Matt Oliveri
2017-12-18 11:52                   ` Thomas Streicher
2017-12-19 11:26                     ` Thorsten Altenkirch [this message]
2017-12-19 13:52                       ` Andrej Bauer
2017-12-19 14:44                         ` Thorsten Altenkirch
2017-12-19 15:31                           ` Thomas Streicher
2017-12-19 16:10                             ` Thorsten Altenkirch
2017-12-19 16:31                               ` Thomas Streicher
2017-12-19 16:37                                 ` Thorsten Altenkirch
2017-12-20 11:00                                   ` Thomas Streicher
2017-12-20 11:16                                     ` Thorsten Altenkirch
2017-12-20 11:41                                       ` Thomas Streicher
2017-12-21  0:42                                         ` Matt Oliveri
2017-12-22 11:18                                           ` Thorsten Altenkirch
2017-12-22 21:20                                             ` Martín Hötzel Escardó
2017-12-22 21:36                                               ` Martín Hötzel Escardó
2017-12-23  0:25                                               ` Matt Oliveri
2017-12-19 16:41                         ` Steve Awodey
2017-12-20  0:14                           ` Andrej Bauer
2017-12-20  3:55                             ` Steve Awodey
     [not found]       ` <fa8c0c3c-4870-4c06-fd4d-70be992d3ac0@skyskimmer.net>
2017-12-14 13:28         ` Thorsten Altenkirch

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=55AAFF96-F751-4A01-BE3E-280A438A55DC@exmail.nottingham.ac.uk \
    --to="thorsten...."@nottingham.ac.uk \
    --cc="homotopyt..."@googlegroups.com \
    --cc="sanz..."@gmail.com \
    --cc="sojakova..."@gmail.com \
    --cc="stre..."@mathematik.tu-darmstadt.de \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
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).