« Up

category-theory 1.0.0 29 m 0 s 🏆

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              4           Virtual package relying on a GMP lib system installation
coq                   8.16.0      Formal proof management system
dune                  3.13.0      Fast, portable, and opinionated build system
ocaml                 4.13.1      The OCaml compiler (virtual package)
ocaml-base-compiler   4.13.1      Official release 4.13.1
ocaml-config          2           OCaml Switch Configuration
ocaml-options-vanilla 1           Ensure that OCaml is compiled with no special options enabled
ocamlfind             1.9.6       A library manager for OCaml
zarith                1.13        Implements arithmetic and logical operations over arbitrary-precision integers
# opam file:
opam-version: "2.0"
maintainer: "johnw@newartisans.com"
homepage: "https://github.com/jwiegley/category-theory"
dev-repo: "git+https://github.com/jwiegley/category-theory.git"
bug-reports: "https://github.com/jwiegley/category-theory/issues"
license: "BSD-3-Clause"
synopsis: "An axiom-free formalization of category theory in Coq"
description: """
An axiom-free formalization of category theory in Coq for personal study and
practical work.
"""
build: [make "-j%{jobs}%"]
install: [make "install"]
depends: [
  "coq" {(>= "8.14" & < "8.17~") | (= "dev")}
  "coq-equations" {(>= "1.2" & < "1.4~") | (= "dev")}
]
url {
  src: "https://github.com/jwiegley/category-theory/archive/refs/tags/1.0.0.tar.gz"
  checksum: "sha256=d8a9fce1e20d0bd6e756957bf40c4deee1d83732c6c949a1dc5c290136ced60b"
}
tags: [
  "keyword: category theory"
  "category: Mathematics/Category Theory"
  "date: 2022-07-22"
  "logpath: Category"
]
authors: [
  "John Wiegley"
]

Lint

Command
true
Return code
0

Dry install 🏜️

Dry install with the current Coq version:

Command
opam install -y --show-action coq-category-theory.1.0.0 coq.8.16.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; timeout 4h opam install -y --deps-only coq-category-theory.1.0.0 coq.8.16.0
Return code
0
Duration
1 m 0 s

Install 🚀

Command
opam list; echo; timeout 4h opam install -y -v coq-category-theory.1.0.0 coq.8.16.0
Return code
0
Duration
29 m 0 s

Installation size

