From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.1 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-wr1-x43e.google.com (mail-wr1-x43e.google.com [IPv6:2a00:1450:4864:20::43e]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 78f068b4 for ; Sun, 17 Feb 2019 09:43:32 +0000 (UTC) Received: by mail-wr1-x43e.google.com with SMTP id l5sf6302169wrv.19 for ; Sun, 17 Feb 2019 01:43:32 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1550396611; cv=pass; d=google.com; s=arc-20160816; b=jnsmiJjEzpsnM3htrf8gA8FVW12d5IarYCygjHgqcZ+C9qQC4xZ1rwqMhIURmedmMr BgNHn6da5RFNLl5xDfNecrgsvC3eG8ibPRMdxurnvz2nNUb3C5tRNy7Mz6iUI8S8X4oD iEcfaWsgPUnhj9XAZwD7ungUjFXWxeMcCyt+bsovWKmPRy5W5gSOQXHsh1clLwxmGF3A y2TR3a2Ruuf8rg7SAX/vX8gJDMlyvwpzyXHKfHXwFuAuuJsoo0CTmwSMZGbvGUmybmMU jHUiXmZyjUMCsaqQqtK4pyyanN7lHTQLopUCMGnx533Of1XYhfRTOyEQezBb5CMZwuAi 0Cag== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:user-agent:in-reply-to:content-disposition :mime-version:references:message-id:subject:cc:to:from:date:sender :dkim-signature; bh=eHaim2VXSnn81mb4vWcOKtSjmcWWhP5lJ6oN5TYshDU=; b=PUP3K4/IZXJz6YqFqwuiSJVdrQmzNfRxlH8tczMG/mwbRCAt2rrBPLQFF9z7u5swcq Uf1BYz79M/GKawBmAcNSopzffee97skWWnYB0s6bhoP29EmSusJxIPb3uYAcm/tOhriC fXGj6Cc14Hk584DgBWp52Rg36qIoRl/9KtKKauPqFXllCr4GUDZ6akPmEwlEWrmkojVU Tdz/7qnrVYY+UCuocx84FcpMkneiCfRZkm6K/flA1qEPuA/lzeer5LbfeURIANo/Jqh2 Y8UBI+gIt/pTNDv5+23BVmkwlllKdA32jKhf+vAiGuOES37mTkv8Oivw172FdnILBpqQ jr/A== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=pass (google.com: best guess record for domain of streicher@mathematik.tu-darmstadt.de designates 130.83.156.231 as permitted sender) smtp.mailfrom=streicher@mathematik.tu-darmstadt.de DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:cc:subject:message-id:references:mime-version :content-disposition:in-reply-to:user-agent:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=eHaim2VXSnn81mb4vWcOKtSjmcWWhP5lJ6oN5TYshDU=; b=OYZXXwAv2xn0gn9IPNm4f3MANtU32l7VmlDouhwtf95B7cOdEj1VzH5bcxeE8ALdYg vGa7XOA6t9JKdReYYUZ4xfhsh3EsfoVIIUCyZrF+Ai9ZsNMu53JGFPzvsxrzMXHZluMb TMPKcmFR27rpOlX+5HybCkBs22s72kuErpmtW3kVk9hgubBaTp9UlnR4H0y9SmQ8lz9C QdOMWsC8r9RvC0O0RFBLqGhvCnYEzjMrIFlP4acap1jgC16//M2zlgc06LDeS0blWmTz M6cC+iIuzI8xsN6689+JjKWxX6hOFqJsiCLaTh7KXxNJwVhWk+5jaVjy7ljYpBAE2tVq VAYg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:cc:subject:message-id :references:mime-version:content-disposition:in-reply-to:user-agent :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=eHaim2VXSnn81mb4vWcOKtSjmcWWhP5lJ6oN5TYshDU=; b=I/X9qacSG6R/ul7Hq4YZ6QaVrFMt3sPnVMFQewpC+DohoCwjrf8yz0FN4ZQxsoeQnU eCCTaGQavWyCPZIEdateXE3koDmyy5gfNsGgVH6FmFMAYxost7yaEDHWPn3FO7DxiXgT /dLfRHEdPD62hPkDXdyrJ1zdwu4nN5ZhAVwa0kaAGLtUssOrBdGHAw+NgMBOFXQawWOc BZXyzn9uvaDP5tEk8xqID6wGQw/Elu+/2EbKBLZkHz1nY5mSJAW+z5G2OSPwrDtbIwsP xsF0f6h+mToNRZMj+8jEsRqNSxE6C+2rXbf/oyRk3FVpj7hVhJOTl55DJ9sjpoPOFTBm orsg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAubZlmKiqGVlQYB+NOXIZQ1jnBF+sH39RsqQ9hBNHjQiXK4YAHSW c0j4nQQQ+m8E1vCTFAEOJdU= X-Google-Smtp-Source: AHgI3IZgeZ0eZk9Rlx/6xcQZ1nY7Ze8roS2wd/UbyxPnByu9fimiGghvOP01pmBzxuT8Z4aBw0wq2Q== X-Received: by 2002:a1c:2dca:: with SMTP id t193mr110959wmt.2.1550396611502; Sun, 17 Feb 2019 01:43:31 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:f209:: with SMTP id s9ls1308866wmc.12.gmail; Sun, 17 Feb 2019 01:43:31 -0800 (PST) X-Received: by 2002:a1c:9c93:: with SMTP id f141mr1076682wme.10.1550396611008; Sun, 17 Feb 2019 01:43:31 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1550396611; cv=none; d=google.com; s=arc-20160816; b=kNf3MyrLbs3QHUgCIv/uEyErigVr/W9bGNhJ3ElpwBRri9zCzFZ0tCSa39l7F2nKWE W0DKmssDkP4w5rHHTuXIdpmXoMCr6hKKQHaKm6CK/IxeCmDiTmHo552BFzCaXw/EE9Nm JifztKqHjx/xvOOujCqs03IZM5gZFrvr2KBWT0PCZMYxDlvgeTcCHFTdk4C7hB+r+QIt g5cot2cSHkwePhHVl9La+mxqVaajM6onRhGalHjHvf1/oqiisyWxkBOkKk9wQDICPogm dyAmaD0zRj3LGrJP4cRykftXlqlw3etRSUjlci1KUxH90bC5hbjf63W4oqftMBs5HUuv F5AA== 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; bh=eV/DThuz49HHLfBrWx8WfPAM3dGe2tTlsgvM4Cjpbdg=; b=eGQd1NMqjDQ4OzAfSD3g1ve/jYspsDDmg49XpjB/2BJPSObCmBRTcNpckrNwnSduYR rXch0AZEfCgXPyoVoAa0mJ6TcawRUVbMc+GV5LWMLMaqsU+YNPrOpp1cF8wuEq3pMyX/ rH5+D1HOaU9HGM1z93UUxcjkcjy7WYMxM+rC99kAm02IEgifG4VkvTVTmKVFTE/44olN OoumRQVM2kTwQUz3+/DEo6B7RbSukJ42CIgWmV/5iL9wEEHOwrDu0iSAGioz2vyWxoPo BpP2NQgGbUaUeglaWFWGHNcVjBI9NI6j8epkWUy2uGbvY1cmJO3XeMdz25sEc136rHuA s18A== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: best guess record for domain of streicher@mathematik.tu-darmstadt.de designates 130.83.156.231 as permitted sender) smtp.mailfrom=streicher@mathematik.tu-darmstadt.de Received: from mail-relay231.hrz.tu-darmstadt.de (mail-relay231.hrz.tu-darmstadt.de. [130.83.156.231]) by gmr-mx.google.com with ESMTPS id t23si663345wmt.1.2019.02.17.01.43.30 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 17 Feb 2019 01:43:30 -0800 (PST) Received-SPF: pass (google.com: best guess record for domain of streicher@mathematik.tu-darmstadt.de designates 130.83.156.231 as permitted sender) client-ip=130.83.156.231; Received: from fb04281.mathematik.tu-darmstadt.de (fb04281.mathematik.tu-darmstadt.de [130.83.2.21]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (Client did not present a certificate) by mail-relay231.hrz.tu-darmstadt.de (Postfix) with ESMTPS id 442MWQ4wPtz43ps; Sun, 17 Feb 2019 10:43:30 +0100 (CET) Received: from fb04209.mathematik.tu-darmstadt.de (fb04209.mathematik.tu-darmstadt.de [130.83.2.209]) by fb04281.mathematik.tu-darmstadt.de (8.14.4/8.14.4/Debian-8+deb8u2) with ESMTP id x1H9jKhc022867; Sun, 17 Feb 2019 10:45:20 +0100 Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003) id 75F15C5D3E; Sun, 17 Feb 2019 10:43:30 +0100 (CET) Date: Sun, 17 Feb 2019 10:43:30 +0100 From: Thomas Streicher To: Steve Awodey Cc: Michael Shulman , Anders =?iso-8859-1?B?TcO2cnRiZXJn?= , Homotopy Type Theory Subject: Re: [HoTT] A unifying cartesian cubical type theory Message-ID: <20190217094330.GB3415@mathematik.tu-darmstadt.de> References: <6F861453-7F0E-4FD3-91B7-378B8ED25D7F@cmu.edu> <4d63c003926b2c19e530c107c5b141cd.squirrel@webmail.mathematik.tu-darmstadt.de> <20190216195136.GA11255@mathematik.tu-darmstadt.de> MIME-Version: 1.0 Content-Type: text/plain; charset="UTF-8" Content-Disposition: inline In-Reply-To: User-Agent: Mutt/1.5.23 (2014-03-12) X-Original-Sender: streicher@mathematik.tu-darmstadt.de X-Original-Authentication-Results: gmr-mx.google.com; spf=pass (google.com: best guess record for domain of streicher@mathematik.tu-darmstadt.de designates 130.83.156.231 as permitted sender) smtp.mailfrom=streicher@mathematik.tu-darmstadt.de Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , > I don???t want to minimize the importance of the work on cubical type theory > ??? which I believe is very great ??? but it has focussed on building models of type theory > directly, often within other type theories, rather than on building Quillen model categories. > To be sure, many ideas, and some terminology, from model category theory are used, > but without showing or even claiming that there is a Quillen model structure. They didn't emphasize model structures but they are around and more explicitly in Sattler's work. Admittedly, there are sometimes distinctions which only make sense if the meta theory is constructive. But if one ignores that then they are interpreting syntax in minimal Cisinski model structures defined by open box filling conditions. One does know that minimal and test model structure fall apart when taking as site free finitely generated de Morgan algebras as shown by Sattler. It is unknown when taking the "cartesian site" of finite lattices and monotone maps between them (opposite to free finitely generated distributive lattices and homomorphisms). I agree that in the published papers on cubical TT the model category aspect is not shown bluntly but Thierry is aware of it and it shows up in Christian's work quite explicitly. Moreover, I think it is not important to choose the minimal Cisinski model structures as one can interpret Cubical TT also in the test model structure on cubical sets. There are fewer fibrations since there are more anodyne cofibrations but when interpreting syntax one stays within this more restricted collection of fibrations. The only problem with simplical sets is that finite powers of the interval are not representable. That's overcome by choosing the cubical site. But one may still restrict fibrations to those of the test model structure and one gets the simplical set model when restricting the fibration to simplicial sets. Thomas PS Thierry insists on constructing models in constructive meta theories like CZF with universes or extensional type theory with universes. This has the benefit of obtaining conservation results but is not necessary for the interpreted theories having computational meaning. The theories have their computational meaning independently from the models they are interpreted in. -- 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.