From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBC34PP4V6YCBBVG4VLMQKGQEMXMSXDA@googlegroups.com X-Spam-Checker-Version: SpamAssassin 3.4.1 (2015-04-28) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.6 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.1 Received: from mail-ot0-x23f.google.com (mail-ot0-x23f.google.com [IPv6:2607:f8b0:4003:c0f::23f]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id c986a106 for ; Wed, 20 Jun 2018 19:43:18 +0000 (UTC) Received: by mail-ot0-x23f.google.com with SMTP id a9-v6sf373749otl.21 for ; Wed, 20 Jun 2018 12:43:17 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=PYUK5CKtCuR+HXClNXLxDDP4y08DZODM+NPKnbKVUxk=; b=NhO5NjZRe1YJAz2+sS/6Rr20woG+IIkwp+YXYNreHUVWf8j+mIppUAn795hz2b31lY 3oG5SGlYoalFlD7TYaHlM7U07OqERn03qiZSTm9lMxrqIbsQwfhcXDFd3kHWIju9fXAw Dm/dHJ39QMa9ijShk1db+zYz7G5b6uMsJPAy2yXaqtl6yB0AKSXYK6U5eXGS0RmJTB+N v9sleiz6QobPnMZUWe/NaE6f+7+fZkBG+16aq2IiyQ01xGgUXKIaK9cb+NWx0QXldR9F LJkyx0axRH4Sa81x19TmkF0pkE7V2B9x+lrZY0/OlzUCqJqVYLRPHvO/ESWcnye/XG9V pASw== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:subject:mime-version:x-original-sender :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=PYUK5CKtCuR+HXClNXLxDDP4y08DZODM+NPKnbKVUxk=; b=lf6D4tKcBeKn64MCAbWP5QQOeoghRzsjSTvxEY8HP1RZF6sANHqo5VRMr8jTidfFoB CKXoiYF48lOy9LkPw2GtM9x3DUv7/1rSdXJyLZnRDfTa8aGHT21mk+563P4Bzzwi54tg h3XtEamWTI69WHMkGuwCSU98zRxQ96vWE5HCUKsijGWf+mlLGhbqeSO/6KcZyhMNridA oxXWJZx1Xahde1CvDWF1yFLKIQ/F/2DxRT2VYALpVcx8+r/jGlRQzNmsGyVZj0vnxVpo V/Fpwt8lvYkLxO8eeQ+1XfxZqNfYy2wVI8VbBz4KCApipeqYDMBSqjMz8EmN7/woV5T+ kyIQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:message-id:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :x-spam-checked-in-group:list-post:list-help:list-archive :list-unsubscribe; bh=PYUK5CKtCuR+HXClNXLxDDP4y08DZODM+NPKnbKVUxk=; b=VxwC7YEpSH3pXES80svxGlKqXk+0b2EvAGZP5zdFfnvdiOHoqi2Sze3zWUNB8DRoFJ 6FmwjZO66cMXPml8WbSUq9/+5iCOseSzt3ie5PB5/QqXN9DVt2VuFgxQN95gAyIFiVM3 i/nribH0yPI6FE78Oi/bvmS5hlF47ZOmOhrWH5MA4G0uN6IJcD5A+kTDyRs7p5zfThu4 h4VUi62989jF6mC1awfwQfK2qcaKpIvPlbBcZpkglDNR/mBkIzwmMMHGGd9zo9nOmS6+ xldeCJ8VV0dSZhNJDvO02lvlf0Me/GGNJmmgS0ZiYXA32qqdeURO73MXW+HZY+xi/ODR 8u0Q== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APt69E3we+NmCNkmmZ+5gVNXawAKCR7UL1RiRDEFyV4d1hOQPSMzJDL2 HnJjrv7gtFWjJYzvjuIVDaY= X-Google-Smtp-Source: ADUXVKK2o5NsxZTQoeDkKTy15BFp/xd8TX7EylMXp8TF8BEftumSjj3DjdeiTtI9n3/4b8m7+DwCjw== X-Received: by 2002:a9d:4c96:: with SMTP id m22-v6mr260452otf.6.1529523796265; Wed, 20 Jun 2018 12:43:16 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:4c99:: with SMTP id m25-v6ls1300641otf.0.gmail; Wed, 20 Jun 2018 12:43:16 -0700 (PDT) X-Received: by 2002:a9d:70c2:: with SMTP id w2-v6mr261400otj.2.1529523795649; Wed, 20 Jun 2018 12:43:15 -0700 (PDT) Date: Wed, 20 Jun 2018 12:43:15 -0700 (PDT) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: Subject: [HoTT] Agda formalization question MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_687_1897436652.1529523795222" X-Original-Sender: escardo.martin@gmail.com Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , ------=_Part_687_1897436652.1529523795222 Content-Type: multipart/alternative; boundary="----=_Part_688_636327812.1529523795223" ------=_Part_688_636327812.1529523795223 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable This is really an Agda question, but because it involves HoTT concepts, and= =20 because there are several Agda formalizers here, I prefer to ask it here=20 rather than in the Agda mailing list. Forgive me is the question has a simple answer. Consider the following constructions: is-set' : =E2=88=80 {U} =E2=86=92 U =CC=87 =E2=86=92 U =CC=87 is-set' X =3D {x y : X} =E2=86=92 is-prop(x =E2=89=A1 y) is-set' : =E2=88=80 {U} =E2=86=92 U =CC=87 =E2=86=92 U =CC=87 is-set' X =3D (x y : X) =E2=86=92 is-prop(x =E2=89=A1 y) is-set'-is-set : =E2=88=80 {U} {X : U =CC=87} =E2=86=92 is-set' X =E2=86=92= is-set X is-set'-is-set s {x} {y} =3D s x y is-set-is-set' : =E2=88=80 {U} {X : U =CC=87} =E2=86=92 is-set X =E2=86=92 = is-set' X is-set-is-set' s x y =3D s {x} {y} is-prop-is-set' : =E2=88=80 {U} {X : U =CC=87} =E2=86=92 funext U U =E2=86= =92 is-prop (is-set' X) is-prop-is-set' fe =3D is-prop-exponential-ideal fe (=CE=BB x =E2=86=92 is-prop-exponential-idea= l fe (=CE=BB y =E2=86=92 is-prop-is-prop fe)) Now I am not able to prove that=20 is-prop-is-set : =E2=88=80 {U} {X : U =CC=87} =E2=86=92 funext U U =E2=86= =92 is-prop (is-set X) The reason is that funext has explicit parameters, and I don't seem to be= =20 able to get funext with implicit parameters from funext with explicit=20 parameters. Am I missing something obvious? (I am tempted to make is-set' the official version and ditch is-set, but=20 this will involve major rewriting of the Agda code.) Martin --=20 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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. ------=_Part_688_636327812.1529523795223 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
This is really an Agda question, but because it involves H= oTT concepts, and because there are several Agda formalizers here, I prefer= to ask it here rather than in the Agda mailing list.

Fo= rgive me is the question has a simple answer.

Cons= ider the following constructions:

is-set'= : =E2=88=80 {U} =E2=86=92 U =CC=87 =E2=86=92 U =CC=87
is-set'= ; X =3D {x y : X} =E2=86=92 is-prop(x =E2=89=A1 y)

is-set' : =E2=88=80 {U} =E2=86=92 U =CC=87 =E2=86=92 U =CC= =87
is-set' X =3D (x y : X) =E2=86=92 is-prop(x =E2=89=A1 y)<= /div>

is-set'-is-set : =E2=88=80 {U} {X : U =CC=87} = =E2=86=92 is-set' X =E2=86=92 is-set X
is-set'-is-set s {= x} {y} =3D s x y

is-set-is-set' : =E2=88=80 {U= } {X : U =CC=87} =E2=86=92 is-set X =E2=86=92 is-set' X
is-se= t-is-set' s x y =3D s {x} {y}

is-prop-is-set&#= 39; : =E2=88=80 {U} {X : U =CC=87} =E2=86=92 funext U U =E2=86=92 is-prop (= is-set' X)
is-prop-is-set' fe =3D is-prop-exponential-ide= al fe
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0(=CE=BB x =E2=86=92 is-= prop-exponential-ideal fe
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0(= =CE=BB y =E2=86=92 is-prop-is-prop fe))

Now = I am not able to prove that=C2=A0

is-prop-is-set := =E2=88=80 {U} {X : U =CC=87} =E2=86=92 funext U U =E2=86=92 is-prop (is-se= t X)

The reason is that funext has explicit pa= rameters, and I don't seem to be able to get funext with implicit param= eters from funext with explicit parameters. Am I missing something obvious?=

(I am tempted to make is-set' the official ve= rsion and ditch is-set, but this will involve major rewriting of the Agda c= ode.)

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+unsubscribe@googlegroups.com.
For more options, visit http= s://groups.google.com/d/optout.
------=_Part_688_636327812.1529523795223-- ------=_Part_687_1897436652.1529523795222--