[Agda] Defining Coq(w/o Prop) in Agda using Induction Recursion

[Nils Anders Danielsson]

On 2013-11-26 00:38, Abhishek Anand wrote:
> Has someone tried to define(using IR) a universe closed under both PI
> and strictly-positive-Inductive type-constructors? (Coq's first
> universe seems to match that description precisely.)

Yes:

   Hier Soir, an OTT Hierarchy
   Conor McBride
   http://sneezy.cs.nott.ac.uk/epilogue/?p=1098

> If so, does the definition fit in Set 0 of Agda?

Yes: "We’ve built something like Coq’s hierarchy inside Agda’s lowest
level."

-- 
/NAD