From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBDHM53UG5YFBBSOKZLMQKGQEI6WFUBI@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-pf0-x23e.google.com (mail-pf0-x23e.google.com [IPv6:2607:f8b0:400e:c00::23e]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id c7f86a6e for ; Tue, 26 Jun 2018 20:42:51 +0000 (UTC) Received: by mail-pf0-x23e.google.com with SMTP id h14-v6sf4268594pfi.19 for ; Tue, 26 Jun 2018 13:42:50 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1530045769; cv=pass; d=google.com; s=arc-20160816; b=c9r1PzVRxjVxaxxrEvQA9T9SM49aWPf9cC4/YT7six3RJMNK+PQ2lO2Ixq1LBYaOmL l+0JCKZfjCQICoAq9a+ifcQq2EJQ/wLFc0c3iyKhtkhi3AwX5PeRgSgHt7ubsJ5svbNr vGQk5/BReq6PiGTskdwJirhhIYmkWGfPLfRnYBIaVvnwkJ0Snh8p3fl2dTynPbE+cVM4 4kTKWyVAXejB0f5exAZkN7zBmIwC57zjDWk6rDx11iTqvqxgCATL1+FTX9wzQ04757yw j06905pyRmiMoE9mtN5ubH1mA6RmrsXwWdZeOoeWGGvbFkXh0pXU1zdCRwQ7qj/cxKYI NBLg== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:arc-authentication-results :arc-message-signature:sender:dkim-signature:dkim-signature :arc-authentication-results; bh=fMEDMVyGMv0jhvX0EpiFtYq8ChhdQAkJNA9D9Eh0reM=; b=EYoL6wXIZbEzlqcVQlcBci3NDSQUG92/5mJgj6DdgNnD5TEcStKTJBb/kA6dYCgHsD ZHRFopGCE1MVoGCk2g21u17EEBd3ppq4sCygaeH/ikS9bgoR1oO10Bw4lo1onSai4W1a Wk9HKvCP4ooas4dkOCUFvRdarXiJ4wUZ9Nsi9cz2qbNOfso2cPVxK20wl+bcqOilqXME Pjzabt3+atiotRusJ2vNsRlX1UEWXE0WcMm6yvh4NObFExPTxZMRpXx/2wLdUxLTmx2g mNw4X3l1JFPeCQDJ4o7gXqoHVxzPVZqI6Tislzn1O3JpbxEY3V9ivGpNQbrqTKQnY68f sszQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=iQSmTeOc; spf=pass (google.com: domain of favonia@gmail.com designates 2607:f8b0:400c:c08::231 as permitted sender) smtp.mailfrom=favonia@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:references:in-reply-to:from:date:message-id :subject:to:cc:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=fMEDMVyGMv0jhvX0EpiFtYq8ChhdQAkJNA9D9Eh0reM=; b=kySyeQMW0pvAQp/0QVW10B04sdf/mNeKGpGvHtLsNs/S2NFb4aOoIqHrYAldc/gMcm LQydYdUUuVK/652iSSimThDnfY9z/cxId4+1mWpqFyL33g3bbaz3gOTNxTm6rMG9xea9 ujMtbtf33W3c5PzItg0Yy82dqxx2mMV8O+zn18GFEeK5pRFxetHlUqDlem/zEDqU/SxY 07MYeTwxqAi8DWZH8jWsz3jUuY4p3ox/pEyUaYXm/Pwd5Uzu4yOAmQKKvjk2djIuiZ4P /PxSLPPbzx11BH2jbS6lbGvoOpsteHEbNn2tWuUeeiyot30jYKOx+CO3AvWeA99/uYbH 30bA== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc:x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=fMEDMVyGMv0jhvX0EpiFtYq8ChhdQAkJNA9D9Eh0reM=; b=Oa7OuXit8f74aJKQnixBegP5s88gA7OnB/GUMcT4rn7+F5Egzi8gbjnyK60Xx6mHxV mTHbXyekaXt3hPM0D4Yp0SyhPmyAOOlcLAvrrzBWFnESaLbjATjKK22koxo9rrHkl7XN 2bBw82TBhGXd8/Gkj6e/VJBqDDhOsvTALOUmbCub+QyczomsXWyJoxbnkqcMwrDv7hBw XgqklBeCofLVYTMhWzifSddbuo8qvSs3cRoNx3g9nvYzrmQe78zbfl2K5hDm/MMI7D4e AN5NxyhZnodPPql9d5JQXwqi7QkXKPh7KpL3kMRnm2LCw3Al9123D5hDDQ4yIe3+Nd0J oOmQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:references:in-reply-to:from :date:message-id:subject:to:cc:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :x-spam-checked-in-group:list-post:list-help:list-archive :list-unsubscribe; bh=fMEDMVyGMv0jhvX0EpiFtYq8ChhdQAkJNA9D9Eh0reM=; b=cnVDr5drZY7pmxlAWl6zoHwbs0qPE/wntBeumTOkTFEjkDSBr3tnmHhYFxM1N1KAaB SM6KqsLtOcH20RiBxj68l2xT+rqQAp6l4lcf7VprLY2AxnFJeXL5nT5WkhveStbsZTQG gB1rrfbsmbGni0k5Yut0om3LKZ/xAGLELtMdTSO5A/GNJM/X1tN6oc5jUpSeVwDXI/+/ UL41pkJeK7s0/ZpG4NRLmhZLqhfMJkwYCC3FGS6SkWjYNkanNZv4fK9RaaGCHXKcoDQY s150LmfVAT7WygqKlHx+oGTPdcgaZzUKB3A8M8SPDqy28aKVIcPwgUUAP7HaoSTXyEc6 Vt3g== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APt69E3vkKUa+51rpU7Vj3+gdsfnPzBzJ2s864c0FYJ+wCi06ap/2gsq Dzc4L5Ly6z3/Zg6DcWWV7d4= X-Google-Smtp-Source: ADUXVKKWvYypz/NVhi9Mv9ZNORe4x0/M2vaonNGaxJW30EFV6y+ecnfwALAjl4jbfVVgL2uR66BkZA== X-Received: by 2002:a65:4ac8:: with SMTP id c8-v6mr9609pgu.2.1530045769524; Tue, 26 Jun 2018 13:42:49 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a62:aa06:: with SMTP id e6-v6ls652110pff.6.gmail; Tue, 26 Jun 2018 13:42:49 -0700 (PDT) X-Received: by 2002:a62:908b:: with SMTP id q11-v6mr651647pfk.25.1530045769125; Tue, 26 Jun 2018 13:42:49 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1530045769; cv=none; d=google.com; s=arc-20160816; b=vEckFnvKtyZTBn0B3Jnuf2xvingZnao9JwuoS4Pi+693G4Lwv35tJr5cGPkjFUEYVK p/gNGcK0HATsxRw3ZCLGJgGh4G34zCp92UXRPqomPJBYss0omNciRh826DlzbmSeHUoP /NEIH9pWA37KDbWaOtMxvh4K/TSYAPb8FDlWawpblAzRX/VuEKpzISv3hBxU1QYybY+B iuJOkOA85Xqifvu/RvMCJTcd+YRIzApAP4Ne/eL2Vql/oeVqB650kiVjr43T6fEa+3f3 myI1sEbRzB71ZH4Us9UAsQLAVkePg9KE0K3PLuDqsvzp44KAo+fi2EPjsbeALPnJKw0L YFug== 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:in-reply-to:references :mime-version:dkim-signature:arc-authentication-results; bh=1wO7c1w+y+ogLNxHtslYW/Swo3+szAG/eny1fmeyP40=; b=p3h6NpkLX9s+jR+NPGjJY64YDAKbKXP5lw49ZLSIXoW06sq/FYPo1qNz4fs80aQd4S tRjP/IL5zDhQIbYu/Rpnz49aJbOdkHqJJLms0kE1wEh5mq8gf0TcjHhdtw6v/hw485LF mh8z18EnOy3uvwz//V9y0LIwiaEKwqvTFVvo1BDKE2fdo+hT5YA2kbCiaAMLXpHQTTia CSKr7p1JyGUxCHbZIfA9IrIHY4NyYKBaZYCBaM774gcUdk2N0GbddOpYGlQtqcwIb39s u2yWOkAYQiGODPT9BGULyOo6qRS7tcEb9KlcH7lLtt8pQfSGkDJTcJmoHsq3NQ6eCHdq u8rA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=iQSmTeOc; spf=pass (google.com: domain of favonia@gmail.com designates 2607:f8b0:400c:c08::231 as permitted sender) smtp.mailfrom=favonia@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-ua0-x231.google.com (mail-ua0-x231.google.com. [2607:f8b0:400c:c08::231]) by gmr-mx.google.com with ESMTPS id s13-v6si134175plp.1.2018.06.26.13.42.49 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 26 Jun 2018 13:42:49 -0700 (PDT) Received-SPF: pass (google.com: domain of favonia@gmail.com designates 2607:f8b0:400c:c08::231 as permitted sender) client-ip=2607:f8b0:400c:c08::231; Received: by mail-ua0-x231.google.com with SMTP id 59-v6so11789586uas.5 for ; Tue, 26 Jun 2018 13:42:49 -0700 (PDT) X-Received: by 2002:a9f:24a1:: with SMTP id 30-v6mr2008316uar.65.1530045768504; Tue, 26 Jun 2018 13:42:48 -0700 (PDT) MIME-Version: 1.0 References: <56325711-318f-44de-ae49-6102ae957636@googlegroups.com> In-Reply-To: <56325711-318f-44de-ae49-6102ae957636@googlegroups.com> From: Favonia Date: Tue, 26 Jun 2018 16:42:37 -0400 Message-ID: Subject: Re: [HoTT] Re: Agda formalization question To: =?UTF-8?B?TWFydMOtbiBIw7Z0emVsIEVzY2FyZMOz?= Cc: Homotopy Type Theory Content-Type: multipart/alternative; boundary="0000000000008598fe056f918a46" X-Original-Sender: favonia@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=iQSmTeOc; spf=pass (google.com: domain of favonia@gmail.com designates 2607:f8b0:400c:c08::231 as permitted sender) smtp.mailfrom=favonia@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=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: , --0000000000008598fe056f918a46 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable I see. FYI: with Univalence, we solve this issue in HoTT-Agda by establishing an equivalence like this: https://github.com/HoTT/HoTT-Agda/blob/e48a16bcd719e2fcb409d79e3f7df6c6b812= 23bb/core/lib/types/Pi.agda#L24-L29 As we all know, univalence is a general principle to internalize these identifications. Perhaps special cases can be done in other ways. Best, Favonia On Tue, Jun 26, 2018 at 4:00 PM Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 < escardo.martin@gmail.com> wrote: > Thanks, Favonia. Meanwhile I solved this as in the following commit (file > source/UF-Subsingletons-FunExt.lagda > > ), > https://github.com/martinescardo/TypeTopology/commit/7433e08de497216cbe13= 1727c4a367eaed85847e, > which may be similar to what you are saying. However, the problem with su= ch > a solution is that it has to be specialized to each situation where we ha= ve > inputs defined with some ex/implicit arguments which we want to apply to = a > function defined with some other ex/implicit arguments. In my view, a > definition with implicit arguments should be considered to be the same as > the definition with explicit arguments, as in real-life informal > mathematics. Best, Martin > > > On Tuesday, 26 June 2018 20:16:06 UTC+1, Favonia wrote: > >> Hi Martin, >> >> I don't know your definition of is-prop, but how about this? >> >> open import Agda.Primitive >> >> _* : =E2=88=80 U =E2=86=92 Set (lsuc U) >> U * =3D Set U >> >> data _=E2=89=A1_ {U} {X : U *} (x : X) : X =E2=86=92 U * where >> refl : x =E2=89=A1 x >> >> is-prop : =E2=88=80 {U} =E2=86=92 U * =E2=86=92 U * >> is-prop X =3D (x y : X) =E2=86=92 x =E2=89=A1 y >> >> is-set : =E2=88=80 {U} =E2=86=92 U * =E2=86=92 U * >> 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 * =E2=86=92 U * >> 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 *} =E2=86=92 is-set' X =E2=86=92 i= s-set X >> is-set'-is-set s {x} {y} =3D s x y >> >> is-set-is-set' : =E2=88=80 {U} {X : U *} =E2=86=92 is-set X =E2=86=92 is= -set' X >> is-set-is-set' s x y =3D s {x} {y} >> >> funext : =E2=88=80 U0 U1 =E2=86=92 lsuc (U0 =E2=8A=94 U1) * >> funext U0 U1 =3D {X : U0 *} {Y : X =E2=86=92 U1 *} (f g : (x : X) =E2=86= =92 Y x) =E2=86=92 (=E2=88=80 x =E2=86=92 f >> x =E2=89=A1 g x) =E2=86=92 f =E2=89=A1 g >> >> postulate >> is-prop-is-set' : =E2=88=80 {U} {X : U *} =E2=86=92 funext U U =E2=86= =92 is-prop (is-set' X) >> >> ap : =E2=88=80 {U0 U1} {X : U0 *} {Y : U1 *} (f : X =E2=86=92 Y) {x y : = X} =E2=86=92 x =E2=89=A1 y =E2=86=92 f x >> =E2=89=A1 f y >> ap f refl =3D refl >> >> is-prop-is-set : =E2=88=80 {U} {X : U *} =E2=86=92 funext U U =E2=86=92 = is-prop (is-set X) >> is-prop-is-set fe isset0 isset1 =3D >> ap is-set'-is-set (is-prop-is-set' fe (is-set-is-set' isset0) >> (is-set-is-set' isset1)) >> >> Best, >> Favonia >> > >> On Wed, Jun 20, 2018 at 3:46 PM Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 < >> escardo...@gmail.com> wrote: >> >>> Bad copy and paste. Let me fix this. >>> >>> >>> 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) >>> >>> 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. >>> >> -- > 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. > --=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. --0000000000008598fe056f918a46 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
I see. FYI: with Univalence, we solve this issue in HoTT-A= gda by establishing an equivalence like this:=C2=A0https://github.com/HoTT/HoTT-Agda/blob/e48a16bcd719= e2fcb409d79e3f7df6c6b81223bb/core/lib/types/Pi.agda#L24-L29

As w= e all know, univalence is a general principle to internalize these identifi= cations. Perhaps special cases can be done in other ways.

Best,
= Favonia

On Tue, Jun 26, = 2018 at 4:00 PM Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 <escardo.martin@gmail.com> wrote:
=
Thanks, Favonia. Meanwhile = I solved this as in the following commit (file=C2=A0 source/UF-Subsingletons-FunExt.lagda),=C2=A0https://github.co= m/martinescardo/TypeTopology/commit/7433e08de497216cbe131727c4a367eaed85847= e, which may be similar to what you are saying. However, the problem wi= th such a solution is that it has to be specialized to each situation where= we have inputs defined with some ex/implicit arguments which we want to ap= ply to a function defined with some other ex/implicit arguments. In my view= , a definition with implicit arguments should be considered to be the same = as the definition with explicit arguments, as in real-life informal mathema= tics. Best, Martin=C2=A0=C2=A0


On Tuesday, 26= June 2018 20:16:06 UTC+1, Favonia wrote:
H= i Martin,

I don't know your definition of is-prop, but how about= this?

open import Agda.Primitive

_* : =E2=88=80 U =E2=86=92= Set (lsuc U)
U * =3D Set U

data _=E2=89=A1_ {U} = {X : U *} (x : X) : X =E2=86=92 U * where
= =C2=A0 refl : x =E2=89=A1 x

is-prop : =E2=88=80 {U} =E2=86=92 U * =E2=86=92 U *
is-prop X =3D (x y : X) =E2=86=92 x =E2=89= =A1 y

= is-set : =E2=88=80 {U} =E2=86=92 U * =E2=86=92 U *
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 * =E2=86=92 U *
i= s-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 *} =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 *} =E2=86=92 is-set X =E2=86=92 is-set' X
is-set-is-set' s x y =3D s {x} {y}

