Pushforward Heyting algebras along OrderIso

Stream: Is there code for X?

[Emilie (Shad Amethyst)]

I have constructed the HeytingAlgebra of Opens α, in order to then construct the type of regular open sets as Ro(X) := Heyting.Regular (Opens X), but I would also like to construct the CoheytingAlgebra of Closed α for feature parity. We already have Closed α ≃o (Opens α)ᵒᵈ, so all I need is a way to either push HeytingAlgebra (Opens α) to HeytingAlgebra (Closed α)ᵒᵈ or CoheytingAlgebra (Opens α)ᵒᵈ to CoheytingAlgebra (Closed α), but I can't seem to be able to figure out how to do that exactly. I found docs#HeytAlg.Iso.mk, but I'm afraid the category theory vocabulary is flying over my head

[Yaël Dillies]

This already exists. See docs#TopologicalSpace.Opens.instFrameOpens (sorry, terrible instance name)

[Yaël Dillies]

HeytAlg.Iso.mk is a red herring: this is to construct a categorical equivalence isomorphism between Heyting algebras from an order theoretic isomorphism

[Emilie (Shad Amethyst)]

Oh, I think I saw that Frame at one time but it didn't click in my mind that it refers to a complete heyting algebra

[Yaël Dillies]

Besides the fact that docs#TopologicalSpace.Closeds.instCoframeCloseds already exists too, the way to proceed here is to redo the work. This is because docs#TopologicalSpace.opens and docs#TopologicalSpace.closeds are (different) structures, so the only way to transfer the instance would be to transfer along Closed α ≃o (Opens α)ᵒᵈ, which gives poor-ish definitional equalities.

[Emilie (Shad Amethyst)]

I mean, Frame implies HeytingAlgebra, so that part of the work I was planning to do is already done, all I need to do now is to rephrase my definition of bundled regular open sets in terms of Heyting.Regular, making use of the ambient HeytingAlgebra (Opens X) instance

[Yaël Dillies]

Oh shoot I haven't made Frame extend HeytingAlgebra, so there's technically no HeytingAlgebra (Opens α) instance around yet. I'll open a PR tomorrow.

[Emilie (Shad Amethyst)]

Yeah, just realized that :)

[Emilie (Shad Amethyst)]

Hmm, the definitional equality for himp is going to be challenging

[Yaël Dillies]

Not at all. Keep your eyes peeled :wink: