From mboxrd@z Thu Jan  1 00:00:00 1970
X-Received: by 10.25.0.131 with SMTP id 125mr2356954lfa.28.1477951318873;
        Mon, 31 Oct 2016 15:01:58 -0700 (PDT)
X-BeenThere: homotopytypetheory@googlegroups.com
Received: by 10.28.32.86 with SMTP id g83ls56701wmg.6.gmail; Mon, 31 Oct 2016
 15:01:58 -0700 (PDT)
X-Received: by 10.28.7.68 with SMTP id 65mr1076305wmh.21.1477951318172;
        Mon, 31 Oct 2016 15:01:58 -0700 (PDT)
Return-Path: <neelakantan....@gmail.com>
Received: from mail-wm0-x229.google.com (mail-wm0-x229.google.com. [2a00:1450:400c:c09::229])
        by gmr-mx.google.com with ESMTPS id d62si1409382wmd.0.2016.10.31.15.01.58
        for <HomotopyT...@googlegroups.com>
        (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128);
        Mon, 31 Oct 2016 15:01:58 -0700 (PDT)
Received-SPF: pass (google.com: domain of neelakantan....@gmail.com designates 2a00:1450:400c:c09::229 as permitted sender) client-ip=2a00:1450:400c:c09::229;
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::229 as permitted sender) smtp.mailfrom=neelakantan....@gmail.com;
       dmarc=pass (p=NONE dis=NONE) header.from=gmail.com
Received: by mail-wm0-x229.google.com with SMTP id a197so45961915wmd.0
        for <HomotopyT...@googlegroups.com>; Mon, 31 Oct 2016 15:01:58 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
        d=gmail.com; s=20120113;
        h=subject:to:references:cc:from:message-id:date:user-agent
         :mime-version:in-reply-to:content-transfer-encoding;
        bh=IoE6MWroJsv1lG7pImBY4tua7+1mWuObkM9pXbiYy9c=;
        b=y/P58/VWMtMF3y4Xnym7tgl3+4XScA8Lu0LnutGDMiV2lOyQ+aN3lL9vyfK5v+Y5R/
         l2YWexpuCELcaz/aCLEFhN4Mt2lvcKPKcHwhThvWxunZLNYckuHo/bc9HJDdOg6wqbPs
         eFeac2jw1eRdy6IwBs4zdpEZH4/AUa1w4F9RCkAA1K4mbZMXNNK76Bglw9sCIK58YMF8
         eQiQm+20YXuUnHmKQoNW/q9CjMhL+R4iBlEfl4S3/kKbI1ml12v743ITWitxYjQ1BXF5
         g5odR6tGKscJvwXi6R4HVV7x7wXIMNZSvS2YzG99AcS2tZCnIJfe53pmoMad35R3LmcM
         85ug==
X-Gm-Message-State: ABUngvec7qVKCZx7LRkYuaNqPfc76LI/DMgtW7DH0yhNYKLvxbwjo4DUYY4VC+xTq0retQ==
X-Received: by 10.194.127.161 with SMTP id nh1mr23427205wjb.61.1477951317909;
        Mon, 31 Oct 2016 15:01:57 -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 jx8sm32157969wjc.2.2016.10.31.15.01.57
        (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128);
        Mon, 31 Oct 2016 15:01:57 -0700 (PDT)
Subject: Re: [HoTT] MLTT with proof-relevant judgmental equality?
To: Andrej Bauer <andrej...@andrej.com>
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>
 <bba16179-8529-d8a6-c357-82514c5a5d62@gmail.com>
 <934C25AD-B832-48DD-B035-6522A77473AF@andrej.com>
Cc: Homotopy Type Theory <HomotopyT...@googlegroups.com>
From: Neel Krishnaswami <neelakantan....@gmail.com>
Message-ID: <1fbc7f0c-7a3b-6e0d-761d-7dd45db1de0e@gmail.com>
Date: Mon, 31 Oct 2016 22:01:56 +0000
User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101
 Thunderbird/45.4.0
MIME-Version: 1.0
In-Reply-To: <934C25AD-B832-48DD-B035-6522A77473AF@andrej.com>
Content-Type: text/plain; charset=windows-1252; format=flowed
Content-Transfer-Encoding: 7bit

Hello,

No, the draft I was thinking of was a paper about the categorical
semantics of type theory.

However, this paper is quite relevant to my interests, as is (its
apparent successor) the LFMTP 2013 paper "Explicit Convertibility
Proofs in Pure Type Systems" by Floris van Doorn, Herman Geuvers and
Freek Wiedijk.

So in this sense my query has been unexpectedly successful. :)

Best,
Neel



On 31/10/16 21:43, Andrej Bauer wrote:
> Are you thinking of
>
> http://www.cs.ru.nl/~herman/PUBS/LambdaF.pdf
>
> by any chance?
>
> With kind regards,
>
> Andrej
>