# 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.14.1 Formal proof management system
dune 3.8.1 Fast, portable, and opinionated build system
ocaml 4.05.0 The OCaml compiler (virtual package)
ocaml-base-compiler 4.05.0 Official 4.05.0 release
ocaml-config 1 OCaml Switch Configuration
ocaml-secondary-compiler 4.08.1-1 OCaml 4.08.1 Secondary Switch Compiler
ocamlfind 1.9.1 A library manager for OCaml
ocamlfind-secondary 1.9.1 Adds support for ocaml-secondary-compiler to ocamlfind
zarith 1.12 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"
]
trueDry install with the current Coq version:
opam install -y --show-action coq-category-theory.1.0.0 coq.8.14.1Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
trueopam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-category-theory.1.0.0 coq.8.14.1opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-category-theory.1.0.0 coq.8.14.1Total: 78 M
../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Construction/Product/Monoidal.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Construction/Comma.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Metacategory/ArrowsOnly.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Construction/Slice.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Construction/Comma/Adjunction.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Construction/Comma/Isomorphism.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/Eval.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Traversable/Product.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/Exp.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Cartesian/Closed.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Lib/NETList.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Metacategory.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Lib/MapDecide.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Lib/TList.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/Full.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Construction/Product/Monoidal.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Monoidal/Composition.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/Step.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Solver/Normal.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Construction/Slice/Pullback.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Sets/Part.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Construction/Comma/Adjunction.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Monad/Monoid.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/Ren.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Cones/Comma.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Parallel.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/Sub.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Comp.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Lib/FMapExt.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Construction/Cayley.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Solver/Reflect.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Shapes.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Monoid.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Construction/Product/Strong.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Structure/Monoidal/Compose.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Sets.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Adjunction/Hom.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Monoidal/Product.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Construction/Product/Comma.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Cartesian.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Monoidal/Internal/Product.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Strong/Product.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Structure/Monoidal/Compose.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/BiCCC.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Construction/Enriched.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Monoidal/Cartesian/Proofs.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/AST.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Cones.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Fun.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Adj.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Cocartesian.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Kan/Extension.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Cat.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/Sem.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Closed.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Lib/Equality.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Construction/Product.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Cartesian/Closed/Product.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Traversable.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Monoidal/Naturality.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Cat/Cartesian/Closed.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Solver/Decide.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Bifunctor.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Monoidal/Proofs.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Lib/NETList.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Functor.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Adjunction.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Lib/Datatypes.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Structure/Monoidal.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Solver/Arrows.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Two.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Cat/Cocartesian.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Metacategory/ArrowsOnly.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Span.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Natural/Transformation.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Adjoints.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Lib/TList.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Solver/Denote.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Group/Proofs.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Naturality.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Isomorphism.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Monoidal/Relevant.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Hom/Yoneda.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Hom.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Construction/Product.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Lib/FMapExt.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/Ty.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Monoidal/Proofs.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Monoid.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Lib/Nomega.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Roof.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Category.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Cartesian/Closed.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Structure/Monoidal/Id.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Adjunction/Diagonal/Product.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Construction/Comma/Natural/Transformation.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Solver/Reify.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Strong.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Two/Discrete.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Lib/MapDecide.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Cocartesian.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Cartesian.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Construction/Coproduct.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Metacategory.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/ilist.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Lib/Tree.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Coq/Dist.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Naturality.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/Log.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Shapes.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Group/Proofs.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Fact.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/Norm.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Coq.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Construction/Subcategory.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Adjunction/Hom.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Structure/Cartesian/Closed.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Lib/Nomega.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Pullback/Limit.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Ens.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Adjunction.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Monoidal.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Adjunction/Natural/Transformation/Universal.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Morphisms.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/Sub.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Coproduct.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Comp.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Diagonal.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Lib/Equality.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Monoidal/Semicartesian/Proofs.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Tools/Abstraction.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Cartesian/Product.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/Value.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Hom/Internal.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Functor/Endo.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Construction/Product/Strong.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/BiCCC.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Solver/Env.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Monoidal/Cartesian/Proofs.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Monoidal/Symmetric.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Metacategory/DecideExample.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Solver/Tactics.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Kan/Extension.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Lib/Same_set.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Solver/Categories.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Structure/Cartesian.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Cat/Cartesian.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/Multi.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Structure/Monoidal/Pure.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Monad/Eilenberg/Moore.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Universal/Arrow.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Functor.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/Full.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Lib/Datatypes.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Algebra/Basic.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Monad/Transformer.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Monad/Composition.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Construction/Free.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Zero.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Applicative.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Solver/Expr.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Construction/Opposite.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Fun.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Natural/Transformation.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Coq/Monad.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Category.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Monad/Distributive.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Limit/Kan/Extension.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Monad/Adjunction.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Adjoints.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Category/Raw.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Algebra/Monoid.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Construction/Product/Monoidal.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Coq/Applicative.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Monoidal/Cartesian/Cartesian.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Rel.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Bicategory.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Monad/Kleisli.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Sets/Cocartesian.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Product/Internal.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Dinatural.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Structure/Monoidal.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Cone/Const.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Bifunctor.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Props.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Monoidal/Semicocartesian.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Monoidal/Semicartesian.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Natural/Transformation/Applicative.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Monoidal/Cartesian.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/Eval.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Monoidal/Braided.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Group.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Monad.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Construction/Product.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Solver/Reify.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Adjunction/Natural/Transformation.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/One.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Sets/Cartesian/Closed.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Product.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Adjunction/Natural/Transformation/Opposite.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/Sound.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/Ren.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Solver/Normal.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Cat.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/Sem.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Tools/Represented.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Cone/Natural/Transformation.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Strong/Product.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Category/Semi.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Lib/Tactics.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Wedge.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Natural/Transformation/Monoidal.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Solver/Reflect.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Construction/Comma/Adjunction.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Sets/Cartesian.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Tools/Abstraction.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Traversable.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Construction/Product.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Construction/Comma/Isomorphism.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/End.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Natural/Transformation/Strong.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Monad/Algebra.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Proset.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Structure/Constant.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Lib/IList.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/Example.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Construction/Groupoid.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Pullback.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/AST.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Construction/Enriched.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Structure/Terminal.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Bicartesian.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Isomorphism.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Cones/Limit.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Lib/Setoid.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Cone.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Adjunction/Opposite.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/Ltac.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Terminal.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Lib/FMapExt.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Representable.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Distributive.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Initial.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Limit.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/Step.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Construction/Cayley.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/One/Diagonal.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/Norm.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Sheaf.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Limit/Kan/Extension.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Natural/Transformation/Opposite.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Poset.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Unique.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Opposite.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Equalizer.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Complete.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Lib/NETList.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Construction/Arrow.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Metacategory/DecideExample.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Limit/Universal/Arrow.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Constant.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Lib/TList.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Construction/Comma.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Discrete.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Monoidal.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Morphisms.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Parallel.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Coq/Dist.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Solver/Decide.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/Lib.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Strong.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Metacategory/ArrowsOnly.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/Multi.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Coq.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Algebra/Basic.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Lib.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Lib/MapDecide.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Coq/Monad.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Cat/Cartesian/Closed.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Traversable/Product.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Monoidal/Semicartesian/Proofs.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Hom.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Comp.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Sets/Part.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Lib/IList.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Solver/Denote.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Monoidal/Symmetric.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Structure/Cartesian/Closed.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Metacategory.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Solver/Arrows.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Construction/Subcategory.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Bicategory.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Lib/Foundation.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Sets.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Structure/Cartesian.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Adjunction/Natural/Transformation/Universal.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Lib/Tree.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Lib/Equality.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Monoidal/Naturality.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Shapes.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Construction/Comma/Natural/Transformation.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Structure/Monoidal/Compose.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Construction/Slice/Pullback.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Monad/Kleisli.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Monad/Transformer.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Construction/Slice.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Cartesian/Closed.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/Ltac.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Category.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Lib/Nomega.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/Log.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Naturality.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Adjunction.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/Sub.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Coq/Applicative.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Monad/Composition.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Pullback/Limit.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Monad/Adjunction.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Category/Raw.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Cartesian.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Lib/Same_set.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Universal/Arrow.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Monoidal/Product.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/Exp.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Hom/Yoneda.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Kan/Extension.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Cocartesian.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Monoidal/Relevant.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Construction/Opposite.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Diagonal.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Monoidal/Composition.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/Full.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Cones/Comma.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Cat/Cartesian.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Monoidal/Proofs.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Lib/Datatypes.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Adjoints.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Closed.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Monoid.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Ens.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Lib/Tactics.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Dinatural.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Monad/Distributive.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Functor.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Adjunction/Hom.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Solver/Reify.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Monoidal/Cartesian/Proofs.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Natural/Transformation.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Solver/Expr.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Monoidal/Semicocartesian.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Opposite.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Category/Semi.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Solver/Reflect.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Roof.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Monoidal/Semicartesian.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Functor/Endo.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Group/Proofs.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Sets/Part.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Structure/Monoidal/Pure.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Solver/Normal.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Isomorphism.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Lib/Setoid.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Two.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/Example.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Fun.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/Norm.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Natural/Transformation/Opposite.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Hom/Internal.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Construction/Free.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/Sem.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Monad.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Pullback.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Structure/Monoidal/Id.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Coq/Dist.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/Ren.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/BiCCC.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Props.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Solver/Tactics.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Monad/Monoid.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Monoidal/Cartesian/Cartesian.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Hom/Yoneda.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Adjunction/Opposite.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Parallel.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Two/Discrete.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Span.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Monad/Transformer.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/Step.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/AST.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Sets.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Monoidal/Internal/Product.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Cartesian/Closed/Product.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Bifunctor.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Solver/Partial.vo../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Tools/Abstraction.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Construction/Cayley.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Solver/Env.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Adjunction/Natural/Transformation/Opposite.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Construction/Enriched.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Rel.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Pullback.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Adjunction/Natural/Transformation.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Solver/Tactics.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Coq/Applicative.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Coq.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/ilist.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Algebra/Monoid.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Traversable.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Cat.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Cones.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Cone/Const.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Lib/Same_set.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Construction/Comma/Isomorphism.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Coq/Monad.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/Value.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/Eval.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Monad/Eilenberg/Moore.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Solver/Categories.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Limit/Kan/Extension.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Cat/Cartesian/Closed.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Structure/Monoidal.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Wedge.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Construction/Coproduct.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Sets/Cocartesian.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Natural/Transformation/Monoidal.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Cartesian/Product.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Bicartesian.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Applicative.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Strong/Product.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Solver/Decide.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Lib/IList.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Rel.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Morphisms.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Construction/Product/Strong.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Adj.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Lib/Tactics.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Construction/Product.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Traversable/Product.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/End.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Solver/Arrows.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Monad/Algebra.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/Multi.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Strong.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Cat/Cocartesian.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Construction/Product.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Category/Raw.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Proset.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Fact.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Monoidal/Cartesian.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Initial.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Construction/Comma.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Monoidal/Braided.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Sets/Cartesian.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Lib/Tree.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Lib/Setoid.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Metacategory/DecideExample.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Cone.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Sets/Cartesian/Closed.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Tools/Represented.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Hom.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Monoidal/Naturality.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Monoidal/Semicartesian/Proofs.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Two.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Algebra/Basic.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Natural/Transformation/Strong.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Cone/Const.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Terminal.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Bicategory.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Solver/Denote.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Construction/Slice/Pullback.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Monoidal.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Adjunction/Diagonal/Product.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Pullback/Limit.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Solver/Categories.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Group.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Structure/Constant.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Roof.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Structure/Cartesian.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Construction/Comma/Natural/Transformation.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Construction/Subcategory.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Adjunction/Natural/Transformation/Universal.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Natural/Transformation/Applicative.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Cones/Limit.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Monoidal/Composition.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Closed.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Diagonal.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Product/Internal.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Limit.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Construction/Product/Comma.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Cone/Natural/Transformation.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Solver/Expr.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Monoidal/Product.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Monad/Kleisli.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/One.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Structure/Cartesian/Closed.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Cones/Comma.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Two/Discrete.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Structure/Terminal.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Monad/Composition.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Construction/Coproduct.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Construction/Slice.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Monad/Adjunction.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Cat/Cocartesian.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Coproduct.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Product.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Distributive.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Functor/Endo.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Structure/Monoidal/Id.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Unique.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Monoidal/Relevant.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Props.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Monad/Monoid.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Monoidal/Semicocartesian.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Construction/Free.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Monoidal/Semicartesian.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Proset.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Cat/Cartesian.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Monoidal/Symmetric.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Poset.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/Log.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Monoidal/Cartesian.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/Exp.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Monoidal/Internal/Product.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Sheaf.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Construction/Opposite.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Applicative.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/Sound.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Monoidal/Cartesian/Cartesian.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/One/Diagonal.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/Ltac.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Sets/Cocartesian.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/Value.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Ens.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Zero.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Solver/Env.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Monad.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Dinatural.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Universal/Arrow.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Structure/Monoidal/Pure.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Poset.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Algebra/Monoid.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Category/Semi.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Fact.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Span.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Representable.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Complete.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Adjunction/Opposite.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Construction/Groupoid.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Sets/Cartesian/Closed.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/Example.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Initial.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Adjunction/Natural/Transformation.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Hom/Internal.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Discrete.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Limit.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Adj.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Representable.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Adjunction/Natural/Transformation/Opposite.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Solver/Partial.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Monad/Distributive.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Tools/Represented.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/Ty.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Construction/Product/Comma.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Cartesian/Closed/Product.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Lib/Foundation.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Coproduct.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Opposite.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Natural/Transformation/Opposite.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Adjunction/Diagonal/Product.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Cone/Natural/Transformation.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Zero.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Equalizer.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/One.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Cone.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Lib/Foundation.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Structure/Terminal.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Terminal.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Sets/Cartesian.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Wedge.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Monad/Algebra.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Product.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Group.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Construction/Arrow.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Cones.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Constant.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Natural/Transformation/Applicative.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Monad/Eilenberg/Moore.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Product/Internal.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Cartesian/Product.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Monoidal/Braided.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/Sound.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/End.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Bicartesian.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Unique.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Solver/Partial.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Functor/Structure/Constant.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Natural/Transformation/Monoidal.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory/Sheaf.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/ilist.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Distributive.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/Lib.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Construction/Groupoid.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Cones/Limit.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Natural/Transformation/Strong.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/Ty.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Constant.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/One/Diagonal.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Theory.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Discrete.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Limit/Universal/Arrow.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Equalizer.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Construction/Arrow.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Complete.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Instance/Lambda/Lib.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Structure/Limit/Universal/Arrow.glob../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Lib.v../ocaml-base-compiler.4.05.0/lib/coq/user-contrib/Category/Lib.globopam remove -y coq-category-theory.1.0.0