« Up

unimath 20210807 2 h 41 m

(2021-10-30 10:24:50 UTC)

Context

# Packages matching: installed
# Name                # Installed # Synopsis
base-bigarray         base
base-threads          base
base-unix             base
conf-findutils        1           Virtual package relying on findutils
conf-gmp              3           Virtual package relying on a GMP lib system installation
coq                   8.13.0      Formal proof management system
num                   1.4         The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml                 4.12.0      The OCaml compiler (virtual package)
ocaml-base-compiler   4.12.0      Official release 4.12.0
ocaml-config          2           OCaml Switch Configuration
ocaml-options-vanilla 1           Ensure that OCaml is compiled with no special options enabled
ocamlfind             1.9.1       A library manager for OCaml
zarith                1.12        Implements arithmetic and logical operations over arbitrary-precision integers
# opam file:
opam-version: "2.0"
maintainer: "The UniMath Development Team"
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: [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: "https://github.com/UniMath/UniMath/archive/refs/tags/v20210807.tar.gz"
  checksum: "sha512=db2f660aea7e4c7eda6d10173173b80d357f994ff148102df6d20b0098e4c4e3ec17f9956700e118b7ff043a4ef29827cccd1fe9f5f54b5f5deaebcac60c666c"
}

Lint

Command
true
Return code
0

Dry install

Dry install with the current Coq version:

Command
opam install -y --show-action coq-unimath.20210807 coq.8.13.0
Return code
0

Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:

Command
true
Return code
0

Install dependencies

Command
opam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-unimath.20210807 coq.8.13.0
Return code
0
Duration
10 s

Install

Command
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-unimath.20210807 coq.8.13.0
Return code
0
Duration
2 h 41 m

Installation size

