From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBDTLDGMZRMJBBEVHR3PAKGQEC5VKJQI@googlegroups.com X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.7 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-oi1-x23c.google.com (mail-oi1-x23c.google.com [IPv6:2607:f8b0:4864:20::23c]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id a855180c for ; Sun, 14 Oct 2018 19:05:56 +0000 (UTC) Received: by mail-oi1-x23c.google.com with SMTP id 64-v6sf11967069oii.1 for ; Sun, 14 Oct 2018 12:05:56 -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=ACT/MKQSf0ZX+fT3GpvaGnCvLxDxvs+/HGaRBYSg6Yo=; b=jYMwTVBbNLQpUY41J2L1OO5OKLPToYT5Gwwl9Nro1v3qSk7y2dfdt2BYmqMWadr95t dMXL2V+jzGjoOILRZgQ2X9jPJ+ibfy7POQF/h6vYU6VeoFxhM/jbg9AyhiLDhqsy6qUv 2lGgGFX0gJPkY5j6lI1RlWoCDrXWAk6dJupK1yUhktNI6lw6wven/X/1Sat2P+SHg/0D 5epRW/3p6DLoLSyu8qacXITOcmGk6VNhSADylusr/0sRdwKfKLWDNZc4OGieS7TW1xZK WFHJkISmUibO2A4koqPPb2Poz75zyphjKb2/qYUYPpaCQhLhiAQlo342WBPirkSCEqTV yA7g== 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=ACT/MKQSf0ZX+fT3GpvaGnCvLxDxvs+/HGaRBYSg6Yo=; b=Jx81Umdevzxd8jouPkgKicpeokL6jXCwCXgf/9xZ5ZcMph/idtFl0arSuxTmIcxUPY qBCZx/pKOIVY9RETvCKbUyE15JNW1PF7XaEN621yvShdbdECMK5fJB+3aIUYwu0ESYYC kk5ks1f7rrtjjO6N7rRNTKWDje1TbyyIx0wT52G3kJ2g5Gsswufd1SUOlqBYZ8CLZ7Cp ZioloGspO57VHiyFDIR04D5L6epMAPviagfRe04Eg/KtVQVJgPkCmtPJff2RqIb+OEG8 cW/KFQdB/KgPG7jWy4pknEZyOyDIGnXs3hSZWgZQEdWHmkSDBsiKrTbJxC7/XLaRF2wW M+Jg== 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=ACT/MKQSf0ZX+fT3GpvaGnCvLxDxvs+/HGaRBYSg6Yo=; b=XGfQoQznyjdsDMfNa5GCdPHiQk9fI4RVGAUv98BkZ8ZmRvGYwHzHRy3cDQGdl65C4E ZYt4yxgKSw2Gl+4ZXFg445YEM4IpU2HXvV3Pn4gjCqTygVKdDVFi3k7TPUqKtyPsKrle v7JOgrRBuMLWvVJTGSzraybMWhuMDOmmWKpZdy5ecBkR/k8UKkaxvYT2Hd1wYJF9uecu Ta7soAGcBR6S0bTcvbeIjj8FjKM/1ZonIcnRTo3kbebXKjjY9Z++Hgi6Qcsdos/RacHP X32xaeHMK48jkC/UWISJF386RB1EEy7hMEme7am9YIN9Y0Yh9dg6IMB4iakean2HWP8p kD8A== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ABuFfoiFx01C72pgj+yDFb/mDfqO7kZwtED7OtZF1JIGfuTxCEV/596C TYb1+YIINVnZCViVKCCn1H4= X-Google-Smtp-Source: ACcGV62nY90u1PfvhfMLy806xEjmT4LYVS1RVyY5/m5KsUomQnp4+1kKE+cmK5Y2euvzbTjftPFvRw== X-Received: by 2002:a9d:c42:: with SMTP id 60mr233272otr.7.1539543955002; Sun, 14 Oct 2018 12:05:55 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:e8e:: with SMTP id 14ls912230otj.15.gmail; Sun, 14 Oct 2018 12:05:54 -0700 (PDT) X-Received: by 2002:a9d:528e:: with SMTP id f14mr227602oth.4.1539543954614; Sun, 14 Oct 2018 12:05:54 -0700 (PDT) Date: Sun, 14 Oct 2018 12:05:53 -0700 (PDT) From: Corlin Fardal To: Homotopy Type Theory Message-Id: In-Reply-To: <1627abd4-4ab6-48f3-bd7c-0035d8434c74@googlegroups.com> References: <1627abd4-4ab6-48f3-bd7c-0035d8434c74@googlegroups.com> Subject: [HoTT] On the Use of Computational Paths in Path Spaces of Homotopy Type Theory MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_1395_409283977.1539543953897" X-Original-Sender: fardalcorlin@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_1395_409283977.1539543953897 Content-Type: text/plain; charset="UTF-8" >From vaugely skimming through it, it looks like they define a more explicit version of judgmental equality, from which they found an extensional type theory, and proceed to calculate the fundamental group of different spaces in that theory. -- 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. ------=_Part_1395_409283977.1539543953897--