The Coq mailing list

[Bas Spitters <b.a.w.spitters AT gmail.com>]

I once collected some references here. If any are missing, please add them:
https://ncatlab.org/nlab/show/inductive-inductive+type

On Wed, Nov 15, 2017 at 7:13 PM, Thorsten Altenkirch
<Thorsten.Altenkirch AT nottingham.ac.uk>
 wrote:
> Hi,
>
>
>
> Frederik Forsberg investigated ind-ind types (IITs) in his PhD thesis.
>
> https://personal.cis.strath.ac.uk/fredrik.nordvall-forsberg/thesis/thesis.pdf
>
>
>
> Interestingly he couldn’t find a satisfying translation of IITs into
> ordinary inductive types. However, we have recently revisited his topic and
> found that at least for our standard example there is a translation if you
> have quotient types. I realize that this is not of much help in Coq,,
> though.
>
>
>
> There are many interesting examples of induction-induction if you allow
> equality constructors – we call this quotient inductive inductive types.
> They are special cases of HITs or more precisely HIITs.
>
>
>
> Cheers,
>
> Thorsten
>
>
>
> From: 
> <coq-club-request AT inria.fr>
>  on behalf of Matthieu Sozeau
> <mattam AT mattam.org>
> Reply-To: 
> "coq-club AT inria.fr"
>  
> <coq-club AT inria.fr>
> Date: Wednesday, 15 November 2017 at 10:26
> To: 
> "coq-club AT inria.fr"
>  
> <coq-club AT inria.fr>
> Subject: Re: [Coq-Club] Mutual inductive types with a predicate
>
>
>
> Hi,
>
>
>
>   What you’re trying to formalize are known as inductive-inductive types,
> when an inductive can depend through its indices on a previous inductive in
> the same mutual block, and constructors of later inductives can refer to
> constructors of the previous inductives (the exact order constraints varies,
> Agda implements this in a more flexible way for example). There is an
> experimental branch IR on my GitHub [1] which implements those, based on Coq
> 8.7. You have to write the eliminators by hand though and consistency is not
> proven for this version of the calculus yet. Maybe there are other non
> ind-ind encodings of your types that solve your problem though.
>
>
>
> [1] https://github.com/mattam82/coq/tree/IR?files=1
>
>
>
> Best,
>
> — Matthieu
>
>
>
> Le mer. 15 nov. 2017 à 10:23, Merlin Göttlinger 
> <megoettlinger AT gmail.com>
>  a
> écrit :
>
> Hi,
>
>
>
> what I want to implement is a more complicated version of this:
>
>
>
> Inductive A :=
>
> | a1 : nat -> A
>
> | a2 : nat -> A
>
> | a3 : B -> A -> A
>
> with B :=
>
>      | b1 : nat -> B
>
>      | b2 : { ae : A | P ae} -> B
>
> with P : A -> Prop :=
>
>      | pa3 : forall b a, P a -> P (a3 b a)
>
>      | pa1 : forall n, P (a1 n).
>
>
>
> However that is rejected by coq (8.6.1) with the error The reference A was
> not found in the current environment. at the Type of P.
>
> Why is that the case?
>
>
>
> One way I found to avoid this is to "bake the predicate into the type":
>
>
>
> Inductive A : bool -> Set :=
>
> | a1 : nat -> A true
>
> | a2 : nat -> A false
>
> | a3 {b} : B -> A b -> A b
>
> with B : Set :=
>
>      | b1 : nat -> B
>
>      | b2 : A true -> B.
>
>
>
> But this forces you to wrap and unwrap A everywhere where you do not care
> about the predicate.
>
> Is there a better way?
>
>
>
> Cheers,
>
> Merlin
>
> 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 send it back to me, and immediately delete it.
>
> Please do not use, copy or disclose the information contained in this
> message or in any attachment.  Any views or opinions expressed by the
> author of this email do not necessarily reflect the views of the
> University of Nottingham.
>
> This message has been checked for viruses but the contents of an
> attachment may still contain software viruses which could damage your
> computer system, you are advised to perform your own checks. Email
> communications with the University of Nottingham may be monitored as
> permitted by UK legislation.