Total: 69 M

  • 16 M ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Construction/Product/Monoidal.vo
  • 12 M ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Construction/Comma.vo
  • 6 M ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Metacategory/ArrowsOnly.vo
  • 3 M ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Construction/Slice.vo
  • 2 M ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/Eval.vo
  • 2 M ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Construction/Comma/Adjunction.vo
  • 2 M ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Construction/Comma/Isomorphism.vo
  • 1 M ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Traversable/Product.vo
  • 1 M ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/Exp.vo
  • 1 M ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Cartesian/Closed.vo
  • 966 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Lib/NETList.vo
  • 619 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Metacategory.vo
  • 578 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Lib/MapDecide.vo
  • 555 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Lib/TList.vo
  • 545 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/Full.vo
  • 458 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Construction/Product/Monoidal.glob
  • 334 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/Step.vo
  • 322 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Solver/Normal.vo
  • 310 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Construction/Slice/Pullback.vo
  • 304 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Monoidal/Composition.vo
  • 303 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Sets/Part.vo
  • 301 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Construction/Comma/Adjunction.glob
  • 286 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/Ren.vo
  • 282 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Cones/Comma.vo
  • 281 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Parallel.vo
  • 273 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/Sub.vo
  • 234 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Comp.vo
  • 231 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Monad/Monoid.vo
  • 217 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Lib/FMapExt.vo
  • 196 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Solver/Reflect.vo
  • 196 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Monoid.vo
  • 195 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Construction/Cayley.vo
  • 191 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Structure/Monoidal/Compose.vo
  • 186 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Shapes.vo
  • 186 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Construction/Product/Strong.vo
  • 175 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Adjunction/Hom.vo
  • 169 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Sets.vo
  • 158 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Monoidal/Product.vo
  • 157 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Construction/Product/Comma.vo
  • 150 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Monoidal/Internal/Product.vo
  • 147 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Cartesian.vo
  • 135 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Strong/Product.vo
  • 133 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/BiCCC.vo
  • 132 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Monoidal/Cartesian/Proofs.vo
  • 132 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Structure/Monoidal/Compose.glob
  • 127 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Construction/Enriched.vo
  • 126 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Fun.vo
  • 125 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Adj.vo
  • 122 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/AST.vo
  • 122 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Cocartesian.vo
  • 121 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Kan/Extension.vo
  • 113 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/Sem.vo
  • 112 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Lib/Equality.vo
  • 110 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Closed.vo
  • 109 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Cat.vo
  • 108 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Cones.vo
  • 108 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda.glob
  • 102 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Construction/Product.vo
  • 101 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Cartesian/Closed/Product.vo
  • 100 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Solver/Decide.vo
  • 100 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Monoidal/Proofs.vo
  • 99 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Traversable.vo
  • 99 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Cat/Cartesian/Closed.vo
  • 99 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Monoidal/Naturality.vo
  • 96 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Lib/NETList.glob
  • 96 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Bifunctor.vo
  • 93 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Structure/Monoidal.vo
  • 93 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Adjunction.vo
  • 92 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Lib/Datatypes.vo
  • 90 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Functor.vo
  • 89 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Two.vo
  • 88 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Solver/Arrows.vo
  • 86 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Cat/Cocartesian.vo
  • 84 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Metacategory/ArrowsOnly.glob
  • 82 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Lib/TList.glob
  • 82 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Span.vo
  • 81 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Group/Proofs.vo
  • 81 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Naturality.glob
  • 81 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Natural/Transformation.vo
  • 80 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Adjoints.vo
  • 79 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Solver/Denote.vo
  • 78 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Monoidal/Relevant.vo
  • 77 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Lib/FMapExt.glob
  • 77 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Hom.vo
  • 77 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Isomorphism.vo
  • 76 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Monoidal/Proofs.glob
  • 75 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/Ty.vo
  • 75 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Hom/Yoneda.vo
  • 74 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda.vo
  • 73 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Monoid.glob
  • 73 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Lib/Nomega.vo
  • 73 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Structure/Monoidal/Id.vo
  • 72 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Roof.vo
  • 72 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Cartesian/Closed.glob
  • 71 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Category.vo
  • 69 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Construction/Product.vo
  • 68 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Solver/Reify.vo
  • 67 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Construction/Comma/Natural/Transformation.vo
  • 67 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Strong.vo
  • 65 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Two/Discrete.vo
  • 65 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Adjunction/Diagonal/Product.vo
  • 65 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Lib/MapDecide.glob
  • 65 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Cocartesian.glob
  • 64 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Cartesian.glob
  • 62 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Construction/Coproduct.vo
  • 62 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Metacategory.glob
  • 61 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Coq/Dist.vo
  • 60 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Lib/Tree.vo
  • 60 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/ilist.vo
  • 60 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/Log.vo
  • 60 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Shapes.glob
  • 59 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Naturality.vo
  • 59 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Group/Proofs.glob
  • 58 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/Norm.vo
  • 57 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Fact.vo
  • 57 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Coq.vo
  • 56 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Adjunction/Hom.glob
  • 56 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Structure/Cartesian/Closed.vo
  • 56 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Lib/Nomega.glob
  • 56 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Construction/Subcategory.vo
  • 54 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Adjunction.glob
  • 53 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Ens.vo
  • 52 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Pullback/Limit.vo
  • 52 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Adjunction/Natural/Transformation/Universal.vo
  • 51 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Monoidal.vo
  • 51 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Morphisms.vo
  • 50 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/Sub.glob
  • 50 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Comp.glob
  • 49 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Coproduct.vo
  • 48 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Lib/Equality.glob
  • 48 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Monoidal/Semicartesian/Proofs.vo
  • 47 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Tools/Abstraction.vo
  • 46 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Cartesian/Product.vo
  • 46 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Diagonal.vo
  • 46 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/Value.vo
  • 46 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Construction/Product/Strong.glob
  • 46 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/BiCCC.glob
  • 45 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Hom/Internal.vo
  • 44 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Monoidal/Cartesian/Proofs.glob
  • 44 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Monoidal/Symmetric.vo
  • 44 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Solver/Env.vo
  • 43 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Metacategory/DecideExample.vo
  • 43 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Solver/Tactics.vo
  • 43 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Kan/Extension.glob
  • 43 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Functor/Endo.vo
  • 43 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Solver/Categories.vo
  • 42 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Structure/Cartesian.vo
  • 42 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Lib/Same_set.vo
  • 41 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/Multi.vo
  • 41 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Cat/Cartesian.vo
  • 41 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Structure/Monoidal/Pure.vo
  • 41 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Monad/Eilenberg/Moore.vo
  • 40 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Functor.glob
  • 40 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Algebra/Basic.vo
  • 40 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Universal/Arrow.vo
  • 40 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Lib/Datatypes.glob
  • 40 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/Full.glob
  • 39 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Monad/Transformer.vo
  • 39 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Monad/Composition.vo
  • 38 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Fun.glob
  • 38 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Solver/Expr.vo
  • 38 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Natural/Transformation.glob
  • 38 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Construction/Free.vo
  • 38 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Zero.vo
  • 38 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Applicative.vo
  • 38 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Construction/Opposite.vo
  • 37 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Coq/Monad.vo
  • 36 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Category.glob
  • 36 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Limit/Kan/Extension.vo
  • 35 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Monad/Distributive.vo
  • 35 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Monad/Adjunction.vo
  • 35 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Adjoints.glob
  • 34 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Construction/Product/Monoidal.v
  • 34 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Category/Raw.vo
  • 34 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Algebra/Monoid.vo
  • 33 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Monoidal/Cartesian/Cartesian.vo
  • 33 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Monad/Kleisli.vo
  • 33 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Rel.vo
  • 33 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Coq/Applicative.vo
  • 32 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Bicategory.vo
  • 32 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Sets/Cocartesian.vo
  • 32 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Structure/Monoidal.glob
  • 32 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Dinatural.vo
  • 32 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Product/Internal.vo
  • 32 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Bifunctor.glob
  • 31 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Cone/Const.vo
  • 30 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Props.vo
  • 30 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Monoidal/Semicocartesian.vo
  • 30 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Natural/Transformation/Applicative.vo
  • 29 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/Eval.glob
  • 29 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Monoidal/Semicartesian.vo
  • 29 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Monoidal/Cartesian.vo
  • 29 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Monoidal/Braided.vo
  • 29 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Group.vo
  • 28 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Construction/Product.glob
  • 28 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Solver/Reify.glob
  • 28 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Monad.vo
  • 28 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Adjunction/Natural/Transformation.vo
  • 28 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/One.vo
  • 27 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Sets/Cartesian/Closed.vo
  • 27 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/Ren.glob
  • 27 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/Sound.vo
  • 27 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Product.vo
  • 27 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Solver/Normal.glob
  • 26 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Adjunction/Natural/Transformation/Opposite.vo
  • 26 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Cat.glob
  • 26 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/Sem.glob
  • 26 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Strong/Product.glob
  • 26 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Tools/Represented.vo
  • 25 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Lib/Tactics.vo
  • 25 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Cone/Natural/Transformation.vo
  • 25 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Solver/Reflect.glob
  • 25 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Category/Semi.vo
  • 25 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Wedge.vo
  • 25 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Natural/Transformation/Monoidal.vo
  • 25 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Construction/Comma/Adjunction.v
  • 25 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Tools/Abstraction.glob
  • 25 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Traversable.glob
  • 25 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Construction/Product.glob
  • 24 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Construction/Comma/Isomorphism.glob
  • 24 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Sets/Cartesian.vo
  • 24 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/End.vo
  • 24 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Natural/Transformation/Strong.vo
  • 24 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Monad/Algebra.vo
  • 23 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Proset.vo
  • 23 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Structure/Constant.vo
  • 23 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/Example.vo
  • 23 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Construction/Groupoid.vo
  • 23 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Pullback.vo
  • 23 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/AST.glob
  • 23 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Construction/Enriched.glob
  • 23 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Lib/IList.vo
  • 22 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Isomorphism.glob
  • 22 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Bicartesian.vo
  • 22 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Structure/Terminal.vo
  • 22 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Lib/Setoid.vo
  • 22 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Cone.vo
  • 22 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/Ltac.vo
  • 22 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Cones/Limit.vo
  • 22 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Adjunction/Opposite.vo
  • 22 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Lib/FMapExt.v
  • 22 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Terminal.vo
  • 21 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Representable.vo
  • 21 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Distributive.vo
  • 21 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Initial.vo
  • 21 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Limit.vo
  • 21 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/Step.glob
  • 21 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Construction/Cayley.glob
  • 21 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/One/Diagonal.vo
  • 20 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/Norm.glob
  • 20 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Sheaf.vo
  • 20 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Limit/Kan/Extension.glob
  • 20 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Unique.vo
  • 20 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Poset.vo
  • 20 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Natural/Transformation/Opposite.vo
  • 20 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Opposite.vo
  • 19 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Equalizer.vo
  • 19 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Complete.vo
  • 19 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Lib/NETList.v
  • 19 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Metacategory/DecideExample.glob
  • 19 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Construction/Arrow.vo
  • 19 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Limit/Universal/Arrow.vo
  • 18 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Constant.vo
  • 18 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Lib/TList.v
  • 18 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory.vo
  • 18 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Construction/Comma.glob
  • 17 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Monoidal.glob
  • 17 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Morphisms.glob
  • 17 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Coq/Dist.glob
  • 17 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Parallel.glob
  • 17 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Discrete.vo
  • 17 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Solver/Decide.glob
  • 17 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/Lib.vo
  • 17 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Strong.glob
  • 17 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Metacategory/ArrowsOnly.v
  • 16 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/Multi.glob
  • 16 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Coq.glob
  • 16 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Algebra/Basic.glob
  • 16 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Lib/MapDecide.v
  • 16 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Lib.vo
  • 16 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Coq/Monad.glob
  • 16 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Cat/Cartesian/Closed.glob
  • 15 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Traversable/Product.glob
  • 15 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Monoidal/Semicartesian/Proofs.glob
  • 15 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Hom.glob
  • 14 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Comp.v
  • 14 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Lib/IList.glob
  • 14 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Sets/Part.glob
  • 14 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Solver/Denote.glob
  • 14 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Monoidal/Symmetric.glob
  • 14 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Structure/Cartesian/Closed.glob
  • 14 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Metacategory.v
  • 14 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Solver/Arrows.glob
  • 13 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Construction/Subcategory.glob
  • 13 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Bicategory.glob
  • 13 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Lib/Foundation.vo
  • 13 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Sets.glob
  • 13 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Structure/Cartesian.glob
  • 12 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Adjunction/Natural/Transformation/Universal.glob
  • 12 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Lib/Tree.glob
  • 12 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Lib/Equality.v
  • 12 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Monoidal/Naturality.glob
  • 12 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Shapes.v
  • 12 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Construction/Comma/Natural/Transformation.glob
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Structure/Monoidal/Compose.v
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Construction/Slice/Pullback.glob
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Monad/Kleisli.glob
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Monad/Transformer.glob
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Construction/Slice.glob
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Cartesian/Closed.v
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/Ltac.glob
  • 11 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Category.v
  • 10 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Lib/Nomega.v
  • 10 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/Log.glob
  • 10 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Naturality.v
  • 10 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Adjunction.v
  • 10 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/Sub.v
  • 10 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Coq/Applicative.glob
  • 10 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Monad/Composition.glob
  • 10 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Pullback/Limit.glob
  • 10 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Monad/Adjunction.glob
  • 9 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Category/Raw.glob
  • 9 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Lib/Same_set.glob
  • 9 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Cartesian.v
  • 9 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Universal/Arrow.glob
  • 9 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/Exp.glob
  • 9 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Monoidal/Product.glob
  • 9 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Hom/Yoneda.glob
  • 9 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Kan/Extension.v
  • 9 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Cocartesian.v
  • 9 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Monoidal/Relevant.glob
  • 9 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Construction/Opposite.glob
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Diagonal.glob
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Monoidal/Composition.glob
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/Full.v
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Cones/Comma.glob
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Cat/Cartesian.glob
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Monoidal/Proofs.v
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Lib/Datatypes.v
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Adjoints.v
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Closed.glob
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Monoid.v
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Ens.glob
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Lib/Tactics.glob
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Dinatural.glob
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Monad/Distributive.glob
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Functor.v
  • 8 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Adjunction/Hom.v
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Solver/Reify.v
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Solver/Expr.glob
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Monoidal/Cartesian/Proofs.v
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Natural/Transformation.v
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Monoidal/Semicocartesian.glob
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Opposite.glob
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Category/Semi.glob
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Solver/Reflect.v
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Roof.glob
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Monoidal/Semicartesian.glob
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Functor/Endo.glob
  • 7 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Group/Proofs.v
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Sets/Part.v
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Structure/Monoidal/Pure.glob
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Solver/Normal.v
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Isomorphism.v
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda.v
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Lib/Setoid.glob
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/Example.glob
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Two.glob
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Fun.v
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/Norm.v
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Natural/Transformation/Opposite.glob
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Hom/Internal.glob
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Construction/Free.glob
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/Sem.v
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Monad.glob
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Pullback.glob
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Structure/Monoidal/Id.glob
  • 6 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Coq/Dist.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/Ren.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/BiCCC.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Props.glob
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Solver/Tactics.glob
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Monad/Monoid.glob
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Monoidal/Cartesian/Cartesian.glob
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Hom/Yoneda.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Adjunction/Opposite.glob
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Parallel.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Two/Discrete.glob
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Span.glob
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Monad/Transformer.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/Step.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/AST.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Sets.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Monoidal/Internal/Product.glob
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Cartesian/Closed/Product.glob
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Bifunctor.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Tools/Abstraction.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Construction/Cayley.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Solver/Env.glob
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Adjunction/Natural/Transformation/Opposite.glob
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Construction/Enriched.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Rel.glob
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Solver/Partial.vo
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Pullback.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Adjunction/Natural/Transformation.glob
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Solver/Tactics.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Coq/Applicative.v
  • 5 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Coq.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/ilist.glob
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Algebra/Monoid.glob
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Traversable.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Cat.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/Value.glob
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Cones.glob
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Cone/Const.glob
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Lib/Same_set.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Construction/Comma/Isomorphism.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Coq/Monad.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/Eval.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Monad/Eilenberg/Moore.glob
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Solver/Categories.glob
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Limit/Kan/Extension.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Cat/Cartesian/Closed.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Structure/Monoidal.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Wedge.glob
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Construction/Coproduct.glob
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Sets/Cocartesian.glob
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Natural/Transformation/Monoidal.glob
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Cartesian/Product.glob
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Bicartesian.glob
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Applicative.glob
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Strong/Product.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Solver/Decide.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Lib/IList.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Rel.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Morphisms.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Construction/Product/Strong.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Adj.glob
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Lib/Tactics.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Construction/Product.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Traversable/Product.v
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/End.glob
  • 4 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Solver/Arrows.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Monad/Algebra.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/Multi.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Strong.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Cat/Cocartesian.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Construction/Product.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Category/Raw.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Proset.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Fact.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Monoidal/Cartesian.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Initial.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Construction/Comma.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Monoidal/Braided.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Sets/Cartesian.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Lib/Tree.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Lib/Setoid.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Metacategory/DecideExample.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Cone.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Sets/Cartesian/Closed.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Tools/Represented.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Hom.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Monoidal/Naturality.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Monoidal/Semicartesian/Proofs.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Two.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Algebra/Basic.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Natural/Transformation/Strong.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Cone/Const.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Terminal.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Bicategory.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Solver/Denote.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Construction/Slice/Pullback.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Monoidal.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Adjunction/Diagonal/Product.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Pullback/Limit.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Group.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Solver/Categories.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Structure/Constant.glob
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Roof.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Structure/Cartesian.v
  • 3 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Construction/Comma/Natural/Transformation.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Construction/Subcategory.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Adjunction/Natural/Transformation/Universal.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Natural/Transformation/Applicative.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Cones/Limit.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Monoidal/Composition.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Closed.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Diagonal.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Product/Internal.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Limit.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Construction/Product/Comma.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Cone/Natural/Transformation.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Solver/Expr.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Monoidal/Product.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Monad/Kleisli.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/One.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Structure/Cartesian/Closed.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Cones/Comma.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Two/Discrete.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Structure/Terminal.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Monad/Composition.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Construction/Coproduct.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Construction/Slice.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Monad/Adjunction.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Cat/Cocartesian.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Coproduct.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Product.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Distributive.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Functor/Endo.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Structure/Monoidal/Id.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Unique.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Monoidal/Relevant.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Props.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Monad/Monoid.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Monoidal/Semicocartesian.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Construction/Free.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Monoidal/Semicartesian.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Proset.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Cat/Cartesian.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Monoidal/Symmetric.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Poset.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/Log.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Monoidal/Cartesian.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/Exp.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Monoidal/Internal/Product.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Sheaf.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/Sound.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Applicative.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Construction/Opposite.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Monoidal/Cartesian/Cartesian.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/One/Diagonal.glob
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/Ltac.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Sets/Cocartesian.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/Value.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Ens.v
  • 2 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Zero.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Solver/Env.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Monad.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Dinatural.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Universal/Arrow.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Structure/Monoidal/Pure.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Poset.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Algebra/Monoid.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Category/Semi.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Fact.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Span.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Representable.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Complete.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Adjunction/Opposite.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Construction/Groupoid.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Sets/Cartesian/Closed.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/Example.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Initial.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Adjunction/Natural/Transformation.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Discrete.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Hom/Internal.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Limit.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Adj.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Representable.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Adjunction/Natural/Transformation/Opposite.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Solver/Partial.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Monad/Distributive.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Tools/Represented.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/Ty.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Construction/Product/Comma.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Cartesian/Closed/Product.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Lib/Foundation.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Coproduct.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Opposite.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Natural/Transformation/Opposite.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Adjunction/Diagonal/Product.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Cone/Natural/Transformation.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Zero.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Equalizer.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/One.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Cone.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Lib/Foundation.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Structure/Terminal.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Terminal.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Sets/Cartesian.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Wedge.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Monad/Algebra.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Product.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Group.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Construction/Arrow.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Constant.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Cones.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Natural/Transformation/Applicative.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Monad/Eilenberg/Moore.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Product/Internal.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Cartesian/Product.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Monoidal/Braided.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/Sound.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/End.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Bicartesian.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Unique.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Solver/Partial.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Functor/Structure/Constant.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Natural/Transformation/Monoidal.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory/Sheaf.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/ilist.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Distributive.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/Lib.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Construction/Groupoid.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Cones/Limit.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Natural/Transformation/Strong.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/Ty.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Constant.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/One/Diagonal.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Theory.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Discrete.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Limit/Universal/Arrow.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Equalizer.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Construction/Arrow.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Complete.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Instance/Lambda/Lib.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Structure/Limit/Universal/Arrow.glob
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Lib.v
  • 1 K ../ocaml-base-compiler.4.13.1/lib/coq/user-contrib/Category/Lib.glob

Uninstall 🧹

Command
opam remove -y coq-category-theory.1.0.0
Return code
0
Missing removes
none
Wrong removes
none

Sources are on GitHub © Guillaume Claret 🐣