Awkwardness with coinductive universes

I’ve been playing with coinductive universes.

It’s very awkward to manipulate though.

I think my problem might be related to subject reduction?

I think I ought to refactor

CoInductive U :=
| const (T: Type)
| sum (_ _: U)
| prod (_ _: U)

To a style like

Variant Tag := Const | Sum | Prod.
CoInductive U := {
  tag: Tag ;
  const_u: if tag is Const then Type else Unit: Type ;

Not quite sure how to handle sum/prod here but anyway the point is that cofix plays much nicer with record projections than pattern matching and so I should be able to have a more natural El implementation.

Really the whole deal is very awkward though and so I thought I should go here for advice.