{-# OPTIONS --cubical --safe #-}

module Index where

import Basis
open import FormalTopology
open import Cover

import Poset
import Frame

import Nucleus
import CoverFormsNucleus
import UniversalProperty

import Cubical.Relation.Nullary
import Cubical.Relation.Nullary.DecidableEq
import Cubical.Foundations.Univalence
import Cubical.Foundations.SIP

open import Cubical.Data.Bool using (Bool; _≟_)

open import SnocList Bool _≟_
import Compactness
import CantorSpace

Chapter 2: Foundations

2.3: Equivalence and univalence

Definition 2.1.

_ = Basis.isContr

Definition 2.2.

_ = Basis.fiber

Definition 2.3.

_ = Basis.isEquiv

Definition 2.4.

_ = Basis._≃_

Definition 2.5.

_ = Basis.idEquiv

Definition 2.6.

_ = Cubical.Foundations.Univalence.pathToEquiv

Definition 2.7.

_ = Basis._~_

Proposition 2.8.

_ = Basis.funExt

2.4: Homotopy levels

Definition 2.9.

_ = Basis.isOfHLevel

Proposition 2.10.

_ = Basis.isOfHLevelSuc

Proposition 2.11.

_ = Basis.isOfHLevelΠ

Proposition 2.12.

_ = Basis.isOfHLevelΣ

Definition 2.13 is omitted.

Definition 2.14.

_ = Basis.isProp

Proposition 2.15 is omitted.

Definition 2.16.

_ = Basis.hProp

Proposition 2.17.

_ = Basis.isPropΠ

Proposition 2.18.

_ = Basis.isPropΣ

Proposition 2.19.

_ = Basis.isPropIsProp

Proposition 2.20.

_ = Basis.Σ≡Prop

Definition 2.21. This is defined directly for h-propositions in the cubical library.

_ = Basis._⇔_

Proposition 2.22.

_ = Basis.⇔toPath

Definition 2.23.

_ = Basis.Iso

Proposition 2.24.

_ = Basis.isoToEquiv
_ = Basis.equivToIso

Definition 2.25.

_ = Basis.isSet

Proposition 2.26.

_ = Basis.isProp→isSet

Proposition 2.27.

_ = Basis.isSetHProp

Proposition 2.28.

_ = Basis.isSetΠ

Proposition 2.29.

_ = Basis.isSetΣ

Proposition 2.30.

_ = Basis.isPropIsSet

Definition 2.31.

_ = Cubical.Relation.Nullary.Dec

Definition 2.32.

_ = Cubical.Relation.Nullary.Discrete

Theorem 2.33.

_ = Cubical.Relation.Nullary.DecidableEq.Discrete→isSet

2.5: Powersets

Definition 2.34.

_ = Basis.𝒫

Proposition 2.35.

_ = Basis.𝒫-set

Definition 2.36.

_ = Basis._⊆_

Definition 2.37.

_ = Basis.entire

Definition 2.38.

_ = Basis._∩_

2.6: Families

Definition 2.39.

_ = Basis.Fam

Definition 2.41.

_ = Basis._ε_

Definition 2.42.

_ = Basis._⟨$⟩_

Definition 2.43.

_ = Basis.⟪_⟫

2.8: Truncation

Definition 2.44.

_ = Basis.∥_∥
_ = Basis.∥∥-prop
_ = Basis.∥∥-rec

Chapter 3: Frames

3.1: Partially ordered sets

Definition 3.1.

_ = Poset.Poset
_ = Poset.PosetStr
_ = Poset.PosetAx

Definition 3.2.

_ = Poset.isDownwardsClosed
_ = Poset.DCSubset

Proposition 3.3.

_ = Poset.DCSubset-set

Proposition 3.4.

_ = Frame.DCPoset

Definition 3.5.

_ = Poset.isMonotonic

Definition 3.6.

_ = Poset.isPosetIso

3.2: Definition of a frame

Definition 3.7.

_ = Frame.RawFrameStr
_ = Frame.FrameAx
_ = Frame.FrameStr

Proposition 3.8.

_ = Frame.FrameAx-props

Definition 3.9.

_ = Frame.isFrameHomomorphism
_ = Frame._─f→_
_ = Frame._≅f_

Definition 3.10.

_ = Frame.isFrameIso

Definition 3.11 is not explicitly defined. We refer to it in an ad hoc way by referring to _≅ₚ_ on the underlying posets.

The equivalence of Defn. 3.10 and Defn. 3.11 is stated only in passing in the thesis, not as an explicit proposition but is witnessed in the Agda code by the following function:

_ = Frame.≅ₚ≃≅f

3.3: Some properties of frames

Proposition 3.12.

_ = Frame.comm

Lemma 3.13.

_ = Frame.flatten

Proposition 3.14.

_ = Frame.family-iff

Proposition 3.15.

_ = Frame.sym-distr

3.4: Univalence for frames

Definition 3.16.

_ = Poset.isAMonotonicEqv

Definition 3.17.

_ = Cubical.Foundations.SIP.SIP

Definition 3.18.

_ = Frame.isHomoEqv

Equation 3.19.

_ = Frame.≃f≃≡

Equation 3.20.

_ = Frame.≃f≃≅ₚ

Equation 3.21.

_ = Frame.≅ₚ≃≡

3.5: Frames of downwards-closed subsets

Theorem 3.22.

_ = Frame.DCFrame

3.6: Nuclei and their fixed points

Definition 3.23.

_ = Nucleus.isNuclear
_ = Nucleus.Nucleus

Proposition 3.24.

_ = Nucleus.nuclei-resp-⊤

Lemma 3.25. This is broken up into two functions in the Agda formalisatoin.

_ = Frame.x⊑y⇒x=x∧y
_ = Frame.x=x∧y⇒x⊑y

Proposition 3.26.

_ = Nucleus.mono

Proposition 3.27.

_ = Nucleus.𝔣𝔦𝔵-pos

Theorem 3.28.

_ = Nucleus.𝔣𝔦𝔵

Chapter 4: Formal Topology

4.1: Interaction systems

Definition 4.1.

_ = InteractionStr
_ = InteractionSys

Definition 4.2.

_ = hasMono

Definition 4.3.

_ = hasSimulation

Definition 4.4.

_ = FormalTopology

4.2: Cover relation

Note that Definition 4.5 is not formalised.

Definition 4.7.

_ = CoverFromFormalTopology._◁_

Proposition 4.8.

_ = CoverFromFormalTopology.◁-lem₁

Proposition 4.9.

_ = CoverFromFormalTopology.◁-lem₂

Proposition 4.10.

_ = CoverFromFormalTopology.◁-lem₃

Proposition 4.11.

_ = CoverFromFormalTopology.◁-lem₄

4.3: Covers are nuclei

Theorem 4.12.

_ = CoverFormsNucleus.NucleusFrom.𝕛-nuclear

4.4: Lifting into the generated frame

Definition 4.13.

_ = CoverFormsNucleus.NucleusFrom.η

4.5: Formal topologies present

Definition 4.14.

_ = UniversalProperty.represents

Definition 4.15.

_ = UniversalProperty.isFlat

Theorem 4.16.

The theorem statement is given in:

_ = UniversalProperty.universal-prop

The proof is given in:

_ = UniversalProperty.main

Lemma 4.17.

_ = UniversalProperty.main-lemma

Lemma 4.18.

_ = UniversalProperty.MainProof.resp-⋁-lem

Chapter 5: The Cantor space

5.1: The Cantor interaction system

Definition 5.1.

_ = SnocList._⌢_
_ = SnocList.[]

Definition 5.2.

_ = _++_

Proposition 5.3.

_ = SnocList-discrete

Definition 5.4.

_ = CantorSpace.ℂ-pos

Definition 5.5.

_ = CantorSpace.ℂ-IS

Theorem 5.6.

_ = CantorSpace.cantor

5.2: The Cantor space is compact

Definition 5.7.

_ = Compactness.down

Definition 5.8.

_ = Compactness.isCompact

Lemma 5.9.

_ = CantorSpace.U⊆V⇒◁U⊆◁V

Lemma 5.10. In the Agda formalisation, this is broken up into two functions.

_ = CantorSpace.↓-++-left
_ = CantorSpace.↓-++-right

Lemma 5.11.

_ = CantorSpace.◁^-decide

Theorem 5.12.

_ = CantorSpace.compact