From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.202.60.85 with SMTP id j82mr11875875oia.85.1520457629752; Wed, 07 Mar 2018 13:20:29 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.41.245 with SMTP id g50ls1522549otd.18.gmail; Wed, 07 Mar 2018 13:20:28 -0800 (PST) X-Received: by 10.157.44.193 with SMTP id e1mr13106650otd.109.1520457628824; Wed, 07 Mar 2018 13:20:28 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1520457628; cv=none; d=google.com; s=arc-20160816; b=jkgrxITD47O09onL5iyB1it11pJwkWJ7QtohPtlAV7B+I7ktyVIDPnvoU1tnLqSvCK sB244LVngaepuO154by+Bn5aFB7It+f8lqIuNCm+J+pjFQPktFiqMeL7UQhVxpNc0zBK KCInXkfiFUGYOeAw3DPJg0mtwXJWArBssfBLWybU6y3z3oPb9QbWvkEtXAXNBeLHck7h S3tfmg/UrdCV9k1DRhUQfS/OwAOhrbmgJjvJ4vw9n+Mv1ik4zB/bQTFvVQvmx/pcxQub H67Mq+DgSn8ltR2uDUJbfw4T04K0MMzFa5lrYMhZ3h09MOXUCGkx0MB4+iXmbzNe6Pkz RFtg== 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=kvxzDoL622+Dk5+kuIgpOd3qSUu6/u5PSDhSL20iH0A=; b=hYvdAkHILAUMdsKWMVrHpp/GknUDBMNWRDSRR4yPQ6fZ0WGmvNQBytTNuWV7ckfqZu UhWO6X5BBFhQSugURSMpvBtblI7+rw98vQZV3guvMWeAN2/rUQ5fgUzhsJ+xmrCXi44l nDBVuRU9J+5GLN9oFRa/u+8WLlIvFwTUEcjpo+f9cys80Ngl/2xYUgzPcr/6A+SEeN8w V6DWHBLYaUkRasagaRoQpotaJxU7tACOkbH78B3P6jUuv9AqHCLjDqlJvF2A7NalwwXC giWKxhFyWaggAikWBdTz2QAr8gRrnhACLQ48iEhJf9Zeag8Bz+65TXf+MrEe/fCYPf1z 22zA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=yKUgELVx; spf=neutral (google.com: 2607:f8b0:4002:c09::22c is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-yb0-x22c.google.com (mail-yb0-x22c.google.com. [2607:f8b0:4002:c09::22c]) by gmr-mx.google.com with ESMTPS id e51si1564474otj.4.2018.03.07.13.20.28 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 07 Mar 2018 13:20:28 -0800 (PST) Received-SPF: neutral (google.com: 2607:f8b0:4002:c09::22c is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4002:c09::22c; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=yKUgELVx; spf=neutral (google.com: 2607:f8b0:4002:c09::22c is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-yb0-x22c.google.com with SMTP id v8-v6so1292143ybk.6 for ; Wed, 07 Mar 2018 13:20:28 -0800 (PST) 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=kvxzDoL622+Dk5+kuIgpOd3qSUu6/u5PSDhSL20iH0A=; b=yKUgELVxxckfZUahoUciL75t/tbgMHlWszWwqJDFqXv5YjFynjldla5nyhQAJbAIwg BYOqI+jZtbyTnYYzXdxU0fGPjTHzzks+r6uHc9yIhve1TxiPNNFdp4c5ophTa4DcZKIy 4lUdrC0OswVF7Q6zDV6YtDexB7LhKZpBegWUgG7sL8SSzP0OZh9D+RyResLGFqFAFy2h FqpNEAvb5BEbVuAkENriUBsp5A/9UdeDh8bXUT74s2vc66lCDFE43IBukRdA47fsZtl1 9NOtmHgoos+3iUmCUUZWlabWnudExpuMsOFOGXkikppZm/ebE76JoLct7HxS2gfyOwrz axSg== X-Gm-Message-State: AElRT7HIh+4I7xuvHO5SjGUb+ubaapmPNdpU0HI7nWyySiQ5R7EZpyNa XDwWuca3TxT1DW8K14ogg2bnFBu/ X-Received: by 2002:a25:a145:: with SMTP id z63-v6mr3896609ybh.96.1520457628510; Wed, 07 Mar 2018 13:20:28 -0800 (PST) Return-Path: Received: from mail-yw0-f173.google.com (mail-yw0-f173.google.com. [209.85.161.173]) by smtp.gmail.com with ESMTPSA id n2sm7292622ywl.41.2018.03.07.13.20.27 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 07 Mar 2018 13:20:27 -0800 (PST) Received: by mail-yw0-f173.google.com with SMTP id p70so1259762ywg.10 for ; Wed, 07 Mar 2018 13:20:27 -0800 (PST) X-Received: by 10.13.216.194 with SMTP id a185mr15579051ywe.193.1520457627368; Wed, 07 Mar 2018 13:20:27 -0800 (PST) MIME-Version: 1.0 Received: by 2002:a25:86c2:0:0:0:0:0 with HTTP; Wed, 7 Mar 2018 13:20:06 -0800 (PST) In-Reply-To: <20180307203003.GA11083@mathematik.tu-darmstadt.de> References: <20180307170902.GA5070@mathematik.tu-darmstadt.de> <20180307203003.GA11083@mathematik.tu-darmstadt.de> From: Michael Shulman Date: Wed, 7 Mar 2018 13:20:06 -0800 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Categories with 2-families To: Thomas Streicher Cc: Peter LeFanu Lumsdaine , "HomotopyT...@googlegroups.com" Content-Type: text/plain; charset="UTF-8" On Wed, Mar 7, 2018 at 12:30 PM, Thomas Streicher wrote: > But if you specialize the interpretation of type theory in > comprehension categories to discrete ones you wan't be able to > interpret terms (since the latter are interpreted as morphism in the > fibers, namely as sections). I've never heard anyone say that terms are interpreted as morphisms in the fibers. For one thing, that's only possible if the fibers have terminal objects. It's true in the natural semantic models that a section of the projection G.A -> G in the base category is equivalently a map 1_G -> A in the fiber over G, and also in the syntactic model if you have a strict unit type, but I've never heard anyone suggest that for a general comprehension category (necessarily with terminal objects in the fibers) the "correct" way to interpret terms is as morphisms in the fibers rather than sections in the base. And I'm very interested to hear you say it, because I recently came across an application where this *does* seem to be what I want to do, but I was hesitant because it was different from what I've heard everywhere else. Is there a reference that takes this point of view? > > So I am not sure what you mean... > > Thomas