« Up

category-theory dev 38 m 0 s 🏆

Context

# Packages matching: installed
# Name                # Installed # Synopsis
base-bigarray         base
base-domains          base
base-nnp              base        Naked pointers prohibited in the OCaml heap
base-threads          base
base-unix             base
conf-gmp              4           Virtual package relying on a GMP lib system installation
coq                   dev         The Coq Proof Assistant
coq-core              dev         The Coq Proof Assistant -- Core Binaries and Tools
coq-stdlib            dev         The Coq Proof Assistant -- Standard Library
coqide-server         dev         The Coq Proof Assistant, XML protocol server
dune                  3.13.0      Fast, portable, and opinionated build system
ocaml                 5.1.1       The OCaml compiler (virtual package)
ocaml-base-compiler   5.1.1       Official release 5.1.1
ocaml-config          3           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 "JOBS=%{jobs}%" ]
install: [make "install"]
depends: [
  "coq" {>= "8.14"}
  "coq-equations" {>= "1.3"}
]
tags: [
  "logpath:Category"
]
authors: [
  "John Wiegley"
]
url {
  src: "git+https://github.com/jwiegley/category-theory.git#master"
}

Lint

Command
true
Return code
0

Dry install 🏜️

Dry install with the current Coq version:

Command
opam install -y --show-action coq-category-theory.dev coq.dev
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.dev coq.dev
Return code
0
Duration
1 m 0 s

Install 🚀

Command
opam list; echo; timeout 4h opam install -y coq-category-theory.dev coq.dev
Return code
0
Duration
38 m 0 s

Installation size

