From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a24:b91b:: with SMTP id w27-v6mr2110641ite.41.1527398102311; Sat, 26 May 2018 22:15:02 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a6b:4f03:: with SMTP id d3-v6ls73546iob.2.gmail; Sat, 26 May 2018 22:15:01 -0700 (PDT) X-Received: by 2002:a6b:3956:: with SMTP id g83-v6mr4080552ioa.59.1527398101613; Sat, 26 May 2018 22:15:01 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1527398101; cv=none; d=google.com; s=arc-20160816; b=roCIjwu5r3lL8oZ/TfFe7qJ+xVzMCG7xPUSHCheAHWlITxlWnnri4bNy0wJqhfUuB9 xD2VCl8+sbsl4ViZgX1nv+wKymWue41i8XS6SnSElT/vUCCJrsD34Z6cRcyD9kdFV7hE DfFiRVzGqU0TKn1XMt0GHx3TLw3JSNEcXdD2A0x35afc2JumKITzKFUqCF1047G66gHw bkaEDvgt+ZLdzT2CYq/1YFcmXhUztAhnMweUYZlXSDQHdpFkZkZtCi7inTnYTLwTvt+j BFeyY79t30veqck+xY6msJ3bcKJgrTIESCVrdGWX9xg4yk34aNiyvZxUm9rl3GakcDlV aplA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :references:in-reply-to:mime-version:dkim-signature :arc-authentication-results; bh=pHlEugkSk7N3rMR9xaADD+hYDkWYsiUayNKpn1V6GYc=; b=Vp2OI6HLkZxiEwe11XbrGVXEiadC4H3cnGyhrMH2su6K9qWu+GjylX4XhlnwGZg53w JmuMvtzKqPYCT0tq8YPtr0h80waNro5peX2ua5o6QletnsPZVNB/Jcg3sRCEmnL3jdvd WSbiblHx6Dq0XrHLOz1jsYkevBdnuH0lh+ZMOz5/yzzVmCOYAU8IAQKgyRwSDDRlTU/P pYzlKPToNaozcoWQZWO3GfopE7w1l1S2iKd62rQCaJCxgV+W33UQFWyZiyVkV5ZFkCbt HuBB2V7ijCTZRMer92MS4I7ZJ0lLO0XKHVW+wyNFRC5Z04egZO63p1q91hL8p1dde3/t ZT1Q== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=lF5kfl2b; spf=pass (google.com: domain of b.a.w.s...@gmail.com designates 2607:f8b0:4002:c05::236 as permitted sender) smtp.mailfrom=b.a.w.s...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-yw0-x236.google.com (mail-yw0-x236.google.com. [2607:f8b0:4002:c05::236]) by gmr-mx.google.com with ESMTPS id o70-v6si76662ito.1.2018.05.26.22.15.01 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 26 May 2018 22:15:01 -0700 (PDT) Received-SPF: pass (google.com: domain of b.a.w.s...@gmail.com designates 2607:f8b0:4002:c05::236 as permitted sender) client-ip=2607:f8b0:4002:c05::236; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=lF5kfl2b; spf=pass (google.com: domain of b.a.w.s...@gmail.com designates 2607:f8b0:4002:c05::236 as permitted sender) smtp.mailfrom=b.a.w.s...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-yw0-x236.google.com with SMTP id b125-v6so3964ywe.1 for ; Sat, 26 May 2018 22:15:01 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-transfer-encoding; bh=pHlEugkSk7N3rMR9xaADD+hYDkWYsiUayNKpn1V6GYc=; b=lF5kfl2b9/3z8V6Sx4ui/LmK2gIOIY9X1lxyD+bsOwwwXLyeHA9D8fE0ooe5kN0NDS 4GaJutsGXWnsQ7S1pqHLHBQag4F0Qn8B+ebiPOhsCd+UtCtc2kYXU4xV/c+6ZJaOZk/2 aBMRqLATVpTuvps8FFOCY2GWI02hE/Bq0jBBliTFg9TsTTdaJ5L+9P8VMTobRBAKKGJR iLI/waqn5WbUQRVcmjJZIVqE5AckgEfZJ6vuve1pL4+ZKOnoEujeXpQdqtotidahR9w+ ztzlZkrZV0KgU5nsR0lThiOxHVrtGjm96rsD7RauJI2tssHWI4mzPgewYTxL8FcrfrDS kdpQ== X-Gm-Message-State: ALKqPwcDRzMVUxKp7GE2HbpMVCG5r57aP6IpOVP+e2fgEgsj5+QiAOkT 7WZLT5m46pDUVzM4tETtLCDscZkEQOOm6iBItqc= X-Received: by 2002:a81:9e4b:: with SMTP id v72-v6mr377845ywg.201.1527398101150; Sat, 26 May 2018 22:15:01 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a81:80f:0:0:0:0:0 with HTTP; Sat, 26 May 2018 22:14:40 -0700 (PDT) In-Reply-To: References: <20180526092138.GA7067@mathematik.tu-darmstadt.de> From: Bas Spitters Date: Sun, 27 May 2018 07:14:40 +0200 Message-ID: Subject: Re: [HoTT] Where is the problem with initiality? To: Thomas Streicher Cc: Michael Shulman , Ambrus Kaposi , Altenkirch Thorsten , "HomotopyT...@googlegroups.com" Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable One question that recently came up in our work on modal type theory, https://arxiv.org/abs/1804.05236 is: what is the right notion of morphism for CwF. In the paper (def 9, thm 10) we propose a notion of weak CwF morphism, where comprehension is only preserved upto iso. The notion fits well with the local universe construction, but I hadn't seen it before. Peter Lumsdaine later told me that it sees CwFs as discrete comprehension categories and where one uses pseudo-maps of comp cats. I also noticed that the literature on categories of models of type theory seems quite scattered (I guess this complaint is due to Vladimir). We know how to translate between different models of type theory, but I don't know of a convenient place to find all the functorial properties. On Sat, May 26, 2018 at 6:47 PM, wrot= e: >> 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 issu= e. > > But I thought you just discussed the initiality problem! > For this the laborious part is indeed showing that Lindenbaum-Tarski give= s > 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 =E2=80=9Cisomorph=E2=80=9C. > > Thomas > > -- > 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 HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout.