# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-threads base
base-unix base
conf-gmp 4 Virtual package relying on a GMP lib system installation
coq dev The Coq Proof Assistant
coq-core dev The Coq Proof Assistant -- Core Binaries and Tools
coq-stdlib dev The Coq Proof Assistant -- Standard Library
coqide-server dev The Coq Proof Assistant, XML protocol server
dune 3.12.1 Fast, portable, and opinionated build system
ocaml 4.14.0 The OCaml compiler (virtual package)
ocaml-base-compiler 4.14.0 Official release 4.14.0
ocaml-config 2 OCaml Switch Configuration
ocaml-options-vanilla 1 Ensure that OCaml is compiled with no special options enabled
ocamlfind 1.9.6 A library manager for OCaml
zarith 1.13 Implements arithmetic and logical operations over arbitrary-precision integers
# opam file:
opam-version: "2.0"
maintainer: "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"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-category-theory.dev coq.devDry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
trueopam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-category-theory.dev coq.devopam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y coq-category-theory.dev coq.devTotal: 64 M
../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Construction/Product/Monoidal.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Coq/Par.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Lambda/Eval.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Metacategory/ArrowsOnly.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Lambda/Exp.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Comma/Adjunction.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Comma/Isomorphism.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Slice.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Cartesian/Closed.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Lib/NETList.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Lambda/Sub.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Metacategory.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Lambda/Full.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Comma.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Lib/TList.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Construction/Product/Monoidal.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Traversable/Product.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Lambda/Step.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Lib/MapDecide.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Free/Quiver.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Lambda/Ren.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Compose.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Solver/Normal.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Comma/Adjunction.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Sets/Par.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Parallel.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Monad/Monoid.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Cones/Comma.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Lib/FMapExt.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Cayley.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Slice/Pullback.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Comp.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoid.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Functor.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Construction/Product/Strong.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Shapes.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Map.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Sets.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Universal/Arrow.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Cartesian.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Product.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Adjunction/Hom.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Lambda.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Structure/Monoidal/Compose.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Strong/Product.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Structure/Monoidal/Compose.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Product/Comma.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Natural/Transformation.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Cartesian/Proofs.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Proofs.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Adj.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/BiCCC.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Cocartesian.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Enriched.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Lambda/Sem.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Coq/ParE.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/UniversalProperty/Universal/Arrow.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Adjunction.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/UniversalProperty/Cartesian.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Lib/NETList.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Two/Discrete.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Closed.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Solver/Reify.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Cat/Cartesian/Closed.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Lib/IList.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/UniversalProperty/Limit.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/AST.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Internal/Product.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Kan/Extension.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Construction/Product.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Isomorphism.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Lib/Datatypes.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Naturality.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Metacategory/ArrowsOnly.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Two.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/UniversalProperty.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Functor.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Free/Quiver.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Lib/FMapExt.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Cartesian.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Relevance.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Bifunctor.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Lambda.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Structure/Monoidal.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Cat/Cocartesian.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Span.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Fun.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Proofs.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Hom.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Lambda/Ty.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Free.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoid.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Group/Proofs.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Cartesian/Closed.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Solver/Decide.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Adjoints.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Hom/Yoneda.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/List/Proofs.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Traversable.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Lambda/Log.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Lib/MapDecide.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Category.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Limit/Cartesian.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Cocartesian.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Roof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Lambda/Norm.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Metacategory.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Comp.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Adjunction.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Shapes.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Product.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Fun/Cartesian.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Group/Proofs.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Strong.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Naturality.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/List.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Adjunction/Hom.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Lambda/Value.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Solver/Reify.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Coproduct.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Applicative/Proofs.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Cat.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Internal/Product.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Lib/TList.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Comma/Natural/Transformation.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Pullback/Limit.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Naturality.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Lambda/Sub.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Fact.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Cartesian/Closed/Product.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Ens.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Subcategory.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Tools/Abstraction.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Structure/Monoidal/Id.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/BiCCC.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Construction/Product/Strong.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Morphisms.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Coq.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Map.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Braided.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Metacategory/DecideExample.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Solver/Normal.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Natural/Transformation.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Closed.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Kan/Extension.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Lib/Datatypes.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Adjunction/Natural/Transformation/Universal.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Lambda/Multi.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Semicartesian/Proofs.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Lambda/Full.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Cartesian/Proofs.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Traced.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Fun.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Hom/Internal.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Maybe/Proofs.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/UniversalProperty.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Structure/Cartesian/Closed.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Symmetric.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Cartesian/Product.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Cartesian.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Category.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Adjoints.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Zero.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Construction/Product/Monoidal.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Adjunction/Diagonal/Product.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Cat/Cartesian.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/List.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Coproduct.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Cone.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Structure/Monoidal/Pure.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Monad/Proofs.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Monad/Eilenberg/Moore.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Cones.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Sheaf.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Structure/Monoidal.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Isomorphism.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Structure/Cartesian.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Diagonal.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Coq/Monad.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Bifunctor.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Monad.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Limit/Kan/Extension.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Monad/Transformer.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Monad/Compose.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Binoidal.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Opposite.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Rel.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Lambda/Eval.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Coq/Applicative.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Cone/Natural/Transformation.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Cone/Const.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/List/Proofs.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Category/Raw.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Cat.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Monad/Adjunction.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Sets/Cocartesian.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Construction/Product.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Monad/Kleisli.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Monad/Distributive.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Comma/Isomorphism.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Lambda/Ren.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Solver/Denote.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Algebra.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Lambda/Sem.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Bicategory.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Universal/Arrow.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Product/Internal.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Strong/Product.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Applicative.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Solver/Expr.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Tools/Abstraction.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Props.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Comma/Adjunction.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Balanced.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/UniversalProperty/Limit.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Applicative.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Tools/Represented.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Product.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Lambda/Example.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Coq/Par.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Semicocartesian.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Monad.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Functor/Proofs.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Lib/Setoid.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Functor.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Semicartesian.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Lib/Tactics.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/List/Proofs.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Group.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Sets.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Cartesian/Cartesian.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Enriched.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Dinatural.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Limit.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Lib/FMapExt.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Lambda/Step.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Sets/Cartesian/Closed.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Monad.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/AST.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Free/Quiver.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Cayley.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Limit/Kan/Extension.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Natural/Transformation/Applicative.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Lambda/Norm.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Lib/Tactics2.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Maybe.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Lambda/Sound.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Adjunction/Natural/Transformation.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Fun/Cartesian.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Tuple/Proofs.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Morphisms.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Closed.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Traversable.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Product.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Limit/Terminal.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Tuple.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Comma.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Category/Semi.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Natural/Transformation/Monoidal.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Metacategory/DecideExample.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Lib/NETList.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Wedge.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/One.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Monad/Algebra.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Either/Proofs.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Sets/Cartesian.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Solver/Decide.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Free.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Braided.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Either.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/End.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Parallel.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Structure/Constant.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Adjunction/Natural/Transformation/Opposite.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Pullback.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Natural/Transformation/Strong.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Strong.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/StrictCat.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Coq/Monad.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Metacategory/ArrowsOnly.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Lambda/Multi.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Algebra.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Bicartesian.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Structure/Terminal.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Hom.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Lib/MapDecide.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Tuple.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Sheaf.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Cat/Cartesian/Closed.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Traversable/Product.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Adjunction/Opposite.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Commutative.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Functor.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/One/Diagonal.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Proset.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Groupoid.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Distributive.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Representable.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Cones/Limit.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Terminal.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Semicartesian/Proofs.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Comp.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Lib/IList.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Sets/Par.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Symmetric.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Applicative.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Initial.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Solver.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Opposite.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Natural/Transformation/Opposite.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Lambda/Ltac.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Complete.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Structure/Cartesian/Closed.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Solver/Reify.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Binoidal.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Traversable.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Metacategory.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Equalizer.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Bicategory.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Subcategory.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Arrow.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Maybe/Proofs.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Constant.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Coq.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Semicartesian/Terminal.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Adjunction/Natural/Transformation/Universal.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Structure/Cartesian.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Monad/Compose.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Shapes.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Discrete.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Coq/ParE.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Foldable.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Semigroup.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Monoid.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Poset.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Comma/Natural/Transformation.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Structure/Monoidal/Compose.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Solver/Normal.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Monad/Kleisli.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Coq/Applicative.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Cartesian.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Maybe.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Slice.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Slice/Pullback.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Monad/Transformer.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Adjunction.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Pullback/Limit.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Lambda/Log.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Relevance.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Lambda/Ltac.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Lib.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Traced.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Lib/TList.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Cartesian/Closed.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Functor.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/UniversalProperty/Cartesian.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Category.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Internal/Product.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Map.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Naturality.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Lambda/Sub.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Monad/Adjunction.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/List.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/UniversalProperty.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Applicative/Proofs.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Category/Raw.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Cartesian.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Naturality.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/UniversalProperty/Universal/Arrow.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Cone.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Lambda/Exp.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Lib/Foundation.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Cones/Comma.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Hom/Yoneda.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Diagonal.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Product.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Cocartesian.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Kan/Extension.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Opposite.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Cat/Cartesian.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Sets.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Compose.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Lambda/Full.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Isomorphism.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Ens.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Adjoints.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoid.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Lib/Setoid.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Closed.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Proofs.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Monad/Distributive.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Lib/Datatypes.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Either.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Limit/Cartesian.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Adjunction/Hom.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Dinatural.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Two/Discrete.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Lib/Tactics.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Solver/Denote.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Natural/Transformation.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Roof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Category/Semi.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Monad/Proofs.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Coq/Par.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Opposite.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Semicocartesian.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Semicartesian.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Group/Proofs.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Bicategory.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Two.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Structure/Monoidal/Pure.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Sets/Par.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Cartesian/Proofs.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Lambda/Norm.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Natural/Transformation/Opposite.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/BiCCC.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/UniversalProperty/Limit.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Hom/Internal.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Monad.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Fun.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Structure/Monoidal/Id.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Lambda/Sem.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Lambda/Example.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Lambda.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Monad/Monoid.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Pullback.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Lambda/Ren.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Props.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Lambda/Step.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Adjunction/Opposite.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Cartesian/Closed/Product.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Span.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Hom/Yoneda.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Parallel.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Cone/Const.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Limit.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Cartesian/Cartesian.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Monad/Transformer.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Bifunctor.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Universal/Arrow.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Tools/Abstraction.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Cayley.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Free.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Comma/Isomorphism.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Adjunction/Natural/Transformation/Opposite.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Functor/Proofs.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Adjunction/Natural/Transformation.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Coq/ParE.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Rel.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Cat.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Monad/Eilenberg/Moore.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Pullback.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Limit/Kan/Extension.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Cones.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Monad.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Balanced.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Fun/Cartesian.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Lambda/Value.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Coq/Applicative.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/AST.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Coq/Monad.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Cat/Cartesian/Closed.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Lambda/Eval.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/UniversalProperty/Cartesian.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Comma.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Tuple/Proofs.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Wedge.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Solver/Decide.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Structure/Monoidal.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Coproduct.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Hom.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Closed.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Bicartesian.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Strong/Product.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Morphisms.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Solver/Expr.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Cartesian/Product.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Sets/Cocartesian.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Adj.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Traversable.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Rel.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/End.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Lambda/Multi.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Monad/Algebra.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Natural/Transformation/Monoidal.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Construction/Product/Strong.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Traversable/Product.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Lib/Tactics.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Enriched.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Lib/Tactics2.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Binoidal.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Cat/Cocartesian.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Strong.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Product.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Applicative.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Applicative/Proofs.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Coq.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Construction/Product.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Category/Raw.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Sheaf.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Sets/Cartesian.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Tools/Represented.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Sets/Cartesian/Closed.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/UniversalProperty/Universal/Arrow.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Maybe/Proofs.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Fact.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Initial.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Coproduct.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Natural/Transformation/Strong.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Applicative.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Algebra.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Two/Discrete.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Lib/Tactics2.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Pullback/Limit.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Lib/IList.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Adjunction/Diagonal/Product.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Two.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Cone/Const.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Proset.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Metacategory/DecideExample.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Semicartesian/Proofs.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Cones/Limit.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Structure/Constant.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Terminal.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Symmetric.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Maybe.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Cartesian.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Slice.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Group.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Slice/Pullback.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Diagonal.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Adjunction/Natural/Transformation/Universal.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Functor.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Limit/Terminal.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Cone/Natural/Transformation.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Comma/Natural/Transformation.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Cones/Comma.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Product/Internal.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Product/Comma.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Monad/Compose.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Roof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Closed.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Subcategory.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Lib/Foundation.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Monad/Proofs.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/One.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Cone.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Structure/Cartesian.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Limit/Cartesian.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Compose.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Monad/Kleisli.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Natural/Transformation/Applicative.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Structure/Cartesian/Closed.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Relevance.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Braided.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Distributive.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Lib/Foundation.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Structure/Terminal.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Monad/Adjunction.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Product.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Product.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Lib/Setoid.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Coproduct.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Traversable.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Cat/Cocartesian.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Structure/Monoidal/Id.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/StrictCat.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Cat/Cartesian.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Monad/Monoid.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Lambda/Log.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Lambda/Exp.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Naturality.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Lambda/Sound.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Props.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Semicocartesian.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/One/Diagonal.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Either.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Semicartesian.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Tuple.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Cartesian/Cartesian.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Limit.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Lambda/Ltac.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Functor/Proofs.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Zero.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Lambda/Value.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Semicartesian/Terminal.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Complete.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Solver/Denote.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Representable.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Opposite.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Structure/Monoidal/Pure.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Monad.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Groupoid.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Ens.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Sets/Cocartesian.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Category/Semi.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Limit/Terminal.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Traced.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Discrete.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Proset.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Sets/Cartesian/Closed.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Span.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Dinatural.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Foldable.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Lambda/Ty.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Adjunction/Natural/Transformation.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Hom/Internal.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Poset.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Applicative.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Adjunction/Opposite.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Cartesian/Closed/Product.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Lambda/Example.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Representable.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Adj.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Monad/Distributive.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Tools/Represented.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Commutative.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Initial.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Equalizer.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Adjunction/Natural/Transformation/Opposite.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Product/Comma.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Coproduct.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Poset.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Natural/Transformation/Applicative.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Fact.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/StrictCat.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Adjunction/Diagonal/Product.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/One.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Balanced.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Natural/Transformation/Opposite.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Constant.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Cone/Natural/Transformation.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Arrow.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Opposite.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Tuple/Proofs.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Solver/Expr.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Zero.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Lambda/Sound.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Wedge.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Group.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Monad/Algebra.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Monad/Eilenberg/Moore.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Either/Proofs.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Cones.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/End.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Structure/Terminal.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Natural/Transformation/Monoidal.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Product.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Sets/Cartesian.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Cartesian/Product.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Product/Internal.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Bicartesian.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Traversable.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Semigroup.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Terminal.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Cones/Limit.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Functor/Structure/Constant.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Distributive.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Natural/Transformation/Strong.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/Lambda/Ty.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Either/Proofs.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Instance/One/Diagonal.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Semicartesian/Terminal.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Monoidal/Commutative.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Groupoid.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Monoid.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Constant.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Lib.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Equalizer.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Complete.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Structure/Discrete.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Construction/Arrow.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Foldable.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Semigroup.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Theory/Coq/Monoid.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Solver.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Solver.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/Category/Lib.globopam remove -y coq-category-theory.dev