From mboxrd@z Thu Jan  1 00:00:00 1970
X-Received: by 10.25.16.93 with SMTP id f90mr2171249lfi.30.1477919274178;
        Mon, 31 Oct 2016 06:07:54 -0700 (PDT)
X-BeenThere: homotopytypetheory@googlegroups.com
Received: by 10.28.165.138 with SMTP id o132ls980624wme.5.canary-gmail; Mon,
 31 Oct 2016 06:07:53 -0700 (PDT)
X-Received: by 10.195.17.199 with SMTP id gg7mr2087131wjd.3.1477919273473;
        Mon, 31 Oct 2016 06:07:53 -0700 (PDT)
Return-Path: <neelakantan....@gmail.com>
Received: from mail-wm0-x22e.google.com (mail-wm0-x22e.google.com. [2a00:1450:400c:c09::22e])
        by gmr-mx.google.com with ESMTPS id f4si1995921wmf.1.2016.10.31.06.07.53
        for <HomotopyT...@googlegroups.com>
        (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128);
        Mon, 31 Oct 2016 06:07:53 -0700 (PDT)
Received-SPF: pass (google.com: domain of neelakantan....@gmail.com designates 2a00:1450:400c:c09::22e as permitted sender) client-ip=2a00:1450:400c:c09::22e;
Authentication-Results: gmr-mx.google.com;
       dkim=pass head...@gmail.com;
       spf=pass (google.com: domain of neelakantan....@gmail.com designates 2a00:1450:400c:c09::22e as permitted sender) smtp.mailfrom=neelakantan....@gmail.com;
       dmarc=pass (p=NONE dis=NONE) header.from=gmail.com
Received: by mail-wm0-x22e.google.com with SMTP id t79so46158259wmt.0
        for <HomotopyT...@googlegroups.com>; Mon, 31 Oct 2016 06:07:53 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
        d=gmail.com; s=20120113;
        h=subject:references:to:from:message-id:date:user-agent:mime-version
         :in-reply-to:content-transfer-encoding;
        bh=qVR890IJ5iqFgQqswlGo8aqypcKMghcU3tgwPKWAZFM=;
        b=uwz26o8JU9xDfaE5n+BWEnn7fSHQy9KdIr2T8GHs3R4kSuLCFCpH3Y6JrOrYJ+6QM/
         DxEm4rlVlFAWE1q9/kP5v/fG1aAv4PfPZD1wDvpxC7pBKGMV9o+EXHm1BNCLPMzlVZCE
         Z+XgD7bAo82ffYuAvL5if6TN/ShmZG1g91g/kaS37VbOaTakYlXCoFG123H4NMLsZw07
         TfP3ix2U23zzzjATRDwUtm5sPdzq6Mdbyqdl3L3j8H0bCRXroeLjrzO58oeJqEmFIPMn
         yF98CavZUP/ex1KstkXnmYhn2RU6RceqHsF0rb+f1NktxI7urgCYD1vLwnuOW9ICDprS
         DqcQ==
X-Gm-Message-State: ABUngvcv0hgeruxYYwxqhQD7KMauLGrbr8Z7Ehy06axOtJYaqEqyrqwECC0bM+C+BEWpmA==
X-Received: by 10.194.126.36 with SMTP id mv4mr22628181wjb.221.1477919273016;
        Mon, 31 Oct 2016 06:07:53 -0700 (PDT)
Return-Path: <neelakantan....@gmail.com>
Received: from sheaf.cl.cam.ac.uk (sheaf.cl.cam.ac.uk. [128.232.10.204])
        by smtp.gmail.com with ESMTPSA id ya1sm29928065wjb.23.2016.10.31.06.07.52
        for <HomotopyT...@googlegroups.com>
        (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128);
        Mon, 31 Oct 2016 06:07:52 -0700 (PDT)
Subject: MLTT with proof-relevant judgmental equality?
References: <CALgtc7gp1VhjzF4h5GxpPCcsj0VUiGu4vuwQrrODDQU9u0jO+w@mail.gmail.com>
 <9ced56b8-66bb-4f7f-996e-bbbb84c227ab@googlegroups.com>
 <20161027194440.GA826@richard>
 <a2e93830-17e3-4f99-8261-d7894dcf9774@googlegroups.com>
 <20161030205656.GA1487@richard>
 <CAGYJgtaKz4VW16D0u=svvt7awMvNW47ieQUWcr_+pYr969K0Qw@mail.gmail.com>
To: Homotopy Type Theory <HomotopyT...@googlegroups.com>
From: Neel Krishnaswami <neelakantan....@gmail.com>
Message-ID: <bba16179-8529-d8a6-c357-82514c5a5d62@gmail.com>
Date: Mon, 31 Oct 2016 13:07:51 +0000
User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101
 Thunderbird/45.3.0
MIME-Version: 1.0
In-Reply-To: <CAGYJgtaKz4VW16D0u=svvt7awMvNW47ieQUWcr_+pYr969K0Qw@mail.gmail.com>
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 7bit

Hello,

Some time in the last year or two, I saw a reference to a draft
paper which giving (roughly) a model for Martin-Loef type theory,
weakened so that judgemental equality was proof-relevant.

Unfortunately, I can't seem to find the message announcing the
draft, and was wondering if anyone here remembered it (perhaps
even because they wrote it).

Thanks for your help!

Best,
Neel