From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBDHM53UG5YFBB5NBZLMQKGQEIGZHJTA@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-x23b.google.com (mail-pf0-x23b.google.com [IPv6:2607:f8b0:400e:c00::23b]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 9f7937c5 for ; Tue, 26 Jun 2018 19:16:07 +0000 (UTC) Received: by mail-pf0-x23b.google.com with SMTP id j7-v6sf9157441pff.16 for ; Tue, 26 Jun 2018 12:16:07 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1530040566; cv=pass; d=google.com; s=arc-20160816; b=wk0CYgBg98iC6jaF8iHS15L+GyfXPRcUfsE0/kWdwnU6+3+KjM/7JFHn+XT7KQsZWX t3+CzrJHpppF9CjGKxZxhP0PLiYaoyRgi+xTxt3+1UFv2f8F4eXDfqC3fUups+9S2JMB +JfSYcCnVh5lRGREQGfpEzaLXQENREJ9i7SCR2N1O0RMQykpLcGPQPjGJp9AsYLrL8yk 6w2zYVFR69d7I8kYtOC2SSwJG46neFLcGoFknRxJMKrPqqJRXc6687OsEx2H+ISN8AE7 eL/BWIC0nF36sAO5FC2lPA6/o02rLDqAXDQ+rH9HYSkPm+9wn1+XyUUzmcW6JFP5LLxl y0rQ== 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=wmjP6PeiG/VFBrKmcq7rTWvcu3+ITx7Eru+UMwT/FbY=; b=nQGyDcVR1CeaxNhjORA1zsFdaJrAa3YTzrHdKGQ8T9BqKVV494h/t5U38k4N6Zqesz Wpo4gs7t9/s915drHdYU2Tfnrd7rc/Qv0gp4QPwESfSO0i19ZnhnbK0iiWOi5PGdCuns RSa/wP1/NlMEVk6Cz2KoiDrEPxbIZBSn2AKd6nGDOT9UcAcgTiLvGKY4/raXXu/kT0cu bmkcJbRfSJX1BQZ1+WE1j2UhsfcxMCPQFWmleJoxC5a9/5N882jJ/UJ0/xtXDy+abosO nliD1nPb8QJj3UFgwdLO2LqCld6tLMpEgIG6wYQDaSgXug0u2KjT/vblI7ARxLw5yGoI luyw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=qmt0jX3y; spf=pass (google.com: domain of favonia@gmail.com designates 2607:f8b0:400c:c08::229 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=wmjP6PeiG/VFBrKmcq7rTWvcu3+ITx7Eru+UMwT/FbY=; b=pzGfaXuq1fSvg+nPdgLXCR1VYiAlg2JmRWa3GejIThKfjJWecjKwvE5RTSPRkbaUcL a2T8Q9Nh5IA/5uJh1LVBc585zF0DNv5tO79O7Lo4Zx+SnXqL1c1zIgQYf+7425BgiyQC xleFJqr5yK9ETgrUvcEdZ4nqtRJLSC3kcHkBe+jlq/RqazMo4YZ2dHU/okmuZffXj6BC cnTuDIEw2HQYA7nRRN5uo+6Deh79kihHAApNnSh+pdKxYyC5tq6aLhHLV5pHvwhpXu7V gP6NqtYQpBOmSIkuQRRhd2Zg+VykJruKDBpnSYJdaXKbPKsySJOFHSP9fif0+tKUvBy8 2Dxw== 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=wmjP6PeiG/VFBrKmcq7rTWvcu3+ITx7Eru+UMwT/FbY=; b=F9VeU4jh/HSzt+h8WNedgehREUVqsvSLFS/nV5bEvh+syyC/D9SqHUKMLczZQ8mnV0 e8k4+09w5tA0h/vXjnp9zIDJICSa0NjvP8EH6aXTwxK7g2FTPG+fd1it70S/fM+6DmcG mauoyStqEEM1a8OX/Uj+dNnKS9484HbUWnAsSKmQXSvj91kZ5YFhTOrteiyva/Qe3yMF zPu2ZjnIPBXZGhUw1u6U9/xHgZ8rEymqcHXN8BNXNc+u0H71ykj8Y9TWX0zyzfT6N843 sU8qEb5d+9Bm/PbhNiZ6cvEDsaFDAE2DPmH6zZnrbvX0EutKElqVO0BRp+ZeFcD0q4tc HNtg== 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=wmjP6PeiG/VFBrKmcq7rTWvcu3+ITx7Eru+UMwT/FbY=; b=iI4FSoldk9YOBlgyFxJK86yIXXNDUh8Em+YQ7EBmtQhuFc/ygokzm6eoS0YM6IvHyA 4DpLLP0dD+4ImovcgS4ch5Ts8XNtw0J851rVB5lxY5hmy64ek8KH8le8M8mOGcM/vMK0 TUBzKdJ0jU95QIWx7CZzC/ULhJMv+jjk5tAt7YrhVDhrM0v4G/ThQc0g5tFNdxwFWda9 AIRoYjvUXtT8JaTUmn6Afrv74so+LkLQZ0zyo1NVgh9hPNDl6K41Dp4rddjYCaS7JHCb +LMtDqRGiEtGDneoUjEfT2M+U/YqtxGmPZdmMnqQhudu/p6QnSULVUp8WrsrdJSOD+Rg Q2jg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APt69E1tk0+qgMjXy9FkK28lm6dEEiPyw687lWc/9kNMzx4qlAcGR5FT J3er8tdokwnL28DmAhfoZbo= X-Google-Smtp-Source: ADUXVKK8wG2DTJ32q/g029zYQlgP7Bj5lh+osqFu5XlQkWbIv5r4SNg3yPj1WLfZtlhkALHKCui7Hw== X-Received: by 2002:a17:902:b207:: with SMTP id t7-v6mr16369plr.6.1530040566090; Tue, 26 Jun 2018 12:16:06 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a65:504b:: with SMTP id k11-v6ls617520pgo.27.gmail; Tue, 26 Jun 2018 12:16:05 -0700 (PDT) X-Received: by 2002:a65:45c9:: with SMTP id m9-v6mr563223pgr.159.1530040565620; Tue, 26 Jun 2018 12:16:05 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1530040565; cv=none; d=google.com; s=arc-20160816; b=hw5slNGa38IYLv99isrftnL07pJnHm7Kd8UDQOJlqSLpSS+RKD8PMKfY3h8KgRPKlp nX1Cy6z4mDvKcBJvb1p/XJ3IhFa9sTStnUKtzRMUzUDeQZQmW7pvpMk+RLGLKiy6HGP1 l4DtaFowV+yheSJflc4qsxMia9ycO/kp0E/uNAWeyKQGNp+GEerskXqV6yeUpfSwruyj 2V0txYZHMjlx7EJ5iIntFTed30Q3rWMPf04jgWqzCMTm7iwj2rCkN6cUqBoGKhks1ViT wnAN7LK95+jH3PEV4TAUdSCrKU1LnWI8bEBppl2BJI4u6e0Ra7peVp9GnJDZDzqHfROP 7Nqg== 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=qgsFAOGIorAqSdqlYpq2OfbcFZHSnfUaiQHbBiNC5fI=; b=M0apb8FevU0uURIJ9xAi/CkviW3RR3kDW+kCUeOZxkzuHLZFRJU3jvsa1njixIcAN0 nWhYXYigng8j538WnMRxrtTev6HaoG5y6hwIv0/HVBqsPz0hwhzA1s0/BcQNsOT2quDL 37o34P/EnIFNxI2r20Tr9ICyFjPwH/13CIC8DPWvPp0CTnnpWqod8JKvmeBSuxJZRtTA v2mNRn12hG4ORzjphlKaZRqw2OzihbEDqEwWkSk7YU7SaNXEx49Qzd8J77aCQj8CxAYt eBzEVKwWxrwXgq5bdqBIJjDVpZwRHZRJ+/UpZhuaowWqD7gELMbexXQfmEHn14K1SCRG hdFA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=qmt0jX3y; spf=pass (google.com: domain of favonia@gmail.com designates 2607:f8b0:400c:c08::229 as permitted sender) smtp.mailfrom=favonia@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-ua0-x229.google.com (mail-ua0-x229.google.com. [2607:f8b0:400c:c08::229]) by gmr-mx.google.com with ESMTPS id 73-v6si126183plf.4.2018.06.26.12.16.05 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 26 Jun 2018 12:16:05 -0700 (PDT) Received-SPF: pass (google.com: domain of favonia@gmail.com designates 2607:f8b0:400c:c08::229 as permitted sender) client-ip=2607:f8b0:400c:c08::229; Received: by mail-ua0-x229.google.com with SMTP id y8-v6so366844uan.3 for ; Tue, 26 Jun 2018 12:16:05 -0700 (PDT) X-Received: by 2002:ab0:14f3:: with SMTP id f48-v6mr1811516uae.43.1530040565035; Tue, 26 Jun 2018 12:16:05 -0700 (PDT) MIME-Version: 1.0 References: In-Reply-To: From: Favonia Date: Tue, 26 Jun 2018 15:15:52 -0400 Message-ID: Subject: Re: [HoTT] Re: Agda formalization question To: =?UTF-8?B?TWFydMOtbiBIw7Z0emVsIEVzY2FyZMOz?= Cc: Homotopy Type Theory Content-Type: multipart/alternative; boundary="0000000000005efa5a056f9054a4" 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=qmt0jX3y; spf=pass (google.com: domain of favonia@gmail.com designates 2607:f8b0:400c:c08::229 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: , --0000000000005efa5a056f9054a4 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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-s= et 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-se= t' 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.martin@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. > --=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. --0000000000005efa5a056f9054a4 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Hi Martin,

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

op= en 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 *
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 (U= 0 =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' 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 r= efl

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)
is-prop-is-set fe isset0 isse= t1 =3D
=C2=A0 ap is-set'-is-set (is-pro= p-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.martin@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-pr= op(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.
--0000000000005efa5a056f9054a4--