From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBC34PP4V6YCBBRVWZLMQKGQE2JWUJRQ@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 88965a09 for ; Tue, 26 Jun 2018 20:00:08 +0000 (UTC) Received: by mail-ot0-x23f.google.com with SMTP id l11-v6sf12806337oth.1 for ; Tue, 26 Jun 2018 13:00:07 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:in-reply-to:references:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=v+qKCb/frBOrMh2xQWbeM7xZNESMV9XqIvRqN7/BT8Q=; b=qqLjDFjFkW7xlqqzKc3I0wC3LaMzh18XFQKDAaY3yuDn9trE7wZx/SbSxHK+dW0de1 NFqRuHOdEmxLpofdSP/Q/H4D/6PiK2QVox1QZKoZYVDIk1KD2Ne2kB8IIkUyld3lbIvd L49/v1W4db6EwdUP3nwRRuh1ZHRtHWjMk2qfvjMm5AfhZrniTOXKdxht0dg9chCk4koE zBsiFGrlQNy8pRPhK2SWAkNY4P9GNYtD8eoR1N74mYHB6v+1nSgih/QTAHevKV52BP6o HNO8ZqSo12jYKhxQaF+OZMA8Qiy3jI3+pm0qt2qMFWLDrnb7QrcZlSG4W0zcNUMEzJmH 0jwA== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:in-reply-to:references:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=v+qKCb/frBOrMh2xQWbeM7xZNESMV9XqIvRqN7/BT8Q=; b=BEciRPRYhmi+7WbBFwtaW2vcd67LVwhWmdygmWT2H/xvkfmWeObBdC9chgEVZz18DI jHCNKdDPcVZUYvWAXH/n/SlOHks0c1lAVuOnQCwrepJqjMflJEr4nWaoVppxCbUBmRWj 2I3ayAXORaXZCECABx0Hbx18adfgmYHOOtz4zY6oRUZP2KLfc2aL7GRaleibUCZqXWaY VBLGGMQKBOis+nHcb77VmWHE3le2waHXk9h4/SiALKvEOdtcmOtzgWP722MnksGtOmbu ady5vV881dyFuUn8OQ6jpctzJjTWBwyHYNeGOYEf14cZlVB6N7F89kltTe99VSikTvFP Z8LA== 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:in-reply-to :references: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=v+qKCb/frBOrMh2xQWbeM7xZNESMV9XqIvRqN7/BT8Q=; b=kDScH0KFzNPUUVb5lVhJKnDr12LyOSZe0wbMMYgk6jzUPE9pEBsWYAognRQZBt0CWc I6JxfHemLeHo4Vqm8RfEzEdl3Eijg3U8sKiA85fbrSJQm/l1OgVPCHKMQJ/5mXavUjSv 6lT8BFFCxxnBEdUzg5A5nVfUkcutQVdKGNfIe0v6wN8R7GDJHyGiz1fvqQgeNiYNx8J/ I6TQZD5Rgwq5TiVsnMiPkNJdkDowiHrzh6OFcWKG6yZBNKqMGmliriNt6ERxAKsxCwzE mUGhqlTPjRXcNW0W9UCap5xoi+nTEqSptCd3g6MzNSbUHFLTjifTlWuLD059cNutSjN2 Ne4g== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APt69E0YJgrhq4mT9qulP9eqg15qw5xQ8HMZjjkzhttUD+NW1jJztVxa hPgisJiC8RiLKnBTlhNrQ1U= X-Google-Smtp-Source: AAOMgpd/w/mcrb/TzXKNzGhlVplV/qrrjBS7MXUAYgpjSZvXdE05f595EONIgyW5onb0w8gq4zFm9g== X-Received: by 2002:aca:1a18:: with SMTP id a24-v6mr301370oia.5.1530043206534; Tue, 26 Jun 2018 13:00:06 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:1b04:: with SMTP id b4-v6ls1073682oib.15.gmail; Tue, 26 Jun 2018 13:00:06 -0700 (PDT) X-Received: by 2002:aca:8d2:: with SMTP id 201-v6mr306804oii.0.1530043205895; Tue, 26 Jun 2018 13:00:05 -0700 (PDT) Date: Tue, 26 Jun 2018 13:00:05 -0700 (PDT) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: <56325711-318f-44de-ae49-6102ae957636@googlegroups.com> In-Reply-To: References: Subject: Re: [HoTT] Re: Agda formalization question MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_37425_1677899629.1530043205384" 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_37425_1677899629.1530043205384 Content-Type: multipart/alternative; boundary="----=_Part_37426_618010958.1530043205385" ------=_Part_37426_618010958.1530043205385 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Thanks, Favonia. Meanwhile I solved this as in the following commit (file = =20 source/UF-Subsingletons-FunExt.lagda=20 ), https://github= .com/martinescardo/TypeTopology/commit/7433e08de497216cbe131727c4a367eaed85= 847e,=20 which may be similar to what you are saying. However, the problem with such= =20 a solution is that it has to be specialized to each situation where we have= =20 inputs defined with some ex/implicit arguments which we want to apply to a= =20 function defined with some other ex/implicit arguments. In my view, a=20 definition with implicit arguments should be considered to be the same as= =20 the definition with explicit arguments, as in real-life informal=20 mathematics. Best, Martin =20 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 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=20 > 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=20 > 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 i= s-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)=20 > (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 >> >>> >>> --=20 >> You received this message because you are subscribed to the Google Group= s=20 >> "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n=20 >> 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. ------=_Part_37426_618010958.1530043205385 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Thanks, Favonia. Meanwhile I solved this as in the followi= ng commit (file=C2=A0 sou= rce/UF-Subsingletons-FunExt.lagda),=C2=A0https://github.com/martinescar= do/TypeTopology/commit/7433e08de497216cbe131727c4a367eaed85847e, which may = be similar to what you are saying. However, the problem with such a solutio= n is that it has to be specialized to each situation where we have inputs d= efined 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 wi= th implicit arguments should be considered to be the same as the definition= with explicit arguments, as in real-life informal mathematics. Best, Marti= n=C2=A0=C2=A0

On Tuesday, 26 June 2018 20:16:06 UTC+1, Favonia wrot= e:
Hi Martin,

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

open import Agda.Primitive

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

dat= a _=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 *
is-set' X =3D (x y : X) =E2=86=92 is-prop (x =E2=89=A1 y)=

is-se= t'-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
=C2=A0 is-prop= -is-set' : =E2=88=80 {U} {X : U *} =E2=86=92 funext U U =E2=86=92 is-pr= op (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
=C2=A0 ap is-set'-is-set (is-prop-is-set' fe (is-set-is-set' i= sset0) (is-set-is-set' isset1))

Best,
Favonia

=
On Wed, Jun 20, 2018 at 3:46 PM Mart=C3=ADn H=C3=B6tzel Es= card=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 &= 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.
------=_Part_37426_618010958.1530043205385-- ------=_Part_37425_1677899629.1530043205384--