discrete and contractible types are Rezk

[TashiWalde]

• Show that every arrow in a discrete type is an isomorphism
• Deduce that every discrete type is Rezk. (In particular, every contractible type is Rezk)

Note: I redefined iso-eq to have better definitional computational properties: Now the composite x = y -> Iso x y -> hom x y is definitionally equal to hom-eq : x = y -> hom x y.

[emilyriehl]

@TashiWalde this version seems to have a typechecking error (involving weakextext in the right orthogonal file).

[TashiWalde]

@TashiWalde this version seems to have a typechecking error (involving weakextext in the right orthogonal file).

Yes, I'm fixing it.

[TashiWalde]

@TashiWalde this version seems to have a typechecking error (involving weakextext in the right orthogonal file).

Fixed. The reason is that I am currently getting rid of instances of weakextext and naiveextext whenever I use them and always just replace them with extext, in accordance to our new philosophy of taking extext as the primary axiom.

[emilyriehl]

great!