Add comments to the locale theory development #190
Description
Make sure that each of the following modules is properly commented:
-
AdjointFunctorTheoremForFrames.lagda -
BooleanAlgebra.lagda -
CharacterisationOfContinuity.lagda -
ClassificationOfScottOpens.lagda -
Clopen.lagda -
CompactRegular.lagda -
Compactness.lagda -
Complements.lagda -
Frame.lagda -
GaloisConnection.lagda -
HeytingComplementation.lagda -
HeytingImplication.lagda -
InitialFrame.lagda -
NotationalConventions.lagda -
Nucleus.lagda -
PatchLocale.lagda -
PatchOfOmega.lagda -
PatchProperties.lagda -
PerfectMaps.lagda -
Regular.lagda -
ScottContinuity.lagda -
ScottLocale.lagda -
Sierpinski.lagda -
SmallBasis.lagda -
Stone.lagda -
StoneImpliesSpectral.lagda -
UniversalPropertyOfPatch.lagda -
WellInside.lagda -
ZeroDimensionality.lagda -
index.lagda -
Properties.lagda -
Spectrality.SpectralLocale.lagda -
Spectrality.SpectralMap.lagda -
Spectrality.SpectralityOfOmega.lagda -
WayBelowRelation.Definition.lagda -
WayBelowRelation.Properties.lagda