The Coq mailing list

[Fredrik Nordvall Forsberg <fredrik.nordvall-forsberg AT strath.ac.uk>]

Hi Bas,

On 13/07/15 19:49, Bas Spitters wrote:
>> So why are they not included in Coq?
> 
> Are you really claiming that there is a detailed semantics for
> CIC+IndInd and that all the meta-theory has been done?
> I agree, it should work. However, I haven't seen the details yet.

The classical set-theoretic semantics of MLTT + inductive-inductive
definitions should extend to an impredicative Prop very
straightforwardly. However, you are right that there are no proofs of
e.g. normalization for this theory (or for induction-recursion, for that
matter). I would expect this to work with no problems.

Best regards,
Fredrik

> On Mon, Jul 13, 2015 at 7:59 PM, Thorsten Altenkirch
> <Thorsten.Altenkirch AT nottingham.ac.uk>
>  wrote:
>> Hi Jason,
>>
>> afaik there is no easy way to do this. I discussed this recently with
>> Frederik Forsberg, whose PhD thesis is a good source of information about
>> induction-induction. See section 5.3.
>>
>> You can approximate inductive-inductive definition using a similar 
>> technique
>> as for induction-recursion but you don’t get the right eliminator. E.g. If
>> you define a family A : Set, B : A -> Set you expect that the elimination
>> operators have the form
>>
>> elim-A : (X : Set)(Y : X -> Set) -> … -> A -> X
>> elim-B : (X : Set)(Y : X -> Set) -> … -> (a : A) -> B a -> Y (elim-A X Y …
>> a)
>>
>> the problem here is the dependency of the 2nd operator on the first.
>>
>> However, unlike the problem with univalence and extensionality this one is
>> relatively easy to fix as Agda shows. Inductive-inductive definitions have 
>> a
>> straightforward operational semantics and also it is no problem to derive
>> eliminators and recursors for them. So why are they not included in Coq?
>>
>> Thorsten
>>
>> From: Jason Gross 
>> <jasongross9 AT gmail.com>
>> Reply-To: 
>> "coq-club AT inria.fr"
>>  
>> <coq-club AT inria.fr>
>> Date: Sunday, 12 July 2015 04:58
>> To: coq-club 
>> <coq-club AT inria.fr>
>> Subject: [Coq-Club] Faking induction-induction in Coq?
>>
>> Hi,
>> Is there a (known) way to fake induction-induction in Coq?
>>
>> Abhishek mentioned
>> http://www.cs.ru.nl/~venanzio/publications/induction_recursion.ps last year
>> as a way of faking induction-recursion in Coq.  I'm curious, in particular,
>> about how to define well-typed syntax for dependent type theory in Coq, 
>> and,
>> more specifically, one that supports a quotation function, which sends any
>> syntactic term to a syntactic representation of that syntax, i.e., sends
>> (app 'S' '0'), the syntax representing the numeral 1, to (app (app 'app'
>> "S") "0").
>>
>> Thanks,
>> Jason

-- 
Fredrik Nordvall Forsberg,
Department of Computer and Information Sciences,
University of Strathclyde.
The University of Strathclyde is a charitable body, registered in
Scotland, with registration number SC015263.