# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-threads base
base-unix base
conf-gmp 4 Virtual package relying on a GMP lib system installation
coq dev The Coq Proof Assistant
coq-core dev The Coq Proof Assistant -- Core Binaries and Tools
coq-stdlib dev The Coq Proof Assistant -- Standard Library
coqide-server dev The Coq Proof Assistant, XML protocol server
dune 3.12.1 Fast, portable, and opinionated build system
ocaml 4.14.0 The OCaml compiler (virtual package)
ocaml-base-compiler 4.14.0 Official release 4.14.0
ocaml-config 2 OCaml Switch Configuration
ocaml-options-vanilla 1 Ensure that OCaml is compiled with no special options enabled
ocamlfind 1.9.6 A library manager for OCaml
zarith 1.13 Implements arithmetic and logical operations over arbitrary-precision integers
# opam file:
opam-version: "2.0"
maintainer: "matej.kosik@inria.fr"
homepage: "https://github.com/UniMath/UniMath"
dev-repo: "git+https://github.com/UniMath/UniMath.git"
bug-reports: "https://github.com/UniMath/UniMath/issues"
license: "Kind of MIT"
authors: ["The UniMath Development Team"]
build: [
["bash" "-c" "sed -i.bak 's/PACKAGES += SubstitutionSystems//' Makefile"]
["bash" "-c" "sed -i.bak 's/PACKAGES += Bicategories//' Makefile"]
[make "BUILD_COQ=no" "-j%{jobs}%"]
]
install: [make "BUILD_COQ=no" "install"]
depends: [
"ocaml"
"coq" {>= "8.12.2"}
]
synopsis: "Library of Univalent Mathematics"
url {
src: "git+https://github.com/UniMath/UniMath.git#master"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-unimath.dev coq.devDry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
trueopam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-unimath.dev coq.devopam list; echo; ulimit -Sv 16000000; timeout 8h opam install -y coq-unimath.dev coq.devTotal: 197 M
../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/Derivative.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/EquivalenceWhiskeredNonCurriedMonoidalCategories.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Adjunctions.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/CohomologyComplex.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Isos.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/MappingCone.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/catiso.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Fibrations.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/LocalizingClass.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Inductives/LambdaCalculus.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Adjunctions/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/MonoidalCategoriesTensored.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/DisplayedFunctorEq.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Equivalences/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/GaussianElimination/Elimination.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/MappingCone.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/RealNumbers/NonnegativeReals.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/slicecat.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/ExactCategories/ExactCategories.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/Triangulated.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Groupoids.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/KAPreTriangulated.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/KTriplesEquiv.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Equivalences/CompositesAndInverses.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/RelativeMonads.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Foundations/PartA.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Constructions.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/ExactCategories/ExactCategories.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/RigsAndRings.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/precomp_fully_faithful.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/RigsAndRings.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/CohomologyComplex.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/ReindexingForward.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/BinaryOperations.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/DisplayedCatEq.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/Triangulated.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/PAdics/frac.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Equivalences.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/Functors.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/ElementaryTopos.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Fiber.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Displayed/SymmetricMonoidalBuilder.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Fibrations.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/PAdics/padics.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Free_Monoids_and_Groups.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/Complexes.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/PAdics/padics.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/TranslationFunctors.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/LocalizingClass.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/StandardFiniteSets.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/StandardFiniteSets.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/CategoricalRecursionSchemes.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Foundations/PartA.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Categories.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/KATriangulated.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Foundations/Sets.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/pullbacks.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Actions.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/BinaryOperations.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/Lattice/Lattice.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/GaussianElimination/Corollaries.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Binproducts.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/Kleisli.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/Reindexing.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/StrictTwoSidedDispCat.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/WellOrderedSets.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Adjunctions/Restriction.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/pullbacks.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Functors.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Structure/SymmetricDiagonal.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Dialgebras.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/PAdics/z_mod_p.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/Structures.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Actegories/ConstructionOfActegoryMorphisms.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Abelian.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/MonoidalFunctorCategory.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/Complexes.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Chains/OmegaCocontFunctors.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/RealNumbers/Reals.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/abgrs.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/PAdics/z_mod_p.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Displayed/Symmetric.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Monoids.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/StandardCategories.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/NumberSystems/Integers.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Monoids.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/RezkCompletion/LiftedAssociator.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/elems_slice_equiv.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/RezkCompletion/LiftedAssociator.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EpiFacts.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Terms.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Chains/OmegaCocontFunctors.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/RezkCompletion/LiftedTensor.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DaggerCategories/Functors/Precomp.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/FunctorCategory.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/binproducts.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/PrecategoryBinProduct.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/RepresentableFunctors/Representation.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Foundations/NaturalNumbers.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/MonoidalFunctorCategory.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Functors.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/RealNumbers/NonnegativeRationals.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Domains_and_Fields.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/PAdics/fps.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/ArrowCategory.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Ktheory/GrothendieckGroup.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Foundations/Sets.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/EquivalenceOverId.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Adjunctions/Core.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/BinDirectSums.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/PAdics/fps.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Actegories/ConstructionOfActegoryMorphisms.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/ReindexingForward.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/MappingCylinder.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/WellOrderedSets.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Groups.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/Reindexing.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/RepresentableFunctors/Representation.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/PartA.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/BinDirectSums.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/StrictTwoSidedDispCat.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/bincoproducts.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Enriched/Enriched.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/Examples/IsoCommaLimits.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/PreAdditive.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/SyntheticHomotopyTheory/Circle2.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/RelativeMonads.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/MappingCone.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/RealNumbers/NonnegativeReals.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/limits.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Structure/SymmetricDiagonal.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/PrecategoryBinProduct.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/Preservation.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Comonoids/Symmetric.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/limits.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Groups.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Colimits/Examples/StructureEnrichedColimits.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Binproducts.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/AugmentedSimplexCategory.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/TranslationFunctors.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/AlternativeDefinitions/FixedPointTheorems.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Domains_and_Fields.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/RightKanExtension.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/TwoSidedDispCat.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/GaussianElimination/Elimination.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Colimits/Examples/PosetEnrichedColimits.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Semantics/LinearLogic/LinearCategory.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Displayed/MonoidalFunctorLifting.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Limits/Examples/StructureEnrichedLimits.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/Preservation.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/DisplayedCartesianMonoidal.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Displayed/Monoidal.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/Examples/EilenbergMooreLimits.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Comonoids/Monoidal.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Equivalences.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/Presheaves.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/GaussianElimination/Vectors.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/SyntheticHomotopyTheory/AffineLine.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/DispCatOnTwoSidedDispCat.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Modules/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Limits/Examples/PosetEnrichedLimits.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/RezkCompletion/LiftedMonoidal.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Topology/Topology.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/FunctorAlgebras.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/precomp_ess_surj.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/Functors.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/RezkCompletion/PrecompEssentiallySurjective.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Foundations/PartD.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Topology/Filters.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Enrichment.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Enriched/Opposite.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/Examples/AlgebraStructuresColimits.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/Slice.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Induction/FunctorAlgebras_legacy.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/MoreFibrations/CartesiannessOfComposites.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Subobjects.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Enrichment.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DaggerCategories/Functors/Precomp.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Profunctors/Transformation.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/FunctorCategory.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/WhiskeredBifunctors.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Adjunctions.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/TotalAdjunction.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/Examples/EilenbergMooreLimits.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Foundations/PartC.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/PartA.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/DisplayedCartesianMonoidal.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/SubobjectClassifier.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Foundations/PartB.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/Presheaves.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Total.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/Isos.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/AbelianToAdditive.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Actegories/Actegories.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/RelMonads_Coreflection.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/NumberSystems/Integers.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/MonoidalCategoriesTensored.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/slicecat.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Structures/StructureLimitsAndColimits.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/PathsOver.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/KleisliCategory.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/KAPreTriangulated.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/binproducts.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/colimits.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/AlternativeDefinitions/FixedPointTheorems.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/CategoryEquality.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Foundations/NaturalNumbers.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/ProductEnriched.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Enriched/Enriched.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/SyntheticHomotopyTheory/AffineLine.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/Reindex.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/ShortExactSequences.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Structure/Closed.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/PreAdditive.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/RealNumbers/NonnegativeReals.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/AugmentedSimplexCategory.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Actegories/MorphismsOfActegories.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Structures/StructuresSmashProduct.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/Examples/AlgebraStructuresColimits.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/GaussianElimination/RowOps.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/NaturalTransformations.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Displayed/Symmetric.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/Derivative.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Displayed/WhiskeredDisplayedBifunctors.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/DisplayedMonoidalTensored.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/IteratedBinaryOperations.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/GroupAction.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Limits/Examples/SelfEnrichedLimits.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Categories.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/LambdaCalculus.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Presheaf.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/Sigma.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/StructuredCospans.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Displayed/Monoidal.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/MonoidalDialgebras.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/Examples/IsoCommaLimits.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/StructuredCospans.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/CategoricalRecursionSchemes.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Abelian.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Foundations/PartC.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/MoreFibrations/FibrationsCharacterisation.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Adjunctions.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/IndexedCategories/IndexedCategoryToFibration.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/AlgebraStructures.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/NumberSystems/RationalNumbers.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/NaturalTransformations.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/PAdics/lemmas.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Structure/Symmetric.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/ShortExactSequences.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Dialgebras.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/YonedaLemma.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/DisplayedMonoidalTensored.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/bincoproducts.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Actegories/MorphismsOfActegories.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/ZFstructures.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/GaussianElimination/Matrices.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/RezkCompletion/LiftedMonoidal.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Free_Monoids_and_Groups.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/KleisliCategory.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/StreetFibration.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/Opp.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Total.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/RepresentationTheorem.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/EquivalenceOverId.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/AdditiveFunctors.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/ExponentiationLeftAdjoint.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/PathsOver.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Modules/Quotient.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Archimedean.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/RepresentableFunctors/Bifunctor.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/SyntheticHomotopyTheory/Circle.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/PAdics/lemmas.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Displayed/MonoidalSections.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/exponentials.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/RezkCompletion/PrecompEssentiallySurjective.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Limits/Examples/PosetEnrichedLimits.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Colimits/Examples/StructureEnrichedColimits.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/colimits.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/MappingCylinder.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/abgrs.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Limits/Examples/StructureEnrichedLimits.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Comonoids/Category.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/SmashStructureEnriched.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/MonoidalDialgebras.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/PowerObject.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/RepresentableFunctors/Precategories.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/SmashProductMonoidal.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/PseudoElements.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DaggerCategories/FunctorCategory.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Colimits/Examples/PosetEnrichedColimits.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/ConstructiveStructures.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Terms.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/SmashProductMonoidal.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/AdditiveFunctors.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/WellFoundedRelations.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/cokernels.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/DialgebraEnriched.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/DisplayedFunctor.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Structures/StructureLimitsAndColimits.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/KTriples.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Modules/Core.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/Monads.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/kernels.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/AlgebraStructures.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Induction/M/ComputationalM.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Structure/Closed.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/GaussianElimination/Corollaries.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/GaussianElimination/Matrices.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/FiniteSequences.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/OppositeCategory/OppositeOfFunctorCategory.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Induction/M/Chains.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/Monads.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/DialgebraEnriched.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/TwoCategories.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/StructureEnriched.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/StreetFibration.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Structures/CartesianStructure.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/WhiskeredBifunctors.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicGeometry/Spec.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Isos.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedBinaryCoproducts.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/RealNumbers/DedekindCuts.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Profunctors/Transformation.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/DisplayedNatTrans.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/Yoneda.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Inductives/Lists.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/TotalAdjunction.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/PrecompEquivalence.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/IndexedCategories/IndexedCategoryToFibration.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/ProductEnriched.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/TwoSidedDispCat.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/PAdics/frac.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Folds/folds_isomorphism.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/pushouts.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/GroupAction.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Foundations/PartD.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/pullbacks.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/Relations.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Limits/Examples/SelfEnrichedLimits.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedBinaryProducts.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/precomp_ess_surj.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/Spans.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Foundations/PartB.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/PresheafCategory.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/Lattice/Lattice.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/coequalizers.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/Lenses.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/DispCatOnTwoSidedDispCat.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/FiveLemma.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/StreetOpFibration.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/LambdaCalculus.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Limits.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Constructions.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/FiveLemma.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Induction/M/Chains.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Archimedean.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Semantics/EnrichedEffectCalculus/ContinuationModel.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/PresheafCategory.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Examples/BinaryProducts.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Colimits/Examples/SelfEnrichedColimits.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Colimits/Examples/SelfEnrichedColimits.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Tactics/Nat_Tactics.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Functors.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/MonadAlgebras.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Foundations/PartA.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/Yoneda.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/Reindex.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Displayed/TotalMonoidal.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/pushouts.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/KleisliEnriched.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Semantics/EnrichedEffectCalculus/ContinuationModel.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/Spans.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/DisplayedFunctor.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Inductives/Lists.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/MonoidalPointedObjects.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/Comonads.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/OrderedSets.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/KleisliEnriched.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Comonoids/Tensor.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/RealNumbers/Reals.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/Sigma.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/Examples/CategoryProductLimits.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/Isos.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedLimits.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/FunctorCategory.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Profunctors/Squares.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/FiniteSequences.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/CategoriesOfMonoids.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedLimits.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/DisplayedMonoidalCurried.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Induction/ImpredicativeInductiveSets.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Semantics/EnrichedEffectCalculus/CopowerModel.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/NaturalTransformations.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/SmashStructureEnriched.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/KA.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/IteratedBinaryOperations.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Semantics/LinearLogic/LinearToLinearNonLinear.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Induction/M/Limits.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/UnivalentKleisliMapping.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/SyntheticHomotopyTheory/Circle2.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Foundations/Propositions.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/coproducts.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/FunctorCategory.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Displayed/WhiskeredDisplayedBifunctors.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedCoequalizers.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/PseudoElements.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/RepresentableFunctors/Precategories.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/catiso.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Chains/CoAdamek.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedEqualizers.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/Lenses.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Equivalences/Core.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/ElementaryTopos.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Foundations/UnivalenceAxiom.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/LiftPoset.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedColimits.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/TwoSidedFibration.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Additive.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedColimits.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Functors.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Projection.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/equalizers.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/exponentials.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/SliceFamEquiv.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/Nat.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/RepresentationTheorem.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Semantics/EnrichedEffectCalculus/CopowerModel.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Actegories/CoproductsInActegories.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Actegories/ProductActegory.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/cats/limits.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/elems_slice_equiv.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/RezkCompletion/LiftedUnitors.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/LambdaTheoryCategory.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/RigsAndRings.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Semantics/LinearLogic/LinearToLinearNonLinear.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/All.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/CohomologyComplex.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/UnivalentKleisliEnriched.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/Equivalences.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/KleisliCategory.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/DisplayedMonoidalCurried.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/AlternativeDefinitions/Dcpo.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedConicalColimits.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/All.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/LatticeObject.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/BinaryOperations.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Comonoids/MonoidalCartesianBuilder.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/Comonads.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/EilenbergMoore.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/coequalizers.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/BicatOfCatsElementary.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedCoproducts.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/ProdOfTwosidedDispCat.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/PrecompEquivalence.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/cones.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/EnrichmentTransformation.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Structure/Symmetric.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/CoEilenbergMoore.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/RezkCompletion/LiftedUnitors.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Induction/FunctorCoalgebras_legacy.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/OrderedSets.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/PosetEnriched.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Profunctors/Examples.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/StreetOpFibration.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedConicalLimits.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/Tests.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Displayed/MonoidalSections.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Foundations/Sets.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/products.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/CommaCategories.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/ExactCategories/ExactCategories.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/Examples/CategoryProductLimits.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/NaturalTransformations.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/GrothendieckConstruction/Projection.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Actegories/Actegories.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Profunctors/Squares.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/DisplayedNatTrans.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/HomotopicalCategory.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/pushouts.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/equalizers.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/GrothendieckConstruction/Projection.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Topology/Topology.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedProducts.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/coequalizers.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Core.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/FiberwiseProduct.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/AbelianToAdditive.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/UnivalentKleisliEnriched.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Displayed/SymmetricMonoidalBuilder.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Equivalences/CompositesAndInverses.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/Relations.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Topology/Filters.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/opp_precat.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/SetWithSubset.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/CartesianMonoidal.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedCoequalizers.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedBinaryCoproducts.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Semantics/LinearLogic/RelationalModel.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/RealNumbers/NonnegativeRationals.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Folds/folds_pre_2_cat.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/pullbacks.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/LeftKanExtension.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/Relations.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/FiniteSets.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Actegories/ProductActegory.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Adjunctions/Examples.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Elements.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Comonoids/Category.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedEqualizers.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/NumberSystems/RationalNumbers.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/GaussianElimination/Auxiliary.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/EquivalenceWhiskeredNonCurriedMonoidalCategories.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedConicalColimits.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/AbelianPushoutPullback.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Tactics/Nat_Tactics.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DaggerCategories/FunctorCategory.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedBinaryProducts.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Adjunctions.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Structures/CartesianStructure.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/equalizers.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Limits.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/Triangulated.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/GaussianElimination/Vectors.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/MonoidalPointedObjects.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedConicalLimits.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/EnrichmentFunctor.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/MoreFibrations/DispCatsEquivFunctors.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/LModules.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Fibrations.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Comonoids/CartesianAsComonoids.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Semantics/LinearLogic/LinearCategory.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/LambdaAlgebraMonoid.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/Relations.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/coequalizers.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Comonoids/Tensor.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Semantics/LinearLogic/RelationalModel.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Displayed/MonoidalFunctorLifting.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicGeometry/Spec.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/LeftKanExtension.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/pushouts.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/GaussianElimination/Auxiliary.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/KTriplesEquiv.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/MonoidalFunctorsTensored.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/IsoCommaCategory.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Subcategory/Limits.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Induction/FunctorAlgebras_legacy.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Examples/BinarySums.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/ChangeOfBase.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Chains/OmegaContFunctors.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/Complexes.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/Sigma.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/HorizontalComposition.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/modules.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/AlgebraicTheoryCategory.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Structures/StructuresSmashProduct.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Enriched/EnrichmentEquiv.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Morphisms.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/RepresentableFunctors/Bifunctor.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/pullbacks_slice_products_equiv.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/AlgebraicTheories.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/GaussianElimination/RowOps.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/Nat.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/FunctorAlgebras.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Profunctors/Core.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/CategoriesOfMonoids.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/Categories.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/CategorySum.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Examples/IdealCompletion.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/FunctorCoalgebras.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/TranslationFunctors.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/MonoidalCategoriesCurried.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/UnivalentKleisliMapping.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/kernels.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/ComprehensionC.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Core/ScottContinuous.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Fiber.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/DisplayedCatEq.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/EnrichmentFunctor.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/ChangeOfBase.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Total.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/IndexedCategories/IndexedCategory.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/GrothendieckConstruction/IsOpfibration.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/KTriples.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/IndexedCategories/IndexedCategory.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/SyntheticHomotopyTheory/Circle.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/PosetEnriched.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Additive.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Fiber.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/ZFstructures.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/EnrichmentTransformation.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/cats/limits.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/FunctorCategory.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Structure/Cartesian.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Relations.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/LocalizingClass.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/Structures.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/EilenbergMooreEnriched.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Examples/BinarySums.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/TwoCategories.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/coproducts.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/cokernels.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/TwoSidedFibration.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/MoreFibrations/Prefibrations.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/HorizontalComposition.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/PAdics/padics.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/CommaCategories.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/CartesianMonoidal.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/opp_precat.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/OppositeEnriched.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Actegories/ActionBasedStrongMonads.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/StructureEnriched.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/Subtypes.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Elements.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Profunctors/Examples.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedCoproducts.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/Sigma.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/MoreFibrations/Prefibrations.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/RelativeModules.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/ProdOfTwosidedDispCat.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/Equivalences.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Displayed/TotalMonoidal.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/Filtered.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/CGraph.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Enriched/EnrichmentEquiv.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/Limits.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedProducts.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/ExactCategories/Tests.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Actegories/CoproductsInActegories.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/PAdics/z_mod_p.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/MoreLists.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/Propositions.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/StandardFiniteSets.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/RezkCompletion/PrecompFullyFaithful.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Isos.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/SelfEnriched.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/Cartesian.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/LModules.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/AlgebraicTheoryCategory.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/products.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/RezkCompletion/LiftedTensor.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Morphisms.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/SelfEnriched.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Folds/folds_isomorphism.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/bincoproducts.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/OppositeEnriched.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/MoreFibrations/DispCatsEquivFunctors.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/Coends.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/RezkCompletion/PrecompFullyFaithful.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/FinOrdCoproducts.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/Ends.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Actegories/ConstructionOfActegories.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/KA.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/RezkCompletion/LiftedTensorUnit.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Actegories/ConstructionOfActegories.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/CategorySum.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Subcategory/Full.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Examples/BinaryProducts.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/SkewMonoidal/SkewMonoidalCategories.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Colimits/CopowerFunctor.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/TransportLaws.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/MoreFibrations/DisplayedDisplayedCats.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Induction/W/Naturals.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/NegativePropositions.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Chains/OmegaContFunctors.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/equalizers.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/Opp.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Total.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/FunctorCoalgebras.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/TransportLaws.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Colimits/CopowerFunctor.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/FiberwiseProduct.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Induction/ImpredicativeInductiveSets.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/PAdics/fps.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Basis/Basis.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/CatIsoInserter.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Projection.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/Univalence.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/NumberSystems/NaturalNumbersAlgebra.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/PrecategoriesWithAbgrops.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Monoids.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Examples/IdealCompletion.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/bincoproducts.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Examples/Sums.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Inductives/PropositionalLogic.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/RelativeModules.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Induction/M/ComputationalM.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/Lists.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/StandardCategories.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/KleisliCategory.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/LambdaTheoryCategory.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/FinOrdProducts.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/abgrs.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Foundations/NaturalNumbers.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Basis/Continuous.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/NegativePropositions.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/StandardDiagrams.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/MonoidalFunctorsTensored.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/Posets/PointedPosets.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/IndexedCategories/IndexedFunctorToCartesian.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/YonedaLemma.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/IsoCommaCategory.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/MonoidalCategoriesReordered.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/LatticeObject.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/Tests.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/NumberSystems/Integers.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/IndexedCategories/OpIndexedCategory.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/Colimits.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/UnitalBinop.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Folds/folds_pre_2_cat.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Abelian.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/FilteredColimits.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Subcategory/Full.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Presheaf.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/yoneda.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/MonadAlgebras.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Comonoids/CartesianAsComonoids.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/IndexedCategories/IndexedFunctor.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/FiniteSets.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Functors.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Profunctors/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/GrothendieckConstruction/TotalCategory.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Actions.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/Lists.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedPowers.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/Colimits.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/PointedPosetStrict.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/ProfunctorTwosidedDispCat.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/WellFoundedRelations.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/MoreFibrations/CartesiannessOfComposites.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/ExponentiationLeftAdjoint.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/WellOrderedSets.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/FunctorCategories.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/RightKanExtension.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Categories.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/ElementsOp.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/PowerObject.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/yoneda.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/RealNumbers/Reals.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/eqdiag.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Comonoids/MonoidalCartesianBuilder.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/Cartesian.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/Sets.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/ProfunctorTwosidedDispCat.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedPowers.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/monoids.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/SubobjectClassifier.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Chains/OmegaCocontFunctors.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Modules/Examples.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/PointedSetCartesianMonoidal.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/CategoryOfPosets.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/AlternativeDefinitions/Dcpo.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/OppositeCategory/OppositeOfFunctorCategory.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/DisplayedFunctorEq.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/ElementsOp.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Strictness.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/CategoryOfSetCategories.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/pullbacks.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/IndexedCategories/FibrationToIndexedCategory.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/Examples/CategoryOfSetcategoriesLimits.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Examples/Sums.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/ConstructiveStructures.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/Coends.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/MonoidalFunctorsCurried.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/RelMonads_Coreflection.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/CategoriesOfMonoids.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Fiber.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/MoreFibrations/DisplayedDisplayedCats.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/TransportMorphisms.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Groups.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/StrongMonad.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/RealNumbers/NonnegativeRationals.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Binproducts.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/SetEnriched.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/FilteredColimits.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/RealNumbers/Sets.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/DecidablePropositions.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/MonoidalFunctorsCurried.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/binproducts.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/Posets/QuotientPoset.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/SliceEnriched.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/MoreLists.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/Comma.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Elements/Maximal.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/GaussianElimination/Elimination.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/Ends.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Equivalences.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/Vectors.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Subobjects.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/AlternativeDefinitions/FixedPointTheorems.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Isos.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/EilenbergMooreEnriched.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/Arrow.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal/HVectors.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Matrix.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Enriched/ChangeOfBase.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedCopowers.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/StandardDiagrams.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedCopowers.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/BraidedMonoidalCategories.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/CatIsoInserter.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/Examples/CategoryOfSetcategoriesLimits.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/Subtypes.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/MoreEquivalences.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/RezkCompletion/LiftedTensorUnit.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Foundations/Propositions.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/LambdaAlgebraMonoid.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Semantics/LinearLogic/LinearCategoryEilenbergMooreAdjunction.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/UnitEnriched.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/Reindexing.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/Posets/MonotoneFunctions.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Adjunctions/Examples.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/IndexedCategories/CartesianToIndexedFunctor.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/SkewMonoidal/SkewMonoidalCategories.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/HomotopicalCategory.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/SkewMonoidal/CategoriesOfMonoids.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Actegories/Examples/ActionOfEndomorphismsInCATElementary.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Enriched/ChangeOfBase.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/KATriangulated.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Relations.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/CatIsoDisplayed.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Basis/CompactBasis.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Structure/Cartesian.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/binproducts.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/cones.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/bincoproducts.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Chains/Adamek.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Inductives/LambdaCalculus.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Inductives/Trees.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/RepresentableFunctors/Test.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/Bimodules.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/Examples/EndomorphismTheory.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/EnrichmentAdjunction.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/category_binops.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/Lattice/Lattice.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Semantics/LinearLogic/LiftingModel.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Limits/Examples/OppositeEnrichedLimits.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/CatIsoDisplayed.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Structure/SymmetricDiagonal.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/FunctorCategories.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Universal_Algebra/Algebras.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/GrothendieckConstruction/TotalCategory.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/whiskering.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monics.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Colimits/Examples/OppositeEnrichedColimits.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/Limits.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Inductives/Trees.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/FunctorCategory.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/LambdaTheories.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/AugmentedSimplexCategory.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/IndexedCategories/CoreIndexedCategory.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/CategoryOfSetCategories.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Tactics/Abmonoids_Tactics.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/pullbacks_slice_products_equiv.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/AbelianPushoutPullback.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/Examples/FreeMonoidTheory.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/FullyFaithful.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/DCPOStructures.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Apartness.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Domains_and_Fields.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/SliceFamEquiv.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/StrictTwoSidedDispCat.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/DivisionRig.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Actegories/Examples/ActionOfEndomorphismsInCATElementary.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/PreAdditive.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/NumberSystems/NaturalNumbersAlgebra.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Foundations/UnivalenceAxiom.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/Vectors.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/PrecategoryBinProduct.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Inductives/PropositionalLogic.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/LiftPoset.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/Presheaves.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Foundations/PartC.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Modules/Quotient.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal/HVectors.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/PointedSetStructures.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Topology/Prelim.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/BinopCartesianMonoidal.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/Propositions.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Folds/folds_precat.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/ArrowCategory.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/CompletelyIterativeAlgebras.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/PointedPosetStrict.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Comonoids/TransportComonoidAlongRetraction.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/zero.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Induction/W/Naturals.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/ShortExactSequences.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/RelativeMonads.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/flds.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Actegories/ConstructionOfActegoryMorphisms.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/SplitMonicsAndEpis.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/CategoriesOfMonoids.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Modules/Multimodules.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/Bimodules.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/HomFunctor.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/CoEilenbergMoore.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/MappingCylinder.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Adjunctions/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Matrix.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/Examples/EndomorphismTheory.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/CartesianCubicalSets.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Profunctors/Transformation.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/Constant.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/IndexedCategories/IndexedTransformationToTransformation.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/FullyFaithful.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Examples/Exponentials.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/NumberSystems/Tests.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/RezkCompletion/RezkUniversalProperty.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Comonoids/TransportComonoidAlongRetraction.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/AlgebraCategory.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/PartA.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/EilenbergMoore.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/DiagonalFunctor.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/Examples/FreeTheory.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Core/ScottContinuous.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/PointedDCPOStrict.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/UnitalBinop.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Comonoids/CommComonoidsCartesian.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Foundations/PartB.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/DisplayedCartesianMonoidal.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/Functors.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/DecidablePropositions.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/limits.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/EnrichmentAdjunction.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/UnitorsAndAssociatorsForEndofunctors.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Topology/Filters.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/eqdiag.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/AlgebraicTheories.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/SymmetricMonoidalCoEilenbergMoore.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/PosetStructures.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/IsoComma.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DaggerCategories/Functors/Precomp.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/intdoms.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/Univalence.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/BicatOfCatsElementary.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/IndexedCategories/NatTransToIndexed.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/RepresentableFunctors/Representation.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/RezkCompletion/PrecompEssentiallySurjective.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/SkewMonoidal/CategoriesOfMonoids.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DaggerCategories/Unitary.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Basis/Basis.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/Profunctor.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/Opposite.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/ReindexingForward.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Core/Basics.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/Fullsub.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/RealNumbers/DedekindCuts.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/GrothendieckConstruction/IsOpfibration.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Examples/Tests.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/AlgebraFibration.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/UnitEnriched.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedInitial.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/SetValuedFunctors.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Actegories/Examples/SelfActionInCATElementary.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Enriched/UnderlyingCategory.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedTerminal.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/TotalDisplayedMonoidalCurried.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/IndexedCategories/OpIndexedCategory.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/SetEnriched.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/MoreEquivalences.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Foundations/PartD.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/TotalCategoryFacts.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Discrete.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/BinDirectSums.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/monoids.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Displayed/TransportLemmas.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/Categories.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Codomain.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/HomFunctor.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Groupoids.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/CGraph.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/Examples/EilenbergMooreLimits.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DaggerCategories/Functors/Factorization.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/CategoryEquality.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/Presheaves.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Equivalences/FullyFaithful.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/precomp_fully_faithful.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/commrings.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Tactics/Nat_Tactics.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Paradoxes/GirardsParadox.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Topology/Topology.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/ZigZag.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/Sets.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/PointedDCPOStructures.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/Univalence.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/Filtered.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/zero.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Induction/W/Uniqueness.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Folds/from_precats_to_folds_and_back.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Induction/M/Limits.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Induction/W/Fibered.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/GrothendieckTopos.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Modules/Multimodules.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/TwoSidedDispCat.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Algebras.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Displayed/TransportLemmas.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/All.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/Preservation.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Chains/CoAdamek.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/binproducts.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Univalence.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Core/DirectedSets.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/MonoidalCategoriesReordered.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Equivalences/FullyFaithful.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/ExactCategories/Tests.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Elements/Maximal.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Subcategory/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/EmptyEnriched.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/slicecat.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/grs.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/MonoidalFunctorCategory.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Subcategory/Core.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/Posets/PointedPosets.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Strictness.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/PrecategoriesWithAbgrops.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Folds/from_precats_to_folds_and_back.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/AbelianToAdditive.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/DCPOStructures.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Examples/Exponentials.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/abmonoids.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Examples/Tests.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/Posets/QuotientPoset.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/zero.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/LambdaTheories.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/commrigs.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monics.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Adjunctions.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Examples/Equalizers.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Colimits/Examples/PosetEnrichedColimits.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Modules/Submodule.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Topology/Prelim.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/Presheaves.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Induction/M/Uniqueness.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/StrongMonad.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/rings.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Colimits/Examples/StructureEnrichedColimits.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Chains/Chains.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/SmashProductMonoidal.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Basis/CompactBasis.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/StructuredCospans.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/FunctorCategory.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Semantics/All.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/IndexedCategories/IndexedFunctor.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal/VTerms.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/RezkCompletion/EnrichedRezkCompletion.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/KAPreTriangulated.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/MonoidalCategoriesCurried.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Limits/Examples/PosetEnrichedLimits.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/RepresentableFunctors/Test.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/PAdics/lemmas.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/Arrow.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Limits/Examples/StructureEnrichedLimits.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Basis/Continuous.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Terms.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/All.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/IndexedCategories/IndexedTransformation.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/IndexedCategories/FibrationToIndexedCategory.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/CategoryOfPosets.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/FullSubEnriched.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/initial.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/ZigZag.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Adjunctions/Restriction.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/Isos.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/UnderCategories.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Foundations/Tests.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/YonedaBinproducts.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Actegories/ProductsInActegories.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/Product.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/modules.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/OppositeCategory/LimitsAsColimits.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/ConstantFunctor.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/rigs.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Examples/Equalizers.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/DiagonalFunctor.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/wosets.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Enrichment.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/AlgebraicTheoryMorphisms.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Total.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/ProductEnriched.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/RealNumbers/Sets.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Enriched/UnderlyingCategory.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedInitial.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/AlgebraCategory.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/KFiniteTypes.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/rezk_completion.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedTerminal.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/Examples/FreeMonoidTheory.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/terminal.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/Lattice/Examples/Subsets.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Core/FubiniTheorem.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/MonoidalDialgebras.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/coslicecat.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Ktheory/GrothendieckGroup.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Structures/StructuresSmashProduct.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Subcategory/FullEquivalences.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/Posets/MonotoneFunctions.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/PointedFunctors.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/setwith2binops.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/terminal.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/WhiskeredBifunctors.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/Examples/IsoCommaLimits.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/Examples/AlgebraStructuresColimits.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/whiskering.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DaggerCategories/Examples/Relations.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/SymmetricMonoidalDialgebras.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/category_binops.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/NumberSystems/RationalNumbers.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/ZFstructures.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Displayed/Symmetric.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Free_Monoids_and_Groups.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Structure/Closed.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Univalence.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Subcategory/Limits.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/AlgebraicTheoryMorphisms.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/TotalDisplayedMonoidalCurried.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Archimedean.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/FixpointTheorems/Pataraia.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/RepresentableFunctors/RawMatrix.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/DisplayedMonoidalTensored.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/NaturalTransformations.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Examples/Products.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/MoreFibrations/FibrationsCharacterisation.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/precomp_ess_surj.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/NumberSystems/NaturalNumbers_le_Inductive.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/ImageEnriched.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Induction/FunctorCoalgebras_legacy.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/SplitMonicsAndEpis.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Enriched/Enriched.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/Examples/UnitCategoryLimits.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/GaussianElimination/Corollaries.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/Examples/LambdaCalculus.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/Algebras.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/EquivalenceOverId.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/terminal.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/setwith2binops.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/Precomposition.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Constructions.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/Slice.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/rezk_completion.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DaggerCategories/Functors/FullyFaithful.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Dialgebras.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/RepresentableFunctors/DirectSum.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Chains/Adamek.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/AdditiveFunctors.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DaggerCategories/Categories.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Tactics/Abmonoids_Tactics.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/Univalence.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Displayed/Monoidal.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/MonadsAsMonoidsElementary.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Structures/StructureLimitsAndColimits.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/Comma.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Epis.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Modules/Submodule.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/SetStructures.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/ProductCategory.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Semantics/LinearLogic/LafontCategory.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/CategoricalRecursionSchemes.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/RigsAndRings/Ideals.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DaggerCategories/Functors/FullyFaithful.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Epis.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Examples/BinaryProducts.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/RezkCompletion/LiftedMonoidal.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/Orders.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EpiFacts.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/SmashStructureEnriched.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/RezkCompletion/LiftedAssociator.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Univalence.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Modules/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Examples/Products.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Core/Basics.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/zero.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Examples/ListDataType.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/RigsAndRings/Ideals.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/FiveLemma.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/SetValuedFunctors.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Actegories/Examples/SelfActionInCATElementary.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/commrings.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/GrothendieckConstruction/IsosInTotal.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/SymmetricMonoidalCoEilenbergMoore.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/abmonoids.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/commrigs.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/intdoms.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/Algebras.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/SetWithSubset.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Semantics/LinearLogic/RelationalModel.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/NumberSystems/Tests.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/colimits.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Induction/W/Fibered.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/RepresentableFunctors/DirectSum.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/PresheafCategory.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Examples/Discrete.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/Profunctor.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/RezkCompletion/MonoidalRezkCompletion.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Limits/Examples/SelfEnrichedLimits.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/rings.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/FiniteSequences.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Folds/folds_precat.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/flds.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/CompletelyIterativeAlgebras.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/rigs.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Core/FubiniTheorem.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/ComprehensionC.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/GrothendieckTopos.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/FixpointTheorems/LeastFixpoint.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/PseudoElements.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/Kleisli.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/GroupAction.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/SyntheticHomotopyTheory/AffineLine.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/UnderCategories.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/DispFunctorPair.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Basis/Algebraic.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/UnitorsAndAssociatorsForEndofunctors.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/grs.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/initial.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/AlgebraStructures.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Algebras.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DaggerCategories/Functors/WeakEquivalences.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal/FreeAlgebras.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/FixpointTheorems/LeastFixpoint.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Codomain.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/OrderedSets.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Semantics/EnrichedEffectCalculus/EECModel.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/Spans.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/IndexedCategories/CartesianToIndexedFunctor.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/Derivative.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/SetCoends.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Limits/Examples/OppositeEnrichedLimits.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/PointedPosetStructures.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/PointedSetCartesianMonoidal.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Modules/Examples.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Comonoids/Monoidal.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/Posets/Basics.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Colimits/Examples/OppositeEnrichedColimits.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/SetCartesianMonoidal.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/PosetsMonoidal.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/StreetFibration.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/ProductCategory.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/SIP.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/GrothendieckConstruction/IsosInTotal.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/RepresentationTheorem.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Core/ScottTopology.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/Opposite.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Examples/Discrete.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/PointedSetStructures.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Actegories/MorphismsOfActegories.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Foundations/Propositions.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/KA.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/FixpointTheorems/Pataraia.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Comonoids/CommComonoidsCartesian.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Structure/Symmetric.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Universal_Algebra/Algebras.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Isos.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/EnrichmentMonad.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/MonoEpiIso.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Core/DirectedSets.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/PointedDCPOStrict.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Semantics/LinearLogic/LinearNonLinear.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Structures/CartesianStructure.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/WeakEquivalences.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/Graph.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Chains/Cochains.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/NumberSystems/NaturalNumbers_le_Inductive.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Connected.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Apartness.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/OppositeCategory/OppositeAdjunction.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/Examples/FreeTheory.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/SliceEnriched.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Displayed/WhiskeredDisplayedBifunctors.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/All.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/KFiniteSubtypes.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/KFiniteTypes.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/Lenses.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/BraidedMonoidalCategories.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Examples/Bool.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Examples/BinarySums.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/StructuresMonoidal.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Foundations/Preamble.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/Reindex.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/initial.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Universal_Algebra/EqAlgebras.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/AxiomOfChoice.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/DialgebraEnriched.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/TotalCategoryFacts.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/GaussianElimination/Matrices.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/SimplicialSets.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/DispCatOnTwoSidedDispCat.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/PathsOver.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/DivisionRig.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/WeakEquivalences.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Actegories/Actegories.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/Posets/PosetSum.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/Opp.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/DisplayedFunctor.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Induction/W/Uniqueness.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/RezkCompletion/RezkUniversalProperty.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Induction/M/Uniqueness.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Inductives/Lists.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/exponentials.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DaggerCategories/Examples/Groupoids.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/EndofunctorsMonoidalElementary.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/Lattice/Examples/Subsets.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/Relations.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Semantics/EnrichedEffectCalculus/ContinuationModel.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DaggerCategories/Categories.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/SyntheticHomotopyTheory/Test.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Displayed/TotalMonoidal.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicGeometry/Spec.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DaggerCategories/Univalence.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/Constant.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Discrete.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/Monads.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/cokernels.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/OppositeCategory/LimitsAsColimits.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/catiso.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/GraphPaths.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DaggerCategories/Unitary.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/AlternativeDefinitions/Dcpo.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedBinaryCoproducts.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/Yoneda.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Equivalences/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Examples/IdealCompletion.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/kernels.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/MonoEpiIso.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DaggerCategories/CatIso.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/Structures.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/FunctorAlgebras.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Profunctors/Squares.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Basis/Algebraic.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/CartesianCubicalSets.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/MetricTree.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/DispFunctorPair.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/PosetStructures.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Core/ScottTopology.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/MetricTree.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal/VTerms.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/TransportMorphisms.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/PAdics/frac.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/IndexedCategories/IndexedCategoryToFibration.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedBinaryProducts.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Comonoids/Tensor.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Elements.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/RealNumbers/Prelim.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Semantics/EnrichedEffectCalculus/CopowerModel.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Elements/Sharp.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Foundations/HLevels.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicGeometry/SheavesOfRings.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/Examples/CategoryProductLimits.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/PresheafMorphisms.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/Examples/LambdaCalculus.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Paradoxes/GirardsParadox.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/Posets/Basics.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Colimits/Examples/SelfEnrichedColimits.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/IndexedCategories/IndexedTransformation.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/IteratedBinaryOperations.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/initial.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/KleisliCategory.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DaggerCategories/Functors/Factorization.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/PointedDCPOStructures.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Core/IntrinsicApartness.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/KleisliEnriched.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/WeakEquivalences.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/FinOrdCoproducts.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/NoInjectivePairing.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/RealNumbers/DedekindCuts.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/FunctorCategory.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Connected.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/PointedFunctors.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/IndexedCategories/IndexedTransformationToTransformation.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Comonoids/Category.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Examples/Bool.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/Tests.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/RepresentableFunctors/RawMatrix.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/CartesianMonoidal.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/cokernels.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/Posets/PosetSum.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/ConstructiveStructures.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Additive.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/terminal.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/SyntheticHomotopyTheory/Halfline.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/KTriplesEquiv.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/StreetOpFibration.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/ElementaryTopos.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/KFiniteSubtypes.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Topology/CategoryTop.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/Posets/LiftPoset.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Chains/Chains.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DaggerCategories/Examples/Groupoids.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Induction/FunctorAlgebras_legacy.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/FiniteSets.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Functors.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/IsoComma.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Induction/All.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/kernels.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/FullSubEnriched.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/Setcategories.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/RepresentableFunctors/Precategories.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/pushouts.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Semantics/LinearLogic/LinearToLinearNonLinear.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedCoequalizers.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/TotalAdjunction.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/RezkCompletion/MonoidalRezkCompletion.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/kernels.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/AlgebraFibration.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/Examples/UnitCategoryLimits.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/MonoidalCategoriesTensored.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/GaussianElimination/Auxiliary.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/Tuples.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/LambdaTheoryMorphisms.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/PartD.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/Examples/Plus1Presheaf.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Examples/Nat.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/Orders.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Folds/folds_isomorphism.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Foundations/UnivalenceAxiom.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/BinopCartesianMonoidal.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Examples/SubDCPO.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/BoundedSearch.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/SyntheticHomotopyTheory/Circle2.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/NaturalTransformations.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Actegories/ProductsInActegories.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/coproducts.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Type/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedEqualizers.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/DisplayedNatTrans.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Chains/All.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Actegories/ActionBasedStrongMonads.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Core/IntrinsicApartness.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/AxiomOfChoice.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedConicalColimits.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/AbelianPushoutPullback.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/UnivalentKleisliEnriched.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/Setcategories.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/pullbacks.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Actegories/CoproductsInActegories.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/cokernels.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Core/CoordinateContinuity.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/GaussianElimination/Tests.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/PrecompEquivalence.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/TwoSidedFibration.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Examples/Group.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/SyntheticHomotopyTheory/Halfline.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Displayed/MonoidalSections.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/Coproducts.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Univalence.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Foundations/Init.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Examples/Monoid.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/elems_slice_equiv.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal/FreeAlgebras.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Basis/Basis.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/StructureIdentity.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/Comonads.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/AlgebraicTheoryMorphisms2.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/GaussianElimination/Tests.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/CommaCategories.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/GrothendieckConstruction/Projection.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/MonoidalPointedObjects.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Enriched/Opposite.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Subcategory/Full.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Induction/ImpredicativeInductiveSets.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/EnrichmentTransformation.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedConicalLimits.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/RezkCompletion/LiftedUnitors.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/ChangeOfBase.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/LambdaCalculus.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/EndofunctorsMonoidalElementary.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/LeftKanExtension.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/opp_precat.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DaggerCategories/Examples/Relations.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Core/CoordinateContinuity.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Equivalences/CompositesAndInverses.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DaggerCategories/Univalence.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Core/ScottContinuous.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/EmptyEnriched.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/AlgebraicTheories2.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/IndexedCategories/IndexedFunctorToCartesian.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/CategorySum.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/UnivalentKleisliMapping.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Elements/Sharp.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/NoInjectivePairing.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DaggerCategories/Functors/WeakEquivalences.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/FinOrdProducts.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/QuotientSet.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/coequalizers.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Projection.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/StandardCategories.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DaggerCategories/Functors.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Basis/Continuous.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/GaussianElimination/RowOps.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/coslicecat.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/StructureEnriched.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Profunctors/Examples.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Total.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/RealNumbers/Prelim.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Semantics/LinearLogic/LinearCategory.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/covyoneda.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/wosets.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedCoproducts.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Actions.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedColimits.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/preorder_categories.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedLimits.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Induction/PolynomialFunctors.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/ConstantFunctor.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/Subtypes.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Displayed/MonoidalFunctorLifting.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/SyntheticHomotopyTheory/Test.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/products.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/Nat.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/Equivalences.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Comonoids/CartesianAsComonoids.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/Graph.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/BoundedSearch.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Examples/Monoid.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/TotalDisplayedMonoidalCurried.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Subcategory/FullEquivalences.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedProducts.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/LModules.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/PosetEnriched.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Induction/M/Chains.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/equalizers.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/IsoCommaCategory.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/Relations.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Core/WayBelow.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DaggerCategories/FunctorCategory.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Examples/Unit.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/PointedPosetStrict.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/GaussianElimination/Vectors.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Chains/Cochains.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DaggerCategories/Functors.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/All.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/EnrichmentFunctor.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/All.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DaggerCategories/Transformations.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/NNO.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/FilteredColimits.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/FinSet.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Folds/folds_pre_2_cat.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Chains/OmegaContFunctors.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/YonedaBinproducts.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Tactics/Monoids_Tactics.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/Sigma.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/pushouts.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/AlgebraicTheoryCategory.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/ProdOfTwosidedDispCat.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/covyoneda.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/RezkCompletion/PrecompFullyFaithful.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/RezkCompletion/EnrichedRezkCompletion.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Semantics/LinearLogic/LinearCategoryEilenbergMooreAdjunction.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/IndexedCategories/NatTransToIndexed.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/cats/limits.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/NullHomotopies.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/OppositeCategory/OppositeAdjunction.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/EquivalenceWhiskeredNonCurriedMonoidalCategories.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Core/WayBelow.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Actegories/ProductActegory.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Subcategory/Reflective.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/All.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/TwoCategories.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Fiber.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/PresheafMorphisms.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal/SortedTypes.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/KTriples.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/SetCoends.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/Filtered.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/RelativeModules.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DaggerCategories/Transformations.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/PointedFunctorsComposition.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/CGraph.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/Colimits.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Structure/Cartesian.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Limits.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/Lattice/Distributive.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/SymmetricMonoidalDialgebras.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/Fullsub.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/Posets/PointedPosets.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/Tactics.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Relations.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/DecidablePropositions.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicGeometry/Topology.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Type/Structures.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/Posets/QuotientPoset.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/GraphPaths.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/NullHomotopies.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/IndexedCategories/CoreIndexedCategory.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/PointedFunctorsComposition.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/Tuples.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Induction/M/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Induction/W/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/coequalizers.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/RealNumbers/DecidableDedekindCuts.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/OppositeEnriched.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Presheaf.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/LatticeObject.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/Lattice/Examples/Bool.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/covyoneda.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Foundations/Tests.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Profunctors/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/LiftPoset.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal/TermAlgebras.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/AlgebraMorphisms.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/DisplayedMonoidalCurried.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/Univalence.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/AlgebraicTheoryMorphisms2.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/All.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Examples/Sums.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Elements/Maximal.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/TransportLaws.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/SelfEnriched.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/DisplayedCatEq.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Examples/SubDCPO.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/CategoryOfSetCategories.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/Propositions.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/Notations.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/NegativePropositions.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Isos.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/MonoidalCategoriesReordered.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Fiber.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/preorder_categories.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/SyntheticHomotopyTheory/Circle.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Basis/CompactBasis.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/Examples/ProjectionsTheory.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/Sigma.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Semantics/LinearLogic/LiftingModel.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Quotobjects.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/AlgebraicTheories2.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicGeometry/SheavesOfRings.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/KleisliCategory.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Subobjects.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/FiberwiseProduct.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/SyntheticHomotopyTheory/Coproduct.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/HorizontalComposition.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/MoreFibrations/DispCatsEquivFunctors.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/Cartesian.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/NNO.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DaggerCategories/Examples/Fullsub.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/WeakEquivalences.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal/SortedTypes.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/equalizers.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Tactics/Abmonoids_Tactics.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/EssentiallyAlgebraic.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/LambdaTheoryMorphisms.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/MonadAlgebras.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/Examples/OnePointTheory.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Ktheory/All.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/UnitalBinop.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/Lattice/Bounded.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/MoreLists.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/Limits.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Foundations/HLevels.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Tests.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/ProfunctorTwosidedDispCat.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/PowerObject.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/ExponentiationLeftAdjoint.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/SIP.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Adjunctions.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/ImageEnriched.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/Lattice/Distributive.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Examples/Propositions.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Enriched/EnrichmentEquiv.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/Posets/LiftPoset.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/yoneda.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/RezkCompletion/LiftedTensor.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Examples/Group.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Comonoids/MonoidalCartesianBuilder.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/LambdaTheoryCategory.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/SubobjectClassifier.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/SimplicialSets.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Morphisms.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/bincoproducts.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/RepresentableFunctors/Bifunctor.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/Coends.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Foundations/UnivalenceAxiom2.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Foundations/Preamble.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/Core.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/YonedaLemma.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/StandardDiagrams.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/QuotientSet.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/OppositeCategory/OppositeOfFunctorCategory.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/Categories.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/CategoriesWithBinOps.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/EssentiallyAlgebraic.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/SyntheticHomotopyTheory/Coproduct.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/ExactCategories/Tests.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/MonadsAsMonoidsElementary.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/VectorsTests.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/Coproducts.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/BicatOfCatsElementary.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal/HVectors.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/Ends.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Adjunctions/Examples.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Displayed/SymmetricMonoidalBuilder.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/AlternativeProofs.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/Lattice/Boolean.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Examples/Propositions.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Inductives/LambdaCalculus.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/MoreFibrations/Prefibrations.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/FunctorCoalgebras.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/EnrichmentMonad.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/VectorsTests.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/eqdiag.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Matrix.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/Notations.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Induction/M/ComputationalM.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/FunctorCategories.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/UnitEnriched.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/EilenbergMooreEnriched.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/monoids.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Colimits/CopowerFunctor.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/AlgebraicTheories.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/ArrowCategory.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/PartD.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/KATriangulated.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/MonoidalCategoriesCurried.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/Lattice/Bounded.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/Lists.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/IndexedCategories/IndexedCategory.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/RezkCompletion/LiftedTensorUnit.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Comonoids/Symmetric.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Actegories/ConstructionOfActegories.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/PrecategoriesWithAbgrops.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Induction/W/Naturals.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Groupoids.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Actegories/Examples/ActionOfEndomorphismsInCATElementary.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/MoreFibrations/CartesiannessOfComposites.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/Posets/MonotoneFunctions.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Examples/Fixpoints.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/Examples/Plus1Presheaf.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/WellFoundedRelations.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/CatIsoInserter.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Semantics/LinearLogic/LinearNonLinear.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Examples/Exponentials.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Inductives/PropositionalLogic.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Type/Colimits.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/Univalence.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Type/Limits.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/RelMonads_Coreflection.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Examples/ListDataType.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/zero.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Subcategory/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/Precomposition.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/Sets.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Signatures.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Graph.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/DisplayedFunctorEq.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/CGraph.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/SetStructures.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/Examples/CategoryOfSetcategoriesLimits.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedPowers.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Core/Basics.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Examples/Nat.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/SetCartesianMonoidal.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/Lattice/Complement.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedCopowers.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Examples/Unit.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/SplitMonicsAndEpis.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Graph.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/LambdaAlgebraMonoid.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicGeometry/All.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/MoreFibrations/DisplayedDisplayedCats.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Type/Core.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/RealNumbers/Fields.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal/EqAlgebras.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/CoEilenbergMoore.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/MonoidalFunctorsTensored.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/Equivalence_Relations.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/HomotopicalCategory.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Topology/All.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/NumberSystems/NaturalNumbersAlgebra.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/RealNumbers/All.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/SliceFamEquiv.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Signatures.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Topology/Prelim.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/EilenbergMoore.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Subcategory/Limits.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/DCPOStructures.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/All.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/Product.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/FunctorCategory.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/RealNumbers/Sets.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/cones.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/Examples/EndomorphismTheory.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/FiniteSetSkeleton.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Modules/Quotient.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicGeometry/Topology.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/Lattice/Heyting.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Tests.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/Slice.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/Vectors.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/GrothendieckConstruction/TotalCategory.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/SetEnriched.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Equations.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal/TermAlgebras.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/CategoriesOfMonoids.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/modules.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Induction/PolynomialFunctors.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Equations.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Strictness.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/UnitorsAndAssociatorsForEndofunctors.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/HomFunctor.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/terminal.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Examples/Discrete.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/pullbacks_slice_products_equiv.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Apartness.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/OppositeCategory/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Modules/Multimodules.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/CGraph.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Inductives/Trees.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Folds/from_precats_to_folds_and_back.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/StructureIdentity.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/PointedSetStructures.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Limits/EnrichedTerminal.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Tactics/Groups_Tactics.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/FixpointTheorems/LeastFixpoint.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Adjunctions/Restriction.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/Presheaves.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/EnrichmentAdjunction.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Core/DirectedSets.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/ZigZag.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/RightKanExtension.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/Arrow.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/FixpointTheorems/Pataraia.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/NumberSystems/Tests.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/whiskering.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/CatIsoDisplayed.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/FullyFaithful.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/Lattice/Boolean.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monics.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/Examples/FreeMonoidTheory.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/GrothendieckTopos.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/ElementsOp.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/wosets.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/Subposets.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/PointedPosetStructures.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Foundations/Init.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/category_binops.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Induction/M/Limits.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/RealNumbers/DecidableDedekindCuts.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/KFiniteTypes.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Enriched/ChangeOfBase.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/CategoryOfPosets.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Semantics/EnrichedEffectCalculus/EECModel.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/IndexedCategories/FibrationToIndexedCategory.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/PointedDCPOStrict.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Type/Univalence.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/MoreEquivalences.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/SetWithSubset.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/rezk_completion.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Core/ScottTopology.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/SliceEnriched.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Type/MonoEpiIso.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/DivisionRig.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/CategoryEquality.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/Bimodules.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/SetValuedFunctors.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Semantics/LinearLogic/LafontCategory.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/Lattice/Examples/Subsets.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/setwith2binops.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Colimits/EnrichedInitial.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Comonoids/Monoidal.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/Examples/FreeTheory.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/Comma.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/SyntheticHomotopyTheory/All.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/precomp_fully_faithful.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Examples/Products.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Basis/Algebraic.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/Maybe.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Chains/Adamek.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/AlgebraCategory.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/DiagonalFunctor.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Core/FubiniTheorem.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/Lattice/Heyting.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Paradoxes/GirardsParadox.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Core/IntrinsicApartness.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Chains/CoAdamek.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/Interval.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/RepresentableFunctors/Test.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Examples/Tests.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/Interval.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/Posets/PosetSum.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/Constant.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/AlgebraMorphisms.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/AlgebraicTheoryMorphisms.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Tactics/Utilities.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/abmonoids.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/KFiniteSubtypes.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/LambdaTheories.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/CategoriesWithBinOps.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Examples/Equalizers.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/Orders.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/commrings.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/GrothendieckConstruction/IsOpfibration.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Induction/M/Core.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Equivalences/FullyFaithful.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Induction/W/Fibered.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Induction/W/Core.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/Posets.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/Prelude.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Univalence.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/commrigs.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/RezkCompletion/EnrichedRezkCompletion.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/All.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/initial.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/IndexedCategories/OpIndexedCategory.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/Profunctor.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/intdoms.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Folds/folds_precat.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/SymmetricMonoidalCoEilenbergMoore.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EpiFacts.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/PosetStructures.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/CartesianCubicalSets.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Limits/Examples/OppositeEnrichedLimits.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/TransportMorphisms.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/AxiomOfChoice.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Universal_Algebra/Algebras.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Colimits/Examples/OppositeEnrichedColimits.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/binproducts.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Actegories/Examples/SelfActionInCATElementary.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/rings.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/IndexedCategories/CartesianToIndexedFunctor.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/rigs.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/RezkCompletion/RezkUniversalProperty.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Elements/Sharp.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/flds.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/zero.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Subcategory/Reflective.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/ProductCategory.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Induction/FunctorCoalgebras_legacy.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/grs.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/Subposets.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Comonoids/CommComonoidsCartesian.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/RigsAndRings/Ideals.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/PAdics/All.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Comonoids/TransportComonoidAlongRetraction.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/MonoEpiIso.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/SkewMonoidal/SkewMonoidalCategories.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/PointedSetCartesianMonoidal.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Modules/Examples.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Epis.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/SkewMonoidal/CategoriesOfMonoids.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Foundations/UnivalenceAxiom2.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Foundations/Preamble.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/MonoidalFunctorsCurried.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/MoreFibrations/FibrationsCharacterisation.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/ComprehensionC.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/NumberSystems/All.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/GaussianElimination/Tests.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/Examples/LambdaCalculus.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal/EqAlgebras.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DaggerCategories/Unitary.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/Opposite.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Codomain.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/CompletelyIterativeAlgebras.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/Univalence.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/IndexedCategories/IndexedFunctor.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/Equivalence_Relations.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/UnderCategories.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/PointedDCPOStructures.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Modules/Submodule.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/PosetsMonoidal.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Foundations/HLevels.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Induction/M/Uniqueness.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/Tactics.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/TotalCategoryFacts.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/DoubleNegation.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/Examples/UnitCategoryLimits.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DaggerCategories/Functors/FullyFaithful.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Enriched/UnderlyingCategory.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/BinopCartesianMonoidal.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/Examples/OnePointTheory.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/Algebras.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/Lattice/Complement.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Algebras.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/Univalence.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/CategoriesOfMonoids.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/Maybe.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/StructuresMonoidal.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/Posets/Basics.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Displayed/TransportLemmas.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/NumberSystems/NaturalNumbers_le_Inductive.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Connected.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Core/WayBelow.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/initial.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/Bool.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/DispFunctorPair.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Induction/W/Uniqueness.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/OppositeCategory/LimitsAsColimits.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DaggerCategories/Examples/Fullsub.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/Lattice/Examples/Bool.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/RezkCompletion.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/Bool.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Quotobjects.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Ktheory/GrothendieckGroup.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/terminal.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Examples/Fixpoints.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Discrete.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/IsoComma.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/Kleisli.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DaggerCategories/Functors/Factorization.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/WeakEquivalences.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/FinOrdCoproducts.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/RezkCompletion/MonoidalRezkCompletion.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Universal_Algebra/EqAlgebras.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/IndexedCategories/IndexedFunctorToCartesian.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/EmptyEnriched.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/StrongMonad.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/coslicecat.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/GrothendieckConstruction/IsosInTotal.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DaggerCategories/Categories.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/IndexedCategories/NatTransToIndexed.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Semantics/EnrichedEffectCalculus/EECModel.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Actegories/ProductsInActegories.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Semantics/LinearLogic/LiftingModel.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/AlternativeProofs.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/IndexedCategories/IndexedTransformationToTransformation.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Chains/Chains.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/Posets/LiftPoset.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/AlgebraFibration.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/RealNumbers/Fields.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Tactics/All.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/FullSubEnriched.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Tactics/Monoids_Tactics.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Semantics/LinearLogic/LinearCategoryEilenbergMooreAdjunction.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/DoubleNegation.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Type/Structures.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/Examples/ProjectionsTheory.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Examples/Bool.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Comonoids/Symmetric.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/Graph.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/MetricTree.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/RepresentableFunctors/DirectSum.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DaggerCategories/Examples/Relations.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/PointedFunctors.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DaggerCategories/CatIso.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/Test.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/Fullsub.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Semantics/LinearLogic/LinearNonLinear.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DaggerCategories/Examples/Groupoids.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DaggerCategories/Univalence.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Enriched/Opposite.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Foundations/Tests.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/Test.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/cokernels.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Actegories/ActionBasedStrongMonads.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/RealNumbers/Prelim.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/EndofunctorsMonoidalElementary.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Tactics/Monoids_Tactics.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/FinSet.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal/VTerms.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/IndexedCategories/IndexedTransformation.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/BoundedSearch.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/YonedaBinproducts.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/ImageEnriched.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/kernels.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Subcategory/FullEquivalences.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/FinOrdProducts.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Folds/All.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Univalence.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Modules.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/SymmetricMonoidalDialgebras.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal/SortedTypes.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/Tactics.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/NoInjectivePairing.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/TwoSidedDisplayedCats/Examples/Product.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/ConstantFunctor.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/Tuples.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/SetCoends.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DaggerCategories/Functors/WeakEquivalences.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Examples/SubDCPO.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/Setcategories.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/RepresentableFunctors/RawMatrix.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/IndexedCategories/CoreIndexedCategory.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Topology/CategoryTop.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/SetStructures.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Type/MonoEpiIso.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Semantics/LinearLogic/LafontCategory.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Universal_Algebra/EqAlgebras.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Examples/Monoid.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Examples/Unit.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/WeakEquivalences.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/CGraph.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal/FreeAlgebras.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Core/CoordinateContinuity.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/All.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/AlgebraicTheoryMorphisms2.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Chains/Cochains.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/SyntheticHomotopyTheory/Halfline.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/AlgebraicTheories2.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/preorder_categories.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DaggerCategories/Transformations.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Graph.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/PresheafMorphisms.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/PointedPosetStructures.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/FiniteSetSkeleton.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/GraphPaths.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/SimplicialSets.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/PosetsMonoidal.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/All.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/Notations.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/SyntheticHomotopyTheory/Test.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DaggerCategories/Functors.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/EnrichmentMonad.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/FinSet.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Examples/Group.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Tactics/Utilities.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/MonadsAsMonoidsElementary.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Tactics/Groups_Tactics.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/Lattice/Boolean.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/BraidedMonoidalCategories.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/EnrichedCats/Examples/Precomposition.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Signatures.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Induction/PolynomialFunctors.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicGeometry/SheavesOfRings.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/LambdaTheoryMorphisms.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Type/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/Examples/Plus1Presheaf.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/Coproducts.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/All.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/NullHomotopies.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Foundations/All.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Paradoxes/All.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Type/Structures.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/QuotientSet.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/Lattice/Distributive.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/All.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/SIP.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/Examples/ProjectionsTheory.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/DecSet.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/SyntheticHomotopyTheory/Coproduct.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/EssentiallyAlgebraic.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Tactics/Groups_Tactics.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Examples/Nat.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/SetCartesianMonoidal.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/OppositeCategory/OppositeAdjunction.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/StructureIdentity.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicGeometry/Topology.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Examples/Propositions.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/Lattice/Examples/Bool.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Examples/StructuresMonoidal.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/Examples/OnePointTheory.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Examples/ListDataType.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Tests.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs/Examples/Fixpoints.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Foundations/UnivalenceAxiom2.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Subcategory/Reflective.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Tactics/Utilities.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Equations.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/PointedFunctorsComposition.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/DCPOs.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Induction/M/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/Subposets.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/PartD.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/All.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Folds/UnicodeNotations.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/Univalence.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/RealNumbers/DecidableDedekindCuts.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/CategoriesWithBinOps.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/Lattice/Bounded.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Induction/W/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/All.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/AlgebraMorphisms.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/RezkCompletion.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/OppositeCategory/Core.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal/TermAlgebras.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DaggerCategories/Examples/Fullsub.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Quotobjects.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/All.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/VectorsTests.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/DecSet.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/All.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/NNO.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Topology/CategoryTop.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/Interval.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Type/Colimits.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Type/Limits.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/All.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/DaggerCategories/CatIso.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Type/Univalence.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/Lattice/Complement.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/Maybe.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal/EqAlgebras.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/Equivalence_Relations.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Type/Colimits.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/All.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Type/Limits.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/RealNumbers/Fields.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicTheories/FiniteSetSkeleton.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/DoubleNegation.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/Lattice/Heyting.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/Bool.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/All.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/All.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Foundations/Init.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/Test.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Folds/UnicodeNotations.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Semantics/All.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/MoreFoundations/AlternativeProofs.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Induction/All.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Semantics/All.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Induction/All.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Foundations/All.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/OppositeCategory/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/All.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Foundations/All.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Combinatorics/DecSet.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/All.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Type/MonoEpiIso.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/Prelude.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/All.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Tactics/EnsureStructuredProofs.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Type/Univalence.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/RealNumbers/All.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/RezkCompletion.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/All.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/RealNumbers/All.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/Posets.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/OrderTheory/Posets.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/SyntheticHomotopyTheory/All.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/Prelude.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Tactics/EnsureStructuredProofs.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Tactics/All.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Tactics/All.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/SyntheticHomotopyTheory/All.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Folds/All.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Chains/All.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/NumberSystems/All.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Folds/All.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/NumberSystems/All.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/PAdics/All.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/PAdics/All.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Topology/All.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicGeometry/All.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/CategoryTheory/Chains/All.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Topology/All.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Folds/UnicodeNotations.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/AlgebraicGeometry/All.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Universal.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Paradoxes/All.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Ktheory/All.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Modules.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Ktheory/All.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Paradoxes/All.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Tactics/EnsureStructuredProofs.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/UniMath/Algebra/Modules.vopam remove -y coq-unimath.dev