CPP2022-paper.md.

Version of Sunday, January 22, 2023, 10:42 PM

# Agda formalisation

```{-# OPTIONS --without-K --exact-split  #-}

module CPP2022-paper where

open import foundations.Core
open import foundations.Finite
open import foundations.Cyclic

open import lib.graph-definitions.Graph
open import lib.graph-walks.Walk
open import lib.graph-walks.Walk.isSet

open import lib.graph-walks.Walk.QuasiSimple
open WR

open import lib.graph-walks.Walk.QuasiSimpleFinite
open finiteness-lemmas

open import lib.graph-embeddings.Map
open import lib.graph-embeddings.Map.Face
open import lib.graph-embeddings.Map.Face.Walk.Homotopy
open import lib.graph-embeddings.Map.Face.Walk.Whiskering
open import lib.graph-embeddings.Map.Spherical
open import lib.graph-embeddings.Map.Spherical-is-enough
```

## Paper’s results

```-- 2. Basics of homotopy type theory
Thm-2∙1 = hedberg
Def-2∙2 = isFinite
Lem-2∙3 = equiv-preserves-finiteness
Lem-2∙4 = decidable-→-≡-is-finite
Def-2∙5 = CyclicSet

-- 3. The type of graphs
Def-3∙1  = Graph

-- 4. Walks
Def-4∙1 = Walk
Lem-4∙2 = Walk-is-set
Def-4∙3 = _⊰_
Lem-4∙4 = ∑∑walk-wf
Thm-4∙5 = ∑∑walk-rec

-- 4.3 Quasi-simple walk
Def-4∙6  = ∈-walk._∈w_
Lem-4∙7  = _?∈_
Def-4∙8  = quasi-simple-walks.isQuasi
Lem-4∙9  = quasi-simple-walks.being-quasi-simple-is-prop
Lem-4∙10 = ⊙-quasi-simple-is-quasi-simple
Lem-4∙11 = conservation
Cor-4∙12a = quasi-simple-walks.one-point-walk-is-quasi-simple
Cor-4∙12b = one-edge-is-quasi-simple
Lem-4∙13 = ?is-quasi-simple

-- 4.4 Finiteness
Lem-4∙14 = equiv-fin-sigma-∈
Lem-4∙15 = ∈w-is-finite
Def-4∙16 = finite-quasi-simple-walks-type
Lem-4∙17 = qswalk-equiv-sigmas
Lem-4∙18 = finite-qswalks
Lem-4∙19 = sigma-qswalks-forms-finite-set
Lem-4∙20 = qswalks-has-bounded-length
Lem-4∙21 = quasi-quasi-simple-equiv-qswalk
Thm-4∙22 = finite-graph-has-finite-quasi-simple-walks

-- 4.5 Walk splitting
Def-4∙23 = Prefix
Lem-4∙24 = find-suffix
Def-4∙25 = SplitAt
Lem-4∙26 = split_at_

-- 4.6 Normal forms
Def-4∙27-1 = Loop
Def-4∙27-2 = Trivial
Def-4∙27-3 = NonTrivial
Def-4∙27-4 = NoReduce
Def-4∙27-5 = NonTrivialLoop
Def-4∙28-1 = different-endpoints-is-nontrivial
Def-4∙28-2 = ∈-non-trivial
Def-4∙28-3 = is-concat
Def-4∙29   = _→r_
Def-4∙30   = _→r*_
Def-4∙31-1 = nf-∈
Def-4∙31-2 = length-lem→r
Def-4∙32   = Reduce
Def-4∙33   = Normal
Lem-4∙34   = Normal-is-prop
Ex-4∙35    = No-reduce-is-normal
Def-4∙36   = Progress
Thm-4∙37   = normalize
Cor-4∙38-1 = ?reduce
Cor-4∙38-2 = ?normal
Cor-4∙38-3 = progress

-- 5. The notion of walk homotopy
Def-5∙1 = Map
Rem-4   = Face

-- 5.1. Homotopy of walks
Def-5∙2   = HomotopyWalks._∼hwalk_
Lem-5∙3-1 = Whiskering.whiskerR
Lem-5∙3-2 = Whiskering.whiskerL
Lem-5∙3-3 = Whiskering.whisker-h

-- 5.2 Homotopy walks in the sphere
Def-5∙4 = isSphericalMap
Def-5∙5 = isSphericalMap'
Lem-5∙6 = hom-normalisation.e⊙∼
Thm-5∙7 = hom-normalisation.hom-normalize
Cor-5∙8 = spherical-equiv
```

## Latest changes

```(2022-12-28)(57c278b4) Last updated: 2021-09-16 15:00:00 by jonathan.cubides
(2022-07-06)(d3a4a8cf) minors by jonathan.cubides
(2022-01-26)(4aef326b) [ reports ] added some revisions by jonathan.cubides
(2021-12-20)(049db6a8) Added code of cubical experiments. by jonathan.cubides
(2021-12-20)(961730c9) [ html ] regular update by jonathan.cubides
(2021-12-20)(e0ef9faa) Fixed compilation and format, remove hidden parts by jonathan.cubides
(2021-12-20)(5120e5d1) Added cubical experiment to the master by jonathan.cubides
(2021-12-17)(828fdd0a) More revisions added for CPP by jonathan.cubides
(2021-12-15)(0d6a99d8) Fixed some broken links and descriptions by jonathan.cubides
(2021-12-15)(662a1f2d) [ .gitignore ] add by jonathan.cubides
(2021-12-15)(0630ce66) Minor fixes by jonathan.cubides
(2021-12-13)(04f10eba) Fixed a lot of details by jonathan.cubides
(2021-12-10)(24195c9f) [ .gitignore ] ignore .zip and arxiv related files by jonathan.cubides
(2021-12-09)(538d2859) minor fixes before dinner by jonathan.cubides
(2021-12-09)(36a1a69f) [ planar.pdf ] w.i.p revisions to share on arxiv first by jonathan.cubides
```