search

rzk-lang / sHoTT

Formalisations for simplicial HoTT and synthetic ∞-categories.
https://rzk-lang.github.io/sHoTT/
44 stars 12 forks source link

Discrete fibers Cor. 8.20 RS17 #135

Closed StiephenPradal closed 10 months ago

StiephenPradal commented 12 months ago

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 commented 11 months ago

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 commented 11 months ago

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 commented 11 months ago

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 commented 11 months ago

Nice work on all this by the way.

emilyriehl commented 10 months ago

@StiephenPradal sorry to be so slow. Merging now!