Hi

I have found a technique for doing that kind of thing some time ago (I don’t claim any credit, but I haven’t seen it anywhere before in the context of handling “positive” coinductive types), not sure how widely known it is in the Coq community.

Here’s a proposal I made that contains a basic description of the technqiue: Convenient syntax sugar for coinductive types that could also possibly fix problems with positive coinductives · Issue #14020 · coq/coq · GitHub

In case of your universe, this would be

```
Inductive UX (X : Type) :=
| ConstX (T : Type)
| SumX (u v : X)
| ProdX (u v : X).
CoInductive U : Type :=
{
Out : UX U;
}.
```

Basically, you define the “base functor” of the type you want as an **Inductive** type (here it’s called `UX`

). This base functor looks like the type you want to define (your original `U`

), but it’s only “one layer deep”, i.e. you replace occurrences of the original `U`

by the parameter `X`

. Then, you tie the knot by defining a **CoInductive** type with one field that represents the fixpoint of the base functor (here this is `U`

).

For convenience, you may then set implicit arguments and define smart constructors for your type, which will just refer to the constructors of the base functor.

```
Arguments ConstX {X} _.
Arguments SumX {X} _ _.
Arguments ProdX {X} _ _.
Definition Const (T : Type) : U :=
{|
Out := ConstX T;
|}.
Definition Sum (u v : U) : U :=
{|
Out := SumX u v;
|}.
Definition Prod (u v : U) : U :=
{|
Out := ProdX u v;
|}.
```

Proofs by coinduction with this representation are pretty OK, and you can easily `destruct`

an `u : U`

using `destruct u as [[T | u v | u v]]`

(note the double square brackets - you need to first destruct the coinductive, then the base functor).

Hope this helps. Any motivation for why you want coinductive universes? Any resources on that topic? The typical thing you do with a universe is defining an interpretation function `El : U -> Type`

, but in your case you can’t use recursion for that, because `U`

is not inductive, and you can’t use corecursion, because `Type`

is not coinductive, so you’re kind of stuck.