Discussion of Homotopy Type Theory and Univalent Foundations
 help / Atom feed
From: "András Kovács" <puttamalac@gmail.com>
To: Bas Spitters <b.a.w.spitters@gmail.com>
Cc: Thorsten Altenkirch <Thorsten.Altenkirch@nottingham.ac.uk>,
	 homotopytypetheory <homotopytypetheory@googlegroups.com>,
	 Ambrus Kaposi <kaposi.ambrus@gmail.com>
Subject: Re: [HoTT] Semantics of QIITs ?
Date: Thu, 16 May 2019 18:15:30 +0200
Message-ID: <CAA3CDBbsxaxrYsoabfNAP0DxLtqUATTOSW2PfX1EreKnOe2ozQ@mail.gmail.com> (raw)
In-Reply-To: <CAOoPQuQT+cX7QbmKT+OsNgO+YGeDrqqOYXxcx714NWZo6ZO2bQ@mail.gmail.com>

[-- Attachment #1: Type: text/plain, Size: 5521 bytes --]

Hi,

In "Constructing QIITs", we only considered signatures and their semantics
in the setting of extensional TT. It is currently an open problem whether
construction of QIITs (in the style of our paper) can be performed without
UIP, and also whether the syntax of QIIT signatures itself is constructible
in such setting. Jasper Hugunin's recent work on constructing some
inductive-inductive types in cubical TT could relevant here.

best regards
András

Bas Spitters <b.a.w.spitters@gmail.com> ezt írta (időpont: 2019. máj. 16.,
Cs, 17:50):

> Hi Thorsten,
>
> Yes, I saw your result (congratulations!) However, I may be
> overlooking something, but do we know that the theory of codes is
> available in any of the standard models of HoTT?
> That doesn't seem to be stated in your paper.
>
> Best regards,
>
> Bas
>
>
> On Thu, May 16, 2019 at 5:39 PM Thorsten Altenkirch
> <Thorsten.Altenkirch@nottingham.ac.uk> wrote:
> >
> > Hi Bas,
> >
> > Our POPL 2019 paper does address this I think, maybe not exactly in the
> way you expect. We define a theory of codes (based on earlier work by
> Ambrus and Andras) which is an intrinsic type theory such that a context is
> a representation of a quotient inductive-inductive type. The formation of
> Pi-types is restricted so that you can only form strictly positive types,
> it is indeed a special case of a directed type theory. Now the semantics
> are categories with an initial object and it turns out we can construct the
> semantics just from assuming the existence of the theory of codes. The
> category assigned to a context is the category of algebras and the initial
> object is the intended interpretation of the QIIT, equivalently we get the
> expected elimination principle. The theory of codes can "eat itself" it is
> an instance of a QIIT definable in itself. Hence this QIIT is in a certain
> sense universal.
> >
> > One would also like to interpret QIITs that are indexed by "external"
> types which are already defined and in particular include infinitary
> constructors. One can extend the theory but the semantics suffered from a
> coherence issue. However, I think Andras made some progress on this.
> >
> > My view is that this programme can be extended to HIITs by considering
> higher order versions of type theory and in particular the theory of codes.
> However, this is maybe an overkill, since one can normalize the
> substitutions (make them implicit) and address the coherence issues this
> way. I think that is basically what Andras has done.
> >
> > Here is a link to the pdf:
> > https://akaposi.github.io/finitaryqiit.pdf
> >
> > Thorsten
> >
> > On 16/05/2019, 15:58, "homotopytypetheory@googlegroups.com on behalf
> of Bas Spitters" <homotopytypetheory@googlegroups.com on behalf of
> b.a.w.spitters@gmail.com> 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/CAOoPQuQBwyvbY_f3qNZOgEB7nxQHGUigqXjNhbDmCvB3xnVaOw%40mail.gmail.com
> .
> >     For more options, visit https://groups.google.com/d/optout.
> >
> >
> >
> >
> >
> > This message and any attachment are intended solely for the addressee
> > and may contain confidential information. If you have received this
> > message in error, please contact the sender and delete the email and
> > attachment.
> >
> > Any views or opinions expressed by the author of this email do not
> > necessarily reflect the views of the University of Nottingham. Email
> > communications with the University of Nottingham may be monitored
> > where permitted by law.
> >
> >
> >
> >
>
> --
> 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/CAOoPQuQT%2BcX7QbmKT%2BOsNgO%2BYGeDrqqOYXxcx714NWZo6ZO2bQ%40mail.gmail.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.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAA3CDBbsxaxrYsoabfNAP0DxLtqUATTOSW2PfX1EreKnOe2ozQ%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.

[-- Attachment #2: Type: text/html, Size: 7692 bytes --]

  reply index

Thread overview: 19+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2019-05-16 14:57 Bas Spitters
2019-05-16 15:39 ` Thorsten Altenkirch
2019-05-16 15:50   ` Bas Spitters
2019-05-16 16:15     ` András Kovács [this message]
2019-05-16 18:50       ` Bas Spitters
2019-05-20 16:16         ` Thorsten Altenkirch
2019-05-20 17:54           ` Bas Spitters
2019-05-20 18:35             ` Thorsten Altenkirch
2019-05-20 19:59               ` Jon Sterling
2019-05-20 21:04                 ` Bas Spitters
2019-05-20 22:17                   ` Thorsten Altenkirch
2019-05-20 23:26                     ` Jon Sterling
2019-05-21  0:28                       ` Matt Oliveri
2019-05-21  2:45                         ` Jasper Hugunin
2019-05-21  8:33                         ` Thorsten Altenkirch
2019-05-21 19:56                           ` Matt Oliveri
2019-05-21  8:39                       ` Thorsten Altenkirch
2019-05-21 11:47 ` [HoTT] " Andrew Swan
2019-05-21 12:14   ` Bas Spitters

Reply instructions:

You may reply publically to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=CAA3CDBbsxaxrYsoabfNAP0DxLtqUATTOSW2PfX1EreKnOe2ozQ@mail.gmail.com \
    --to=puttamalac@gmail.com \
    --cc=Thorsten.Altenkirch@nottingham.ac.uk \
    --cc=b.a.w.spitters@gmail.com \
    --cc=homotopytypetheory@googlegroups.com \
    --cc=kaposi.ambrus@gmail.com \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link

Discussion of Homotopy Type Theory and Univalent Foundations

Archives are clonable: git clone --mirror http://inbox.vuxu.org/hott

Newsgroup available over NNTP:
	nntp://inbox.vuxu.org/vuxu.archive.hott


AGPL code for this site: git clone https://public-inbox.org/ public-inbox