Total: 196 M

  • 17 M ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/Derivative.vo
  • 6 M ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Actions.vo
  • 6 M ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Adjunctions.vo
  • 5 M ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/Prod.vo
  • 4 M ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Core.vo
  • 3 M ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/CohomologyComplex.vo
  • 2 M ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Adjunctions/Core.vo
  • 2 M ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/catiso.vo
  • 2 M ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/ContravariantFunctor.vo
  • 2 M ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Inductives/LambdaCalculus.vo
  • 2 M ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Display/Map1Cells.vo
  • 2 M ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/MappingCone.glob
  • 2 M ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/LocalizingClass.vo
  • 2 M ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/ActionBasedStrengthOnHomsInBicat.vo
  • 2 M ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Biadjunction.vo
  • 2 M ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Display/StrictCompositor.vo
  • 2 M ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Constructions.vo
  • 2 M ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Display/Compositor.vo
  • 2 M ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/LamFromBindingSig.vo
  • 2 M ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/Algebras.vo
  • 1 M ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/DispTransformation.vo
  • 1 M ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/DispBicatOfDispCats.vo
  • 1 M ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Equivalences/Core.vo
  • 1 M ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/slicecat.vo
  • 1 M ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/MappingCone.vo
  • 1 M ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/RealNumbers/NonnegativeReals.glob
  • 1 M ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/ExactCategories/ExactCategories.vo
  • 1 M ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Groupoids.vo
  • 1 M ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/KTriplesEquiv.vo
  • 1019 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/KAPreTriangulated.vo
  • 999 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Examples/BicatOfCats.vo
  • 988 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/Triangulated.vo
  • 901 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/DispPseudofunctor.vo
  • 860 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/RigsAndRings.vo
  • 841 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/RelativeMonads.vo
  • 837 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Foundations/PartA.glob
  • 794 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/Sigma.vo
  • 788 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/WkCatEnrichment/Cat.vo
  • 769 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/ExactCategories/ExactCategories.glob
  • 755 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Examples/OpMorBicat.vo
  • 753 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/MultiSorted.vo
  • 738 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/DispInvertibles.vo
  • 727 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Equivalences/CompositesAndInverses.vo
  • 719 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/PAdics/frac.vo
  • 691 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/DispAdjunctions.vo
  • 688 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Display/PseudoFunctorBicat.vo
  • 687 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/CohomologyComplex.glob
  • 670 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/DisplayedInserter.vo
  • 654 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Equivalences.vo
  • 649 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Examples/Strictify.vo
  • 645 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/RigsAndRings.glob
  • 626 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/Functors.vo
  • 614 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/Triangulated.glob
  • 613 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/DispBicat.vo
  • 611 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Fibrations.vo
  • 606 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/precomp_fully_faithful.vo
  • 593 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/DispBicat.glob
  • 588 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Free_Monoids_and_Groups.vo
  • 588 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/BinaryOperations.glob
  • 583 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/PAdics/padics.vo
  • 580 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Examples/OpCellBicat.vo
  • 572 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/FiberBicategory/FiberBicategory1.glob
  • 556 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Adjunctions/Restriction.vo
  • 534 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/StandardFiniteSets.vo
  • 523 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/KATriangulated.vo
  • 520 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/Complexes.glob
  • 512 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/Algebras.glob
  • 507 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/PAdics/padics.glob
  • 506 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Foundations/PartA.vo
  • 504 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/TranslationFunctors.glob
  • 502 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/LocalizingClass.glob
  • 498 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples.vo
  • 494 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/StandardFiniteSets.glob
  • 487 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/WkCatEnrichment/whiskering.vo
  • 473 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/EquivToAdjequiv.vo
  • 470 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/FiberBicategory/FiberBicategory2.glob
  • 465 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Foundations/Sets.glob
  • 455 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/DisplayedCatToBicat.vo
  • 452 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/STLC.vo
  • 447 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/FiberBicategory/FiberBicategory1.vo
  • 438 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/BinaryOperations.vo
  • 425 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/WellOrderedSets.vo
  • 424 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/CategoricalRecursionSchemes.vo
  • 403 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Bicat.glob
  • 403 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Core.glob
  • 401 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/Kleisli.vo
  • 396 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/PAdics/z_mod_p.vo
  • 390 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Modifications/Modification.vo
  • 385 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Monoids.vo
  • 380 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/ActionBasedStrength.vo
  • 377 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/Structures.vo
  • 374 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/StandardCategories.vo
  • 374 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/PAdics/z_mod_p.glob
  • 371 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/Complexes.vo
  • 370 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Abelian.glob
  • 370 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/DisplayedInserter.glob
  • 367 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/elems_slice_equiv.vo
  • 361 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Chains/OmegaCocontFunctors.vo
  • 361 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/RealNumbers/Reals.glob
  • 360 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/abgrs.glob
  • 355 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Terms.vo
  • 355 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/SignatureExamples.vo
  • 354 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/EpiFacts.vo
  • 352 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Chains/OmegaCocontFunctors.glob
  • 341 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/NumberSystems/Integers.glob
  • 341 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Ktheory/GrothendieckGroup.vo
  • 338 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Domains_and_Fields.vo
  • 335 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/pullbacks.vo
  • 334 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Examples/RestrictImage.vo
  • 333 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Monoids.glob
  • 329 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/PointedOneTypes.vo
  • 327 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/YonedaLemma.vo
  • 319 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/pullbacks.glob
  • 318 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Foundations/Sets.vo
  • 318 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/PAdics/fps.vo
  • 316 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SyntheticHomotopyTheory/Circle2.vo
  • 314 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/RepresentableFunctors/Representation.glob
  • 312 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Foundations/NaturalNumbers.glob
  • 308 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Display/StrictIdentitor.vo
  • 303 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/RealNumbers/NonnegativeRationals.glob
  • 300 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Enriched/Enriched.vo
  • 295 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Examples/Strictify.glob
  • 293 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/BinDirectSums.vo
  • 287 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/PAdics/fps.glob
  • 284 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/RepresentableFunctors/Representation.vo
  • 281 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/MappingCylinder.glob
  • 281 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/WellOrderedSets.glob
  • 279 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/Trivial.vo
  • 275 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/RelativeMonads.glob
  • 273 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/BinDirectSums.glob
  • 272 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/ArrowCategory.vo
  • 270 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SyntheticHomotopyTheory/AffineLine.vo
  • 270 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/PreAdditive.glob
  • 268 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/DispModification.vo
  • 267 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/RealNumbers/NonnegativeReals.vo
  • 265 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Adjunctions/Core.glob
  • 263 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/MappingCone.v
  • 262 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Modules/Core.vo
  • 261 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/AdjointUnique.glob
  • 255 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/Slice.vo
  • 255 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/DispDepProd.vo
  • 254 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/limits.vo
  • 251 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Domains_and_Fields.glob
  • 248 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/TranslationFunctors.vo
  • 247 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/FiberCategory.vo
  • 247 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/limits.glob
  • 246 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Groups.glob
  • 244 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Groups.vo
  • 243 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/Sigma.glob
  • 243 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Display/Identitor.vo
  • 241 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/RightKanExtension.vo
  • 236 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/Prod.glob
  • 236 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Transformations/Examples/Whiskering.vo
  • 235 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Topology/Topology.glob
  • 235 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/ActionBasedStrengthOnHomsInBicat.glob
  • 233 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/WkCatEnrichment/internal_equivalence.vo
  • 233 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/RelMonads_Coreflection.vo
  • 232 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/precomp_ess_surj.glob
  • 232 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Examples/PointedOneTypesBicat.vo
  • 230 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Foundations/PartD.glob
  • 228 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Topology/Filters.glob
  • 225 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Bicat.vo
  • 223 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Equivalences_bis.vo
  • 222 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/NumberSystems/Integers.vo
  • 221 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/LiftingInitial.glob
  • 221 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/CategoryEquality.vo
  • 219 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/DispInvertibles.glob
  • 218 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/FunctorAlgebras.vo
  • 216 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/LiftingInitial_alt.glob
  • 216 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Foundations/PartC.glob
  • 214 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Foundations/NaturalNumbers.vo
  • 213 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/FullSub.vo
  • 213 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/bincoproducts.glob
  • 212 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Display/Map2Cells.vo
  • 211 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Foundations/PartB.glob
  • 210 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/ShortExactSequences.glob
  • 209 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/FixedPointTheorems.vo
  • 209 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/AbelianToAdditive.glob
  • 209 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Display/Base.vo
  • 208 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/slicecat.glob
  • 205 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Strictness.vo
  • 205 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Constructions.glob
  • 205 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/Add2Cell.vo
  • 204 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/PathsOver.vo
  • 203 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Examples/PathGroupoid.vo
  • 201 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/FixedPointTheorems.glob
  • 201 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/GroupAction.vo
  • 201 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/Isos.glob
  • 199 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/KAPreTriangulated.glob
  • 199 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Transformations/PseudoTransformation.vo
  • 199 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/AdjointUnique.vo
  • 199 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/MonadKtripleBiequiv.vo
  • 198 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/IteratedBinaryOperations.vo
  • 197 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/SignatureCategory.vo
  • 197 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/KleisliCategory.vo
  • 195 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/PartA.glob
  • 195 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/PreAdditive.vo
  • 195 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SyntheticHomotopyTheory/AffineLine.glob
  • 192 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/DispPseudofunctor.glob
  • 191 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Presheaf.vo
  • 190 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/Derivative.glob
  • 188 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/StrictPseudoFunctor.vo
  • 188 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Foundations/PartC.vo
  • 188 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/RealNumbers/NonnegativeReals.v
  • 188 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Display/Map1Cells.glob
  • 186 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/CategoricalRecursionSchemes.glob
  • 184 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/Functors.glob
  • 184 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/colimits.glob
  • 183 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Modules/Quotient.vo
  • 183 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/ShortExactSequences.vo
  • 183 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/Monads.vo
  • 183 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Abelian.vo
  • 180 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Transformations/Examples/Associativity.vo
  • 179 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/LiftingInitial.vo
  • 179 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/DispAdjunctions.glob
  • 178 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/LiftingInitial_alt.vo
  • 177 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SyntheticHomotopyTheory/Circle.vo
  • 176 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/PAdics/lemmas.glob
  • 175 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/NumberSystems/RationalNumbers.glob
  • 174 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/FiberBicategory/FiberBicategory2.vo
  • 173 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Colimits/Initial.vo
  • 172 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Equivalences.glob
  • 172 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/FinOrdProducts.vo
  • 172 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/PAdics/lemmas.vo
  • 171 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/DispBiadjunction.vo
  • 170 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/Signatures.vo
  • 168 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/ZFstructures.glob
  • 167 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/KTriples.vo
  • 167 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Lattice.glob
  • 167 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/DispTransformation.glob
  • 166 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/ExponentiationLeftAdjoint.vo
  • 165 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/Opp.glob
  • 163 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Free_Monoids_and_Groups.glob
  • 163 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/AdditiveFunctors.glob
  • 161 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Archimedean.glob
  • 160 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/RepresentableFunctors/Bifunctor.vo
  • 160 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/CCS.vo
  • 159 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/FinOrdCoproducts.vo
  • 158 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Induction/M/ComputationalM.vo
  • 157 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/MappingCylinder.vo
  • 157 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/PathsOver.glob
  • 157 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/PartA.vo
  • 157 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/Monads.vo
  • 156 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Fibrations.glob
  • 155 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/abgrs.vo
  • 155 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/RepresentableFunctors/Precategories.glob
  • 155 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/PseudoElements.glob
  • 154 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/MonadKtripleBiequiv.glob
  • 152 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/SubstitutionSystems.vo
  • 151 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/WellFoundedRelations.vo
  • 151 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Strictness.glob
  • 151 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/binproducts.glob
  • 150 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/bincoproducts.vo
  • 149 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/NaturalTransformations.vo
  • 149 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/ConstructiveStructures.glob
  • 149 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Terms.glob
  • 149 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/colimits.vo
  • 147 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Induction/M/Chains.vo
  • 147 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/cokernels.glob
  • 146 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/Cofunctormap.vo
  • 146 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Modules/Core.glob
  • 145 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/Monads.glob
  • 145 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Actions.glob
  • 144 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/kernels.glob
  • 142 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/FiniteSequences.glob
  • 142 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Display/StrictPseudoFunctorBicat.vo
  • 141 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Foundations/PartB.vo
  • 140 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/FiveLemma.glob
  • 139 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Foundations/PartD.vo
  • 139 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/MonadAlgebras.vo
  • 139 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/MonadsFromSubstitutionSystems.glob
  • 138 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/SignatureExamples.glob
  • 137 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/RealNumbers/DedekindCuts.glob
  • 135 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Yoneda.vo
  • 135 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/Lam.vo
  • 135 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Inductives/Lists.vo
  • 134 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/pullbacks.glob
  • 134 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Archimedean.vo
  • 133 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/pushouts.glob
  • 133 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/PAdics/frac.glob
  • 133 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Folds/folds_isomorphism.glob
  • 132 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/GroupAction.glob
  • 132 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/PrecategoryBinProduct.glob
  • 132 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/coequalizers.vo
  • 131 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Examples/OpFunctor.vo
  • 131 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/StrictPseudoFunctor.glob
  • 131 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/DispUnivalence.vo
  • 131 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/AdditiveFunctors.vo
  • 130 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Induction/M/Limits.vo
  • 129 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Induction/M/Chains.glob
  • 129 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/CategoriesOfMonoids.vo
  • 128 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/OrderedSets.vo
  • 128 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Foundations/PartA.v
  • 128 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/FiveLemma.vo
  • 127 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/pushouts.glob
  • 125 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/TransportLaws.vo
  • 125 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/FiniteSequences.vo
  • 125 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Representable.vo
  • 125 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/TwoCategories.glob
  • 124 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/Isos.vo
  • 124 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/ActionBasedStrength.glob
  • 124 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/precomp_ess_surj.vo
  • 124 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/binproducts.vo
  • 124 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/ConstructionOfActions.glob
  • 123 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/RealNumbers/Reals.vo
  • 122 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Inductives/Lists.glob
  • 121 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/YonedaLemma.glob
  • 120 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Colimits/Final.vo
  • 120 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/BicategoryLaws.glob
  • 119 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/ModulesFromSignatures.glob
  • 119 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/Monads.glob
  • 118 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/RepresentableFunctors/Precategories.vo
  • 117 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Transformations/Examples/Unitality.vo
  • 117 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/KA.glob
  • 117 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/SubstitutionSystems.glob
  • 116 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/IteratedBinaryOperations.glob
  • 116 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/MultiSorted.glob
  • 116 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Induction/ImpredicativeInductiveSets.vo
  • 116 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SyntheticHomotopyTheory/Circle2.glob
  • 115 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Foundations/Propositions.glob
  • 115 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/BicatOfBicategory.vo
  • 114 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/Signatures.glob
  • 114 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Examples/Composition.vo
  • 114 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/Nat.vo
  • 113 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/KleisliTriple.vo
  • 113 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/SignatureCategory.glob
  • 113 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Tactics/Nat_Tactics.vo
  • 112 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/PseudoElements.vo
  • 111 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Examples/PathGroupoid.glob
  • 111 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Equivalences_bis.glob
  • 111 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/elems_slice_equiv.glob
  • 111 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Foundations/UnivalenceAxiom.glob
  • 110 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/SliceFamEquiv.vo
  • 110 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Additive.glob
  • 109 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/ModulesFromSignatures.vo
  • 108 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/BicategoryOfBicat.vo
  • 108 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Equivalences/Core.glob
  • 108 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/cats/limits.glob
  • 107 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/cones.vo
  • 107 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/PseudoFunctor.glob
  • 106 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/CohomologyComplex.v
  • 106 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/RigsAndRings.v
  • 105 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/Equivalences.glob
  • 105 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Subcategory/Limits.vo
  • 105 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/PointedGroupoid.vo
  • 104 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Limits.vo
  • 104 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/EquivToAdjequiv.glob
  • 104 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/LatticeObject.glob
  • 104 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/Displayed2Inserter.vo
  • 103 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/DispDepProd.glob
  • 103 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/NumberSystems/RationalNumbers.vo
  • 102 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/FunctorCoalgebras.vo
  • 102 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/AbelianPushoutPullback.glob
  • 101 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/OrderedSets.glob
  • 101 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/ExactCategories/ExactCategories.v
  • 101 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Foundations/Sets.v
  • 100 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/Tests.glob
  • 100 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/KleisliTriple.glob
  • 100 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/WkCatEnrichment/whiskering.glob
  • 99 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/PrecategoryBinProduct.vo
  • 99 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Transformations/PseudoTransformation.glob
  • 99 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/MonadsMultiSorted.glob
  • 99 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/coequalizers.glob
  • 99 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/FiberCategory.glob
  • 99 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Examples/BicategoryFromMonoidal.glob
  • 98 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/MonadsFromSubstitutionSystems.vo
  • 98 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/MonadsMultiSorted.vo
  • 97 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Topology/Topology.vo
  • 97 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/FunctorCategory.vo
  • 97 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/LamSignature.vo
  • 97 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/ConstructionOfActions.vo
  • 97 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/FromBindingSigsToMonads_Summary.glob
  • 97 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/RealNumbers/NonnegativeRationals.vo
  • 96 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Topology/Filters.vo
  • 96 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Examples/BicatOfCats.glob
  • 96 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/BinaryOperations.v
  • 96 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/pushouts.vo
  • 95 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Univalence.glob
  • 95 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/FunctorCategory.glob
  • 95 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples.glob
  • 95 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/pullbacks.vo
  • 94 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/AbelianToAdditive.vo
  • 94 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/FiniteSets.glob
  • 94 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Folds/folds_pre_2_cat.glob
  • 93 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/KTriplesEquiv.glob
  • 91 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/PseudoFunctor.vo
  • 91 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Tactics/Nat_Tactics.glob
  • 91 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/DispBuilders.vo
  • 91 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Adjunctions/Examples.vo
  • 91 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/PointedFunctorsMonoidal.vo
  • 91 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/catiso.glob
  • 90 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Adjunctions.glob
  • 90 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/equalizers.glob
  • 90 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/modules.vo
  • 90 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/Triangulated.v
  • 89 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/WkCatEnrichment/prebicategory.vo
  • 88 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/WkCatEnrichment/prebicategory.glob
  • 88 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Morphisms.vo
  • 87 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/SubstitutionSystems_Summary.glob
  • 86 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/ComprehensionC.vo
  • 86 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/pushouts.vo
  • 86 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/MonoidalFunctors.vo
  • 85 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/Complexes.v
  • 85 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/NaturalTransformations.glob
  • 84 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/equalizers.vo
  • 84 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/FunctorAlgebras.glob
  • 84 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/RepresentableFunctors/Bifunctor.glob
  • 84 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/ZFstructures.vo
  • 83 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/CwF.vo
  • 83 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/FiberBicategory/FiberBicategory1.v
  • 83 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/GenMendlerIteration_alt.glob
  • 82 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/Nat.glob
  • 82 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Biadjunction.glob
  • 82 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/MonoidalCategories.glob
  • 82 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/KTriples.glob
  • 82 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/TranslationFunctors.v
  • 82 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/pullbacks_slice_products_equiv.vo
  • 81 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Display/StrictCompositor.glob
  • 81 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/kernels.vo
  • 80 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/coproducts.glob
  • 80 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SyntheticHomotopyTheory/Circle.glob
  • 80 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/PAdics/padics.v
  • 79 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Additive.vo
  • 79 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Dcpo.glob
  • 79 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/MoreLists.vo
  • 79 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/LocalizingClass.v
  • 78 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/LamSignature.glob
  • 78 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/equalizers.glob
  • 78 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/cats/limits.vo
  • 78 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Lattice.vo
  • 77 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/TwoCategories.vo
  • 77 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/AlgebraicGeometry/Spec.vo
  • 77 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/Categories.glob
  • 77 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/Equivalences.vo
  • 77 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/MonoidalCategories.vo
  • 77 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Display/Compositor.glob
  • 76 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/Structures.glob
  • 76 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/products.glob
  • 76 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/cokernels.vo
  • 76 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/DispBiequivalence.vo
  • 76 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/PAdics/z_mod_p.v
  • 76 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/LModules.vo
  • 76 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/FunctorCategory.vo
  • 75 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/Lam.glob
  • 75 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/LModules.glob
  • 75 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/RelativeModules.glob
  • 75 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/ActionBasedStrongFunctorCategory.vo
  • 75 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/bincoproducts.vo
  • 74 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/FiberBicategory/FiberBicategory2.v
  • 74 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/ExactCategories/Tests.glob
  • 73 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/Propositions.glob
  • 73 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Projection.vo
  • 73 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/RealNumbers/Sets.glob
  • 73 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/Limits.vo
  • 73 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/StandardFiniteSets.v
  • 72 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Induction/W/Naturals.vo
  • 71 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/NegativePropositions.vo
  • 71 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Morphisms.glob
  • 70 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Folds/folds_isomorphism.vo
  • 69 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/NumberSystems/NaturalNumbersAlgebra.vo
  • 68 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Univalence.vo
  • 68 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/PrecategoriesWithAbgrops.glob
  • 68 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/BicategoryLaws.vo
  • 68 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/PAdics/fps.v
  • 67 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/KA.vo
  • 67 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Discreteness.vo
  • 67 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/All.vo
  • 67 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/SkewMonoidal/SkewMonoidalCategories.vo
  • 67 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/DispToFiberEquivalence.vo
  • 66 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Core.v
  • 66 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/bincoproducts.glob
  • 66 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Induction/ImpredicativeInductiveSets.glob
  • 66 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/DispToFiberEquivalence.glob
  • 65 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Examples/StrictToPseudo.vo
  • 65 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/BinSumOfSignatures.vo
  • 65 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/RelativeModules.vo
  • 65 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/equalizers.vo
  • 65 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/Opp.vo
  • 64 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/CwF.glob
  • 64 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/Tests.vo
  • 64 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Inductives/PropositionalLogic.glob
  • 63 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/Lists.vo
  • 63 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Induction/M/ComputationalM.glob
  • 63 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Display/Base.glob
  • 63 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/yoneda.glob
  • 63 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/HLevel.vo
  • 62 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Display/PseudoFunctorBicat.glob
  • 62 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Invertible_2cells.glob
  • 62 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Monoids.v
  • 62 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Colimits/Initial.glob
  • 62 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/abgrs.v
  • 62 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/coproducts.vo
  • 62 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Modules/Examples.vo
  • 61 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Foundations/NaturalNumbers.v
  • 61 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/NegativePropositions.glob
  • 61 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/GenMendlerIteration.glob
  • 61 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/coequalizers.glob
  • 61 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Examples/PseudofunctorFromMonoidal.vo
  • 61 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Folds/folds_pre_2_cat.vo
  • 61 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/GenMendlerIteration_alt.vo
  • 60 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/yoneda.vo
  • 60 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/BinProductOfSignatures.vo
  • 59 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/NumberSystems/Integers.v
  • 59 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Abelian.v
  • 59 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/LatticeObject.vo
  • 59 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Display/StrictPseudoFunctorBicat.glob
  • 58 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/MonadAlgebras.glob
  • 58 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/ExponentiationLeftAdjoint.glob
  • 58 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Presheaf.glob
  • 58 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Examples/BicategoryFromMonoidal.vo
  • 58 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Auxiliary.vo
  • 58 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/WellFoundedRelations.glob
  • 57 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/WellOrderedSets.v
  • 57 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/UnitalBinop.vo
  • 57 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Biequivalence.glob
  • 57 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Chains/OmegaCocontFunctors.v
  • 57 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/FiniteSets.vo
  • 57 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/eqdiag.glob
  • 57 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/RightKanExtension.glob
  • 56 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/RealNumbers/Reals.v
  • 56 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/DispUnivalence.glob
  • 56 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/Lists.glob
  • 56 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/opp_precat.glob
  • 55 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Biequivalence.vo
  • 55 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/DispBicat.v
  • 55 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/monoids.vo
  • 55 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Colimits/Final.glob
  • 54 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/products.vo
  • 54 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Dcpo.vo
  • 54 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Foundations/Propositions.vo
  • 54 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/coequalizers.vo
  • 54 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/Univalence.glob
  • 54 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Equivalences/CompositesAndInverses.glob
  • 54 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Matrix.vo
  • 54 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/ActionBasedStrongFunctorCategory.glob
  • 54 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/RelMonads_Coreflection.glob
  • 54 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/ElementsOp.glob
  • 53 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/BraidedMonoidalCategories.vo
  • 53 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Modifications/Examples/Unitality.vo
  • 53 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/ContravariantFunctor.glob
  • 53 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/ElementsOp.vo
  • 53 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/DisplayedCatToBicat.glob
  • 53 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/DecidablePropositions.glob
  • 53 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/binproducts.glob
  • 53 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Transformations/Examples/Unitality.glob
  • 52 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/MoreLists.glob
  • 52 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/RealNumbers/NonnegativeRationals.v
  • 52 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/TransportMorphisms.glob
  • 52 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/Vectors.glob
  • 51 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/FixedPointTheorems.v
  • 51 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal/HVectors.glob
  • 51 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/ConstructiveStructures.vo
  • 51 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Cats.vo
  • 50 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/category_binops.vo
  • 50 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/BindingSigToMonad.vo
  • 50 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/MoreEquivalences.glob
  • 50 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Bicat.v
  • 50 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/PointedGroupoid.glob
  • 50 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/DisplayedInserter.v
  • 50 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/opp_precat.vo
  • 49 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Invertible_2cells.vo
  • 49 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/CCS.glob
  • 49 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/SumOfSignatures.vo
  • 49 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Examples/PseudofunctorFromMonoidal.glob
  • 49 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/MonoidalFunctors.glob
  • 49 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Inductives/LambdaCalculus.glob
  • 49 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Transformations/Examples/ApTransformation.vo
  • 49 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Adjunctions/Examples.glob
  • 49 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/PointedFunctorsMonoidal.glob
  • 49 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/SkewMonoidal/SkewMonoidalCategories.glob
  • 48 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/CommaCategories.vo
  • 48 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/SkewMonoidal/CategoriesOfMonoids.vo
  • 48 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/Sets.glob
  • 48 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/BindingSigToMonad.glob
  • 48 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/CommaCategories.glob
  • 48 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/KATriangulated.glob
  • 48 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/LamFromBindingSig.glob
  • 47 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/RepresentableFunctors/Test.glob
  • 47 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Inductives/Trees.glob
  • 47 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Modifications/Modification.glob
  • 47 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Examples/StrictCats.vo
  • 47 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Apartness.glob
  • 47 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/WkCatEnrichment/Cat.glob
  • 47 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/cones.glob
  • 46 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Groups.v
  • 46 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/GenMendlerIteration.vo
  • 46 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/DispBicatOfDispCats.glob
  • 46 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Foundations/UnivalenceAxiom.vo
  • 46 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/FunctorCategory.glob
  • 46 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/pullbacks_slice_products_equiv.glob
  • 45 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/Vectors.vo
  • 45 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Subcategory/Full.glob
  • 45 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/Propositions.vo
  • 45 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal/HVectors.vo
  • 45 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Examples/OneTypes.vo
  • 45 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/DispBiequivalence.glob
  • 45 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Adjunctions.glob
  • 45 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Transformations/Examples/Whiskering.glob
  • 45 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/SliceFamEquiv.glob
  • 44 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Domains_and_Fields.v
  • 44 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/DivisionRig.glob
  • 44 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/EndofunctorsMonoidal.vo
  • 44 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/PreAdditive.v
  • 44 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/flds.vo
  • 44 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/NumberSystems/NaturalNumbersAlgebra.glob
  • 44 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/AbelianPushoutPullback.vo
  • 44 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Topology/Prelim.glob
  • 44 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/Limits.glob
  • 44 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/All.vo
  • 43 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Subcategory/Full.vo
  • 43 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Foundations/PartC.v
  • 43 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Modules/Quotient.glob
  • 43 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/ShortExactSequences.v
  • 43 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Folds/folds_precat.glob
  • 43 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/DecidablePropositions.vo
  • 43 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Examples/Strictify.v
  • 42 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/pullbacks.v
  • 42 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/RelativeMonads.v
  • 42 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/zero.glob
  • 42 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Induction/W/Naturals.glob
  • 42 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Adjunctions.vo
  • 42 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/SplitMonicsAndEpis.glob
  • 42 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/BinProductOfSignatures.glob
  • 42 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Modules/Multimodules.glob
  • 41 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/MappingCylinder.v
  • 41 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Matrix.glob
  • 41 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Tactics/Abmonoids_Tactics.vo
  • 41 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Profunctors/Core.vo
  • 41 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Enriched/Enriched.glob
  • 41 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Inductives/Trees.vo
  • 41 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/DispModification.glob
  • 41 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Transformations/Examples/Associativity.glob
  • 41 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/intdoms.vo
  • 41 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/rezk_completion.glob
  • 40 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/NumberSystems/Tests.glob
  • 40 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/CartesianCubicalSets.vo
  • 40 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/exponentials.vo
  • 40 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Examples/OpCellBicat.glob
  • 40 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Chains/Adamek.vo
  • 40 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Modifications/Examples/Associativity.vo
  • 40 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Foundations/PartB.v
  • 40 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/exponentials.glob
  • 40 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/UnitalBinop.glob
  • 40 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/Colimits.vo
  • 40 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/ActionBasedStrengthOnHomsInBicat.v
  • 40 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/MoreEquivalences.vo
  • 40 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/initial.vo
  • 40 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/eqdiag.vo
  • 39 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/whiskering.glob
  • 39 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/TransportLaws.glob
  • 39 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/SkewMonoidal/CategoriesOfMonoids.glob
  • 39 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Inductives/PropositionalLogic.vo
  • 39 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Groupoids.glob
  • 39 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Constructions.v
  • 39 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/RealNumbers/Sets.vo
  • 39 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/FullSub.glob
  • 39 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/RepresentableFunctors/Representation.v
  • 39 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/terminal.vo
  • 39 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Topology/Filters.v
  • 39 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Universal_Algebra/Algebras.vo
  • 39 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Examples/TwoType.vo
  • 39 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Induction/W/Fibered.vo
  • 38 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Equivalences_bis.v
  • 38 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Profunctors/Core.glob
  • 38 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/Add2Cell.glob
  • 38 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Examples/Composition.glob
  • 38 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/monoids.glob
  • 38 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/MLTT79.vo
  • 38 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Induction/W/Uniqueness.vo
  • 38 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/limits.v
  • 37 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Modules/Multimodules.vo
  • 37 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Foundations/PartD.v
  • 37 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/ActionOfEndomorphismsInBicat.vo
  • 37 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Display/StrictIdentitor.glob
  • 37 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Adjunctions/Core.v
  • 37 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Algebras.vo
  • 37 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/Sigma.v
  • 37 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/Algebras.v
  • 37 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/BinSumOfSignatures.glob
  • 37 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/commrings.vo
  • 37 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/CategoriesOfMonoids.glob
  • 37 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Auxiliary.glob
  • 37 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Equivalences.v
  • 37 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/Categories.vo
  • 37 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/BinDirectSums.v
  • 36 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/FinOrdProducts.glob
  • 36 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/precomp_fully_faithful.glob
  • 36 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/GrothendieckTopos.vo
  • 36 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Examples/OpMorBicat.glob
  • 36 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/FinOrdCoproducts.glob
  • 36 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/FromBindingSigsToMonads_Summary.vo
  • 36 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/RealNumbers/DedekindCuts.vo
  • 36 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/DispBuilders.glob
  • 36 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Tactics/Nat_Tactics.v
  • 36 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Paradoxes/GirardsParadox.glob
  • 35 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Modules/Submodule.vo
  • 35 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Folds/from_precats_to_folds_and_back.glob
  • 35 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monics.vo
  • 35 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Induction/M/Limits.glob
  • 35 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Topology/Topology.v
  • 35 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Induction/M/Uniqueness.vo
  • 35 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/bincoproducts.v
  • 35 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/CategoryEquality.glob
  • 35 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Codomain.vo
  • 35 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/ExactCategories/Tests.vo
  • 35 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/zero.vo
  • 35 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/grs.vo
  • 35 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Folds/from_precats_to_folds_and_back.vo
  • 35 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/Colimits.glob
  • 35 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/slicecat.v
  • 35 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/SetValuedFunctors.vo
  • 35 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/Univalence.vo
  • 34 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/zero.glob
  • 34 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/abmonoids.vo
  • 34 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Equivalences/FullyFaithful.glob
  • 34 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/Trivial.glob
  • 34 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/commrigs.vo
  • 34 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/binproducts.vo
  • 34 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Representable.glob
  • 34 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/STLC.glob
  • 34 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/AbelianToAdditive.v
  • 34 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/All.vo
  • 34 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/PrecategoriesWithAbgrops.vo
  • 34 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Topology/Prelim.vo
  • 34 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Examples/Tests.glob
  • 34 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Subobjects.vo
  • 33 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Projection.glob
  • 33 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Transformations/Examples/AlgebraMap.vo
  • 33 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/rings.vo
  • 33 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Chains/Chains.vo
  • 33 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/Functors.v
  • 33 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/Sets.vo
  • 33 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal/VTerms.vo
  • 33 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/initial.vo
  • 33 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/Prod.v
  • 32 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/StandardCategories.glob
  • 32 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Display/Identitor.glob
  • 32 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/PAdics/lemmas.v
  • 32 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/KAPreTriangulated.v
  • 32 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/RepresentableFunctors/Test.vo
  • 32 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Examples/PointedOneTypesBicat.glob
  • 32 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/Subtypes.glob
  • 32 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Terms.v
  • 32 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Equivalences/FullyFaithful.vo
  • 32 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Examples/Tests.vo
  • 31 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Adjunctions/Restriction.glob
  • 31 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Subcategory/Core.glob
  • 31 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/UnderCategories.glob
  • 31 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/Displayed2Inserter.glob
  • 31 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Cats.glob
  • 31 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Foundations/Tests.glob
  • 31 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Modifications/Examples/Unitality.glob
  • 31 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/WkCatEnrichment/internal_equivalence.glob
  • 31 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/modules.glob
  • 31 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/rigs.vo
  • 31 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Examples/Final.vo
  • 30 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/Subtypes.vo
  • 30 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Examples/StrictToPseudo.glob
  • 30 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/YonedaBinproducts.vo
  • 30 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Examples/ListDataType.vo
  • 30 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/SumOfSignatures.glob
  • 30 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Examples/StrictCats.glob
  • 30 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/rezk_completion.vo
  • 30 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Subcategory/Core.vo
  • 30 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/LiftingInitial.v
  • 30 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/MultiSorted.v
  • 30 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Examples/Initial.vo
  • 30 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/Univalence.glob
  • 30 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Examples/RestrictImage.glob
  • 30 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/Isos.v
  • 30 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Examples/Projection.vo
  • 30 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/DispInvertibles.v
  • 30 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/category_binops.glob
  • 30 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/wosets.vo
  • 29 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Examples/ApFunctor.vo
  • 29 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Ktheory/GrothendieckGroup.glob
  • 29 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/setwith2binops.vo
  • 29 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monics.glob
  • 29 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Subcategory/Limits.glob
  • 29 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Examples/BicatOfCatsWithoutUnivalence.vo
  • 29 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Unitors.glob
  • 29 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/NumberSystems/RationalNumbers.v
  • 29 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/ZFstructures.v
  • 29 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/setwith2binops.glob
  • 29 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Fibrations.v
  • 29 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/EpiFacts.glob
  • 29 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Archimedean.v
  • 29 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/SubstitutionSystems_Summary.vo
  • 29 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/RepresentableFunctors/RawMatrix.glob
  • 29 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Subobjects.glob
  • 28 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/HorizontalComposition.glob
  • 28 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/RepresentableFunctors/DirectSum.vo
  • 28 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/terminal.vo
  • 28 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/NumberSystems/NaturalNumbers_le_Inductive.glob
  • 28 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Free_Monoids_and_Groups.v
  • 28 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Chains/Adamek.glob
  • 28 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/ProductCategory.vo
  • 28 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/CategoricalRecursionSchemes.v
  • 28 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Elements.glob
  • 28 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/Slice.glob
  • 28 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/AdditiveFunctors.v
  • 28 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Tactics/Abmonoids_Tactics.glob
  • 28 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Examples/OneTypes.glob
  • 28 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/DispAdjunctions.v
  • 27 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/zero.vo
  • 27 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/FiveLemma.v
  • 27 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Modules/Submodule.glob
  • 27 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Epis.glob
  • 27 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/RigsAndRings/Ideals.vo
  • 27 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/EndofunctorsMonoidal.glob
  • 27 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/YonedaLemma.v
  • 27 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/DispBiadjunction.glob
  • 27 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/PartA.v
  • 27 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/GrothendieckTopos.glob
  • 27 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Yoneda.glob
  • 27 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/precomp_ess_surj.v
  • 27 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Display/Map2Cells.glob
  • 27 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Modules/Core.v
  • 27 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/MonadKtripleBiequiv.v
  • 27 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/commrings.glob
  • 27 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/SetValuedFunctors.glob
  • 27 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/FunctorCoalgebras.glob
  • 26 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Folds/folds_precat.vo
  • 26 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/commrigs.glob
  • 26 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/abmonoids.glob
  • 26 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/intdoms.glob
  • 26 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/ProductCategory.glob
  • 26 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Elements.vo
  • 26 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/KleisliCategory.glob
  • 26 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/LiftingInitial_alt.v
  • 26 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Modifications/Examples/ApModification.vo
  • 26 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/rings.glob
  • 26 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/flds.glob
  • 26 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Strictness.v
  • 26 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Examples/TwoType.glob
  • 26 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/rigs.glob
  • 26 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/RepresentableFunctors/DirectSum.glob
  • 25 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Induction/W/Fibered.glob
  • 25 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/Kleisli.glob
  • 25 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/NumberSystems/Tests.vo
  • 25 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/FiniteSequences.v
  • 25 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/DispTransformation.v
  • 25 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Discreteness.glob
  • 25 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/HorizontalComposition.vo
  • 25 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/RigsAndRings/Ideals.glob
  • 25 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/UnivalenceOp.vo
  • 25 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/UnderCategories.vo
  • 25 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/grs.glob
  • 25 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/ComprehensionC.glob
  • 25 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/PseudoElements.v
  • 25 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/Univalence.vo
  • 25 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Apartness.vo
  • 25 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/GroupAction.v
  • 25 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SyntheticHomotopyTheory/AffineLine.v
  • 25 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/BicategoryOfBicat.glob
  • 25 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/AlgebraicGeometry/Spec.glob
  • 25 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Epis.vo
  • 25 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal/FreeAlgebras.vo
  • 25 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Codomain.glob
  • 25 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Algebras.glob
  • 24 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Examples/PathGroupoid.v
  • 24 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/Derivative.v
  • 24 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/OrderedSets.v
  • 24 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/SplitMonicsAndEpis.vo
  • 24 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/NumberSystems/NaturalNumbers_le_Inductive.vo
  • 24 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/PointedFunctors.vo
  • 24 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Modules/Examples.glob
  • 24 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/PointedOneTypes.glob
  • 24 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Lattice.v
  • 24 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Examples/Identity.vo
  • 24 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/BicatOfBicategory.glob
  • 24 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Examples/Constant.vo
  • 24 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Universal_Algebra/Algebras.glob
  • 24 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Examples/Bool.vo
  • 24 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Foundations/Propositions.v
  • 24 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Examples/Groupoids.vo
  • 23 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/KA.v
  • 23 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/MonoEpiIso.glob
  • 23 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Foundations/Preamble.vo
  • 23 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/colimits.v
  • 23 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/WeakEquivalences.glob
  • 23 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/Monads.v
  • 23 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/LamHSET.vo
  • 23 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/AxiomOfChoice.vo
  • 23 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/DivisionRig.vo
  • 23 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/Cofunctormap.glob
  • 23 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/DispPseudofunctor.v
  • 23 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Fibration.vo
  • 23 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/binproducts.v
  • 23 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/Graph.glob
  • 22 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/SubobjectClassifier.vo
  • 22 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/MonadsFromSubstitutionSystems.v
  • 22 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/whiskering.vo
  • 22 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Display/Map1Cells.v
  • 21 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Chains/Chains.glob
  • 21 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/All.vo
  • 21 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/Opp.v
  • 21 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Induction/W/Uniqueness.glob
  • 21 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Induction/M/Uniqueness.glob
  • 21 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/SimplicialSets.vo
  • 21 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/PrecategoryBinProduct.v
  • 21 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/coslicecat.vo
  • 21 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/MLTT79.glob
  • 21 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SyntheticHomotopyTheory/Test.glob
  • 21 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/PathsOver.v
  • 21 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Chains/Cochains.vo
  • 21 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/MetricTree.vo
  • 21 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/CartesianCubicalSets.glob
  • 21 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Inductives/Lists.v
  • 21 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/SignatureExamples.v
  • 21 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/GraphPaths.glob
  • 21 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/PAdics/frac.v
  • 20 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/AdjointUnique.v
  • 20 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/terminal.glob
  • 20 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/cokernels.v
  • 20 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Examples/BicatOfCatsWithoutUnivalence.glob
  • 20 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/NoInjectivePairing.vo
  • 20 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/initial.glob
  • 20 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/kernels.v
  • 20 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Paradoxes/GirardsParadox.vo
  • 20 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Dcpo.v
  • 20 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Unitors.vo
  • 20 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Topology/CategoryTop.vo
  • 20 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Type/Structures.vo
  • 20 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/MetricTree.glob
  • 20 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal/VTerms.glob
  • 20 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/ModulesFromSignatures.v
  • 20 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/PartD.vo
  • 20 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/initial.glob
  • 20 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/Sub1Cell.vo
  • 20 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/RealNumbers/Prelim.glob
  • 20 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Examples/Image.vo
  • 20 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SyntheticHomotopyTheory/Halfline.vo
  • 20 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Foundations/HLevels.glob
  • 19 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/IteratedBinaryOperations.v
  • 19 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Equivalences/Core.v
  • 19 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/TransportMorphisms.vo
  • 19 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/RepresentableFunctors/RawMatrix.vo
  • 19 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/KTriplesEquiv.v
  • 19 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/SubstitutionSystems.v
  • 19 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/Structures.v
  • 19 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Examples/Bool.glob
  • 19 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/cokernels.glob
  • 19 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/Tests.v
  • 19 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Examples/Nat.vo
  • 19 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/ConstructiveStructures.v
  • 19 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/terminal.glob
  • 19 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Modifications/Examples/Associativity.glob
  • 18 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Univalence.v
  • 18 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Examples/BicatOfCats.v
  • 18 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/pushouts.v
  • 18 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Additive.v
  • 18 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/RealNumbers/DedekindCuts.v
  • 18 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/RepresentableFunctors/Precategories.v
  • 18 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples.v
  • 18 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/FunctorAlgebras.v
  • 18 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/BraidedMonoidalCategories.glob
  • 18 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/kernels.glob
  • 18 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/UnitorsAndAssociatorsForEndofunctors.vo
  • 18 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/kernels.vo
  • 18 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/PointedFunctors.glob
  • 18 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/StructureIdentity.vo
  • 18 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Type/Core.vo
  • 18 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/MonadsMultiSorted.v
  • 18 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Folds/folds_isomorphism.v
  • 18 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/LamSignature.v
  • 18 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Foundations/UnivalenceAxiom.v
  • 18 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/SubobjectClassifier.glob
  • 18 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Examples/Initial.glob
  • 17 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/FiniteSets.v
  • 17 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/BoundedSearch.glob
  • 17 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/MonoEpiIso.vo
  • 17 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SyntheticHomotopyTheory/Circle2.v
  • 17 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/Signatures.v
  • 17 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Examples/Group.vo
  • 17 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/AbelianPushoutPullback.v
  • 17 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/SIP.vo
  • 17 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/AxiomOfChoice.glob
  • 17 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/FromBindingSigsToMonads_Summary.v
  • 17 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/pullbacks.v
  • 17 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/Lam.v
  • 17 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/Monads.v
  • 17 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/elems_slice_equiv.v
  • 17 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SyntheticHomotopyTheory/Halfline.glob
  • 17 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/ActionOfEndomorphismsInBicat.glob
  • 17 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Limits.glob
  • 16 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal/FreeAlgebras.glob
  • 16 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/SignatureCategory.v
  • 16 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Examples/Monoid.vo
  • 16 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/cokernels.vo
  • 16 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Induction/ImpredicativeInductiveSets.v
  • 16 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/UnitorsAndAssociatorsForEndofunctors.glob
  • 16 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/catiso.v
  • 16 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/covyoneda.glob
  • 16 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/NoInjectivePairing.glob
  • 16 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/UnivalenceOp.glob
  • 16 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/QuotientSet.glob
  • 16 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/preorder_categories.vo
  • 16 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/ActionBasedStrength.v
  • 16 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Type/MonoEpiIso.vo
  • 16 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/Graph.vo
  • 16 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Foundations/Init.vo
  • 15 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Examples/OpFunctor.glob
  • 15 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/wosets.glob
  • 15 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/RealNumbers/Prelim.vo
  • 15 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Universal_Algebra/EqAlgebras.vo
  • 15 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/BoundedSearch.vo
  • 15 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/covyoneda.vo
  • 15 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/LModules.v
  • 15 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/FunctorCategory.v
  • 15 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Induction/PolynomialFunctors.vo
  • 15 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/ArrowCategory.glob
  • 15 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/CwF.v
  • 15 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/Actions.v
  • 15 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/Equivalences.v
  • 15 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/DispDepProd.v
  • 15 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/Nat.v
  • 15 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Examples/Monoid.glob
  • 15 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Induction/M/Chains.v
  • 15 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SyntheticHomotopyTheory/Test.vo
  • 14 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Examples/Final.glob
  • 14 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Colimits/Initial.v
  • 14 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Biadjunction.v
  • 14 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/StrictPseudoFunctor.v
  • 14 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/pushouts.v
  • 14 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Folds/folds_pre_2_cat.v
  • 14 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/All.vo
  • 14 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/FinSet.vo
  • 14 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/KTriples.v
  • 14 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/cats/limits.v
  • 14 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/NNO.vo
  • 14 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/NullHomotopies.glob
  • 14 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/NullHomotopies.vo
  • 14 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal/SortedTypes.glob
  • 14 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/YonedaBinproducts.glob
  • 14 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/GraphPaths.vo
  • 14 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/KleisliTriple.v
  • 14 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Foundations/Tests.vo
  • 14 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/RelativeModules.v
  • 13 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/WkCatEnrichment/whiskering.v
  • 13 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Induction/All.vo
  • 13 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Transformations/Examples/ApTransformation.glob
  • 13 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Fibration.glob
  • 13 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Colimits/Final.v
  • 13 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/BicategoryLaws.v
  • 13 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/All.glob
  • 13 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/preorder_categories.glob
  • 13 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/DecidablePropositions.v
  • 13 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/All.vo
  • 13 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Chains/All.vo
  • 13 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/Notations.vo
  • 13 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/coequalizers.v
  • 13 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/covyoneda.v
  • 13 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/PointedGroupoid.v
  • 13 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Induction/M/Core.vo
  • 13 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Presheaf.v
  • 13 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Tactics/Monoids_Tactics.vo
  • 13 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/LatticeObject.v
  • 13 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Induction/W/Core.vo
  • 13 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/WkCatEnrichment/prebicategory.v
  • 13 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Subcategory/Reflective.vo
  • 13 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/PseudoFunctor.v
  • 13 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/WkCatEnrichment/bicategory.vo
  • 13 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/BindingSigToMonad.v
  • 12 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/Propositions.v
  • 12 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/Notation.vo
  • 12 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal/TermAlgebras.vo
  • 12 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/NegativePropositions.v
  • 12 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/VectorsTests.vo
  • 12 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/WkCatEnrichment/Cat.v
  • 12 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/WeakEquivalences.vo
  • 12 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/NaturalTransformations.v
  • 12 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Type/Univalence.vo
  • 12 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SyntheticHomotopyTheory/Circle.v
  • 12 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/FiberCategory.v
  • 12 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Subcategory/Full.v
  • 12 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/All.v
  • 12 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Quotobjects.vo
  • 12 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/RealNumbers/Sets.v
  • 12 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Foundations/HLevels.vo
  • 12 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/FiberBicategory.vo
  • 12 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/coproducts.v
  • 12 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal/SortedTypes.vo
  • 12 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/TwoCategories.v
  • 12 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/yoneda.v
  • 12 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/NNO.glob
  • 12 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Transformations/Examples/AlgebraMap.glob
  • 12 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/DispBicatOfDispCats.v
  • 12 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/Sub1Cell.glob
  • 12 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Tactics/Abmonoids_Tactics.v
  • 12 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/equalizers.v
  • 12 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Type/MonoEpiIso.glob
  • 12 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/EquivToAdjequiv.v
  • 12 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/All.vo
  • 11 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/MonadAlgebras.v
  • 11 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/coslicecat.glob
  • 11 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/SubstitutionSystems_Summary.v
  • 11 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Examples/BicategoryFromMonoidal.v
  • 11 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/MoreLists.v
  • 11 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/ExponentiationLeftAdjoint.v
  • 11 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/WkCatEnrichment/Notations.vo
  • 11 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Ktheory/All.vo
  • 11 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/UnitalBinop.v
  • 11 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/ConstructionOfActions.v
  • 11 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/MonoidalCategories.v
  • 11 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/equalizers.v
  • 11 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Tests.glob
  • 11 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Adjunctions.v
  • 11 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/SIP.glob
  • 11 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/products.v
  • 11 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/PointedFunctorsMonoidal.v
  • 11 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/Limits.v
  • 11 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Chains/Cochains.glob
  • 11 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Examples/Group.glob
  • 11 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Topology/All.vo
  • 11 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/bincoproducts.v
  • 11 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Biequivalence.v
  • 11 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Foundations/UnivalenceAxiom2.vo
  • 11 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Morphisms.v
  • 11 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/RepresentableFunctors/Bifunctor.v
  • 11 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Type/Limits.vo
  • 11 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Type/Colimits.vo
  • 11 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/QuotientSet.vo
  • 11 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/SimplicialSets.glob
  • 11 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/RealNumbers/DecidableDedekindCuts.vo
  • 11 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/AlternativeProofs.vo
  • 11 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/ContravariantFunctor.v
  • 10 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/ExactCategories/Tests.v
  • 10 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/EssentiallyAlgebraic.glob
  • 10 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/CCS.v
  • 10 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Transformations/PseudoTransformation.v
  • 10 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/DispToFiberEquivalence.v
  • 10 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal/HVectors.v
  • 10 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Adjunctions/Examples.v
  • 10 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/CategoriesWithBinOps.vo
  • 10 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Inductives/LambdaCalculus.v
  • 10 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Display/Base.v
  • 10 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/Categories.v
  • 10 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Matrix.v
  • 10 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/Univalence.vo
  • 10 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/VectorsTests.glob
  • 10 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Display/StrictCompositor.v
  • 10 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/eqdiag.v
  • 10 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/Notations.glob
  • 10 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Induction/M/ComputationalM.v
  • 10 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Examples/Constant.glob
  • 10 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/monoids.v
  • 10 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Foundations/Preamble.glob
  • 10 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/DispBiequivalence.v
  • 10 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Invertible_2cells.v
  • 10 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/PrecategoriesWithAbgrops.v
  • 10 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/FullSub.v
  • 10 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/Setcategories.vo
  • 10 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/PartD.glob
  • 10 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Examples/ApFunctor.glob
  • 10 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/KATriangulated.v
  • 10 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Modifications/Examples/ApModification.glob
  • 10 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Auxiliary.v
  • 9 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Cats.v
  • 9 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Groupoids.v
  • 9 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/StandardCategories.v
  • 9 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/LamFromBindingSig.v
  • 9 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Examples/OpCellBicat.v
  • 9 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/opp_precat.v
  • 9 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Induction/W/Naturals.v
  • 9 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/DisplayedCatToBicat.v
  • 9 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/GenMendlerIteration_alt.v
  • 9 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/WellFoundedRelations.v
  • 9 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/HLevel.glob
  • 9 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/Lists.v
  • 9 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/RelMonads_Coreflection.v
  • 9 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Display/Compositor.v
  • 9 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Examples/ListDataType.glob
  • 9 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/zero.v
  • 9 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Graph.vo
  • 9 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Inductives/PropositionalLogic.v
  • 9 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Signatures.vo
  • 9 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Graph.glob
  • 9 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Signatures.glob
  • 9 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/GenMendlerIteration.v
  • 9 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/DispUnivalence.v
  • 9 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/CommaCategories.v
  • 9 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/EssentiallyAlgebraic.vo
  • 9 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/Equivalence_Relations.vo
  • 9 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/Tactics.vo
  • 9 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/RealNumbers/Fields.vo
  • 9 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/LamHSET.glob
  • 9 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Examples/Nat.glob
  • 9 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Examples/Projection.glob
  • 9 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Type/Core.glob
  • 9 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/SplitMonicsAndEpis.v
  • 9 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Transformations/Examples/Unitality.v
  • 9 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/MonoidalFunctors.v
  • 9 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/SliceFamEquiv.v
  • 9 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/Colimits.v
  • 9 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Projection.v
  • 9 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/NumberSystems/NaturalNumbersAlgebra.v
  • 9 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Topology/Prelim.v
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Subcategory/Limits.v
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/PointedFunctorsComposition.vo
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Modifications/Modification.v
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/Core.vo
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Representable.v
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Equivalences/CompositesAndInverses.v
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Subcategory/Core.v
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Modules/Quotient.v
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Display/PseudoFunctorBicat.v
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Apartness.v
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/FunctorCategory.v
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/cones.v
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/ActionBasedStrongFunctorCategory.v
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal/EqAlgebras.vo
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/coequalizers.v
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/Slice.v
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Tests.vo
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Enriched/Enriched.v
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/Vectors.v
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/Cofunctormap.v
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Display/StrictPseudoFunctorBicat.v
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal/TermAlgebras.glob
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Equations.vo
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Equations.glob
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/modules.v
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/MLTT79.v
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/Univalence.v
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/All.glob
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Induction/PolynomialFunctors.glob
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/pullbacks_slice_products_equiv.v
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Examples/OpMorBicat.v
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/Setcategories.glob
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Transformations/Examples/Associativity.v
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/GrothendieckTopos.v
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/BinSumOfSignatures.v
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Modules/Multimodules.v
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/DispModification.v
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Folds/from_precats_to_folds_and_back.v
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Yoneda.v
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Inductives/Trees.v
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/RightKanExtension.v
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/FinOrdCoproducts.v
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/StructureIdentity.glob
  • 8 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Adjunctions/Restriction.v
  • 7 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/Subposets.vo
  • 7 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/STLC.v
  • 7 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/FinOrdProducts.v
  • 7 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/NumberSystems/Tests.v
  • 7 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/rezk_completion.v
  • 7 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Profunctors/Core.v
  • 7 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Foundations/Init.v
  • 7 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Examples/PseudofunctorFromMonoidal.v
  • 7 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Examples/StrictCats.v
  • 7 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/All.v
  • 7 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/Sets.v
  • 7 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Examples/Identity.glob
  • 7 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/DispBiadjunction.v
  • 7 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/wosets.v
  • 7 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Transformations/Examples/Whiskering.v
  • 7 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/BinProductOfSignatures.v
  • 7 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/ElementsOp.v
  • 7 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Induction/M/Limits.v
  • 7 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/Add2Cell.v
  • 7 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/RealNumbers/DecidableDedekindCuts.glob
  • 7 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Tactics/Groups_Tactics.vo
  • 7 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Modifications/Examples/Unitality.v
  • 7 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Adjunctions.v
  • 7 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/category_binops.v
  • 7 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/MoreEquivalences.v
  • 7 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Examples/Groupoids.glob
  • 7 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/setwith2binops.v
  • 7 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Examples/StrictToPseudo.v
  • 7 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/SetValuedFunctors.v
  • 7 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/DivisionRig.v
  • 7 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/KleisliCategory.v
  • 7 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/whiskering.v
  • 7 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/BicatOfBicategory.v
  • 7 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/Interval.vo
  • 7 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/precomp_fully_faithful.v
  • 7 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Type/Structures.glob
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/Maybe.glob
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Chains/Adamek.v
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/CategoryEquality.v
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/Interval.glob
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/RepresentableFunctors/Test.v
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SyntheticHomotopyTheory/All.vo
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Paradoxes/GirardsParadox.v
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Subobjects.v
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/exponentials.v
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/EpiFacts.v
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Examples/Tests.v
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/abmonoids.v
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/Subtypes.v
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/Univalence.glob
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/RealNumbers/All.vo
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/CategoriesWithBinOps.glob
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Examples/RestrictImage.v
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/commrings.v
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Examples/OneTypes.v
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/TransportLaws.v
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/commrigs.v
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Induction/W/Fibered.v
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Induction/M/Core.glob
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Equivalences/FullyFaithful.v
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Discreteness.v
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/intdoms.v
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Induction/W/Core.glob
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/CartesianCubicalSets.v
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/ProductCategory.v
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Folds/folds_precat.v
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monics.v
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/Core.glob
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/All.vo
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/zero.v
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/AxiomOfChoice.v
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/rings.v
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/terminal.v
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/binproducts.v
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Subcategory/Reflective.glob
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/flds.v
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Unitors.v
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/Trivial.v
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/rigs.v
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/grs.v
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Tactics/Utilities.vo
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Universal_Algebra/Algebras.v
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Display/StrictIdentitor.v
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/All.vo
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/initial.v
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/Subposets.glob
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/FunctorCoalgebras.v
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Examples/PointedOneTypesBicat.v
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/SkewMonoidal/SkewMonoidalCategories.v
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/SkewMonoidal/CategoriesOfMonoids.v
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/Displayed2Inserter.v
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Epis.v
  • 6 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/TransportMorphisms.v
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Modules/Examples.v
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/DispBuilders.v
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/MonoEpiIso.v
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Foundations/UnivalenceAxiom2.glob
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Foundations/Preamble.v
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/PAdics/All.vo
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Examples/Image.glob
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Examples/TwoType.v
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/ComprehensionC.v
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/AlgebraicGeometry/Spec.v
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/RigsAndRings/Ideals.v
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal/EqAlgebras.glob
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Codomain.v
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/NumberSystems/All.vo
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/DoubleNegation.vo
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/Maybe.vo
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/Equivalence_Relations.glob
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/UnderCategories.v
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/SumOfSignatures.v
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Quotobjects.glob
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Modules/Submodule.v
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Foundations/HLevels.v
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/BicategoryOfBicat.v
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Induction/M/Uniqueness.v
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/Tactics.glob
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Algebras.v
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/AlgebraicGeometry/All.vo
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/CategoriesOfMonoids.v
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/UnitorsAndAssociatorsForEndofunctors.v
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Type/Univalence.glob
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/initial.v
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/UnivalenceOp.v
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Display/Identitor.v
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/NumberSystems/NaturalNumbers_le_Inductive.v
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/WkCatEnrichment/internal_equivalence.v
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/EndofunctorsMonoidal.v
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Elements.v
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Modifications/Examples/Associativity.v
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Induction/W/Uniqueness.v
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/ActionOfEndomorphismsInBicat.v
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monads/Kleisli.v
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/terminal.v
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Ktheory/GrothendieckGroup.v
  • 5 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Examples/Composition.v
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Chains/Chains.v
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/HorizontalComposition.v
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Examples/BicatOfCatsWithoutUnivalence.v
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Topology/CategoryTop.glob
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Display/Map2Cells.v
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/PointedOneTypes.v
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/Univalence.v
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/AlternativeProofs.glob
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Universal_Algebra/EqAlgebras.glob
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/RealNumbers/Fields.glob
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Tactics/Monoids_Tactics.v
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal.vo
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/DoubleNegation.glob
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/Test.vo
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Examples/Bool.v
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/MetricTree.v
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Examples/HLevel.v
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/RepresentableFunctors/DirectSum.v
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/Graph.v
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Tactics/All.vo
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/Test.glob
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Examples/Final.v
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Examples/OpFunctor.v
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Foundations/Tests.v
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/ArrowCategory.v
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/cokernels.v
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Tactics/Monoids_Tactics.glob
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/FinSet.glob
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/RealNumbers/Prelim.v
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal/VTerms.v
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/BoundedSearch.v
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/YonedaBinproducts.v
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/Limits.v
  • 4 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/PointedFunctors.v
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/limits/graphs/kernels.v
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/LamHSET.v
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Folds/All.vo
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/Prelude.vo
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal/SortedTypes.v
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Modules.vo
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/SubobjectClassifier.v
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/NoInjectivePairing.v
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Transformations/Examples/AlgebraMap.v
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/RepresentableFunctors/RawMatrix.v
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Type/MonoEpiIso.v
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/WkCatEnrichment/bicategory.glob
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Examples/Monoid.v
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/WeakEquivalences.v
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/preorder_categories.v
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal/FreeAlgebras.v
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Examples/Initial.v
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Universal_Algebra/EqAlgebras.v
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SyntheticHomotopyTheory/Halfline.v
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Graph.v
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/Bool.vo
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/GraphPaths.v
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/coslicecat.v
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/Notations.v
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SyntheticHomotopyTheory/Test.v
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/Notation.glob
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/Tactics.v
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Examples/Sub1Cell.v
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Transformations/Examples/ApTransformation.v
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/Fibration.v
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/FinSet.v
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Examples/Group.v
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Tactics/Utilities.glob
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Tactics/Groups_Tactics.v
  • 3 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/SimplicialSets.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Monoidal/BraidedMonoidalCategories.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Type/Limits.glob
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Signatures.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Chains/Cochains.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Examples/Constant.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Examples/Projection.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Examples/ApFunctor.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Induction/PolynomialFunctors.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Type/Colimits.glob
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Type/Core.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/NullHomotopies.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/DecSet.vo
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Foundations/All.vo
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Type/Structures.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Examples/Image.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Modifications/Examples/ApModification.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/QuotientSet.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Paradoxes/All.vo
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/Core/Examples/Groupoids.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/Notation.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/EssentiallyAlgebraic.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Tactics/Groups_Tactics.glob
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/All.glob
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Examples/Nat.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/DisplayedCats/SIP.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/Core.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/StructureIdentity.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/All.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Examples/ListDataType.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Tests.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/PseudoFunctors/Examples/Identity.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Subcategory/Reflective.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Foundations/UnivalenceAxiom2.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/Univalence.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Tactics/Utilities.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal/Equations.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/Setcategories.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/Subposets.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Induction/M/Core.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/PartD.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/CategoriesWithBinOps.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/RealNumbers/DecidableDedekindCuts.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/All.glob
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Induction/W/Core.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/PointedFunctorsComposition.glob
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Folds/UnicodeNotations.vo
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SubstitutionSystems/All.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal/TermAlgebras.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Topology/CategoryTop.v
  • 2 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Quotobjects.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/VectorsTests.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/All.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/DecSet.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/All.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/Bool.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Type/Univalence.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/NNO.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/WkCatEnrichment/Notations.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/Interval.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/WkCatEnrichment/bicategory.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/Maybe.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal/EqAlgebras.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/Equivalence_Relations.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Type/Colimits.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/Type/Limits.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/RealNumbers/Fields.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/DoubleNegation.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/WkCatEnrichment/Notations.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/All.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/All.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/PointedFunctorsComposition.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/All.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Foundations/Init.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/All.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/Test.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/AlternativeProofs.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Folds/UnicodeNotations.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Foundations/All.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Induction/All.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/All.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Foundations/All.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Combinatorics/DecSet.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Induction/All.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/HomologicalAlgebra/All.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/Prelude.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/All.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Folds/aux_lemmas.vo
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/RealNumbers/All.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/categories/HSET/All.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/RealNumbers/All.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/MoreFoundations/Bool.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/FiberBicategory.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Core/Prelude.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Folds/All.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Folds/All.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SyntheticHomotopyTheory/All.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Chains/All.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/NumberSystems/All.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Tactics/All.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Tactics/All.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/SyntheticHomotopyTheory/All.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/NumberSystems/All.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Bicategories/DisplayedBicats/FiberBicategory.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/PAdics/All.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/PAdics/All.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Topology/All.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/CategoryTheory/Chains/All.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Topology/All.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Folds/UnicodeNotations.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/AlgebraicGeometry/All.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Universal.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Paradoxes/All.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Ktheory/All.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Modules.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Ktheory/All.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Paradoxes/All.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/AlgebraicGeometry/All.v
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Folds/aux_lemmas.glob
  • 1 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Algebra/Modules.v
  • 0 K ../ocaml-base-compiler.4.12.0/lib/coq/user-contrib/UniMath/Folds/aux_lemmas.v

Uninstall

Command
opam remove -y coq-unimath.20210807
Return code
0
Missing removes
none
Wrong removes
none