Total: 64 M

  • 12 M ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Construction/Product/Monoidal.vo
  • 8 M ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Coq/Par.vo
  • 6 M ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Lambda/Eval.vo
  • 5 M ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Metacategory/ArrowsOnly.vo
  • 2 M ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Lambda/Exp.vo
  • 2 M ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Comma/Adjunction.vo
  • 2 M ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Comma/Isomorphism.vo
  • 1 M ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Slice.vo
  • 1 M ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Cartesian/Closed.vo
  • 1 M ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Lib/NETList.vo
  • 867 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Lambda/Sub.vo
  • 642 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Metacategory.vo
  • 627 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Lambda/Full.vo
  • 612 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Comma.vo
  • 563 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Lib/TList.vo
  • 456 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Construction/Product/Monoidal.glob
  • 449 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Traversable/Product.vo
  • 419 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Lambda/Step.vo
  • 364 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Lib/MapDecide.vo
  • 351 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Free/Quiver.vo
  • 335 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Lambda/Ren.vo
  • 320 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Compose.vo
  • 306 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Solver/Normal.vo
  • 301 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Comma/Adjunction.glob
  • 293 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Sets/Par.vo
  • 278 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Parallel.vo
  • 240 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Monad/Monoid.vo
  • 222 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Cones/Comma.vo
  • 216 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Lib/FMapExt.vo
  • 201 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Cayley.vo
  • 191 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Slice/Pullback.vo
  • 188 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Comp.vo
  • 183 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoid.vo
  • 179 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Functor.vo
  • 177 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Construction/Product/Strong.vo
  • 174 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Shapes.vo
  • 172 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Map.vo
  • 167 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Sets.vo
  • 158 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Universal/Arrow.vo
  • 149 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Cartesian.vo
  • 149 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Product.vo
  • 139 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Adjunction/Hom.vo
  • 138 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Lambda.glob
  • 135 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Structure/Monoidal/Compose.vo
  • 135 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Strong/Product.vo
  • 132 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Structure/Monoidal/Compose.glob
  • 127 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Product/Comma.vo
  • 127 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Natural/Transformation.vo
  • 127 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Cartesian/Proofs.vo
  • 121 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Proofs.vo
  • 120 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Adj.vo
  • 116 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/BiCCC.vo
  • 116 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Cocartesian.vo
  • 115 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Enriched.vo
  • 115 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Lambda/Sem.vo
  • 111 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Coq/ParE.vo
  • 105 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/UniversalProperty/Universal/Arrow.vo
  • 99 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Adjunction.vo
  • 99 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/UniversalProperty/Cartesian.vo
  • 98 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Lib/NETList.glob
  • 97 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Two/Discrete.vo
  • 97 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Closed.vo
  • 96 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Solver/Reify.glob
  • 95 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Cat/Cartesian/Closed.vo
  • 93 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Lib/IList.vo
  • 93 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/UniversalProperty/Limit.vo
  • 91 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/AST.vo
  • 89 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Internal/Product.vo
  • 88 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Kan/Extension.vo
  • 86 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Construction/Product.vo
  • 86 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Naturality.glob
  • 86 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Isomorphism.vo
  • 86 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Lib/Datatypes.vo
  • 85 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Metacategory/ArrowsOnly.glob
  • 85 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Two.vo
  • 84 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/UniversalProperty.vo
  • 84 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Functor.glob
  • 84 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Free/Quiver.glob
  • 83 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Lib/FMapExt.glob
  • 83 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Cartesian.glob
  • 82 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Relevance.vo
  • 81 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Bifunctor.vo
  • 81 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Lambda.vo
  • 80 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Structure/Monoidal.vo
  • 80 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Cat/Cocartesian.vo
  • 80 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Span.vo
  • 78 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Fun.vo
  • 76 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Proofs.glob
  • 75 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Hom.vo
  • 75 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Lambda/Ty.vo
  • 75 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Free.vo
  • 74 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoid.glob
  • 72 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Group/Proofs.vo
  • 71 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Cartesian/Closed.glob
  • 71 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Solver/Decide.vo
  • 70 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Adjoints.vo
  • 69 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Hom/Yoneda.vo
  • 68 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/List/Proofs.vo
  • 67 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Traversable.vo
  • 67 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Lambda/Log.vo
  • 67 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Lib/MapDecide.glob
  • 65 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Category.vo
  • 65 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Limit/Cartesian.vo
  • 65 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Cocartesian.glob
  • 64 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Roof.vo
  • 63 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Lambda/Norm.vo
  • 62 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Metacategory.glob
  • 62 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Comp.glob
  • 62 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Adjunction.glob
  • 61 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Shapes.glob
  • 61 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Product.vo
  • 60 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Fun/Cartesian.vo
  • 59 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Group/Proofs.glob
  • 58 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Strong.vo
  • 57 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Naturality.vo
  • 57 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/List.vo
  • 57 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Adjunction/Hom.glob
  • 56 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Lambda/Value.vo
  • 55 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Solver/Reify.vo
  • 54 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Coproduct.vo
  • 54 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Applicative/Proofs.vo
  • 53 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Cat.vo
  • 53 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Internal/Product.glob
  • 52 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Lib/TList.glob
  • 52 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Comma/Natural/Transformation.vo
  • 52 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Pullback/Limit.vo
  • 51 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Naturality.vo
  • 50 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Lambda/Sub.glob
  • 50 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Fact.vo
  • 49 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Cartesian/Closed/Product.vo
  • 49 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Ens.vo
  • 49 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Subcategory.vo
  • 48 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Tools/Abstraction.vo
  • 48 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Structure/Monoidal/Id.vo
  • 47 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/BiCCC.glob
  • 46 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal.vo
  • 46 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Construction/Product/Strong.glob
  • 45 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Morphisms.vo
  • 45 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Coq.vo
  • 45 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Map.glob
  • 45 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Braided.vo
  • 45 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Metacategory/DecideExample.vo
  • 45 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Solver/Normal.glob
  • 45 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Natural/Transformation.glob
  • 44 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Closed.vo
  • 44 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Kan/Extension.glob
  • 43 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Lib/Datatypes.glob
  • 42 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Adjunction/Natural/Transformation/Universal.vo
  • 41 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Lambda/Multi.vo
  • 41 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Semicartesian/Proofs.vo
  • 40 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Lambda/Full.glob
  • 40 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Cartesian/Proofs.glob
  • 40 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Traced.vo
  • 39 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Fun.glob
  • 39 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Hom/Internal.vo
  • 39 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/UniversalProperty.glob
  • 39 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Maybe/Proofs.vo
  • 39 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Structure/Cartesian/Closed.vo
  • 38 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Symmetric.vo
  • 38 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Cartesian/Product.vo
  • 38 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Cartesian.vo
  • 37 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Category.glob
  • 35 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Adjoints.glob
  • 35 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Zero.vo
  • 34 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Construction/Product/Monoidal.v
  • 34 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Adjunction/Diagonal/Product.vo
  • 34 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Cat/Cartesian.vo
  • 34 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/List.glob
  • 34 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Coproduct.vo
  • 33 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Cone.vo
  • 33 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Structure/Monoidal/Pure.vo
  • 33 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Monad/Proofs.vo
  • 33 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Monad/Eilenberg/Moore.vo
  • 33 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Cones.vo
  • 32 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Structure/Monoidal.glob
  • 32 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Sheaf.vo
  • 32 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Isomorphism.glob
  • 32 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Structure/Cartesian.vo
  • 32 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Diagonal.vo
  • 32 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Bifunctor.glob
  • 32 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Coq/Monad.vo
  • 31 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Monad.vo
  • 31 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Limit/Kan/Extension.vo
  • 31 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Monad/Transformer.vo
  • 30 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Monad/Compose.vo
  • 30 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Binoidal.vo
  • 30 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Opposite.vo
  • 30 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Rel.vo
  • 30 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Lambda/Eval.glob
  • 29 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Coq/Applicative.vo
  • 29 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Cone/Natural/Transformation.vo
  • 29 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Cone/Const.vo
  • 29 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/List/Proofs.glob
  • 28 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Cat.glob
  • 28 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Category/Raw.vo
  • 28 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Monad/Adjunction.vo
  • 28 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Sets/Cocartesian.vo
  • 28 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Construction/Product.glob
  • 28 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq.vo
  • 27 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Monad/Kleisli.vo
  • 27 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Monad/Distributive.vo
  • 27 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Comma/Isomorphism.glob
  • 27 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Lambda/Ren.glob
  • 27 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Solver/Denote.vo
  • 26 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Algebra.vo
  • 26 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Lambda/Sem.glob
  • 26 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Universal/Arrow.glob
  • 26 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Bicategory.vo
  • 26 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Product/Internal.vo
  • 26 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Strong/Product.glob
  • 26 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Applicative.vo
  • 25 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Tools/Abstraction.glob
  • 25 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Solver/Expr.vo
  • 25 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Props.vo
  • 25 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Comma/Adjunction.v
  • 24 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/UniversalProperty/Limit.glob
  • 24 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Balanced.vo
  • 24 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Applicative.vo
  • 24 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Product.glob
  • 24 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Tools/Represented.vo
  • 24 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Coq/Par.glob
  • 24 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Lambda/Example.vo
  • 24 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Semicocartesian.vo
  • 24 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Monad.vo
  • 24 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Functor/Proofs.vo
  • 23 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Lib/Setoid.vo
  • 23 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Functor.vo
  • 23 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/List/Proofs.v
  • 23 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Semicartesian.vo
  • 23 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Lib/Tactics.vo
  • 23 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Sets.glob
  • 23 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Group.vo
  • 23 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Cartesian/Cartesian.vo
  • 23 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Enriched.glob
  • 23 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Dinatural.vo
  • 22 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Limit.vo
  • 22 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Lib/FMapExt.v
  • 22 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Lambda/Step.glob
  • 22 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Monad.glob
  • 21 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/AST.glob
  • 21 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Sets/Cartesian/Closed.vo
  • 21 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Free/Quiver.v
  • 21 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Cayley.glob
  • 21 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Limit/Kan/Extension.glob
  • 21 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Lambda/Norm.glob
  • 21 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Natural/Transformation/Applicative.vo
  • 21 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Lib/Tactics2.vo
  • 21 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Maybe.vo
  • 21 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Lambda/Sound.vo
  • 21 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Fun/Cartesian.glob
  • 20 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Adjunction/Natural/Transformation.vo
  • 20 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Tuple/Proofs.vo
  • 20 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Morphisms.glob
  • 20 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Closed.glob
  • 20 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Traversable.glob
  • 20 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Product.vo
  • 19 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Limit/Terminal.vo
  • 19 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Comma.glob
  • 19 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Tuple.vo
  • 19 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Category/Semi.vo
  • 19 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Metacategory/DecideExample.glob
  • 19 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Natural/Transformation/Monoidal.vo
  • 19 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Lib/NETList.v
  • 19 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Wedge.vo
  • 18 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/One.vo
  • 18 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Monad/Algebra.vo
  • 18 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Solver/Decide.glob
  • 18 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Either/Proofs.vo
  • 18 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Sets/Cartesian.vo
  • 18 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Free.glob
  • 18 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Braided.glob
  • 18 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Either.vo
  • 18 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Parallel.glob
  • 18 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/End.vo
  • 18 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Structure/Constant.vo
  • 17 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal.glob
  • 17 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Adjunction/Natural/Transformation/Opposite.vo
  • 17 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Pullback.vo
  • 17 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Natural/Transformation/Strong.vo
  • 17 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Strong.glob
  • 17 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Coq/Monad.glob
  • 17 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/StrictCat.vo
  • 17 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Metacategory/ArrowsOnly.v
  • 17 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Lambda/Multi.glob
  • 17 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Algebra.glob
  • 16 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Bicartesian.vo
  • 16 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Hom.glob
  • 16 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Structure/Terminal.vo
  • 16 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Lib/MapDecide.v
  • 16 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Tuple.glob
  • 16 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Sheaf.glob
  • 16 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Cat/Cartesian/Closed.glob
  • 16 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Traversable/Product.glob
  • 16 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Adjunction/Opposite.vo
  • 16 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Commutative.vo
  • 15 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Functor.v
  • 15 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/One/Diagonal.vo
  • 15 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Proset.vo
  • 15 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Groupoid.vo
  • 15 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Distributive.vo
  • 15 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Representable.vo
  • 15 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Cones/Limit.vo
  • 15 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Semicartesian/Proofs.glob
  • 15 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Comp.v
  • 15 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Terminal.vo
  • 15 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Lib/IList.glob
  • 15 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Sets/Par.glob
  • 14 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Symmetric.glob
  • 14 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Applicative.glob
  • 14 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Initial.vo
  • 14 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Solver.vo
  • 14 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Opposite.vo
  • 14 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Lambda/Ltac.vo
  • 14 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Natural/Transformation/Opposite.vo
  • 14 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Structure/Cartesian/Closed.glob
  • 14 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Solver/Reify.v
  • 14 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Binoidal.glob
  • 14 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Complete.vo
  • 14 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Metacategory.v
  • 14 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Traversable.vo
  • 13 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Bicategory.glob
  • 13 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Equalizer.vo
  • 13 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Subcategory.glob
  • 13 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Arrow.vo
  • 13 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Maybe/Proofs.glob
  • 13 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Constant.vo
  • 13 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Coq.glob
  • 13 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Adjunction/Natural/Transformation/Universal.glob
  • 13 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory.vo
  • 13 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Semicartesian/Terminal.vo
  • 12 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Structure/Cartesian.glob
  • 12 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Monad/Compose.glob
  • 12 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Shapes.v
  • 12 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Coq/ParE.glob
  • 12 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Discrete.vo
  • 12 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Foldable.vo
  • 12 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Semigroup.vo
  • 12 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Monoid.vo
  • 12 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Comma/Natural/Transformation.glob
  • 12 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Structure/Monoidal/Compose.v
  • 12 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Poset.vo
  • 12 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Solver/Normal.v
  • 11 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Monad/Kleisli.glob
  • 11 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Coq/Applicative.glob
  • 11 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Cartesian.v
  • 11 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Maybe.glob
  • 11 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Slice.glob
  • 11 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Slice/Pullback.glob
  • 11 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Monad/Transformer.glob
  • 11 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Adjunction.v
  • 11 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Pullback/Limit.glob
  • 11 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Lambda/Log.glob
  • 11 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Relevance.glob
  • 11 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Lambda/Ltac.glob
  • 11 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Traced.glob
  • 10 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Lib/TList.v
  • 10 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Lib.vo
  • 10 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Cartesian/Closed.v
  • 10 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Functor.glob
  • 10 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/UniversalProperty/Cartesian.glob
  • 10 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Category.v
  • 10 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Internal/Product.v
  • 10 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Map.v
  • 10 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Naturality.v
  • 10 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Lambda/Sub.v
  • 10 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Monad/Adjunction.glob
  • 10 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/List.v
  • 10 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/UniversalProperty.v
  • 10 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Applicative/Proofs.glob
  • 10 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Category/Raw.glob
  • 9 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Cartesian.glob
  • 9 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Naturality.glob
  • 9 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/UniversalProperty/Universal/Arrow.glob
  • 9 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Cone.glob
  • 9 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Lambda/Exp.glob
  • 9 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Lib/Foundation.vo
  • 9 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Cones/Comma.glob
  • 9 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Hom/Yoneda.glob
  • 9 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Diagonal.glob
  • 9 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Product.glob
  • 9 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Cocartesian.v
  • 9 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Kan/Extension.v
  • 8 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Opposite.glob
  • 8 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Cat/Cartesian.glob
  • 8 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Sets.v
  • 8 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Compose.glob
  • 8 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Lambda/Full.v
  • 8 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Isomorphism.v
  • 8 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Ens.glob
  • 8 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Adjoints.v
  • 8 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoid.v
  • 8 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Lib/Setoid.glob
  • 8 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Closed.glob
  • 8 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Proofs.v
  • 8 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Monad/Distributive.glob
  • 8 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Lib/Datatypes.v
  • 8 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Either.glob
  • 8 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Limit/Cartesian.glob
  • 8 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Adjunction/Hom.v
  • 8 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Dinatural.glob
  • 8 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Two/Discrete.glob
  • 7 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Lib/Tactics.glob
  • 7 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Solver/Denote.glob
  • 7 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Roof.glob
  • 7 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Natural/Transformation.v
  • 7 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Category/Semi.glob
  • 7 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Monad/Proofs.glob
  • 7 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Coq/Par.v
  • 7 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Opposite.glob
  • 7 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Semicocartesian.glob
  • 7 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Semicartesian.glob
  • 7 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Group/Proofs.v
  • 7 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Bicategory.v
  • 6 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Two.glob
  • 6 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Structure/Monoidal/Pure.glob
  • 6 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Sets/Par.v
  • 6 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Cartesian/Proofs.v
  • 6 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Lambda/Norm.v
  • 6 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Natural/Transformation/Opposite.glob
  • 6 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/BiCCC.v
  • 6 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/UniversalProperty/Limit.v
  • 6 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Hom/Internal.glob
  • 6 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Monad.glob
  • 6 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Fun.v
  • 6 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Structure/Monoidal/Id.glob
  • 6 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Lambda/Sem.v
  • 6 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Lambda/Example.glob
  • 6 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Lambda.v
  • 6 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Monad/Monoid.glob
  • 6 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Pullback.glob
  • 6 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Lambda/Ren.v
  • 5 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Props.glob
  • 5 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Lambda/Step.v
  • 5 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Adjunction/Opposite.glob
  • 5 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Cartesian/Closed/Product.glob
  • 5 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Span.glob
  • 5 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Hom/Yoneda.v
  • 5 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Parallel.v
  • 5 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Cone/Const.glob
  • 5 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Limit.glob
  • 5 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Cartesian/Cartesian.glob
  • 5 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Monad/Transformer.v
  • 5 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Bifunctor.v
  • 5 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Universal/Arrow.v
  • 5 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Tools/Abstraction.v
  • 5 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Cayley.v
  • 5 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Free.v
  • 5 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Comma/Isomorphism.v
  • 5 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Adjunction/Natural/Transformation/Opposite.glob
  • 5 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Functor/Proofs.glob
  • 5 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Adjunction/Natural/Transformation.glob
  • 5 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Coq/ParE.v
  • 5 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Rel.glob
  • 4 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Cat.v
  • 4 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Monad/Eilenberg/Moore.glob
  • 4 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Pullback.v
  • 4 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Limit/Kan/Extension.v
  • 4 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Cones.glob
  • 4 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Monad.v
  • 4 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Balanced.glob
  • 4 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Fun/Cartesian.v
  • 4 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Lambda/Value.glob
  • 4 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Coq/Applicative.v
  • 4 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/AST.v
  • 4 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Coq/Monad.v
  • 4 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Cat/Cartesian/Closed.v
  • 4 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Lambda/Eval.v
  • 4 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/UniversalProperty/Cartesian.v
  • 4 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Comma.v
  • 4 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Tuple/Proofs.glob
  • 4 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Wedge.glob
  • 4 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Solver/Decide.v
  • 4 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Structure/Monoidal.v
  • 4 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Coproduct.glob
  • 4 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Hom.v
  • 4 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Closed.v
  • 4 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Bicartesian.glob
  • 4 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Strong/Product.v
  • 4 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Morphisms.v
  • 4 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Solver/Expr.glob
  • 4 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Cartesian/Product.glob
  • 4 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Sets/Cocartesian.glob
  • 4 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Adj.glob
  • 4 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Traversable.v
  • 4 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Rel.v
  • 4 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/End.glob
  • 4 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Lambda/Multi.v
  • 4 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Monad/Algebra.glob
  • 4 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Natural/Transformation/Monoidal.glob
  • 4 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Construction/Product/Strong.v
  • 4 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Traversable/Product.v
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Lib/Tactics.v
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Enriched.v
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Lib/Tactics2.glob
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Binoidal.v
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Cat/Cocartesian.glob
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Strong.v
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Product.v
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Applicative.glob
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Applicative/Proofs.v
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Coq.v
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Construction/Product.v
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Category/Raw.v
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Sheaf.v
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Sets/Cartesian.glob
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Tools/Represented.glob
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Sets/Cartesian/Closed.glob
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/UniversalProperty/Universal/Arrow.v
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Maybe/Proofs.v
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Fact.glob
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Initial.glob
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Coproduct.glob
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Natural/Transformation/Strong.glob
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Applicative.v
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Algebra.v
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Two/Discrete.v
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Lib/Tactics2.v
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Pullback/Limit.v
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Lib/IList.v
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Adjunction/Diagonal/Product.glob
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Two.v
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Cone/Const.v
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Proset.glob
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Metacategory/DecideExample.v
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Semicartesian/Proofs.v
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Cones/Limit.glob
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Structure/Constant.glob
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Terminal.glob
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Symmetric.v
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Maybe.v
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Cartesian.v
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Slice.v
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Group.glob
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Slice/Pullback.v
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Diagonal.v
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Adjunction/Natural/Transformation/Universal.v
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Functor.v
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Limit/Terminal.glob
  • 3 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal.v
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Cone/Natural/Transformation.glob
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Comma/Natural/Transformation.v
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Cones/Comma.v
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Product/Internal.glob
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Product/Comma.glob
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Monad/Compose.v
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Roof.v
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Closed.v
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Subcategory.v
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Lib/Foundation.glob
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Monad/Proofs.v
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/One.glob
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Cone.v
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Structure/Cartesian.v
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Limit/Cartesian.v
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Compose.v
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Monad/Kleisli.v
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Natural/Transformation/Applicative.glob
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Structure/Cartesian/Closed.v
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Relevance.v
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Braided.v
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Distributive.glob
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Lib/Foundation.v
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Structure/Terminal.glob
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Monad/Adjunction.v
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Product.v
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Product.glob
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Lib/Setoid.v
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Coproduct.v
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Traversable.glob
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Cat/Cocartesian.v
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Structure/Monoidal/Id.v
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/StrictCat.glob
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Cat/Cartesian.v
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Monad/Monoid.v
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Lambda/Log.v
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Lambda/Exp.v
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Naturality.v
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Lambda/Sound.glob
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Props.v
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Semicocartesian.v
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/One/Diagonal.glob
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Either.v
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Semicartesian.v
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Tuple.v
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Cartesian/Cartesian.v
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Limit.v
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Lambda/Ltac.v
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Functor/Proofs.v
  • 2 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Zero.glob
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Lambda/Value.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Semicartesian/Terminal.glob
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Complete.glob
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Solver/Denote.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Representable.glob
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Opposite.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Structure/Monoidal/Pure.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Monad.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Groupoid.glob
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Ens.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Sets/Cocartesian.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Category/Semi.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Limit/Terminal.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Traced.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Discrete.glob
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Proset.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Sets/Cartesian/Closed.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Span.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Dinatural.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Foldable.glob
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Lambda/Ty.glob
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Adjunction/Natural/Transformation.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Hom/Internal.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Poset.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Applicative.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Adjunction/Opposite.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Cartesian/Closed/Product.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Lambda/Example.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Representable.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Adj.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Monad/Distributive.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Tools/Represented.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Commutative.glob
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Initial.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Equalizer.glob
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Adjunction/Natural/Transformation/Opposite.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Product/Comma.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Coproduct.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Poset.glob
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Natural/Transformation/Applicative.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Fact.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/StrictCat.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Adjunction/Diagonal/Product.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/One.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Balanced.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Natural/Transformation/Opposite.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Constant.glob
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Cone/Natural/Transformation.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Arrow.glob
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Opposite.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Tuple/Proofs.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Solver/Expr.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Zero.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Lambda/Sound.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Wedge.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Group.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Monad/Algebra.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Monad/Eilenberg/Moore.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Either/Proofs.glob
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Cones.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/End.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Structure/Terminal.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Natural/Transformation/Monoidal.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Product.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Sets/Cartesian.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Cartesian/Product.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Product/Internal.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Bicartesian.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq.glob
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Traversable.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Semigroup.glob
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Terminal.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Cones/Limit.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Functor/Structure/Constant.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Distributive.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Natural/Transformation/Strong.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/Lambda/Ty.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory.glob
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Either/Proofs.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Instance/One/Diagonal.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Semicartesian/Terminal.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Monoidal/Commutative.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Groupoid.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Monoid.glob
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Constant.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Lib.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Equalizer.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Complete.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Structure/Discrete.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Construction/Arrow.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Foldable.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Semigroup.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Theory/Coq/Monoid.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Solver.glob
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Solver.v
  • 1 K ../ocaml-base-compiler.5.1.1/lib/coq/user-contrib/Category/Lib.glob

Uninstall 🧹

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

Sources are on GitHub © Guillaume Claret 🐣