search

martinescardo / TypeTopology

Logical manifestations of topological concepts, and other things, via the univalent point of view.
GNU General Public License v3.0
220 stars 40 forks source link

Prove that isomorphic frames are equal #261

Closed ayberkt closed 2 months ago

ayberkt commented 3 months ago

This PR adds a proof that the notion of frame (as implemented in frame-structure in Locales.Frame) is a standard notion of structure.

Furthermore, it adds two corollaries of this fact:

  1. Isomorphic frames are equal (using the structure identity principle).
  2. “Transport lemma” for isomorphic frames: if a frame F satisfies some predicate P : Frame (𝓤 ⁺) 𝓤 𝓤 → Ω 𝓣 then any frame G with F ≅ G also satisfies P.
tomdjong commented 3 months ago

I'll leave further reviewing on this PR to @martinescardo.

ayberkt commented 2 months ago

Can you take a look at this when you get the chance @martinescardo?