module Cubical.Everything where import Cubical.Algebra.AbGroup import Cubical.Algebra.AbGroup.Base import Cubical.Algebra.AbGroup.Instances.DiffInt import Cubical.Algebra.AbGroup.Instances.DirectProduct import Cubical.Algebra.AbGroup.Instances.DirectSumFun import Cubical.Algebra.AbGroup.Instances.DirectSumHIT import Cubical.Algebra.AbGroup.Instances.FreeAbGroup import Cubical.Algebra.AbGroup.Instances.Hom import Cubical.Algebra.AbGroup.Instances.Int import Cubical.Algebra.AbGroup.Instances.IntMod import Cubical.Algebra.AbGroup.Instances.NProd import Cubical.Algebra.AbGroup.Instances.Pi import Cubical.Algebra.AbGroup.Instances.Unit import Cubical.Algebra.AbGroup.Properties import Cubical.Algebra.AbGroup.TensorProduct import Cubical.Algebra.Algebra import Cubical.Algebra.Algebra.Base import Cubical.Algebra.Algebra.Properties import Cubical.Algebra.Algebra.Subalgebra import Cubical.Algebra.Algebra.Univalence import Cubical.Algebra.BooleanRing import Cubical.Algebra.BooleanRing.Base import Cubical.Algebra.ChainComplex import Cubical.Algebra.ChainComplex.Base import Cubical.Algebra.ChainComplex.Finite import Cubical.Algebra.ChainComplex.Homology import Cubical.Algebra.CommAlgebra import Cubical.Algebra.CommAlgebra.AsModule import Cubical.Algebra.CommAlgebra.AsModule.Base import Cubical.Algebra.CommAlgebra.AsModule.FreeCommAlgebra import Cubical.Algebra.CommAlgebra.AsModule.FreeCommAlgebra.Base import Cubical.Algebra.CommAlgebra.AsModule.FreeCommAlgebra.OnCoproduct import Cubical.Algebra.CommAlgebra.AsModule.FreeCommAlgebra.Properties import Cubical.Algebra.CommAlgebra.AsModule.Ideal import Cubical.Algebra.CommAlgebra.AsModule.Instances.Initial import Cubical.Algebra.CommAlgebra.AsModule.Instances.Pointwise import Cubical.Algebra.CommAlgebra.AsModule.Instances.Unit import Cubical.Algebra.CommAlgebra.AsModule.Kernel import Cubical.Algebra.CommAlgebra.AsModule.Localisation import Cubical.Algebra.CommAlgebra.AsModule.LocalisationAlgebra import Cubical.Algebra.CommAlgebra.AsModule.Properties import Cubical.Algebra.CommAlgebra.AsModule.QuotientAlgebra import Cubical.Algebra.CommAlgebra.AsModule.Subalgebra import Cubical.Algebra.CommAlgebra.AsModule.UnivariatePolyList import Cubical.Algebra.CommAlgebra.Base import Cubical.Algebra.CommAlgebra.FGIdeal import Cubical.Algebra.CommAlgebra.FP import Cubical.Algebra.CommAlgebra.FP.Base import Cubical.Algebra.CommAlgebra.FP.Instances import Cubical.Algebra.CommAlgebra.FP.Properties import Cubical.Algebra.CommAlgebra.FP.Quotient import Cubical.Algebra.CommAlgebra.Ideal import Cubical.Algebra.CommAlgebra.Instances.Initial import Cubical.Algebra.CommAlgebra.Instances.Terminal import Cubical.Algebra.CommAlgebra.Kernel import Cubical.Algebra.CommAlgebra.Localisation import Cubical.Algebra.CommAlgebra.Notation import Cubical.Algebra.CommAlgebra.Polynomials import Cubical.Algebra.CommAlgebra.Properties import Cubical.Algebra.CommAlgebra.Quotient import Cubical.Algebra.CommAlgebra.Quotient.Base import Cubical.Algebra.CommAlgebra.Quotient.FGIdealSum import Cubical.Algebra.CommAlgebra.Quotient.IdealSum import Cubical.Algebra.CommAlgebra.Quotient.Properties import Cubical.Algebra.CommAlgebra.Univalence import Cubical.Algebra.CommMonoid import Cubical.Algebra.CommMonoid.Base import Cubical.Algebra.CommMonoid.CommMonoidProd import Cubical.Algebra.CommMonoid.GrothendieckGroup import Cubical.Algebra.CommMonoid.Instances.FreeComMonoid import Cubical.Algebra.CommMonoid.Properties import Cubical.Algebra.CommRing import Cubical.Algebra.CommRing.Base import Cubical.Algebra.CommRing.BinomialThm import Cubical.Algebra.CommRing.DirectProd import Cubical.Algebra.CommRing.FGIdeal import Cubical.Algebra.CommRing.FiberedProduct import Cubical.Algebra.CommRing.Ideal import Cubical.Algebra.CommRing.Ideal.Base import Cubical.Algebra.CommRing.Ideal.Sum import Cubical.Algebra.CommRing.Ideal.SurjectiveImage import Cubical.Algebra.CommRing.Instances.BiInvInt import Cubical.Algebra.CommRing.Instances.Int import Cubical.Algebra.CommRing.Instances.IntMod import Cubical.Algebra.CommRing.Instances.Pointwise import Cubical.Algebra.CommRing.Instances.QuoInt import Cubical.Algebra.CommRing.Instances.Rationals import Cubical.Algebra.CommRing.Instances.Unit import Cubical.Algebra.CommRing.Kernel import Cubical.Algebra.CommRing.LocalRing import Cubical.Algebra.CommRing.Localisation import Cubical.Algebra.CommRing.Localisation.Base import Cubical.Algebra.CommRing.Localisation.InvertingElements import Cubical.Algebra.CommRing.Localisation.Limit import Cubical.Algebra.CommRing.Localisation.PullbackSquare import Cubical.Algebra.CommRing.Localisation.UniversalProperty import Cubical.Algebra.CommRing.Polynomials.MultivariatePoly-Quotient import Cubical.Algebra.CommRing.Polynomials.MultivariatePoly-notationZ import Cubical.Algebra.CommRing.Polynomials.MultivariatePoly-notationZ2 import Cubical.Algebra.CommRing.Polynomials.MultivariatePoly import Cubical.Algebra.CommRing.Polynomials.Typevariate import Cubical.Algebra.CommRing.Polynomials.Typevariate.Base import Cubical.Algebra.CommRing.Polynomials.Typevariate.OnCoproduct import Cubical.Algebra.CommRing.Polynomials.Typevariate.Properties import Cubical.Algebra.CommRing.Polynomials.Typevariate.UniversalProperty import Cubical.Algebra.CommRing.Polynomials.UnivariatePolyFun import Cubical.Algebra.CommRing.Polynomials.UnivariatePolyHIT import Cubical.Algebra.CommRing.Polynomials.UnivariatePolyList import Cubical.Algebra.CommRing.Properties import Cubical.Algebra.CommRing.Quotient import Cubical.Algebra.CommRing.Quotient.Base import Cubical.Algebra.CommRing.Quotient.IdealSum import Cubical.Algebra.CommRing.RadicalIdeal import Cubical.Algebra.CommRing.Univalence import Cubical.Algebra.CommSemiring import Cubical.Algebra.CommSemiring.Base import Cubical.Algebra.CommSemiring.Instances.Nat import Cubical.Algebra.CommSemiring.Instances.UpperNat import Cubical.Algebra.DirectSum.DirectSumFun.Base import Cubical.Algebra.DirectSum.DirectSumFun.Properties import Cubical.Algebra.DirectSum.DirectSumHIT.Base import Cubical.Algebra.DirectSum.DirectSumHIT.Properties import Cubical.Algebra.DirectSum.DirectSumHIT.PseudoNormalForm import Cubical.Algebra.DirectSum.DirectSumHIT.UniversalProperty import Cubical.Algebra.DirectSum.Equiv-DSHIT-DSFun import Cubical.Algebra.DistLattice import Cubical.Algebra.DistLattice.Base import Cubical.Algebra.DistLattice.Basis import Cubical.Algebra.DistLattice.BigOps import Cubical.Algebra.DistLattice.Downset import Cubical.Algebra.DistLattice.Properties import Cubical.Algebra.Field import Cubical.Algebra.Field.Base import Cubical.Algebra.Field.Instances.Rationals import Cubical.Algebra.GradedRing.Base import Cubical.Algebra.GradedRing.DirectSumFun import Cubical.Algebra.GradedRing.DirectSumHIT import Cubical.Algebra.GradedRing.Instances.CohomologyRing import Cubical.Algebra.GradedRing.Instances.CohomologyRingFun import Cubical.Algebra.GradedRing.Instances.Polynomials import Cubical.Algebra.GradedRing.Instances.PolynomialsFun import Cubical.Algebra.GradedRing.Instances.TrivialGradedRing import Cubical.Algebra.Group import Cubical.Algebra.Group.Abelianization.AbelianizationAsCoeq import Cubical.Algebra.Group.Abelianization.Base import Cubical.Algebra.Group.Abelianization.Properties import Cubical.Algebra.Group.Base import Cubical.Algebra.Group.DirProd import Cubical.Algebra.Group.Exact import Cubical.Algebra.Group.Five import Cubical.Algebra.Group.Free import Cubical.Algebra.Group.GroupPath import Cubical.Algebra.Group.Instances.Bool import Cubical.Algebra.Group.Instances.DiffInt import Cubical.Algebra.Group.Instances.Int import Cubical.Algebra.Group.Instances.IntMod import Cubical.Algebra.Group.Instances.NProd import Cubical.Algebra.Group.Instances.Pi import Cubical.Algebra.Group.Instances.Unit import Cubical.Algebra.Group.IsomorphismTheorems import Cubical.Algebra.Group.MorphismProperties import Cubical.Algebra.Group.Morphisms import Cubical.Algebra.Group.Properties import Cubical.Algebra.Group.QuotientGroup import Cubical.Algebra.Group.Subgroup import Cubical.Algebra.Group.ZAction import Cubical.Algebra.IntegerMatrix.Base import Cubical.Algebra.IntegerMatrix.Diagonalization import Cubical.Algebra.IntegerMatrix.Elementaries import Cubical.Algebra.IntegerMatrix.Smith import Cubical.Algebra.IntegerMatrix.Smith.NormalForm import Cubical.Algebra.IntegerMatrix.Smith.Normalization import Cubical.Algebra.Lattice import Cubical.Algebra.Lattice.Base import Cubical.Algebra.Lattice.Properties import Cubical.Algebra.LindenbaumTarski import Cubical.Algebra.Matrix import Cubical.Algebra.Matrix.CommRingCoefficient import Cubical.Algebra.Matrix.Elementaries import Cubical.Algebra.Matrix.RowTransformation import Cubical.Algebra.Module import Cubical.Algebra.Module.Base import Cubical.Algebra.Module.Instances.FinMatrix import Cubical.Algebra.Module.Instances.FinVec import Cubical.Algebra.Module.Properties import Cubical.Algebra.Module.Submodule import Cubical.Algebra.Monoid import Cubical.Algebra.Monoid.Base import Cubical.Algebra.Monoid.BigOp import Cubical.Algebra.Monoid.Instances.Nat import Cubical.Algebra.Monoid.Instances.NatPlusBis import Cubical.Algebra.Monoid.Instances.NatVec import Cubical.Algebra.Monoid.Submonoid import Cubical.Algebra.OrderedCommMonoid import Cubical.Algebra.OrderedCommMonoid.Base import Cubical.Algebra.OrderedCommMonoid.Instances import Cubical.Algebra.OrderedCommMonoid.PropCompletion import Cubical.Algebra.OrderedCommMonoid.Properties import Cubical.Algebra.Polynomials.Multivariate.Base import Cubical.Algebra.Polynomials.Multivariate.EquivCarac.AB-An[X]Bn[X] import Cubical.Algebra.Polynomials.Multivariate.EquivCarac.A[X]X-A import Cubical.Algebra.Polynomials.Multivariate.EquivCarac.An[Am[X]]-Anm[X] import Cubical.Algebra.Polynomials.Multivariate.EquivCarac.An[X]X-A import Cubical.Algebra.Polynomials.Multivariate.EquivCarac.Poly0-A import Cubical.Algebra.Polynomials.TypevariateHIT import Cubical.Algebra.Polynomials.TypevariateHIT.Base import Cubical.Algebra.Polynomials.TypevariateHIT.EquivUnivariateListPoly import Cubical.Algebra.Polynomials.UnivariateFun.Base import Cubical.Algebra.Polynomials.UnivariateHIT.Base import Cubical.Algebra.Polynomials.UnivariateList.Base import Cubical.Algebra.Polynomials.UnivariateList.Poly1-1Poly import Cubical.Algebra.Polynomials.UnivariateList.Properties import Cubical.Algebra.Polynomials.UnivariateList.UniversalProperty import Cubical.Algebra.Ring import Cubical.Algebra.Ring.Base import Cubical.Algebra.Ring.BigOps import Cubical.Algebra.Ring.DirectProd import Cubical.Algebra.Ring.Ideal import Cubical.Algebra.Ring.Ideal.Base import Cubical.Algebra.Ring.Ideal.SurjectiveImage import Cubical.Algebra.Ring.Kernel import Cubical.Algebra.Ring.Properties import Cubical.Algebra.Ring.Quotient import Cubical.Algebra.Semigroup import Cubical.Algebra.Semigroup.Base import Cubical.Algebra.Semilattice import Cubical.Algebra.Semilattice.Base import Cubical.Algebra.Semilattice.Instances.NatMax import Cubical.Algebra.Semiring import Cubical.Algebra.Semiring.Base import Cubical.Algebra.Semiring.BigOps import Cubical.Algebra.SymmetricGroup import Cubical.AlgebraicGeometry.Functorial.ZFunctors.Base import Cubical.AlgebraicGeometry.Functorial.ZFunctors.CompactOpen import Cubical.AlgebraicGeometry.Functorial.ZFunctors.OpenSubscheme import Cubical.AlgebraicGeometry.Functorial.ZFunctors.QcQsScheme import Cubical.AlgebraicGeometry.ZariskiLattice.Base import Cubical.AlgebraicGeometry.ZariskiLattice.Properties import Cubical.AlgebraicGeometry.ZariskiLattice.StructureSheaf import Cubical.AlgebraicGeometry.ZariskiLattice.StructureSheafPullback import Cubical.AlgebraicGeometry.ZariskiLattice.UniversalProperty import Cubical.Axiom.Choice import Cubical.Axiom.Omniscience import Cubical.Axiom.UniquenessOfIdentity import Cubical.CW.Approximation import Cubical.CW.Base import Cubical.CW.ChainComplex import Cubical.CW.Connected import Cubical.CW.Homology import Cubical.CW.Homotopy import Cubical.CW.Map import Cubical.CW.Properties import Cubical.CW.Subcomplex import Cubical.Categories.Abelian import Cubical.Categories.Abelian.Base import Cubical.Categories.Abelian.Instances.Terminal import Cubical.Categories.Additive import Cubical.Categories.Additive.Base import Cubical.Categories.Additive.Instances.Terminal import Cubical.Categories.Additive.Properties import Cubical.Categories.Additive.Quotient import Cubical.Categories.Adjoint import Cubical.Categories.Category import Cubical.Categories.Category.Base import Cubical.Categories.Category.Path import Cubical.Categories.Category.Properties import Cubical.Categories.Commutativity import Cubical.Categories.Constructions.BinProduct import Cubical.Categories.Constructions.DisplayOverTerminal import Cubical.Categories.Constructions.Elements import Cubical.Categories.Constructions.Elements.Properties import Cubical.Categories.Constructions.EssentialImage import Cubical.Categories.Constructions.Free import Cubical.Categories.Constructions.Free.Category import Cubical.Categories.Constructions.Free.Category.Base import Cubical.Categories.Constructions.Free.Category.Quiver import Cubical.Categories.Constructions.Free.Functor import Cubical.Categories.Constructions.FullSubcategory import Cubical.Categories.Constructions.Lift import Cubical.Categories.Constructions.Opposite import Cubical.Categories.Constructions.Power import Cubical.Categories.Constructions.Product import Cubical.Categories.Constructions.Quotient import Cubical.Categories.Constructions.Slice import Cubical.Categories.Constructions.Slice.Base import Cubical.Categories.Constructions.Slice.Functor import Cubical.Categories.Constructions.Slice.Properties import Cubical.Categories.Constructions.SubObject import Cubical.Categories.Constructions.TotalCategory import Cubical.Categories.Constructions.TotalCategory.Base import Cubical.Categories.Constructions.TotalCategory.Properties import Cubical.Categories.Constructions.TwistedArrow import Cubical.Categories.Constructions.Vertical import Cubical.Categories.Displayed.Adjoint import Cubical.Categories.Displayed.Base import Cubical.Categories.Displayed.BinProduct import Cubical.Categories.Displayed.Cartesian import Cubical.Categories.Displayed.Constructions.LeftAdjointToReindex import Cubical.Categories.Displayed.Constructions.PropertyOver import Cubical.Categories.Displayed.Constructions.Reindex.Base import Cubical.Categories.Displayed.Constructions.StructureOver import Cubical.Categories.Displayed.Constructions.StructureOver.Base import Cubical.Categories.Displayed.Constructions.StructureOver.Properties import Cubical.Categories.Displayed.Constructions.TotalCategory import Cubical.Categories.Displayed.Constructions.Weaken.Base import Cubical.Categories.Displayed.Functor import Cubical.Categories.Displayed.HLevels import Cubical.Categories.Displayed.Instances.Codomain import Cubical.Categories.Displayed.Instances.Path import Cubical.Categories.Displayed.Instances.Terminal import Cubical.Categories.Displayed.Instances.Terminal.Base import Cubical.Categories.Displayed.Instances.Terminal.Properties import Cubical.Categories.Displayed.NaturalTransformation import Cubical.Categories.Displayed.Reasoning import Cubical.Categories.Displayed.Section import Cubical.Categories.Displayed.Section.Base import Cubical.Categories.Displayed.Weaken import Cubical.Categories.DistLatticeSheaf.Base import Cubical.Categories.DistLatticeSheaf.ComparisonLemma import Cubical.Categories.DistLatticeSheaf.Diagram import Cubical.Categories.DistLatticeSheaf.Extension import Cubical.Categories.Equivalence import Cubical.Categories.Equivalence.AdjointEquivalence import Cubical.Categories.Equivalence.Base import Cubical.Categories.Equivalence.Properties import Cubical.Categories.Equivalence.WeakEquivalence import Cubical.Categories.Functor import Cubical.Categories.Functor.Base import Cubical.Categories.Functor.Compose import Cubical.Categories.Functor.ComposeProperty import Cubical.Categories.Functor.Equality import Cubical.Categories.Functor.Properties import Cubical.Categories.Functors.Constant import Cubical.Categories.Functors.HomFunctor import Cubical.Categories.Instances.AbGroups import Cubical.Categories.Instances.CommAlgebras import Cubical.Categories.Instances.CommRings import Cubical.Categories.Instances.Cospan import Cubical.Categories.Instances.Discrete import Cubical.Categories.Instances.DistLattice import Cubical.Categories.Instances.DistLattices import Cubical.Categories.Instances.EilenbergMoore import Cubical.Categories.Instances.FunctorAlgebras import Cubical.Categories.Instances.Functors import Cubical.Categories.Instances.Functors.Currying import Cubical.Categories.Instances.Functors.Endo import Cubical.Categories.Instances.Groups import Cubical.Categories.Instances.Lattice import Cubical.Categories.Instances.Lattices import Cubical.Categories.Instances.Poset import Cubical.Categories.Instances.Posets import Cubical.Categories.Instances.RingAlgebras import Cubical.Categories.Instances.Rings import Cubical.Categories.Instances.Semilattice import Cubical.Categories.Instances.Sets import Cubical.Categories.Instances.Terminal import Cubical.Categories.Instances.ZFunctors import Cubical.Categories.Isomorphism import Cubical.Categories.Limits import Cubical.Categories.Limits.BinCoproduct import Cubical.Categories.Limits.BinProduct import Cubical.Categories.Limits.Initial import Cubical.Categories.Limits.Limits import Cubical.Categories.Limits.Pullback import Cubical.Categories.Limits.RightKan import Cubical.Categories.Limits.Terminal import Cubical.Categories.Monad.Base import Cubical.Categories.Monoidal import Cubical.Categories.Monoidal.Base import Cubical.Categories.Monoidal.Enriched import Cubical.Categories.Monoidal.Strict.Monoid import Cubical.Categories.Morphism import Cubical.Categories.NaturalTransformation import Cubical.Categories.NaturalTransformation.Base import Cubical.Categories.NaturalTransformation.Properties import Cubical.Categories.Presheaf import Cubical.Categories.Presheaf.Base import Cubical.Categories.Presheaf.KanExtension import Cubical.Categories.Presheaf.Morphism import Cubical.Categories.Presheaf.NonPresheaf.Cofree import Cubical.Categories.Presheaf.NonPresheaf.Forget import Cubical.Categories.Presheaf.NonPresheaf.Free import Cubical.Categories.Presheaf.Properties import Cubical.Categories.Presheaf.Representable import Cubical.Categories.Profunctor import Cubical.Categories.Profunctor.Base import Cubical.Categories.RezkCompletion import Cubical.Categories.RezkCompletion.Base import Cubical.Categories.RezkCompletion.Construction import Cubical.Categories.Site.Cover import Cubical.Categories.Site.Coverage import Cubical.Categories.Site.Instances.ZariskiCommRing import Cubical.Categories.Site.Sheaf import Cubical.Categories.Site.Sheafification import Cubical.Categories.Site.Sheafification.Base import Cubical.Categories.Site.Sheafification.ElimProp import Cubical.Categories.Site.Sheafification.UniversalProperty import Cubical.Categories.Site.Sieve import Cubical.Categories.TypesOfCategories.TypeCategory import Cubical.Categories.UnderlyingGraph import Cubical.Categories.Yoneda import Cubical.Codata.Conat import Cubical.Codata.Conat.Base import Cubical.Codata.Conat.Bounded import Cubical.Codata.Conat.Properties import Cubical.Codata.Containers.Coalgebras import Cubical.Codata.Containers.CoinductiveContainers import Cubical.Codata.Everything import Cubical.Codata.M.Coalg import Cubical.Codata.M.Coalg.Base import Cubical.Codata.M.Container import Cubical.Codata.M.M import Cubical.Codata.M.M.Base import Cubical.Codata.M.M.Properties import Cubical.Codata.M.MRecord import Cubical.Codata.M.helper import Cubical.Codata.M.itree import Cubical.Codata.M.stream import Cubical.Codata.Stream import Cubical.Codata.Stream.Base import Cubical.Codata.Stream.Properties import Cubical.Cohomology.Base import Cubical.Cohomology.EilenbergMacLane.Base import Cubical.Cohomology.EilenbergMacLane.CupProduct import Cubical.Cohomology.EilenbergMacLane.EilenbergSteenrod import Cubical.Cohomology.EilenbergMacLane.Groups.Connected import Cubical.Cohomology.EilenbergMacLane.Groups.KleinBottle import Cubical.Cohomology.EilenbergMacLane.Groups.RP2 import Cubical.Cohomology.EilenbergMacLane.Groups.RP2wedgeS1 import Cubical.Cohomology.EilenbergMacLane.Groups.RPinf import Cubical.Cohomology.EilenbergMacLane.Groups.Sn import Cubical.Cohomology.EilenbergMacLane.Groups.Torus import Cubical.Cohomology.EilenbergMacLane.Groups.Unit import Cubical.Cohomology.EilenbergMacLane.Groups.Wedge import Cubical.Cohomology.EilenbergMacLane.Gysin import Cubical.Cohomology.EilenbergMacLane.MayerVietoris import Cubical.Cohomology.EilenbergMacLane.RingStructure import Cubical.Cohomology.EilenbergMacLane.Rings.KleinBottle import Cubical.Cohomology.EilenbergMacLane.Rings.RP2 import Cubical.Cohomology.EilenbergMacLane.Rings.RP2wedgeS1 import Cubical.Cohomology.EilenbergMacLane.Rings.RPinf import Cubical.Cohomology.EilenbergMacLane.Rings.Sn import Cubical.Cohomology.EilenbergMacLane.Rings.Z2-properties import Cubical.Core.Glue import Cubical.Core.Primitives import Cubical.Data.BinNat import Cubical.Data.BinNat.BinNat import Cubical.Data.Bool import Cubical.Data.Bool.Base import Cubical.Data.Bool.Properties import Cubical.Data.Bool.SwitchStatement import Cubical.Data.Cardinal import Cubical.Data.Cardinal.Base import Cubical.Data.Cardinal.Properties import Cubical.Data.Containers.Algebras import Cubical.Data.Containers.Base import Cubical.Data.Containers.ContainerExtensionProofs import Cubical.Data.Containers.InductiveContainers import Cubical.Data.DescendingList import Cubical.Data.DescendingList.Base import Cubical.Data.DescendingList.Examples import Cubical.Data.DescendingList.Properties import Cubical.Data.DescendingList.Strict import Cubical.Data.DescendingList.Strict.Properties import Cubical.Data.Empty import Cubical.Data.Empty.Base import Cubical.Data.Empty.Properties import Cubical.Data.Equality import Cubical.Data.Equality.Base import Cubical.Data.Equality.Conversion import Cubical.Data.Equality.FunctionExtensionality import Cubical.Data.Equality.PropositionalTruncation import Cubical.Data.Equality.S1 import Cubical.Data.Equality.Univalence import Cubical.Data.Fin import Cubical.Data.Fin.Arithmetic import Cubical.Data.Fin.Base import Cubical.Data.Fin.Inductive import Cubical.Data.Fin.Inductive.Base import Cubical.Data.Fin.Inductive.Properties import Cubical.Data.Fin.LehmerCode import Cubical.Data.Fin.Literals import Cubical.Data.Fin.Properties import Cubical.Data.Fin.Recursive import Cubical.Data.Fin.Recursive.Base import Cubical.Data.Fin.Recursive.Properties import Cubical.Data.FinData import Cubical.Data.FinData.Base import Cubical.Data.FinData.DepFinVec import Cubical.Data.FinData.FinSet import Cubical.Data.FinData.FiniteChoice import Cubical.Data.FinData.Order import Cubical.Data.FinData.Properties import Cubical.Data.FinInd import Cubical.Data.FinSequence import Cubical.Data.FinSequence.Base import Cubical.Data.FinSequence.Properties import Cubical.Data.FinSet import Cubical.Data.FinSet.Base import Cubical.Data.FinSet.Binary.Large import Cubical.Data.FinSet.Binary.Small import Cubical.Data.FinSet.Binary.Small.Base import Cubical.Data.FinSet.Binary.Small.Properties import Cubical.Data.FinSet.Cardinality import Cubical.Data.FinSet.Constructors import Cubical.Data.FinSet.DecidablePredicate import Cubical.Data.FinSet.FiniteChoice import Cubical.Data.FinSet.Induction import Cubical.Data.FinSet.Properties import Cubical.Data.FinSet.Quotients import Cubical.Data.FinType import Cubical.Data.FinType.Base import Cubical.Data.FinType.FiniteStructure import Cubical.Data.FinType.Properties import Cubical.Data.FinType.Sigma import Cubical.Data.FinWeak import Cubical.Data.FinWeak.Base import Cubical.Data.FinWeak.Properties import Cubical.Data.Graph import Cubical.Data.Graph.Base import Cubical.Data.Graph.Displayed import Cubical.Data.Graph.Examples import Cubical.Data.Graph.Path import Cubical.Data.InfNat import Cubical.Data.InfNat.Base import Cubical.Data.InfNat.Properties import Cubical.Data.Int import Cubical.Data.Int.Base import Cubical.Data.Int.Divisibility import Cubical.Data.Int.IsEven import Cubical.Data.Int.MoreInts.BiInvInt import Cubical.Data.Int.MoreInts.BiInvInt.Base import Cubical.Data.Int.MoreInts.BiInvInt.Properties import Cubical.Data.Int.MoreInts.DeltaInt import Cubical.Data.Int.MoreInts.DeltaInt.Base import Cubical.Data.Int.MoreInts.DeltaInt.Properties import Cubical.Data.Int.MoreInts.DiffInt import Cubical.Data.Int.MoreInts.DiffInt.Base import Cubical.Data.Int.MoreInts.DiffInt.Properties import Cubical.Data.Int.MoreInts.QuoInt import Cubical.Data.Int.MoreInts.QuoInt.Base import Cubical.Data.Int.MoreInts.QuoInt.Properties import Cubical.Data.Int.Order import Cubical.Data.Int.Properties import Cubical.Data.List import Cubical.Data.List.Base import Cubical.Data.List.Dependent import Cubical.Data.List.FinData import Cubical.Data.List.Properties import Cubical.Data.Maybe import Cubical.Data.Maybe.Base import Cubical.Data.Maybe.Properties import Cubical.Data.Nat import Cubical.Data.Nat.Algebra import Cubical.Data.Nat.Base import Cubical.Data.Nat.Coprime import Cubical.Data.Nat.Divisibility import Cubical.Data.Nat.GCD import Cubical.Data.Nat.IsEven import Cubical.Data.Nat.Literals import Cubical.Data.Nat.Lower import Cubical.Data.Nat.Mod import Cubical.Data.Nat.Omniscience import Cubical.Data.Nat.Order import Cubical.Data.Nat.Order.Inductive import Cubical.Data.Nat.Order.Recursive import Cubical.Data.Nat.Properties import Cubical.Data.Nat.Triangular import Cubical.Data.NatMinusOne import Cubical.Data.NatMinusOne.Base import Cubical.Data.NatMinusOne.Properties import Cubical.Data.NatPlusOne import Cubical.Data.NatPlusOne.Base import Cubical.Data.NatPlusOne.MoreNats.AssocNat import Cubical.Data.NatPlusOne.MoreNats.AssocNat.Base import Cubical.Data.NatPlusOne.MoreNats.AssocNat.Properties import Cubical.Data.NatPlusOne.Properties import Cubical.Data.Ordinal import Cubical.Data.Ordinal.Base import Cubical.Data.Ordinal.Properties import Cubical.Data.Prod import Cubical.Data.Prod.Base import Cubical.Data.Prod.Properties import Cubical.Data.Queue import Cubical.Data.Queue.1List import Cubical.Data.Queue.Base import Cubical.Data.Queue.Finite import Cubical.Data.Queue.Truncated2List import Cubical.Data.Queue.Untruncated2List import Cubical.Data.Queue.Untruncated2ListInvariant import Cubical.Data.Quiver.Base import Cubical.Data.Quiver.Reachability import Cubical.Data.Rationals import Cubical.Data.Rationals.Base import Cubical.Data.Rationals.MoreRationals.HITQ import Cubical.Data.Rationals.MoreRationals.HITQ.Base import Cubical.Data.Rationals.MoreRationals.LocQ import Cubical.Data.Rationals.MoreRationals.LocQ.Base import Cubical.Data.Rationals.MoreRationals.QuoQ import Cubical.Data.Rationals.MoreRationals.QuoQ.Base import Cubical.Data.Rationals.MoreRationals.QuoQ.Properties import Cubical.Data.Rationals.MoreRationals.SigmaQ import Cubical.Data.Rationals.MoreRationals.SigmaQ.Base import Cubical.Data.Rationals.MoreRationals.SigmaQ.Properties import Cubical.Data.Rationals.Order import Cubical.Data.Rationals.Properties import Cubical.Data.Sequence import Cubical.Data.Sequence.Base import Cubical.Data.Sequence.Properties import Cubical.Data.Sigma import Cubical.Data.Sigma.Base import Cubical.Data.Sigma.Properties import Cubical.Data.SubFinSet import Cubical.Data.Sum import Cubical.Data.Sum.Base import Cubical.Data.Sum.Properties import Cubical.Data.SumFin import Cubical.Data.SumFin.Base import Cubical.Data.SumFin.Properties import Cubical.Data.Unit import Cubical.Data.Unit.Base import Cubical.Data.Unit.Pointed import Cubical.Data.Unit.Properties import Cubical.Data.Vec import Cubical.Data.Vec.Base import Cubical.Data.Vec.DepVec import Cubical.Data.Vec.NAry import Cubical.Data.Vec.OperationsNat import Cubical.Data.Vec.Properties import Cubical.Data.W.Indexed import Cubical.Data.W.W import Cubical.Displayed.Auto import Cubical.Displayed.Base import Cubical.Displayed.Constant import Cubical.Displayed.Function import Cubical.Displayed.Generic import Cubical.Displayed.Morphism import Cubical.Displayed.Prop import Cubical.Displayed.Properties import Cubical.Displayed.Record import Cubical.Displayed.Sigma import Cubical.Displayed.Subst import Cubical.Displayed.Unit import Cubical.Displayed.Universe import Cubical.Experiments.CohomologyGroups import Cubical.Experiments.Combinatorics import Cubical.Experiments.CountingFiniteStructure import Cubical.Experiments.EscardoSIP import Cubical.Experiments.FunExtFromUA import Cubical.Experiments.Generic import Cubical.Experiments.HAEquivInt import Cubical.Experiments.HAEquivInt.Base import Cubical.Experiments.HInt import Cubical.Experiments.HoTT-UF import Cubical.Experiments.IntegerMatrix import Cubical.Experiments.IsoInt import Cubical.Experiments.IsoInt.Base import Cubical.Experiments.List import Cubical.Experiments.NatMinusTwo import Cubical.Experiments.NatMinusTwo.Base import Cubical.Experiments.NatMinusTwo.Properties import Cubical.Experiments.NatMinusTwo.ToNatMinusOne import Cubical.Experiments.Poset import Cubical.Experiments.Problem import Cubical.Experiments.ZCohomology.Benchmarks import Cubical.Experiments.ZCohomologyOld.Base import Cubical.Experiments.ZCohomologyOld.KcompPrelims import Cubical.Experiments.ZCohomologyOld.Properties import Cubical.Experiments.ZariskiLatticeBasicOpens import Cubical.Foundations.CartesianKanOps import Cubical.Foundations.Cubes import Cubical.Foundations.Cubes.Base import Cubical.Foundations.Cubes.Dependent import Cubical.Foundations.Cubes.HLevels import Cubical.Foundations.Cubes.Subtypes import Cubical.Foundations.Equiv import Cubical.Foundations.Equiv.Base import Cubical.Foundations.Equiv.BiInvertible import Cubical.Foundations.Equiv.Dependent import Cubical.Foundations.Equiv.Fiberwise import Cubical.Foundations.Equiv.HalfAdjoint import Cubical.Foundations.Equiv.PathSplit import Cubical.Foundations.Equiv.Properties import Cubical.Foundations.Function import Cubical.Foundations.GroupoidLaws import Cubical.Foundations.HLevels import Cubical.Foundations.HLevels.Extend import Cubical.Foundations.Interpolate import Cubical.Foundations.Isomorphism import Cubical.Foundations.Path import Cubical.Foundations.Pointed import Cubical.Foundations.Pointed.Base import Cubical.Foundations.Pointed.FunExt import Cubical.Foundations.Pointed.Homogeneous import Cubical.Foundations.Pointed.Homotopy import Cubical.Foundations.Pointed.Properties import Cubical.Foundations.Powerset import Cubical.Foundations.Prelude import Cubical.Foundations.RelationalStructure import Cubical.Foundations.SIP import Cubical.Foundations.Structure import Cubical.Foundations.Transport import Cubical.Foundations.Univalence import Cubical.Foundations.Univalence.Dependent import Cubical.Foundations.Univalence.Universe import Cubical.Functions.Bundle import Cubical.Functions.Embedding import Cubical.Functions.Fibration import Cubical.Functions.Fixpoint import Cubical.Functions.FunExtEquiv import Cubical.Functions.Image import Cubical.Functions.Implicit import Cubical.Functions.Involution import Cubical.Functions.Logic import Cubical.Functions.Morphism import Cubical.Functions.Preimage import Cubical.Functions.Surjection import Cubical.HITs.2GroupoidTruncation import Cubical.HITs.2GroupoidTruncation.Base import Cubical.HITs.2GroupoidTruncation.Properties import Cubical.HITs.AssocList import Cubical.HITs.AssocList.Base import Cubical.HITs.AssocList.Properties import Cubical.HITs.Bouquet import Cubical.HITs.Bouquet.Base import Cubical.HITs.Bouquet.Discrete import Cubical.HITs.Bouquet.FundamentalGroupProof import Cubical.HITs.Colimit import Cubical.HITs.Colimit.Base import Cubical.HITs.Colimit.Examples import Cubical.HITs.Cost import Cubical.HITs.Cost.Base import Cubical.HITs.CumulativeHierarchy import Cubical.HITs.CumulativeHierarchy.Base import Cubical.HITs.CumulativeHierarchy.Constructions import Cubical.HITs.CumulativeHierarchy.Properties import Cubical.HITs.Cylinder import Cubical.HITs.Cylinder.Base import Cubical.HITs.Delooping.Two.Base import Cubical.HITs.Delooping.Two.Properties import Cubical.HITs.DunceCap import Cubical.HITs.DunceCap.Base import Cubical.HITs.DunceCap.Properties import Cubical.HITs.EilenbergMacLane1 import Cubical.HITs.EilenbergMacLane1.Base import Cubical.HITs.EilenbergMacLane1.Properties import Cubical.HITs.FiniteMultiset import Cubical.HITs.FiniteMultiset.Base import Cubical.HITs.FiniteMultiset.CountExtensionality import Cubical.HITs.FiniteMultiset.Properties import Cubical.HITs.FreeAbGroup import Cubical.HITs.FreeAbGroup.Base import Cubical.HITs.FreeComMonoids import Cubical.HITs.FreeComMonoids.Base import Cubical.HITs.FreeComMonoids.Properties import Cubical.HITs.FreeGroup import Cubical.HITs.FreeGroup.Base import Cubical.HITs.FreeGroup.NormalForm import Cubical.HITs.FreeGroup.Properties import Cubical.HITs.FreeGroupoid import Cubical.HITs.FreeGroupoid.Base import Cubical.HITs.FreeGroupoid.GroupoidActions import Cubical.HITs.FreeGroupoid.Properties import Cubical.HITs.GroupoidQuotients import Cubical.HITs.GroupoidQuotients.Base import Cubical.HITs.GroupoidQuotients.Properties import Cubical.HITs.GroupoidTruncation import Cubical.HITs.GroupoidTruncation.Base import Cubical.HITs.GroupoidTruncation.Properties import Cubical.HITs.InfNat import Cubical.HITs.InfNat.Base import Cubical.HITs.InfNat.Properties import Cubical.HITs.Interval import Cubical.HITs.Interval.Base import Cubical.HITs.James import Cubical.HITs.James.Base import Cubical.HITs.James.Inductive import Cubical.HITs.James.Inductive.Base import Cubical.HITs.James.Inductive.Coherence import Cubical.HITs.James.Inductive.ColimitEquivalence import Cubical.HITs.James.Inductive.PushoutFormula import Cubical.HITs.James.Inductive.Reduced import Cubical.HITs.James.LoopSuspEquiv import Cubical.HITs.James.Properties import Cubical.HITs.James.Stable import Cubical.HITs.Join import Cubical.HITs.Join.Base import Cubical.HITs.Join.Properties import Cubical.HITs.KleinBottle import Cubical.HITs.KleinBottle.Base import Cubical.HITs.KleinBottle.Properties import Cubical.HITs.ListedFiniteSet import Cubical.HITs.ListedFiniteSet.Base import Cubical.HITs.ListedFiniteSet.Properties import Cubical.HITs.Localization import Cubical.HITs.Localization.Base import Cubical.HITs.Localization.Properties import Cubical.HITs.MappingCones import Cubical.HITs.MappingCones.Base import Cubical.HITs.MappingCones.Properties import Cubical.HITs.Modulo import Cubical.HITs.Modulo.Base import Cubical.HITs.Modulo.FinEquiv import Cubical.HITs.Modulo.Properties import Cubical.HITs.Nullification import Cubical.HITs.Nullification.Base import Cubical.HITs.Nullification.Properties import Cubical.HITs.Nullification.Topological import Cubical.HITs.PropositionalTruncation import Cubical.HITs.PropositionalTruncation.Base import Cubical.HITs.PropositionalTruncation.MagicTrick import Cubical.HITs.PropositionalTruncation.Monad import Cubical.HITs.PropositionalTruncation.Properties import Cubical.HITs.Pushout import Cubical.HITs.Pushout.Base import Cubical.HITs.Pushout.Flattening import Cubical.HITs.Pushout.KrausVonRaumer import Cubical.HITs.Pushout.Properties import Cubical.HITs.Pushout.PushoutProduct import Cubical.HITs.RPn import Cubical.HITs.RPn.Base import Cubical.HITs.Replacement import Cubical.HITs.Replacement.Base import Cubical.HITs.S1 import Cubical.HITs.S1.Base import Cubical.HITs.S1.Properties import Cubical.HITs.S2 import Cubical.HITs.S2.Base import Cubical.HITs.S2.Properties import Cubical.HITs.S3 import Cubical.HITs.S3.Base import Cubical.HITs.SequentialColimit import Cubical.HITs.SequentialColimit.Base import Cubical.HITs.SequentialColimit.Properties import Cubical.HITs.SetCoequalizer import Cubical.HITs.SetCoequalizer.Base import Cubical.HITs.SetCoequalizer.Properties import Cubical.HITs.SetQuotients import Cubical.HITs.SetQuotients.Base import Cubical.HITs.SetQuotients.EqClass import Cubical.HITs.SetQuotients.Properties import Cubical.HITs.SetTruncation import Cubical.HITs.SetTruncation.Base import Cubical.HITs.SetTruncation.Fibers import Cubical.HITs.SetTruncation.Properties import Cubical.HITs.SmashProduct import Cubical.HITs.SmashProduct.Base import Cubical.HITs.SmashProduct.Hexagon import Cubical.HITs.SmashProduct.Induction import Cubical.HITs.SmashProduct.Pentagon import Cubical.HITs.SmashProduct.SymmetricMonoidal import Cubical.HITs.SmashProduct.SymmetricMonoidalCat import Cubical.HITs.Sn import Cubical.HITs.Sn.Base import Cubical.HITs.Sn.Degree import Cubical.HITs.Sn.Multiplication import Cubical.HITs.Sn.Properties import Cubical.HITs.SphereBouquet import Cubical.HITs.SphereBouquet.Base import Cubical.HITs.SphereBouquet.Degree import Cubical.HITs.SphereBouquet.Properties import Cubical.HITs.Susp import Cubical.HITs.Susp.Base import Cubical.HITs.Susp.LoopAdjunction import Cubical.HITs.Susp.Properties import Cubical.HITs.Susp.SuspProduct import Cubical.HITs.Torus import Cubical.HITs.Torus.Base import Cubical.HITs.Truncation import Cubical.HITs.Truncation.Base import Cubical.HITs.Truncation.FromNegTwo import Cubical.HITs.Truncation.FromNegTwo.Base import Cubical.HITs.Truncation.FromNegTwo.Properties import Cubical.HITs.Truncation.Properties import Cubical.HITs.TypeQuotients import Cubical.HITs.TypeQuotients.Base import Cubical.HITs.TypeQuotients.Properties import Cubical.HITs.UnorderedPair import Cubical.HITs.UnorderedPair.Base import Cubical.HITs.UnorderedPair.Properties import Cubical.HITs.Wedge import Cubical.HITs.Wedge.Base import Cubical.HITs.Wedge.Properties import Cubical.Homotopy.Base import Cubical.Homotopy.BlakersMassey import Cubical.Homotopy.Connected import Cubical.Homotopy.EilenbergMacLane.Base import Cubical.Homotopy.EilenbergMacLane.CupProduct import Cubical.Homotopy.EilenbergMacLane.CupProductTensor import Cubical.Homotopy.EilenbergMacLane.GradedCommTensor import Cubical.Homotopy.EilenbergMacLane.GroupStructure import Cubical.Homotopy.EilenbergMacLane.Order2 import Cubical.Homotopy.EilenbergMacLane.Properties import Cubical.Homotopy.EilenbergMacLane.WedgeConnectivity import Cubical.Homotopy.EilenbergSteenrod import Cubical.Homotopy.Freudenthal import Cubical.Homotopy.Group.Base import Cubical.Homotopy.Group.Join import Cubical.Homotopy.Group.LES import Cubical.Homotopy.Group.Pi3S2 import Cubical.Homotopy.Group.Pi4S3.BrunerieExperiments import Cubical.Homotopy.Group.Pi4S3.BrunerieNumber import Cubical.Homotopy.Group.Pi4S3.DirectProof import Cubical.Homotopy.Group.Pi4S3.S3PushoutIso import Cubical.Homotopy.Group.Pi4S3.S3PushoutIso2 import Cubical.Homotopy.Group.Pi4S3.Summary import Cubical.Homotopy.Group.PinSn import Cubical.Homotopy.Group.SuspensionMap import Cubical.Homotopy.HSpace import Cubical.Homotopy.HiltonMilnor import Cubical.Homotopy.Hopf import Cubical.Homotopy.HopfInvariant.Base import Cubical.Homotopy.HopfInvariant.Brunerie import Cubical.Homotopy.HopfInvariant.Homomorphism import Cubical.Homotopy.HopfInvariant.HopfMap import Cubical.Homotopy.Loopspace import Cubical.Homotopy.MayerVietorisCofiber import Cubical.Homotopy.Prespectrum import Cubical.Homotopy.Spectrum import Cubical.Homotopy.WedgeConnectivity import Cubical.Homotopy.Whitehead import Cubical.Homotopy.WhiteheadsLemma import Cubical.Induction.WellFounded import Cubical.Modalities.Instances.Closed import Cubical.Modalities.Instances.DoubleNegation import Cubical.Modalities.Instances.Identity import Cubical.Modalities.Instances.Open import Cubical.Modalities.Instances.Zero import Cubical.Modalities.Lex import Cubical.Modalities.Modality import Cubical.Papers.AffineSchemes import Cubical.Papers.CohomologyRings import Cubical.Papers.ComputationalSyntheticCohomology import Cubical.Papers.FunctorialQcQsSchemes import Cubical.Papers.Pi4S3-JournalVersion import Cubical.Papers.Pi4S3 import Cubical.Papers.RepresentationIndependence import Cubical.Papers.SmashProducts import Cubical.Papers.Synthetic import Cubical.Papers.ZCohomology import Cubical.Reflection.Base import Cubical.Reflection.RecordEquiv import Cubical.Reflection.StrictEquiv import Cubical.Relation.Binary import Cubical.Relation.Binary.Base import Cubical.Relation.Binary.Extensionality import Cubical.Relation.Binary.Order import Cubical.Relation.Binary.Order.Apartness import Cubical.Relation.Binary.Order.Apartness.Base import Cubical.Relation.Binary.Order.Apartness.Properties import Cubical.Relation.Binary.Order.Loset import Cubical.Relation.Binary.Order.Loset.Base import Cubical.Relation.Binary.Order.Loset.Properties import Cubical.Relation.Binary.Order.Poset import Cubical.Relation.Binary.Order.Poset.Base import Cubical.Relation.Binary.Order.Poset.Instances.Embedding import Cubical.Relation.Binary.Order.Poset.Instances.PosetalReflection import Cubical.Relation.Binary.Order.Poset.Mappings import Cubical.Relation.Binary.Order.Poset.Properties import Cubical.Relation.Binary.Order.Poset.Subset import Cubical.Relation.Binary.Order.Proset import Cubical.Relation.Binary.Order.Proset.Base import Cubical.Relation.Binary.Order.Proset.Properties import Cubical.Relation.Binary.Order.Quoset import Cubical.Relation.Binary.Order.Quoset.Base import Cubical.Relation.Binary.Order.Quoset.Properties import Cubical.Relation.Binary.Order.QuosetReasoning import Cubical.Relation.Binary.Order.StrictOrder import Cubical.Relation.Binary.Order.StrictOrder.Base import Cubical.Relation.Binary.Order.StrictOrder.Properties import Cubical.Relation.Binary.Order.Toset import Cubical.Relation.Binary.Order.Toset.Base import Cubical.Relation.Binary.Order.Toset.Properties import Cubical.Relation.Binary.Order.Woset import Cubical.Relation.Binary.Order.Woset.Base import Cubical.Relation.Binary.Order.Woset.Properties import Cubical.Relation.Binary.Order.Woset.Simulation import Cubical.Relation.Binary.Properties import Cubical.Relation.Nullary import Cubical.Relation.Nullary.Base import Cubical.Relation.Nullary.DecidablePropositions import Cubical.Relation.Nullary.HLevels import Cubical.Relation.Nullary.Properties import Cubical.Relation.ZigZag.Applications.MultiSet import Cubical.Relation.ZigZag.Base import Cubical.Structures.Auto import Cubical.Structures.Axioms import Cubical.Structures.Constant import Cubical.Structures.Function import Cubical.Structures.LeftAction import Cubical.Structures.Macro import Cubical.Structures.Maybe import Cubical.Structures.MultiSet import Cubical.Structures.Parameterized import Cubical.Structures.Pointed import Cubical.Structures.Product import Cubical.Structures.Queue import Cubical.Structures.Record import Cubical.Structures.Relational.Auto import Cubical.Structures.Relational.Constant import Cubical.Structures.Relational.Equalizer import Cubical.Structures.Relational.Function import Cubical.Structures.Relational.Macro import Cubical.Structures.Relational.Maybe import Cubical.Structures.Relational.Parameterized import Cubical.Structures.Relational.Pointed import Cubical.Structures.Relational.Product import Cubical.Structures.Successor import Cubical.Structures.Transfer import Cubical.Structures.TypeEqvTo import Cubical.Tactics.CategorySolver.Examples import Cubical.Tactics.CategorySolver.Reflection import Cubical.Tactics.CategorySolver.Solver import Cubical.Tactics.CommRingSolver import Cubical.Tactics.CommRingSolver.AlgebraExpression import Cubical.Tactics.CommRingSolver.EvalHom import Cubical.Tactics.CommRingSolver.Examples import Cubical.Tactics.CommRingSolver.HornerEval import Cubical.Tactics.CommRingSolver.HornerForms import Cubical.Tactics.CommRingSolver.IntAsRawRing import Cubical.Tactics.CommRingSolver.RawAlgebra import Cubical.Tactics.CommRingSolver.RawRing import Cubical.Tactics.CommRingSolver.Reflection import Cubical.Tactics.CommRingSolver.Solver import Cubical.Tactics.CommRingSolver.Utility import Cubical.Tactics.FunctorSolver.Examples import Cubical.Tactics.FunctorSolver.Reflection import Cubical.Tactics.FunctorSolver.Solver import Cubical.Tactics.MonoidSolver.CommSolver import Cubical.Tactics.MonoidSolver.Examples import Cubical.Tactics.MonoidSolver.MonoidExpression import Cubical.Tactics.MonoidSolver.Reflection import Cubical.Tactics.MonoidSolver.Solver import Cubical.Tactics.NatSolver import Cubical.Tactics.NatSolver.EvalHom import Cubical.Tactics.NatSolver.Examples import Cubical.Tactics.NatSolver.HornerForms import Cubical.Tactics.NatSolver.NatExpression import Cubical.Tactics.NatSolver.Reflection import Cubical.Tactics.NatSolver.Solver import Cubical.Tactics.Reflection import Cubical.Tactics.Reflection.Utilities import Cubical.Tactics.Reflection.Variables import Cubical.Talks.EPA2020 import Cubical.WildCat.Base import Cubical.WildCat.BraidedSymmetricMonoidal import Cubical.WildCat.Free import Cubical.WildCat.Functor import Cubical.WildCat.Instances.Categories import Cubical.WildCat.Instances.NonWild import Cubical.WildCat.Instances.Path import Cubical.WildCat.Instances.Pointed import Cubical.WildCat.Instances.Types import Cubical.WildCat.Product import Cubical.WildCat.UnderlyingGraph import Cubical.ZCohomology.Base import Cubical.ZCohomology.CohomologyRings.CP2 import Cubical.ZCohomology.CohomologyRings.Coproduct import Cubical.ZCohomology.CohomologyRings.CupProductProperties import Cubical.ZCohomology.CohomologyRings.KleinBottle import Cubical.ZCohomology.CohomologyRings.RP2 import Cubical.ZCohomology.CohomologyRings.RP2wedgeS1 import Cubical.ZCohomology.CohomologyRings.S0 import Cubical.ZCohomology.CohomologyRings.S1 import Cubical.ZCohomology.CohomologyRings.S2wedgeS4 import Cubical.ZCohomology.CohomologyRings.Sn import Cubical.ZCohomology.CohomologyRings.Unit import Cubical.ZCohomology.EilenbergSteenrodZ import Cubical.ZCohomology.GroupStructure import Cubical.ZCohomology.Groups.CP2 import Cubical.ZCohomology.Groups.Connected import Cubical.ZCohomology.Groups.Coproduct import Cubical.ZCohomology.Groups.KleinBottle import Cubical.ZCohomology.Groups.Prelims import Cubical.ZCohomology.Groups.RP2 import Cubical.ZCohomology.Groups.RP2wedgeS1 import Cubical.ZCohomology.Groups.S2wedgeS1wedgeS1 import Cubical.ZCohomology.Groups.S2wedgeS4 import Cubical.ZCohomology.Groups.Sn import Cubical.ZCohomology.Groups.SphereProduct import Cubical.ZCohomology.Groups.Torus import Cubical.ZCohomology.Groups.Unit import Cubical.ZCohomology.Groups.Wedge import Cubical.ZCohomology.Gysin import Cubical.ZCohomology.MayerVietorisUnreduced import Cubical.ZCohomology.Properties import Cubical.ZCohomology.RingStructure.CohomologyRing import Cubical.ZCohomology.RingStructure.CohomologyRingFun import Cubical.ZCohomology.RingStructure.CupProduct import Cubical.ZCohomology.RingStructure.GradedCommutativity import Cubical.ZCohomology.RingStructure.RingLaws