From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.99.168.15 with SMTP id o15mr4653333pgf.179.1511150095956; Sun, 19 Nov 2017 19:54:55 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.99.124.83 with SMTP id l19ls2433359pgn.26.gmail; Sun, 19 Nov 2017 19:54:55 -0800 (PST) X-Received: by 10.101.70.142 with SMTP id h14mr4569160pgr.102.1511150095010; Sun, 19 Nov 2017 19:54:55 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1511150094; cv=none; d=google.com; s=arc-20160816; b=Et4L+Z0QE4C9R/dy4r/LlEJwhL8yMW8tUp7Yrj6VeVs6ENnplsh/OssRrPFqj3Jy6O UF1BYCnQCf5tcsuoeHPHf48cuF3g7i12tGS0Pw18gW3rIztdFPJCV9y4q0TMCMJzMU/g rj1vyFmCvXlvcSpOYH0SDLhHOkbCgsum98+Q8TZ8spLBd53B/ddwXjkMByk5ql78ubUO ofjG7H/ZIETew3Kc0uz0v1BYDrZkDxkuYO241IUz2JnIGALbPc1nJFslD7CDAb92DgSN s179FXmOefX+0CspADSqNv3y6PN6xfiCwND8tYTR2avngzfGcFyy/0LNbkORNpjZVKs8 HYkw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:references:in-reply-to:reply-to :mime-version:dkim-signature:arc-authentication-results; bh=TC4WRun3NW3DXiy9cmBIo3zfNcV9fZJLXQT1PBzghlc=; b=bksPBB9vDxyRmBCrNkDzSsTNueJio0hLD5yrCVwowGsFZsQ2doSQxAOZ5zsUysrwzO eH8TSawxxX0p4YCy4TKacbOaUNdcaNNNAejFVsPrDO6X+LhUqphFb38I5rWgYGoz8+SN vWZEXcBhE7WnrVLa0KYqPJS+sXiUKxbien9ViYRjeF3bOpRsyATDH8OWLoBAjO9Eg/Bx bh1r3QnIq/Etm9Hq+mEEfH3BDN6z8zfJrWP3Sn6S42uhyd7/hvOqPUmra6D4304dtS6n GGVGA0DrvHXPtPWquMiQ+zGwJCqlqq1Oh65YC948qL1cveyxAQap3c8nZRxqRFsJAkWG 9/9w== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=nfrlkfeJ; spf=pass (google.com: domain of temp....@gmail.com designates 2607:f8b0:4002:c09::22b as permitted sender) smtp.mailfrom=temp....@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-yb0-x22b.google.com (mail-yb0-x22b.google.com. [2607:f8b0:4002:c09::22b]) by gmr-mx.google.com with ESMTPS id l27si687372pfb.4.2017.11.19.19.54.54 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 19 Nov 2017 19:54:54 -0800 (PST) Received-SPF: pass (google.com: domain of temp....@gmail.com designates 2607:f8b0:4002:c09::22b as permitted sender) client-ip=2607:f8b0:4002:c09::22b; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=nfrlkfeJ; spf=pass (google.com: domain of temp....@gmail.com designates 2607:f8b0:4002:c09::22b as permitted sender) smtp.mailfrom=temp....@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-yb0-x22b.google.com with SMTP id w203so2526290ybe.9 for ; Sun, 19 Nov 2017 19:54:54 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:reply-to:in-reply-to:references:from:date:message-id :subject:to:cc; bh=TC4WRun3NW3DXiy9cmBIo3zfNcV9fZJLXQT1PBzghlc=; b=nfrlkfeJPTTvgu68Y7cnBrwWi6aAavTDJtAk9q2EqUWYBbRf04IEXM7zLj3uD9cnq7 cSAgRIk5dBF12Vj0+r3E64ly4VfBMw0aoBboMu7uWf1oUfgLAu375wU0ljFv7ZY9fdtU tP+8SYCAyRANKXlsUGFzKx5Mchd1ZPM4lvAhB7hinpNv6DLgfIJ8juefhXxvbImHd/jm TYBkM9YwaWXTDtZOB4BVEVw3fot6sb0phuV2Q9F+knBuY/h5A1wd+r0kNuEo5Ktoe2jN ic6JhrN8ZwGuswL9e9+kjkSLLHTlH+k0p/RfSnRrIErt28u4uR6fy2fLCDLp0l6C4Nz+ 3FZw== X-Gm-Message-State: AJaThX52PoKS5u76wwZbuy8JYfS18v4/WPhk31IRvYEc/sjtgQfu7wTV 0ZbveNnbVqq7bu1wwY1h93TD+rOwEM3SJUy1Pnk= X-Received: by 10.37.185.72 with SMTP id s8mr7700052ybm.444.1511150094294; Sun, 19 Nov 2017 19:54:54 -0800 (PST) MIME-Version: 1.0 Received: by 10.129.121.4 with HTTP; Sun, 19 Nov 2017 19:54:53 -0800 (PST) Reply-To: temp....@gmail.com In-Reply-To: References: From: y Date: Sun, 19 Nov 2017 19:54:53 -0800 Message-ID: Subject: Re: [HoTT] Yet another characterization of univalence To: =?UTF-8?B?TWFydMOtbiBIw7Z0emVsIEVzY2FyZMOz?= Cc: Homotopy Type Theory Content-Type: multipart/alternative; boundary="089e0826803492a3ab055e620c54" --089e0826803492a3ab055e620c54 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Can you elaborate on why it is true? Also as this statement is similar to Yoneda's lemma, do we have something like For a type X : U and B : X -> U, Id (X -> U) (Id X x) B is equivalent to B x? On Fri, Nov 17, 2017 at 3:53 PM, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 < escardo...@gmail.com> wrote: > Consider the identity type former Id of the type X:U in the universe U: > > Id : X -> (X -> U). > > I've known for some years that this is an embedding of the type X into th= e > type (X->U). This means that the fibers of Id are propositions, or, > equivalently, that the maps ap Id : x =3D y -> Id x =3D Id y are equival= ences > for all x,y:X. > > This depends on univalence. I've just realized that this is actually > *equivalent* to univalence. Has anybody noticed this before? > > 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 HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. > --089e0826803492a3ab055e620c54 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Can you elaborate on why it is true? Also as this statemen= t is similar to Yoneda's lemma, do we have something like=C2=A0
For a type X : U and B : X -> U, Id (X -> U) (Id X x) B i= s equivalent to B x?

On Fri, Nov 17, 2017 at 3:53 PM, Mart=C3=ADn H=C3=B6tzel E= scard=C3=B3 <escardo...@gmail.com> wrote:
Consider the identity type former = Id of the type X:U in the universe U:

=C2=A0 =C2= =A0 Id : X -> (X -> U).

I've known for some y= ears that this is an embedding of the type X into the type (X->U). This = means that the fibers of Id are propositions, or, equivalently, that the ma= ps ap Id=C2=A0 : x =3D y -> Id x =3D Id y are equivalences for all x,y:X= .

This depends on univalence. I've just realized tha= t this is actually *equivalent* to univalence. Has anybody noticed this bef= ore?

Martin

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

--089e0826803492a3ab055e620c54--