Discussion of Homotopy Type Theory and Univalent Foundations
 help / Atom feed
From: Thorsten Altenkirch <Thorsten.Altenkirch@nottingham.ac.uk>
To: Bas Spitters <b.a.w.spitters@gmail.com>,
	homotopytypetheory <homotopytypetheory@googlegroups.com>
Cc: "Ambrus Kaposi" <kaposi.ambrus@gmail.com>,
	"Kovács András" <kovacsandras@inf.elte.hu>
Subject: Re: [HoTT] Semantics of QIITs ?
Date: Thu, 16 May 2019 15:39:28 +0000
Message-ID: <99645C4A-A893-459A-B027-5607E89A37EF@nottingham.ac.uk> (raw)
In-Reply-To: <CAOoPQuQBwyvbY_f3qNZOgEB7nxQHGUigqXjNhbDmCvB3xnVaOw@mail.gmail.com>

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/99645C4A-A893-459A-B027-5607E89A37EF%40nottingham.ac.uk.
For more options, visit https://groups.google.com/d/optout.

  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 [this message]
2019-05-16 15:50   ` Bas Spitters
2019-05-16 16:15     ` András Kovács
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=99645C4A-A893-459A-B027-5607E89A37EF@nottingham.ac.uk \
    --to=thorsten.altenkirch@nottingham.ac.uk \
    --cc=b.a.w.spitters@gmail.com \
    --cc=homotopytypetheory@googlegroups.com \
    --cc=kaposi.ambrus@gmail.com \
    --cc=kovacsandras@inf.elte.hu \
    /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