From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a1c:32c1:: with SMTP id y184-v6mr463023wmy.4.1527326502206; Sat, 26 May 2018 02:21:42 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:adf:98f6:: with SMTP id w109-v6ls8704260wrb.2.gmail; Sat, 26 May 2018 02:21:41 -0700 (PDT) X-Received: by 2002:adf:e387:: with SMTP id e7-v6mr432305wrm.9.1527326501315; Sat, 26 May 2018 02:21:41 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1527326501; cv=none; d=google.com; s=arc-20160816; b=bBDNzWpXI8vkJlJIeLF6xy+3WqHomLlR514kjMn2ow3QYaR9bakEM+QGV6wdwPF31l d2fl0JyLwzJBye3Q9SN38koDjXsyxgsYb2uLnpVWFNXpHRbVm/Ltxk+0zAQXoTsgxbV9 aQnLDP5crtmTPgIYkeQHEaU62YlgzXr8x5sid28pD/dFoKcBImh/3kJjxmyb0eD6+WIH 19yIIKMT1xBcxoW3vAkJKYmlRRK0WeFaCgYIBg4IW3ZZH0+W4D/J4DC8dLyvUC3ReEtc sPadiv3wxUt3LmFPhJ5+P77WzeOJkz2TumXL+J0oATV8Htty7Co5N+7R42mSlNmO3xk2 Erjw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=user-agent:in-reply-to:content-disposition:mime-version:references :message-id:subject:cc:to:from:date:arc-authentication-results; bh=+gQI9g5M3/bAlHgvQMlxvOPXz4vkyAYdDnP6b31pW28=; b=C7LkZyG15+2UD3jMEsoKbQCejSmVEzVjEilXDmnB9SxQPUX9BDBcyqWYpwUbF+dMZ6 DYf+ymlfCueYheYd0yBxSeROkSLCKWy2gOZr+T8Zw8KMKVznKIx12bfUpKI1NSbRwmlx wlb9um/ROSZv3nqoMLAr1VZn05O0/RD4LIbGPnncWdUdEeEwaeZpsz6S83V71175NUJm L/XddsR4/7vKniobz2H3wPIfgNORn4fjlKYiDwPl9TUxM8S7neVTwu98E75pm1S46Z8J W+CYLqajJ/PJKH2/vmi26k+6dZe5XGpseZQ1FrblCDroh4R+Y+i3PiG3ZsTUWPFwNkvz Zirw== 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: 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 g12-v6si645753wrm.4.2018.05.26.02.21.41 for (version=TLS1 cipher=AES128-SHA bits=128/128); Sat, 26 May 2018 02:21:41 -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 w4Q9L7q3031122; Sat, 26 May 2018 11:21:07 +0200 (envelope-from stre...@mathematik.tu-darmstadt.de) Received: from fb04209.mathematik.tu-darmstadt.de (fb04209.mathematik.tu-darmstadt.de [130.83.2.209]) by fb04281.mathematik.tu-darmstadt.de (8.12.3/8.12.3/Debian-7.2) with ESMTP id w4Q9Ldi6022344; Sat, 26 May 2018 11:21:39 +0200 Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003) id EF0211A0B66; Sat, 26 May 2018 11:21:38 +0200 (CEST) Date: Sat, 26 May 2018 11:21:38 +0200 From: Thomas Streicher To: Michael Shulman Cc: Ambrus Kaposi , Altenkirch Thorsten , "HomotopyT...@googlegroups.com" Subject: Re: [HoTT] Where is the problem with initiality? Message-ID: <20180526092138.GA7067@mathematik.tu-darmstadt.de> References: MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: User-Agent: Mutt/1.5.23 (2014-03-12) X-PMX-TU: seen v1.2 by 5.6.1.2065439, Antispam-Engine: 2.7.2.376379, Antispam-Data: 2018.5.26.91516 X-PMX-RELAY: outgoing Triggered by your mails I have tried to recall what I think has to be shown for verifying the initiality conjecture. Given a type theory with its catgeorical semantics we can construct 2 models M_a and M_s where M_a is the initial model of the respective essentially algebraic theory and M_s is the Lindenbaum-Tarski model obtained by factoring syntax modulo provable (judgemental) equality. Then we have homomorphism h : M_a -> M_s (by initiality) and h' : M_s -> M_a (essential the interpretation function for the theory in M_a). Trivially h' \circ h is the identity. For showing that h \circ h' is the identity one essentailly shows that interpreting syntax in M_a and translating the result back to syntax with variables is the identity. This last step should be a straightforward induction over syntax. Thus the main task is to show that M_s is actually a model. This latter task I performed for CoC in my old Thesis. This is fairly tedious when performed in detail. When I wrote my Thesis I didn't think about M_a at all. Instead I used the obvious fact that interpreting syntax in M_s just amounts to taking equivalence classes modulo provable equivalence. This suffices for obtaining the completeness theorem I wanted to have. That M_s is initial is then sort of obvious since M_s is term generated and interpretation of syntax gives a morphism from M_s to any other model. So summing up the key is to show that the Lindenbaum-Tarksi construction gives rise to a model. Thomas