From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a65:62d7:: with SMTP id m23-v6mr1065798pgv.34.1527335280030; Sat, 26 May 2018 04:48:00 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a65:5a0e:: with SMTP id y14-v6ls456600pgs.0.gmail; Sat, 26 May 2018 04:47:59 -0700 (PDT) X-Received: by 2002:a65:6391:: with SMTP id h17-v6mr1054541pgv.104.1527335279050; Sat, 26 May 2018 04:47:59 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1527335279; cv=none; d=google.com; s=arc-20160816; b=Sc/dk0bz7i5yblX1X6IrFDuzzEAVR3ZAIDchANmmev/pNgP7hQEClKd1jqBpRjcYBg nW/XNIOwG9RrYZs/wf5uLx5SIjxQh7l/ph9OLzmmFHQjiMar7Z/c/YH6+JXQn95l6Hqm HENC/B9RxAgcek1sCfM7l8MjY3mMERocSt+dW6UIW2lum6cOhLReh2N9HE9ZPbgMMhjc wbX22UTygIuZQM/n0E79DVCDCvgYKzJWUK3tfqopGWvSOJETbSlimgE9JocpRdmZO4Yb 2bwvKGhS/Xz1hpJY3bxLHwWq1uNJ1iaC8uZLPBMVdpQbihWjk+y94FcgNlItP/Sih/D+ Beiw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:references:in-reply-to :mime-version:dkim-signature:arc-authentication-results; bh=GPb4f00Yk0qNfu3soN6CPsEbF+1jRiYvTqneFpqVsX8=; b=f7XZooCA1nxr6soldcutL/w0PCXovZSjBMzOaCqdca3+huVRjSx4LrpeAeCyaYiVFr 8RUjYtEqoHys5O3WKxkwi8RnDoejlD7BJr+nxkRAi9DhTvlLaosN522OrK2U+iUnVvp7 NQ5nVSDpHYJtk9rS/8g9V+Bozj8bFYXVgdkyAlabMabrQKdKiefvbiengCwB9d6fGpWa 1UsJpQ7CLnqf8aOV8aB6hv4NTqAHNZGy8EPG9r1H8KGpNbNT/M8b5HhTZaVnyGbKfyKL 9jIKp46Lp0sRb6BWIgt2+d8obeDBJaYcoSvIpDpbnLkr47PtQ0Bw3QY6r/aaV1pqMtZD NFEw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=yfrwcL4L; spf=neutral (google.com: 2607:f8b0:4002:c05::234 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-yw0-x234.google.com (mail-yw0-x234.google.com. [2607:f8b0:4002:c05::234]) by gmr-mx.google.com with ESMTPS id o63-v6si1327017pfg.4.2018.05.26.04.47.59 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 26 May 2018 04:47:59 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c05::234 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4002:c05::234; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=yfrwcL4L; spf=neutral (google.com: 2607:f8b0:4002:c05::234 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-yw0-x234.google.com with SMTP id v68-v6so2541863ywd.3 for ; Sat, 26 May 2018 04:47:58 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=sandiego-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=GPb4f00Yk0qNfu3soN6CPsEbF+1jRiYvTqneFpqVsX8=; b=yfrwcL4LZCcSoTv7Q/2/6uKS4p2z8p4yLiJrDP+FVlJcgno7y1a05OnLMxDD8amoTu OkUrrZ1zwB5vuPWft/HstMyYQhAjvcpuhIlxZk4MzCUsE27b2vzhtLK+rUqj7a9/L9pX kuvIZtjUcSfa5R2IOtiFM/uVxKhseUYIx9G0G3/xTZy/IcDdYfas4ugC4z/u1LomrwZp TDhVFAOxYMkw74GMoMacRt0ZZORLgtyF5Y+TF9yXgbAPgGjB8I2NAi8pQzhknXZdppLf wzbwPHR4huDghnC1kMo9SZRIxlTt60CUrOjX3ScnO/bFpapAm4Cdu5Yv4nR/TiYgCQ2a SQXA== X-Gm-Message-State: ALKqPweuqM22k+Zujjtghn9QQBHp4nbdFoJOAXm71juSatDreeERePrD 3ngh/Tt3IK91f5xdoyPcQYkVoRQZ X-Received: by 2002:a81:5606:: with SMTP id k6-v6mr3354960ywb.512.1527335278098; Sat, 26 May 2018 04:47:58 -0700 (PDT) Return-Path: Received: from mail-yb0-f169.google.com (mail-yb0-f169.google.com. [209.85.213.169]) by smtp.gmail.com with ESMTPSA id q124-v6sm10319127ywh.78.2018.05.26.04.47.57 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 26 May 2018 04:47:57 -0700 (PDT) Received: by mail-yb0-f169.google.com with SMTP id p22-v6so2681140yba.13 for ; Sat, 26 May 2018 04:47:57 -0700 (PDT) X-Received: by 2002:a25:d885:: with SMTP id p127-v6mr3308137ybg.290.1527335277221; Sat, 26 May 2018 04:47:57 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a25:d2ce:0:0:0:0:0 with HTTP; Sat, 26 May 2018 04:47:36 -0700 (PDT) In-Reply-To: <20180526092138.GA7067@mathematik.tu-darmstadt.de> References: <20180526092138.GA7067@mathematik.tu-darmstadt.de> From: Michael Shulman Date: Sat, 26 May 2018 04:47:36 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Where is the problem with initiality? To: Thomas Streicher Cc: Ambrus Kaposi , Altenkirch Thorsten , "HomotopyT...@googlegroups.com" Content-Type: text/plain; charset="UTF-8" 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. On Sat, May 26, 2018 at 2:21 AM, Thomas Streicher wrote: > 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 > > -- > 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.