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=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-wr1-x43f.google.com (mail-wr1-x43f.google.com [IPv6:2a00:1450:4864:20::43f]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id d570e2c8 for ; Tue, 19 Mar 2019 04:01:13 +0000 (UTC) Received: by mail-wr1-x43f.google.com with SMTP id e14sf8518786wrt.12 for ; Mon, 18 Mar 2019 21:01:13 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1552968072; cv=pass; d=google.com; s=arc-20160816; b=rG8AmuFkFk2Q3mpV05wLZeFwxDPsj43TPT+oEnYFjw6WYpvkBf4SEGDeWHugIQiXo7 V3h0jInvHhEX2/ZlUtCC10zRtuCpblqd/RFwdotgwF0JxTbOjQkNGHX+gCDQid4TMPkZ J7pybF4DFlrV8MhXTvTffBI1xktsYlcOfKBBBJZq1DHvq3/aHaUCrsL6vj7nk9LHTY+O kgfIUq4edqpY5o7DFOfYASNrcoJftvMzRd1Z0nVGHM58kygHAT8awPvz9ot5mnce+Ko2 gyRFjpj8wCA2lhCOHs2vD69lrqG2qDSkTJm3ZoXWO+A+yHx5A6MGPZp1RbBUZfjDnztn WarQ== 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 :dkim-signature; bh=G8by/R4dcVmN6Rb76DPhyBZKauyDrr1sithTBrABWeQ=; b=k5BFXG4lTGsI16EJY9aEiEtBWQic8+qdGOnKH7PLv6kBn+0pJ6esU7wDelj7WRUPhW XTbzlUuXMFY+sdBT4F0py0f8XQWBp1qbUzRoUKMjEYNp8hYgkkA1Pu4gb1x0h/xaqrA0 Vr4f8pzO0ZoiHvQiEMnH7Qo1XyZFrceKEz61bB/hzRm0GcahWF55K28vNVOSAcmzFVKg zeRcQ6uzPCkeQCaKDJVCyMrRJp505eqNmI/vq/GanedU3IVKBXGgvyhbdEoHEoxhP8q+ GCbxSnHXDy5w5S9ECFd0fJZWf/S+BARSit4JRASp1B3vFj4Zo/NtaTycyPSEEBxdO7Hr /zgg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=LjjPbLkJ; spf=pass (google.com: domain of e.m.rijke@gmail.com designates 2a00:1450:4864:20::32a as permitted sender) smtp.mailfrom=e.m.rijke@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com 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=G8by/R4dcVmN6Rb76DPhyBZKauyDrr1sithTBrABWeQ=; b=F9VUJEPKJb0FGUljdDKVKnAkKlDijUqzd04GSrGfcqkrnUTmgsKSadVwF+edoiGmGP e4nwMhrXT5wJS3floCcMQWFvm934WJlzmafb46xKX2wpvinj+2WFZIIyYQblzGaLIoc6 /nzbTWIW9wtZbaAbrY4FOxLCoCPLDo4aa2/Yn6XW1kahrEpZLXjtuUjeiBwxvjfUVluX OpFPkNibJ/fP7qp+iJzOd6hgG1K8uU1/zMmi7qHdYODXqiMP13VIiaKKpEhDOKD0Vvue uluNK6jnMNOubSJqlj/pDphnmn61sHm9cbMIer/szVPuJIKcNlSoR1JH9xIhD6Xwmh7b I+5Q== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=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=G8by/R4dcVmN6Rb76DPhyBZKauyDrr1sithTBrABWeQ=; b=PidOfqDW5JAuLj1F3lBHwfNZ3ClqcNUy5bDbSntR73eK384g7Pho0bWDeSGC/E71P2 MyXXmsStc1TatXbJ93yU82gBOlrHH6dJgH54mjGGaBwIhNqi3Yj7T/w3Pki5JZgIYJZr atSF0M6hjWZ9BhUNtaZzJIkWNAUcYDlFDOJVQCoBqkFWi5kxWL107AKqq/+8MyRAy/fa lEpratSLl206k2D9Ng4cbqNtsjlEX4Rtpfw1zWyTGuqYqFZgrJdRpCJGNd9uyeoGWPUz nOoeHWhLxj4ZNkiAH/5ST9l44oz/Zbz/IOoCrIvIug8xh7Uo+bQKis0GpbpVObmQevIc dsiA== 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=G8by/R4dcVmN6Rb76DPhyBZKauyDrr1sithTBrABWeQ=; b=s23CyOYLbUU6+i+Meqy6G2PrNC1ZyJvaAR82N448qhPSSmOsQuvTRF9B+UAMCo6EVz WjuF9FiMtA4Hvg7s5/rw5+gcWFaleammRWjUWZec97EKmmyuMPqOSN2KQBgzaOQZVsdS wt+df0AoE5wQajRm1sZXU0C3DY2Z1bLhgbLv+cCXdKMkwddtJ1UGjDR+bG99RTDOxUUI Nn9mVOT+GKTdjlf8vLyeQN3A+h4wp9Jk1Tfd0VhrQSFIfXCAAKnfdhV7JEF4p5m85cZh r/8FPQhQ3YiwZqmKNF7cQhY4xPCQFzMVHrBTZ2ICo9U00oWZ2bTsuHJgIiXdgRVt00YV qVjw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAUboIKzQ/lli+6mIyJsfipsy91IAb1/urxuSdL3wKiM4cOZaKuk F4ieG1lLSjdzmm9dK1xkcew= X-Google-Smtp-Source: APXvYqyz1k3o2D9X6qG1DIUtqmvyvFLnVmUmRrZE4JOHh9f600vw0tdziwtjPFNs/WD09ZwH7SirLQ== X-Received: by 2002:a1c:730d:: with SMTP id d13mr1622569wmb.37.1552968072488; Mon, 18 Mar 2019 21:01:12 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a7b:c0cc:: with SMTP id s12ls221442wmh.14.gmail; Mon, 18 Mar 2019 21:01:11 -0700 (PDT) X-Received: by 2002:a05:600c:2110:: with SMTP id u16mr140320wml.11.1552968071883; Mon, 18 Mar 2019 21:01:11 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1552968071; cv=none; d=google.com; s=arc-20160816; b=PrdbPBfBzLOjM5CQN+8hpzGHYmNE3DYrc+CzmY1pZ4GC7v/OMBi0a3BR6gVqvaXfFC QFTigEjAflE1V1TTR5HdSxJYCfxhYMFd7T74wpOidMmakdH1ybjHRu/CFn59s5FZhMx4 EIGSexUJBjCEmnG9JYW+XrzfElDJJ9PoW/60dMIGJGZv0g9ALBawIPT+U12uERHdRXZI ndbo/gMuw0hu807fLnWqHDI8Y98j7SSYsKZ4QhZePb3cW+eMDwuR1a+aSVs6sOSUkmZL LC/VsjYvhCqN9ne1JPau/QB/diltgoidfGt+XurrS0B6eis/8GVmkOLbEUXciaYjikLU wCjw== 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=XfVr/BfU8pX7ireXnXwuXutW7qRM5JE8k+V17Bqy84I=; b=U8vUN6GkcwLd5JKb+TjJwtE7pB+CILhWIQ9BSsl6el0XyieKrcQYX7lCDrBgtKuvIN w/A+pIZWK83lUcKaAIZRw8At0yLdGABILwLkzaUM5SwozTyJFjj8yDjG3NyFGYH8RCg2 dUYKfMVEzdNJHa0ThvXfzVoSF1jpiuvKosjEMoR0hqhVc6RTlxQVou2CcZjDyZKTgVr7 zikPQ5/n58cmmFCwaZr4c+9ItIA+9nQlrqDyspxlursB8vui6RlyV0hpUvU37Y8NnwZp 1aMwFjqk1yx0nLY8HGAdo9bnltzPjRForW7FQkuypGCsZ0zCCHSTmDS5f/4JLVtEy/At i9zg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=LjjPbLkJ; spf=pass (google.com: domain of e.m.rijke@gmail.com designates 2a00:1450:4864:20::32a as permitted sender) smtp.mailfrom=e.m.rijke@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-wm1-x32a.google.com (mail-wm1-x32a.google.com. [2a00:1450:4864:20::32a]) by gmr-mx.google.com with ESMTPS id p4si77929wmh.0.2019.03.18.21.01.11 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 18 Mar 2019 21:01:11 -0700 (PDT) Received-SPF: pass (google.com: domain of e.m.rijke@gmail.com designates 2a00:1450:4864:20::32a as permitted sender) client-ip=2a00:1450:4864:20::32a; Received: by mail-wm1-x32a.google.com with SMTP id a184so1135670wma.2 for ; Mon, 18 Mar 2019 21:01:11 -0700 (PDT) X-Received: by 2002:a1c:e143:: with SMTP id y64mr1518747wmg.141.1552968071457; Mon, 18 Mar 2019 21:01:11 -0700 (PDT) MIME-Version: 1.0 References: <76b61890-3a9d-46c0-948b-454c2a7040dd@googlegroups.com> In-Reply-To: <76b61890-3a9d-46c0-948b-454c2a7040dd@googlegroups.com> From: Egbert Rijke Date: Mon, 18 Mar 2019 23:01:00 -0500 Message-ID: Subject: Re: [HoTT] Geometry in Modal HoTT now on Youtube To: Felix Wellen Cc: Homotopy Type Theory Content-Type: multipart/alternative; boundary="0000000000003f30b605846a8e42" X-Original-Sender: E.M.Rijke@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=LjjPbLkJ; spf=pass (google.com: domain of e.m.rijke@gmail.com designates 2a00:1450:4864:20::32a as permitted sender) smtp.mailfrom=e.m.rijke@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com 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: , --0000000000003f30b605846a8e42 Content-Type: text/plain; charset="UTF-8" Dear all, During my lecture on modal descent someone in the audience (my apologies, I forgot who it was) asked the question whether reflective factorization systems (i.e. orthogonal factorization systems for which the left class satisfies the 3-for-2 property) also characterize modalities. I thought this was a very nice question, because we have a theorem like that for stable factorization systems (i.e. orthogonal factorization systems for which the left class is stable under pullback). During the lecture I didn't know the answer, but now I do: It is indeed the case that modalities are equivalently described as reflective factorization systems. I wanted to attach hand-written notes containing the proof, but the files are too large to be contained in a message to this google group. I'll write it up properly soon. In particular it follows that the poset of stable factorization systems is the same as the poset of reflective factorization systems, even though there are subtle differences between the stable factorization system of a modality, and the reflective factorization system of a modality (i.e. under this equivalence the left and right classes have to change slightly). My lecture is available via the link Felix just shared. With kind regards, Egbert On Mon, Mar 18, 2019 at 11:53 AM Felix Wellen wrote: > Dear all, > > I just finished uploading the recordings of last week's workshop > > Geometry in Modal HoTT > > > to youtube . > I'm afraid the audio is not good, but with enough volume it should be > possible to understand everything. > You can get an overview of the talks on the abstracts-page: > > http://www.andrew.cmu.edu/user/fwellen/abstracts.html > > All the best, > Felix > > -- > 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. > -- egbertrijke.com -- 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. --0000000000003f30b605846a8e42 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Dear all,

During my le= cture on modal descent someone in the audience (my apologies, I forgot who = it was)=C2=A0asked the question=C2=A0whether reflective f= actorization systems (i.e. orthogonal factorization systems for which the l= eft class satisfies the 3-for-2 property) also characterize modalities. I t= hought this was a very nice question, because we have a theorem like that f= or stable factorization systems (i.e. orthogonal factorization systems for = which the left class is stable under pullback).

Du= ring the lecture I didn't know the answer, but now I do: It is indeed t= he case that modalities are equivalently described as reflective factorizat= ion systems. I wanted to attach hand-written notes containing the proof, bu= t the files are too large to be contained in a message to this google group= . I'll write it up properly soon.

In particula= r it follows that the poset of stable factorization systems is the same as = the poset of reflective factorization systems, even though there are subtle= differences between the stable factorization system of a modality, and the= reflective factorization system of a modality (i.e. under this equivalence= the left and right classes have to change slightly).

<= div>My lecture is available via the link Felix just shared.

<= /div>
With kind regards,
Egbert

On Mon, Mar 18, 20= 19 at 11:53 AM Felix Wellen <f= elix.wellen@gmail.com> wrote:
Dear all,

I just finished uploading the = recordings of last week's workshop


= to youtube. I'm afraid the audio is not good, but with = enough volume it should be possible to understand everything.
You can get an overview of the talks on the abstracts-page:

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail 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 &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit http= s://groups.google.com/d/optout.
--0000000000003f30b605846a8e42--