Everything

{-# OPTIONS --without-K --exact-split --rewriting --allow-unsolved-metas #-}
module Everything where

open import AgdaContents
open import CPP2022-paper
open import foundations.AlgebraOnDependentPaths
open import foundations.AlgebraOnPaths
open import foundations.BasicEquivalences
open import foundations.BasicFunctions
open import foundations.BasicTypes
open import foundations.CoproductIdentities
open import foundations.Core
open import foundations.Cyclic
open import foundations.DecidableEquality
open import foundations.DependentAlgebra
open import foundations.EquivalenceReasoning
open import foundations.EquivalenceType
open import foundations.FibreType
open import foundations.Finite
open import foundations.Fin
open import foundations.FunExtAxiom
open import foundations.FunExtTransportDependent
open import foundations.FunExtTransport
open import foundations.HalfAdjointType
open import foundations.HedbergLemmas
open import foundations.HLevelLemmas
open import foundations.HLevelTypes
open import foundations.HomotopyLemmas
open import foundations.HomotopyType
open import foundations.IntegerType
open import foundations.MonoidType
open import foundations.Nat
open import foundations.NaturalsType
open import foundations.PiPreserves
open import foundations.ProductIdentities
open import foundations.QuasiinverseLemmas
open import foundations.QuasiinverseType
open import foundations.RelationType
open import foundations.Rewriting
open import foundations.SectionsAndRetractions
open import foundations.SigmaEquivalence
open import foundations.SigmaPreserves
open import foundations.Transport
open import foundations.TransportLemmas
open import foundations.TruncationType
open import foundations.Type
open import foundations.TypesofMorphisms
open import foundations.UnivalenceAxiom
open import foundations.UnivalenceIdEquiv
open import foundations.UnivalenceLemmas
open import foundations.UnivalenceTransport
open import lib.graph-calculation-reasoning.Isos
open import lib.graph-classes.CompleteGraph
open import lib.graph-classes.ConnectedGraph
open import lib.graph-classes.CyclicGraph.isFiniteGraph
open import lib.graph-classes.CyclicGraph
open import lib.graph-classes.CyclicGraph.Stuff
open import lib.graph-classes.CyclicGraph.Walk
open import lib.graph-classes.EmptyGraph
open import lib.graph-classes.FiniteGraph
open import lib.graph-classes.PartiteGraph
open import lib.graph-classes.StarGraph
open import lib.graph-classes.UndirectedGraph
open import lib.graph-classes.UnitGraph
open import lib.graph-definitions.Alternative-definition-is-equiv
open import lib.graph-definitions.Graph.EquivalencePrinciple
open import lib.graph-definitions.Graph.isGroupoid
open import lib.graph-definitions.Graph.IsomorphismInduction
open import lib.graph-definitions.Graph
open import lib.graph-embeddings.Finiteness
open import lib.graph-embeddings.HIT.Homotopic-are-equal
open import lib.graph-embeddings.HIT
open import lib.graph-embeddings.HIT.toProp
open import lib.graph-embeddings.Map.Face.Example
open import lib.graph-embeddings.Map.Face.isSet
open import lib.graph-embeddings.Map.Face
open import lib.graph-embeddings.Map.Face.Walk.Homotopy
open import lib.graph-embeddings.Map.Face.Walk
open import lib.graph-embeddings.Map.Face.Walk.Whiskering
open import lib.graph-embeddings.Map
open import lib.graph-embeddings.Map.Spherical-is-enough
open import lib.graph-embeddings.Map.Spherical
open import lib.graph-embeddings.Planar.isSet
open import lib.graph-embeddings.Planar
open import lib.graph-families.BouquetGraph
open import lib.graph-families.CompleteGraph
open import lib.graph-families.CycleGraph.isCyclicGraph
open import lib.graph-families.CycleGraph.isFiniteGraph
open import lib.graph-families.CycleGraph.Isomorphisms.IdentityType
open import lib.graph-families.CycleGraph.Isomorphisms.Lemmas
open import lib.graph-families.CycleGraph
open import lib.graph-families.CycleGraph.Map
open import lib.graph-families.CycleGraph.RotHom
open import lib.graph-families.CycleGraph.Walk
open import lib.graph-homomorphisms.classes.EdgeInjective
open import lib.graph-homomorphisms.classes.EdgeInjective.Lemmas
open import lib.graph-homomorphisms.classes.Injective
open import lib.graph-homomorphisms.classes.Isomorphisms.Exponentiation
open import lib.graph-homomorphisms.classes.Isomorphisms
open import lib.graph-homomorphisms.classes.Isomorphisms.Trivial
open import lib.graph-homomorphisms.Hom
open import lib.graph-homomorphisms.Lemmas
open import lib.graph-relations.Homomorphic
open import lib.graph-relations.Isomorphic.isSet
open import lib.graph-relations.Isomorphic
open import lib.graph-transformations.Inv
open import lib.graph-transformations.U
open import lib.graph-transformations.W
open import lib.graph-walks.Walk.Composition
open import lib.graph-walks.Walk.Equality
open import lib.graph-walks.Walk.isSet
open import lib.graph-walks.Walk
open import lib.graph-walks.Walk.QuasiSimpleFinite
open import lib.graph-walks.Walk.QuasiSimple
open import lib.graph-walks.Walk.SigmaWalks
open import README

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