funext : =E2= =88=80 U0 U1 =E2=86=92 lsuc (U0 =E2=8A=94 U1) *
funext U0 U1 =3D {X : U0 *} {Y : X =E2=86=92 U1 *} (f g : (x : X) =E2= =86=92 Y x) =E2=86=92 (=E2=88=80 x =E2=86=92 f x =E2=89=A1 g x) =E2=86=92 f= =E2=89=A1 g

postulate
=C2=A0 is-prop-is-set'= : =E2=88=80 {U} {X : U *} =E2=86=92 funext U U =E2=86=92 is-prop (is-set&#= 39; X)

ap : =E2=88=80 {U0 U1} {X : U0 *} {Y : U1 *} (f : X =E2=86=92 Y) {x y : X}= =E2=86=92 x =E2=89=A1 y =E2=86=92 f x =E2=89=A1 f y
ap f refl =3D refl

is-prop-is-set : =E2=88=80 {U} {X : U *} =E2=86=92 f= unext U U =E2=86=92 is-prop (is-set X)
is-p= rop-is-set fe isset0 isset1 =3D
=C2=A0 ap i= s-set'-is-set (is-prop-is-set' fe (is-set-is-set' isset0) (is-s= et-is-set' isset1))

Best,
Favonia

On Wed, Jun 20, 2018 at 3:46 PM Mart=C3=ADn H= =C3=B6tzel Escard=C3=B3 <escardo...@gmail.com>= ; wrote:
Bad copy = and paste. Let me fix this.


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= 9; X =3D (x y : X) =E2=86=92 is-prop(x =E2=89=A1 y)

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 https://groups.google.com/d/optout.

--
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 https://groups.google.com/d/optout.

--
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.
--0000000000008598fe056f918a46--