Discrete fibers Cor. 8.20 RS17

[StiephenPradal]

Here is the last result for discrete fibers. There are also more stuff about ap-hom and hom-eq that I needed for failed attemps to prove the corollary. I let it there for now in case it's interesting for the library.

[TashiWalde]

The fact that discrete types are closed under equivalence is also a direct corollary of is-local-type-equiv-is-local-type (since the discrete types are precisely those that are local for {0} -> Δ¹).

[StiephenPradal]

The fact that discrete types are closed under equivalence is also a direct corollary of is-local-type-equiv-is-local-type (since the discrete types are precisely those that are local for {0} -> Δ¹).

Oh great! I didn't see that it had already been proven more generally. I have written this proof and it's much more compact and clear, should we replace the previous one with this one?

[emilyriehl]

It's hard to know what's in the library already when it's been going so fast. But, yes, I'd say now that those general results are there we might as well use them.

[emilyriehl]

Nice work on all this by the way.

[emilyriehl]

@StiephenPradal sorry to be so slow. Merging now!