search

homotopy-io / homotopy-rs

A Rust/WASM implementation of homotopy.io
https://homotopy.io
BSD 3-Clause "New" or "Revised" License
79 stars 6 forks source link

Lemma not contractible to identity #1338

Open wilfofford opened 5 months ago

wilfofford commented 5 months ago

Cap Lemma.hom.zip

It feels like the cell in the workspace above should contract down to the identity. All it does is pull one of the caps above the other, then push it back down again. When everything is marked as orientable, it does contract. Perhaps my intuition is wrong and this shouldn't be weakly equivalent to the identity?

doctorn commented 5 months ago

To add some weight to the intuition this should contract, adding a very small amount to either end of the diagram does allow it to contract: homotopy_io_export.hom.zip

jamievicary commented 5 months ago

Yes I agree. @NickHu this is one for you I think.

calintat commented 5 months ago

So what happens here is we produce a contraction/expansion cospan $X \rightarrow Y \leftarrow Z$ and $Z$ does not typecheck (however the diagram $X \rightarrow Y \leftarrow Z$ does typecheck which is one of the conjectures about contraction). We decided a while ago that if this happens, we should fail but I can't quite remember why.

calintat commented 5 months ago

Also this works fine if you replace the algebraic cap with a homotopy cap (i.e. mark the generator as invertible).