From mboxrd@z Thu Jan  1 00:00:00 1970
X-Received: by 2002:a1c:ca04:: with SMTP id a4-v6mr599452wmg.21.1527353276134;
        Sat, 26 May 2018 09:47:56 -0700 (PDT)
X-BeenThere: homotopytypetheory@googlegroups.com
Received: by 2002:a1c:41d5:: with SMTP id o204-v6ls4664670wma.1.gmail; Sat, 26
 May 2018 09:47:55 -0700 (PDT)
X-Received: by 2002:a1c:f50e:: with SMTP id t14-v6mr539085wmh.27.1527353275148;
        Sat, 26 May 2018 09:47:55 -0700 (PDT)
ARC-Seal: i=1; a=rsa-sha256; t=1527353275; cv=none;
        d=google.com; s=arc-20160816;
        b=EO2VZMP/pgXuwC1twrdUagDN5/+I8z/Vx6lrMNHwB4N0Iwza4FrMqGb4yxEwyIPY2/
         MWjK3coRp7MdeG8MnjM4CFMDqS4BWMpDhGhbDVVgK4qfLUijoW0ZaooQkrM2AW7sHAEa
         Cq5eYE9QrTUlIoBA8h5QD0rbZ8Y5gl3GB3eoYySokovyDug3L0aLZ5CGNVprN04cc8YF
         OSr1IjsphSg6q4CmkxhZbPRb3DPFt90LjVKf+A2v6OGvM97uNGZ2jZEllKcwvmtRT9Bc
         aD9U17U82J4xquHGfwLuonEZjGCkCjQKTKFAIqxqVqWQclmguAIhy0iklpf4NEEyJ6+D
         kH/Q==
ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816;
        h=importance:content-transfer-encoding:mime-version:user-agent:cc:to
         :from:subject:date:references:in-reply-to:message-id
         :arc-authentication-results;
        bh=pYtT1b+BtB23+qB1/3h9nrLxZ2/1ekWaAgS7vddgKfA=;
        b=Qz76LAQJEL5Ayn9WUJvFIxKMoXbrkuQdcwmxXSndWlbd8azovvMrhq+D2XSxvK3pKf
         vmq0MT+h+FdFMADjhE+uxczSecFvDbCrlaCgCx89aaXiFjELKQwzU3xvgaGTOJIPU138
         P9wghBokweGnstcB6gGqvulTt3ytCr/fK6Mh2KdP1XvAceNnKtm3AjUQ2BhFWZa3FbAG
         HiMlapr9103pVGGsPI/+twsN/oaPDZUXRzNz144fwU3JRfk9XTRALm8cPHsBd1wjvNDO
         LEMiwJD4lZO5/HUaDf7+9zHzXoQsGAXCHw1QChWvima5zi94+D79d1wi25bZC9oZFclE
         3MoA==
ARC-Authentication-Results: i=1; gmr-mx.google.com;
       spf=pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.239 as permitted sender) smtp.mailfrom=stre...@mathematik.tu-darmstadt.de
Return-Path: <stre...@mathematik.tu-darmstadt.de>
Received: from lnx503.hrz.tu-darmstadt.de (mail-relay239.hrz.tu-darmstadt.de. [130.83.156.239])
        by gmr-mx.google.com with ESMTPS id d18-v6si507998wrm.0.2018.05.26.09.47.55
        for <homotopyt...@googlegroups.com>
        (version=TLS1 cipher=AES128-SHA bits=128/128);
        Sat, 26 May 2018 09:47:55 -0700 (PDT)
Received-SPF: pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.239 as permitted sender) client-ip=130.83.156.239;
Authentication-Results: gmr-mx.google.com;
       spf=pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.239 as permitted sender) smtp.mailfrom=stre...@mathematik.tu-darmstadt.de
Received: from fb04281.mathematik.tu-darmstadt.de (fb04281.mathematik.tu-darmstadt.de [130.83.2.21])
	by lnx503.hrz.tu-darmstadt.de (8.14.4/8.14.4/HRZ/PMX) with ESMTP id w4QGlKwq015166;
	Sat, 26 May 2018 18:47:20 +0200
	(envelope-from stre...@mathematik.tu-darmstadt.de)
