From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.2 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,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.2 Received: from mail-oi1-x23b.google.com (mail-oi1-x23b.google.com [IPv6:2607:f8b0:4864:20::23b]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id b2d0d9cb for ; Wed, 30 Jan 2019 11:54:09 +0000 (UTC) Received: by mail-oi1-x23b.google.com with SMTP id e185sf12111557oih.18 for ; Wed, 30 Jan 2019 03:54:09 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=v3PdNDTwpnH8LM97XzDJLgsK9aNLph2Nf8O8+08G5n8=; b=lRnn4p5gzryQ6m3ErLLFp6Egfn38ABWntG5ulnCpOmONSQsLnszV9xgAm+Yzu+DJcI S56YtYWXB2Lj7+j2+Gzybr0jjkytroIo/w9zX5mHOFRp06gpfOkRhft6HVc/qoH0vAMh UeiflsaQu7u2zsVtA60aaM7iRJpI2E0lR/83Kwfzb4gX74N8WMrd7hd8Bqu0qIcphpbV qpbsDOcQ2JE5pjDUgsla3HLSoqd80GiMF0s0ehilDdsg4ZgfNTuAV7gcekffCGO1RzZ/ 4WCeFiY2CGKXsfnQytK8vTkULGf5emBKFE9ZUzbJ0wXj6DGugxtb4YPSS91cZIrdI/cX 9Jbg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:subject:mime-version:x-original-sender :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=v3PdNDTwpnH8LM97XzDJLgsK9aNLph2Nf8O8+08G5n8=; b=aOwo/zkP/E0R751mDnWWxfXffb5pBaJBDYDfw1Seudx5MRn3eUKOvoC+O5/wGKAP7J WmFURWbgXKUtFk9b8lP3PlzadAD9g40/f/34SP9Nr9BmvfBtQIqb4zDB2yP/eWmHNVK8 abrH1vXs5RAQ27wpuRLAsXt3lF9skPmzQOJU9Htl82vTHS1rVRUNyWqbPbL2zTbYfH70 qSekHAr7QxhVDhRbvzP89slNYKxgloY1GUbMsVQVSKxVw6PvUQpNjnSOnNA2+6Nq6kNq xuVdCg+wTv5ByUqQa2iJKjlp84HiYtflZ1ouBkqbFf6y2/DdNyTbJOp4eKXJ379DDNBd YQIg== 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: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=v3PdNDTwpnH8LM97XzDJLgsK9aNLph2Nf8O8+08G5n8=; b=ZLFNC8N0cP/Sv8T4PCqHVPd2TLmz81sCR1kadc11AadUKlF7hSuT/ipE/2us0cLkgf Di2sP3rTM6VCzUwRFgBaRgzc5G0uLNq5C5+qfM6b4EXDEF1/wDjLx4CikOR6VgyRJLuc QEIsgaQRY/YbkBheZDITmRZTOk6LtfiF5Gz29bhaVj+o/1fxr4myZE7MJFc+bvOzpysN AQn6N4xCjkKyeNOuob1X/FemSjLEBrzpKFJQRPGM0FOax5zlpkcPWyGPzmsq6O5OV/mS C1Vlacmrhvrawm7L+AbvQACRUiv8pDhxtP7wEvoh5huRNVF0TCA+V2Lw3jk9APDIxWas cRDg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuZlqg7QwSawDipSYiWQIYA/UIYM5v4TNO6C7Hi2WNq3vgvrqhg1 EguTGsfNn2s2kiUShdpmBPU= X-Google-Smtp-Source: AHgI3IZOd5LFHWewnPxZfkhuS4cY0f4SlLSBTKUCzgOBoKojWFo7QuGBeqIKXEulOIRSOvWo5CWAcg== X-Received: by 2002:aca:4c97:: with SMTP id z145mr138147oia.2.1548849248394; Wed, 30 Jan 2019 03:54:08 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:6485:: with SMTP id g5ls883156otl.6.gmail; Wed, 30 Jan 2019 03:54:08 -0800 (PST) X-Received: by 2002:a9d:148:: with SMTP id 66mr130262otu.5.1548849247920; Wed, 30 Jan 2019 03:54:07 -0800 (PST) Date: Wed, 30 Jan 2019 03:54:07 -0800 (PST) From: Felix Rech To: Homotopy Type Theory Message-Id: Subject: [HoTT] Why do we need judgmental equality? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_2574_661185559.1548849247081" X-Original-Sender: s9ferech@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_2574_661185559.1548849247081 Content-Type: multipart/alternative; boundary="----=_Part_2575_1818288559.1548849247082" ------=_Part_2575_1818288559.1548849247082 Content-Type: text/plain; charset="UTF-8" In section 1.1 of the HoTT book it says "In type theory there is also a need for an equality judgment." Currently it seems to me like one could, in principle, replace substitution along judgmental equality with explicit transports if one added a few sensible rules to the type theory. Is there a fundamental reason why the equality judgment is still necessary? Thanks, Felix Rech -- 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_2575_1818288559.1548849247082 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
In section 1.1 of the HoTT book it says "In type= theory there is also a need for an equality judgment." Currently it s= eems to me like one could, in principle, replace substitution along judgmen= tal equality with explicit transports if one added a few sensible rules to = the type theory. Is there a fundamental reason why the equality judgment is= still necessary?

Thanks,
Felix Rech=

--
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_2575_1818288559.1548849247082-- ------=_Part_2574_661185559.1548849247081--