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-ot1-x33a.google.com (mail-ot1-x33a.google.com [IPv6:2607:f8b0:4864:20::33a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 90d02f79 for ; Tue, 8 Oct 2019 15:07:18 +0000 (UTC) Received: by mail-ot1-x33a.google.com with SMTP id d12sf7730150ote.0 for ; Tue, 08 Oct 2019 08:07:18 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=o+/SuXNKFDz9wGAUKORSW4yW+GsYKdtuZfdOd2vGwMY=; b=sJUQJxT95VLdqd4Dxco7ZXUNtUIdyjQytY2Vg+3KodlSiffhYY45P9AAwsRfOk4U7Q zP9tTv1n97AqOzSyWyG94zOt0YnFNcbQ+1ho/Sl0C+4GL3jBC7D9p2ykasEQ4M9IeeOG FGCMYVlgGeFL8lA05fg1FVy9HlgxukOnbGkLcNNiA8Aknv1odO3ZBRhwbe7VaLaNfqCh cVqfmf3J0gykifnr4A/aBidKGmjPK/lN9n+Cqgqf3UsoXmowc4iZv3ab6Zz5kfr4cOBt tqoVV61rfEVVw9RmEpVWkawlhfMqR/Cq8cKpOQ2D90AUxVhsxsfxMpuwXN7OOEBgJGH+ cWTg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:subject:mime-version:x-original-sender :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=o+/SuXNKFDz9wGAUKORSW4yW+GsYKdtuZfdOd2vGwMY=; b=jtHQIBGyIz+blA5sigq3HPAidK1lXyoAEratZj/MfeTK5Lw6hSau1uUXC3s9dhqGPI 3rg/seWTzTpGidiCtlAjKH9ff8Wo75l3kDjwibcN3KA83uP++YWxlbqQlggTtzb+IaQ+ nfgo2VZ9M9417oPCGSLp8ckz4whHMz1EQsY4bdKHKiVbcSYZMQ/b4bZiMwhvVNoNq40s JJEb2FOYN9jRwkWbAOx+w2LWJp56NcDWgOTgIzEkfqxdydM88XiceKSGp4UW/Ns7bozL hdXi67pcsfcgOdd8ZIzz8KcmdOF1h4lGy7wFAwvAVNpBujfaTAA5UEYbAZ1a+fnhuSK8 Clng== 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:message-id:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :x-spam-checked-in-group:list-post:list-help:list-archive :list-unsubscribe; bh=o+/SuXNKFDz9wGAUKORSW4yW+GsYKdtuZfdOd2vGwMY=; b=BdKZ7KEeNF3iwSVZYJEoaXsUTc96Jc+JKqvlgJp5T4TnXHYG3d12pbFb6mugGnuXsz Ni2G88qNOXsgalqTQjlA8Dg1sOpCpft3k2tlKLusZ5vE/amYxjDpvj4iBZMp1aBeKyjx 9bcBs9HxCKGkwQEKm6laEYpOrMolN10vYQ3lCTG7+0uNm06UFXqrCSSjlKQu/DKcxv4a HzF0Cld74KCl8keXwkcBb1Tsub1KQxqRO4JPNYjtgM/xoMq2oGEgq8y9cYEpyMrxt0bC lCUdJMerFxHW8GBAffFmEG2ob8lToPitAKNuHGh4vuSzCUhQH3tdcE4NfkJ9re0JBJ88 ZkIQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAX+dKyN4ZqQoBnQ6sesWkqbepDua8Zp5Vhe8RMntTpfcSv/TxBU swVzd2UiFj557B6N/dsq/WY= X-Google-Smtp-Source: APXvYqxW1deWNES0GgfeRtOz2CHYdJJKkx0txl9yVOi2WwFOFVT3BdPtvULkKX8F6PlCnVQNpEkV1g== X-Received: by 2002:aca:c594:: with SMTP id v142mr4302898oif.21.1570547236611; Tue, 08 Oct 2019 08:07:16 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:4fcd:: with SMTP id d196ls700295oib.16.gmail; Tue, 08 Oct 2019 08:07:16 -0700 (PDT) X-Received: by 2002:aca:dd07:: with SMTP id u7mr4465438oig.106.1570547236044; Tue, 08 Oct 2019 08:07:16 -0700 (PDT) Date: Tue, 8 Oct 2019 08:07:15 -0700 (PDT) From: Alexander Gietelink Oldenziel To: Homotopy Type Theory Message-Id: <1b613bab-505c-4880-9778-4e3206872294@googlegroups.com> Subject: [HoTT] Kripke-Joyal Semantics and HoTT MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_2327_243807693.1570547235311" X-Original-Sender: a.f.d.a.gietelinkoldenziel@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: , ------=_Part_2327_243807693.1570547235311 Content-Type: multipart/alternative; boundary="----=_Part_2328_2062838255.1570547235312" ------=_Part_2328_2062838255.1570547235312 Content-Type: text/plain; charset="UTF-8" Dear all, It is my understanding that the interpretation of HoTT inside higher topoi is an ongoing field of research. Much of this business involves subtle strictness properties and things like contextual and syntactic categories. In the 1-topos case there is the Kripke-Joyal/Stack - semantics. These semantics are easy to use in practice. Naively, it seems one could lift the Kripke-Joyal semantics by not asking for truth but simply an inhabitant of a type. Has this been investigated at all? Is it ultimately fruitless? -- 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. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/1b613bab-505c-4880-9778-4e3206872294%40googlegroups.com. ------=_Part_2328_2062838255.1570547235312 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Dear all,

It is my understanding that t= he interpretation of HoTT inside higher topoi is an ongoing field of resear= ch. Much of this business involves subtle strictness properties and things = like contextual and syntactic categories.=C2=A0
In the 1-topos ca= se there is the Kripke-Joyal/Stack - semantics. These semantics are easy to= use in practice.=C2=A0 Naively, it seems one could lift the Kripke-Joyal s= emantics by not asking for truth but simply an inhabitant of a type.=C2=A0<= /div>

Has this been investigated at all? Is it ultimatel= y fruitless?

--
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.
To view this discussion on the web visit https://groups.google.co= m/d/msgid/HomotopyTypeTheory/1b613bab-505c-4880-9778-4e3206872294%40googleg= roups.com.
------=_Part_2328_2062838255.1570547235312-- ------=_Part_2327_243807693.1570547235311--