Received: from webmail.mathematik.tu-darmstadt.de (fb04277.mathematik.tu-darmstadt.de [130.83.2.17])
	by fb04281.mathematik.tu-darmstadt.de (8.12.3/8.12.3/Debian-7.2) with ESMTP id w4QGlpi6024027;
	Sat, 26 May 2018 18:47:51 +0200
Received: from 87.166.23.12
        (SquirrelMail authenticated user streicher)
        by webmail.mathematik.tu-darmstadt.de with HTTP;
        Sat, 26 May 2018 18:47:51 +0200
Message-ID: <ac2f6239b66c27aa3598ea8d62d10a5f.squirrel@webmail.mathematik.tu-darmstadt.de>
In-Reply-To: 
 <CAOvivQzH2q8Y=p8pcK4R1sqe1SnCCN=amS=B99dMYZxZy+qL8w@mail.gmail.com>
References: 
    <CAOvivQxmrTLRW8wk7cu+A9zF3LCrXSfqsp6R2UN_sz9tF-5UHQ@mail.gmail.com>
    <D72B4DAF.ABAC2%psztxa@exmail.nottingham.ac.uk>
    <CAOvivQxMvZXcSA12xTorbDkJx5y_kngCiEsk_7+8132B8Q7XfQ@mail.gmail.com>
    <D72C2F89.ABB6D%psztxa@exmail.nottingham.ac.uk>
    <CACSS4jkJHOO9frDMCTmjELf8Lsnote3isPPbEN2NFhgErj+qXA@mail.gmail.com>
    <CAOvivQxf9Gq8dWO4LdTvw6KX7g1K=qkVWOA4Wcg1D_hnWbEZpQ@mail.gmail.com>
    <20180526092138.GA7067@mathematik.tu-darmstadt.de>
    <CAOvivQzH2q8Y=p8pcK4R1sqe1SnCCN=amS=B99dMYZxZy+qL8w@mail.gmail.com>
Date: Sat, 26 May 2018 18:47:51 +0200
Subject: Re: [HoTT] Where is the problem with initiality?
From: stre...@mathematik.tu-darmstadt.de
To: "Michael Shulman" <shu...@sandiego.edu>
Cc: "Thomas Streicher" <stre...@mathematik.tu-darmstadt.de>,
        "Ambrus Kaposi" <kaposi...@gmail.com>,
        "Altenkirch Thorsten" <thorsten....@nottingham.ac.uk>,
        "HomotopyT...@googlegroups.com" <homotopyt...@googlegroups.com>
User-Agent: SquirrelMail/1.4.21
MIME-Version: 1.0
Content-Type: text/plain;charset=iso-8859-1
Content-Transfer-Encoding: 8bit
X-Priority: 3 (Normal)
Importance: Normal
X-PMX-TU: seen v1.2 by 5.6.1.2065439, Antispam-Engine: 2.7.2.376379, Antispam-Data: 2018.5.26.163917
X-PMX-RELAY: outgoing

> Thomas, are you saying that the hard part is proving that the syntax
> of type theory is a CwF?  I always thought that was perfectly obvious
> and the hard part was interpreting the syntax into some other CwF.

That was a misunderstanding on my side. Correctness is also quite an issue.

But I thought you just discussed the initiality problem!
For this the laborious part is indeed showing that Lindenbaum-Tarski gives
a model. I mean this is intuitively clear and without any surprises.
If one is not overly formalist one is happy to believe this. I possibly
was more formalist those days (:-

But formulating the correctness in terms of a partial interpretation
function on raw syntax is a nice unorthodox idea. To perform it is also a
bit dull but getting the idea how to proceed took me some time.

If I had thought in terms of initial models for essentially algebraic
theories I wouldn't have proven my completeness theorem but rather relied
on algebraic and variable syntax as obviously “isomorph“.

Thomas