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.2 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-x33b.google.com (mail-ot1-x33b.google.com [IPv6:2607:f8b0:4864:20::33b]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 0da718b4 for ; Tue, 21 May 2019 11:47:18 +0000 (UTC) Received: by mail-ot1-x33b.google.com with SMTP id x23sf9509043otp.5 for ; Tue, 21 May 2019 04:47:17 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:in-reply-to:references:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=eIecGzGzgOFSom6XOWeu8tvFoGZsX/ye0F1JQtp/XL8=; b=q8l7bk14Q+yKeephEyMX07izKCVPTPQJK5gKMihIy/i4cpn4LUnmHy+xcBk+ZahyR4 ACj+Fbp29KFzOYmHH5g7PQRIoS5DJbUG/Svlwqhrx2cPLI4tGl+xv9mDOfn5UzV8sMCT 73SpzhnLLaB2pgahOWishIMfUtdDOZECjThRlaoyJbrqQpcxAga0SiIIu6wfuLwY8T82 PrTymk9WjOfinS7wZ/ec9zXf//MyeTTPJEgu13mguJ/3Elaz/DL5oxggsoOaFCn15nEU WtKXQNB7XHygk9l9J8Aa0/+gJHrJT+a/St7usJaO3gikNTEXO36kWjIQytHKR8sDNFV/ orlg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:in-reply-to:references:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=eIecGzGzgOFSom6XOWeu8tvFoGZsX/ye0F1JQtp/XL8=; b=uKAXj8R/4YeK4UYbS5ckuY0cmKMdFOSjZh8/41H6RKIFxZDrEwda+HM8c8gr9s3oZO 2rOm0bPUlPn+20ACc2dTmynq873G8PpIk0ayK01z/Rrf4y+Evvm5lEuRqgo8DxnrXRxt uMChES9HQK1aBiKqDTi0+EmWdGFoVHQ7efni9EJo5ZoqpRTlXN394EFTw0R0eR6gxVRg EdPq9OoIZs8FxkWFm5DFWP/OHm6IxPpjJw8tUtFp0vSXP16e0lLAec8BtddCRkz8n9pn uWmW+7AdHCF0R5w47J3ZxrbhvtrJRfeD1n0iY4+uj1cRbZtc6VDnX03Ycgd2h9s45pBb z4/Q== 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:in-reply-to :references: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=eIecGzGzgOFSom6XOWeu8tvFoGZsX/ye0F1JQtp/XL8=; b=e5U5tSNPYNhjXy0m8gw+Y+BlYN4hL8UK0XBMylLojmV/KyxgtVp7EEW3Xiz7YWhxXs lFNbsIeEJL1C7Ps6odtVhkQwyLKC7MFVqS3Tlsvg9vDKu3xR6GRmESoioxQ9xBoaZ1xk bVThOF04BvBhJdSvg/A74imgMha4sjI39p2Fjd2l1bq9B6RV3x+aXgqHElluAqSanHxW gvCbwIETFnkw/Lhvm71dZZUMmnmn/HblTmF44u5ayTbt7O9OKYTVEf1agPz0tUCDBPYl j4Zn0XUwASSN//VroEDNnSi8J4LDwXGc1z38TW17tprJRVzD4GWMQRLwtMPJhEwvXCeu jiKg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAU/DXSSmw23+2pQNIGY3rBnIzGeALbXH166y0K1+vExuJvKD4bq 7viDWiin1/Syt7rA4IjowuM= X-Google-Smtp-Source: APXvYqxo7ohf8bOaxWj9BYiB5WQsHmdmDmBgPo0lzCZY3k40UBCEMy5wh6MM7fPky708vN1fEklPVA== X-Received: by 2002:a9d:148:: with SMTP id 66mr44340032otu.32.1558439236943; Tue, 21 May 2019 04:47:16 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:df02:: with SMTP id w2ls2980615oig.6.gmail; Tue, 21 May 2019 04:47:16 -0700 (PDT) X-Received: by 2002:aca:f4c3:: with SMTP id s186mr2891430oih.68.1558439236258; Tue, 21 May 2019 04:47:16 -0700 (PDT) Date: Tue, 21 May 2019 04:47:15 -0700 (PDT) From: Andrew Swan To: Homotopy Type Theory Message-Id: In-Reply-To: References: Subject: [HoTT] Re: Semantics of QIITs ? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_2275_376597692.1558439235451" X-Original-Sender: wakelin.swan@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_2275_376597692.1558439235451 Content-Type: multipart/alternative; boundary="----=_Part_2276_931843634.1558439235451" ------=_Part_2276_931843634.1558439235451 Content-Type: text/plain; charset="UTF-8" Regarding the Cauchy reals, I believe it is known that countable choice holds and set quotients exist in simplicial sets, but I think under these conditions the usual construction of the Cauchy reals as a quotient of sequences of rationals satisfies the constructors for the HIT Cauchy reals, and also the higher induction principle. I think the HIT cumulative hierarchy can be constructed using W types and univalence, using the characterisation of it as a retract of the Aczel cumulative hierarchy by Hakon Gylterud in the paper at https://doi.org/10.1017/jsl.2017.84 . If so, similar arguments should work for ordinals and surreal numbers. Are there any other examples in the HoTT book? Best, Andrew On Thursday, 16 May 2019 16:57:36 UTC+2, Bas Spitters wrote: > > What is the status of the semantics of quotient inductive inductive types? > Looking at the literature there's some progress on reducing QIITs to > simpler constructions, but this does not seem to have led to a > convenient semantic result. > E.g. QIITs do not seem to be treated in the work by Lumdaine and Shulman. > > https://ncatlab.org/nlab/show/inductive-inductive+type > > Do we know that the prototypical QIITs from the book (e.g. Cauchy > reals) are supported in the usual models of HoTT? > > Thanks, > > Bas > -- 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/f580d237-12b5-4107-92c4-7738fd89e59f%40googlegroups.com. For more options, visit https://groups.google.com/d/optout. ------=_Part_2276_931843634.1558439235451 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Regarding the Cauchy reals, I believe it is known that cou= ntable choice holds and set quotients exist in simplicial sets, but I think= under these conditions the usual construction of the Cauchy reals as a quo= tient of sequences of rationals satisfies the constructors for the HIT Cauc= hy reals, and also the higher induction principle.

I thi= nk the HIT cumulative hierarchy can be constructed using W types and unival= ence, using the characterisation of it as a retract of the Aczel cumulative= hierarchy by=C2=A0Hakon=C2=A0Gylterud in the paper at=C2=A0https://doi.org= /10.1017/jsl.2017.84 . If so, similar arguments should work for ordinals an= d surreal numbers.

Are there any other examples in= the HoTT book?

Best,
Andrew

On T= hursday, 16 May 2019 16:57:36 UTC+2, Bas Spitters wrote:
What is the status of the semantics of quotient= inductive inductive types?
Looking at the literature there's some progress on reducing QIITs t= o
simpler constructions, but this does not seem to have led to a
convenient semantic result.
E.g. QIITs do not seem to be treated in the work by Lumdaine and Shulma= n.

https://ncatlab.org/nlab/show/inductive-inductive+t= ype

Do we know that the prototypical QIITs from the book (e.g. Cauchy
reals) are supported in the usual models of HoTT?

Thanks,

Bas

--
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/f580d237-12b5-4107-92c4-7738fd89e59f%40googleg= roups.com.
For more options, visit http= s://groups.google.com/d/optout.
------=_Part_2276_931843634.1558439235451-- ------=_Part_2275_376597692.1558439235451--