This PR adds a proof that the Scott locale of the Sierpiński dcpo has the universal property of the Sierpiński locale (i.e. the property of being the free frame on one generator).
In order to prove this, I had to prove that the basic opens of the Scott locale of the Sierpiński dcpo are either one of 𝟏, 𝟎, or {⊤}. This is the proof implemented by the function basis-trichotomy.
Additionally, this PR also contains a proof of the fact that the compact opens of the initial frame are exactly its clopens, which are the decidable propositions. This fact wasn’t needed in the proof in the end, but I’m including it in the PR regardless.
This PR adds a proof that the Scott locale of the Sierpiński dcpo has the universal property of the Sierpiński locale (i.e. the property of being the free frame on one generator).
In order to prove this, I had to prove that the basic opens of the Scott locale of the Sierpiński dcpo are either one of
𝟏,𝟎, or{⊤}. This is the proof implemented by the functionbasis-trichotomy.Additionally, this PR also contains a proof of the fact that the compact opens of the initial frame are exactly its clopens, which are the decidable propositions. This fact wasn’t needed in the proof in the end, but I’m including it in the PR regardless.