Agda formalisation

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

module AgdaContents where


-- Graph theoretical framework
------------------------------

-- ∙ What is a graph?
import lib.graph-definitions.Graph
import lib.graph-definitions.Alternative-definition-is-equiv

-- ∙ Graph forms a univalent category
import lib.graph-definitions.Graph.EquivalencePrinciple
import lib.graph-definitions.Graph.IsomorphismInduction
import lib.graph-definitions.Graph.isGroupoid
import lib.graph-homomorphisms.Hom
import lib.graph-homomorphisms.classes.Isomorphisms
import lib.graph-homomorphisms.classes.Isomorphisms.Exponentiation
import lib.graph-homomorphisms.classes.EdgeInjective
import lib.graph-homomorphisms.classes.Injective
import lib.graph-homomorphisms.classes.EdgeInjective.Lemmas
import lib.graph-homomorphisms.Lemmas

-- ∙ Isomorphisms
import lib.graph-relations.Isomorphic
import lib.graph-relations.Isomorphic.isSet
import lib.graph-relations.Homomorphic
import lib.graph-calculation-reasoning.Isos

-- ∙ Walks in a graph
import lib.graph-walks.Walk
import lib.graph-walks.Walk.Composition
import lib.graph-walks.Walk.SigmaWalks
import lib.graph-walks.Walk.Equality
import lib.graph-walks.Walk.isSet

-- ∙ Special kind of walks
import lib.graph-walks.Walk.QuasiSimple
import lib.graph-walks.Walk.QuasiSimpleFinite

-- ∙ Graph transformation
import lib.graph-transformations.U
import lib.graph-transformations.W
import lib.graph-transformations.Inv

-- ∙ What is a map?
import lib.graph-embeddings.Map
import lib.graph-embeddings.Map.Face
import lib.graph-embeddings.Map.Face.isSet
import lib.graph-embeddings.Map.Face.Walk
import lib.graph-embeddings.Finiteness

-- ∙ What is homotopy for walks?
import lib.graph-embeddings.Map.Face.Walk.Homotopy
import lib.graph-embeddings.Map.Face.Walk.Whiskering

-- ∙ A special kind of map
import lib.graph-embeddings.Map.Spherical
import lib.graph-embeddings.Map.Spherical-is-enough

-- ‌∙ What is a planar graph-embedding?
import lib.graph-embeddings.Planar
import lib.graph-embeddings.Planar.isSet

-- Examples:
-- ∙ The one-point graph is planar.
import lib.graph-embeddings.Map.Face.Example

-- ∙ The higher-inductive of a graph
-- Here is the reason why we need the flag --rewriting.
import lib.graph-embeddings.HIT
import lib.graph-embeddings.HIT.toProp
import lib.graph-embeddings.HIT.Homotopic-are-equal

-- ∙ Families of graphs
import lib.graph-families.CycleGraph
import lib.graph-families.CycleGraph.RotHom
import lib.graph-families.CycleGraph.Isomorphisms.IdentityType
import lib.graph-families.CycleGraph.Isomorphisms.Lemmas
import lib.graph-families.CycleGraph.Map
import lib.graph-families.CycleGraph.isCyclicGraph
import lib.graph-families.CycleGraph.isFiniteGraph
import lib.graph-families.CycleGraph.Walk
import lib.graph-families.BouquetGraph
import lib.graph-families.CompleteGraph

-- ∙ Graph classes
import lib.graph-classes.CyclicGraph
import lib.graph-classes.CyclicGraph.Stuff
import lib.graph-classes.CyclicGraph.isFiniteGraph
import lib.graph-classes.CyclicGraph.Walk
import lib.graph-classes.EmptyGraph
import lib.graph-classes.UnitGraph
import lib.graph-classes.StarGraph
import lib.graph-classes.CompleteGraph
import lib.graph-classes.ConnectedGraph
import lib.graph-classes.FiniteGraph
import lib.graph-classes.UndirectedGraph
import lib.graph-classes.PartiteGraph

-- Appendix. Univalent foundations
----------------------------------

import foundations.Core        -- ∙ Basic results in HoTT
import foundations.Nat         -- ∙ More lemmas on naturals
import foundations.Fin         -- ∙ ⟦ n ⟧ ∶≡ { 0,1,2,⋯, n-1}.
import foundations.Finite      -- ∙ Finite types ∑[ n ] ∥ A ≃ ⟦ n ⟧ ∥.
import foundations.Cyclic      -- ∙ Cyclic types

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