The Coq mailing list

[Guilhem Moulin <guilhem.moulin AT chalmers.se>]

On Sat, 18 Sep 2010 at 14:04:12 -0400, Vladimir Voevodsky wrote:
> I wonder if the following "mutually inductive" definition is possible  in 
> any  of the languages/proof assistants (e.g. Agda):
> […]
> The intuition behind it is to define the universe U generated by a type T 
> with respect to dependent products together with the function elem: U -> T 
> which sends X:U to its underlying "type of elements". 
> 
> The basic problem here is that a type is inductively defined simultaneously 
> with a fix-point function on it. 
 
Agda supports inductive-recursive definitions:

mutual
  data U (t : Set) : Set where
    gen  : U t
    Π : (A : U t) → (B : El A → U t) → U t

  El : {t : Set} → (A : U t) → Set
    El {t} gen  = t
    El (Π A B) = ∀ (a : El A) → El (B a)


See also
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.RulesForTheStandardSetFormers

The following page lists the main differences between Agda and Coq:
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.AgdaVsCoq

Attachment: signature.asc
Description: Digital signature