[Agda] [HoTT] Re: Why do we need judgmental equality?

[Thomas Streicher]

admittedly, by coinductive I understand terminal coalgebra

in MLTT even function types are inductive though that's a bit of
cheating in my eyes

so I must say I don't understand what you mean by codata types
technically

I know positive and negative polarity in the sense of linear logic people
presumably, that'scloser to what you have in mind

thomas