From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBC34PP4V6YCBBJG6VLMQKGQE4OVRIWQ@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-oi0-x23c.google.com (mail-oi0-x23c.google.com [IPv6:2607:f8b0:4003:c06::23c]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id e1cfa33f for ; Wed, 20 Jun 2018 19:46:45 +0000 (UTC) Received: by mail-oi0-x23c.google.com with SMTP id q129-v6sf394694oic.9 for ; Wed, 20 Jun 2018 12:46:45 -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=soeXmLSgMzq7PvFudrxm+ClVsPw2SOIBvSSuAmgMNOg=; b=geafhxaeeafaStoZ48tZMAyW4JfEAjsMjbkfpDQs9/c4C69gxkBM6nZioDvsOzQUYq yuRCnjPhPcEAPTkBehd+i5SrxItXcbPwolSxbVZRsInG+c9sPivnc0Zjz/IhPIUYK9HW gQXgIdeuLV4zdTiSJIfRsB+OJj0mRLv575B/VAGmgjA4vGsljnLLXB7pBAOEU3WzVv9a gu2FL0+ogVVTPPv6lXKX/HDbCjOSSKkMVn7MFlkYhNCnk7msIAQbBapESBjbtpLGP7XJ JwBttedJLy70tUbho278OSSxbuQW7OI211Hp3tMStwwbXbO2g5gJqxJGhVi2BCcfAVgB vsxQ== 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=soeXmLSgMzq7PvFudrxm+ClVsPw2SOIBvSSuAmgMNOg=; b=F9c3uwHdFgcIeNXiG6zrP9wSic5Apn6bA2mhOYyhTYerFkD8NeNcRSCZKU8HiilhPG 40rHCcBv05l2tQL5sON5/7pbO7jzlA39UNvthwkhede3gYel85iZdOk2552W9gp8ueAE +sA11JVGeluRYFBWm4xlPWzKSYPiY8MBgBwdPXDrX8cSqme67NnDHitxC8mT0s8kpIPp pgBHXwQ85XU/mY/vXo3OgglYNuKVxt+Eks/HV5j/t9JYudiF0G1V9WiKRNcxSJNT3Eun t+dnIkmHu3IMn1F+MlSEuzxhjjIcLQSLXbbr6bmDM5Wgar3qk0bm+BJXsTSZFHRhLAXH ms/A== 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=soeXmLSgMzq7PvFudrxm+ClVsPw2SOIBvSSuAmgMNOg=; b=NZZq22tnKuoCH+nEqpRLMRqBCiK1Y8w/WeRtFAKCSFPaMVabwEyrOG5RNYR2go2j/c 5966mrejZvVOuZZatWgL/rM6NX1E12WNG1NargcHyMp/FiQ4UHFnb2nqxrZk6MNzDGJS eWTrV6cexYXzMoiELVs69Z/EkikCJFTETd25d6zqPUUUtOIqZ14jYXjg24GgUOA7S8pa /FlyeX9UXXVwCuN26gZ/B5KrzhCOHtbvCof9NF72k0aiJsFZBTjm8UBv1Bk+Xx3B8hVu U8wCg1V6XCy/tZGljwQLOnYmE5VI0OhD1hGwWWzbJbacKUNkP1JCPXDbMhSat3V8JGsc arHQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APt69E2qE7ZACY1XnFrZONYDft/jrVyF04tNGGIainyc5yELcwVml1MB X+oG2eZ/m2X2lNwlljEigSM= X-Google-Smtp-Source: ADUXVKLwPKgoN6kUIWn7AN+/GWzf+6j+IJsJShEKVmI4cJDikCuNAlGQZMZJmftIuXhytjkUh2w3Uw== X-Received: by 2002:aca:d448:: with SMTP id l69-v6mr1021478oig.0.1529524004554; Wed, 20 Jun 2018 12:46:44 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:6284:: with SMTP id x4-v6ls1435872otk.2.gmail; Wed, 20 Jun 2018 12:46:44 -0700 (PDT) X-Received: by 2002:a9d:4b04:: with SMTP id q4-v6mr263623otf.3.1529524003791; Wed, 20 Jun 2018 12:46:43 -0700 (PDT) Date: Wed, 20 Jun 2018 12:46:43 -0700 (PDT) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: In-Reply-To: References: Subject: [HoTT] Re: Agda formalization question MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_652_160067582.1529524003247" 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_652_160067582.1529524003247 Content-Type: multipart/alternative; boundary="----=_Part_653_1937635056.1529524003248" ------=_Part_653_1937635056.1529524003248 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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 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_653_1937635056.1529524003248 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
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&= #39; : =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 http= s://groups.google.com/d/optout.
------=_Part_653_1937635056.1529524003248-- ------=_Part_652_160067582.1529524003247--