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=-0.9 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-qk1-x73f.google.com (mail-qk1-x73f.google.com [IPv6:2607:f8b0:4864:20::73f]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id e1c4a9bd for ; Thu, 8 Nov 2018 14:39:03 +0000 (UTC) Received: by mail-qk1-x73f.google.com with SMTP id 92sf38118568qkx.19 for ; Thu, 08 Nov 2018 06:39:03 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1541687942; cv=pass; d=google.com; s=arc-20160816; b=runb26vx/8lS9xqtirh942FxAeo6sLFr5iht1O4nyTNXM/PS7mglW6M9IycjfLnqQU gdMcIoA34RW75QAyljcRIS00dN4yqpDgd/c/emw7hmNPKxCWX+3KmmduTMvQEEc4ku6d G1a6WybJfzjyU0+qpQrPTQOCE4oE05wbxBzkD+QsCPgkfngBNz06LiuwR7vR4iFrTn2v fdaqSFQ5G/D424JIDdpvxG05UYE62X4kvk9wv+diXrXZobaANfCaWc4UtPrABRiTx8u0 wOVgFopZe5o4aU3kThkApp5hsAtx6kSt3otKJBWEgyWvwc2v8ouI6gZLzaG4jlKuVGO7 5LmA== 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:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:sender:dkim-signature; bh=oZ1HnnMBJBkaYluHXej72hQ0/hyMy/0KfFg1EKLoHuo=; b=b9Eisz1bI0YvldHYVToPGhSBT6XCC+HVyDkVhFAXdxM60XAxQXgpww9MK71foezcsx RON6oiLb29bwD2SIVzhVHKCFWYFKDz+FhQzcZZ0aH2lotNmL7/WaF1YBCj5gmYBGc8Kn VwLEMF0Y98Omql93C0mjDk0AhSZWc3OhBIG1Pf+PpPS2mynredoFHcOJ0WPTH4FPyz9V zfdoSXubCwJqDzALje3yCOKdaxNw47sMyY+sbIlIMsse5wkv2ae7UMkkDgsbE6kGPFuh 6bbG6Ijli79+sSnGlwCkoUqIoGBbgHr+hlkIMg0ob0+k1AWZcaQcyUWPB7Q1nCPDaEnu X0QA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=ENSNxzKz; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b29 as permitted sender) smtp.mailfrom=shulman@sandiego.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:references:in-reply-to:from:date:message-id :subject:to:cc:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=oZ1HnnMBJBkaYluHXej72hQ0/hyMy/0KfFg1EKLoHuo=; b=p6QmaSWgKE0rt2A85Ksaag/uUeSsG2b+V333lISFlM/IF54XB4fPORySxZ+Bu3R2ZP /MrP6kiNdhM1q5jyMoVWdo/g+pnuEccJSEcITpKqY6vwVElDGnTy04+/zLXPFSM1vEkV JWbGl5UJIFfP8l83AGaB5z5hXXcZKQrvQXRbSEDPbxKNY+IOsBZBuI1lLF0NaR0Wk0qf blu1NoC6nOyXO9kHmmbsEcyYp2CaCc82FbYytfl5dPaQBOoA/3NY5fiQcy0Bn2Kpglei NDff3XSKTDxVWfOJmqUyaYAA9lJmyWsSalAt4WmPTn3wARFlpmUjKtSiLQ5GRIVMaE2I 8/Jw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:references:in-reply-to:from :date:message-id:subject:to:cc: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=oZ1HnnMBJBkaYluHXej72hQ0/hyMy/0KfFg1EKLoHuo=; b=i59oR89OEkhqSb1PZ59986NcAKgMrpIdWrFY0kpFo+WnnlJSF3s4ii6f9ZJmVNJUmT F59t2HOS+LtaNV97Q6jdPT8MdHmDDZLgw5F0KZVbHYRazNFXUxg4QfJXU0jyQrZh6ndG oGmCVicCrPoLtPuzWgnIGtMp/uRGUOnGApw/usxwM4jE4jq1WOlAVISmsbOfPleL+bX0 W/2zhgycwGAMkypSOrcfzfTalHVPXJYzRfDULfiPfH9zZVxzvC+EUs2IrLMZHy5QsKiF 1JItdtSa9tzqaBfw0TQFUGyl5cpr6Fq79352u1hGnfEnvWRdAdVgcIa+Juq9SCN4/VDZ Bbaw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gIHWj60zg0THTcKC8WfNdXIVljEmC0E9DyU+rHMkV+/0m9A8HDT VvGo9Mhn95OtZBaM/R7xN+Y= X-Google-Smtp-Source: AJdET5cPcGbP7MMiULnNPqoLxZUJENsbf/eEzfe0a9jLZDl2bKtYbYS2MRLqx/Vd0BQN3PyFNC5YyA== X-Received: by 2002:aed:2a0c:: with SMTP id c12mr41444qtd.2.1541687942613; Thu, 08 Nov 2018 06:39:02 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a0c:b51d:: with SMTP id d29ls789786qve.3.gmail; Thu, 08 Nov 2018 06:39:02 -0800 (PST) X-Received: by 2002:a0c:bd9b:: with SMTP id n27mr2973186qvg.61.1541687942354; Thu, 08 Nov 2018 06:39:02 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1541687942; cv=none; d=google.com; s=arc-20160816; b=QwVACBxHrpYQE+8WE1CUPNVK2yMcHhQ4GjPNmzRcuPWYympaMOqGSjpW9J96v9PmTb VMuO8jP/xt3x9ssOCjObZkLDpwYL6oYSFz1SnmsJn0XWfpysNH0k6Q7GRJOn9tw63fa0 2t5ehOEDfhio8TKCOBIMZqiC0iirk1emgp4VGhXHtEsplx4ibfYaS/6BOsuYtsXefEie ahqhy5vQ/51jS7HeO+EwNgy7FUHcOKfa4ZmVtt8Zc0zNRoQhtbHDeV79LNucS+FEL4+A HIZMXdOI6jMCxasBQxGI9dL3lVGd0NJwUeHCa4PGaRWKa1gWxsLaKbdElkIQiSAo17BU h/rQ== 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:in-reply-to:references :mime-version:dkim-signature; bh=BJm/PKP90OdB1ZrSR1vd1hMt5Pp/Igbsv06bw0DsQx0=; b=cm5hSJdsDi8l9doZmVJZn8S7RfqQKMQmJyzGFtu+8yLQ9ClRr6lg3hyAtsPSkBr8p8 KW8XOfDhXsbvUEEP6RvgTASYcOxSmwxhrxFXXc0FVo5p0QuKWfJGj+pPf26ONp2qrlAG Cq6IkJ1HtJI2V96shmxHfBo0CpDdo06Xa6WdwGo1M2Y9jOcSDBAEEGYM24kVdREJiuUe duTyy351RjlI2QlnC3u6idLOYxQ2QYUSP7OKpxSPGZ81BEalJlUmBWg3/ZGIJEho3SoM 5H3m19SG5wcf/4CTu4j7L4xp1CZvKzG6D2kALz5LPYFmsnj/N6Ta+U5Xiu53kNInXw0T pGMg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=ENSNxzKz; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b29 as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yb1-xb29.google.com (mail-yb1-xb29.google.com. [2607:f8b0:4864:20::b29]) by gmr-mx.google.com with ESMTPS id 21si225862qkr.2.2018.11.08.06.39.02 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 08 Nov 2018 06:39:02 -0800 (PST) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b29 as permitted sender) client-ip=2607:f8b0:4864:20::b29; Received: by mail-yb1-xb29.google.com with SMTP id t13-v6so8387316ybb.8 for ; Thu, 08 Nov 2018 06:39:02 -0800 (PST) X-Received: by 2002:a25:a567:: with SMTP id h94-v6mr4718208ybi.362.1541687941632; Thu, 08 Nov 2018 06:39:01 -0800 (PST) Received: from mail-yb1-f174.google.com (mail-yb1-f174.google.com. [209.85.219.174]) by smtp.gmail.com with ESMTPSA id 203-v6sm1089209ywv.35.2018.11.08.06.38.58 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 08 Nov 2018 06:38:59 -0800 (PST) Received: by mail-yb1-f174.google.com with SMTP id i78-v6so8410782ybg.0 for ; Thu, 08 Nov 2018 06:38:58 -0800 (PST) X-Received: by 2002:a25:5a57:: with SMTP id o84-v6mr4480435ybb.458.1541687938390; Thu, 08 Nov 2018 06:38:58 -0800 (PST) MIME-Version: 1.0 References: <3c553ba0-2181-44ec-b790-969a8115ea1f@googlegroups.com> <1a3288ec-ca0e-48ce-80ad-9cad01f56845@googlegroups.com> <4ae4c745-a00e-4ebd-9de2-e29474b75d48@googlegroups.com> <20181107153556.GC26970@mathematik.tu-darmstadt.de> <20181108115815.GA5022@mathematik.tu-darmstadt.de> In-Reply-To: <20181108115815.GA5022@mathematik.tu-darmstadt.de> From: Michael Shulman Date: Thu, 8 Nov 2018 06:38:44 -0800 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Re: Precategories, Categories and Univalent categories To: Thomas Streicher Cc: Thorsten Altenkirch , Ulrik Buchholtz , homotopytypetheory@googlegroups.com Content-Type: text/plain; charset="UTF-8" X-Original-Sender: shulman@sandiego.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=ENSNxzKz; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b29 as permitted sender) smtp.mailfrom=shulman@sandiego.edu 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: , Actually, you don't need strict equality on categories to talk about strict Grothendieck fibrations in type theory: https://ncatlab.org/nlab/show/displayed+category On Thu, Nov 8, 2018 at 3:58 AM Thomas Streicher wrote: > > Thorsten asked why I prefer to have strict equality on categories. > The answer is that one needs it in category theory typically when > speaking about Grothendieck fibrations. > And the latter is most useful in many contexts in particular when > understanding geometric morphisms. This by the way also extends to > Grothendieck fibrations in quasicategories as in Joyal and Lurie's > accounts. > > 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. -- 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.