« Up

concat 8.5.0 1 m 0 s 🏆

Context

# Packages matching: installed
# Name              # Installed # Synopsis
base-bigarray       base
base-num            base        Num library distributed with the OCaml compiler
base-threads        base
base-unix           base
camlp5              7.14        Preprocessor-pretty-printer of OCaml
conf-findutils      1           Virtual package relying on findutils
conf-perl           2           Virtual package relying on perl
coq                 8.5.2       Formal proof management system
num                 0           The Num library for arbitrary-precision integer and rational arithmetic
ocaml               4.03.0      The OCaml compiler (virtual package)
ocaml-base-compiler 4.03.0      Official 4.03.0 release
ocaml-config        1           OCaml Switch Configuration
# opam file:
opam-version: "2.0"
maintainer: "matej.kosik@inria.fr"
homepage: "https://github.com/coq-contribs/concat"
license: "LGPL 2"
build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-R" "%{lib}%/coq/user-contrib/ConCaT"]
depends: [
  "ocaml"
  "coq" {>= "8.5" & < "8.6~"}
]
tags: [ "keyword:category theory" "category:Mathematics/Category Theory" ]
authors: [ "Amokrane Saïbi <>" ]
bug-reports: "https://github.com/coq-contribs/concat/issues"
dev-repo: "git+https://github.com/coq-contribs/concat.git"
synopsis: "Constructive Category Theory"
flags: light-uninstall
url {
  src: "https://github.com/coq-contribs/concat/archive/v8.5.0.tar.gz"
  checksum: "md5=21a4371b2648fec6b8dd3c1bcb5f50c7"
}

Lint

Command
true
Return code
0

Dry install 🏜️

Dry install with the current Coq version:

Command
opam install -y --show-action coq-concat.8.5.0 coq.8.5.2
Return code
0

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

Command
true
Return code
0

Install dependencies

Command
opam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-concat.8.5.0 coq.8.5.2
Return code
0
Duration
1 m 0 s

Install 🚀

Command
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-concat.8.5.0 coq.8.5.2
Return code
0
Duration
1 m 0 s

Installation size

Total: 4 M

  • 147 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/FREYD_THEOREM/FAFT_Part2_Proof1.vo
  • 90 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/Adjunction1.glob
  • 77 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/FREYD_THEOREM/FAFT_Part2_Proof1.glob
  • 73 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/CONSTRUCTIONS/Binary_Products.glob
  • 64 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/CCC/FunProd.glob
  • 61 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/Th_CoAdjoint.glob
  • 59 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/Th_Adjoint.glob
  • 56 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMITS/Pullbacks1.glob
  • 54 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMITS/PA.glob
  • 51 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMITS/PULB.glob
  • 48 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/Adjunction1.vo
  • 46 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/Adjunction.glob
  • 41 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMIT_CONSTRUCTIONS/Th_Limits.glob
  • 39 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/NT/InterChangeLaw.glob
  • 37 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMITS/PULB.vo
  • 37 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMITS/Equalizers1.vo
  • 36 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMITS/PA.vo
  • 35 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMITS/UniversalArrow.glob
  • 34 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMIT_CONSTRUCTIONS/Th_Limits.vo
  • 32 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/Th_CoAdjoint.vo
  • 32 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMITS/Pullbacks1.vo
  • 31 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/HomFunctor2.glob
  • 31 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/Th_Adjoint.vo
  • 31 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMITS/Equalizers1.glob
  • 30 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/CONSTRUCTIONS/CatProperty.glob
  • 30 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMIT_CONSTRUCTIONS/Th_Initial.vo
  • 30 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/HomFunctor2.vo
  • 29 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMIT_CONSTRUCTIONS/Comma_Complete.vo
  • 28 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/FUNCTOR/Comma.vo
  • 27 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/CONSTRUCTIONS/CatProperty.vo
  • 27 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/Category.glob
  • 27 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMIT_CONSTRUCTIONS/Th_Initial.glob
  • 26 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/Adj_UA.glob
  • 25 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/CCC/Cartesian1.vo
  • 25 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMIT_CONSTRUCTIONS/Comma_Complete.glob
  • 24 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/CONSTRUCTIONS/Binary_Products.vo
  • 23 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMITS/CoUniversalArrow.vo
  • 22 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/FUNCTOR/Functor.vo
  • 22 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/CONSTRUCTIONS/Equalizers.glob
  • 22 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMITS/Limit.vo
  • 22 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/Adjunction.vo
  • 22 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMITS/UniversalArrow.vo
  • 22 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMITS/CoLimit.vo
  • 21 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/Category.vo
  • 21 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/PROD.vo
  • 20 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMITS/CoUniversalArrow.glob
  • 20 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/SETOID/STRUCTURE/Inverses_Group.vo
  • 20 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/NT/YONEDA_LEMMA/YonedaLemma.glob
  • 20 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/LeftAdj_Iso.glob
  • 20 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/NT/YONEDA_LEMMA/YonedaLemma.vo
  • 20 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/FUNCTOR/Functor.glob
  • 19 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/CONSTRUCTIONS/Pullbacks.vo
  • 19 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/CCC/CCC1.vo
  • 19 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMITS/Products1.vo
  • 19 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/SETOID/STRUCTURE/Inverses_Group.glob
  • 18 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/NT/InterChangeLaw.vo
  • 18 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/NT/NatIso.glob
  • 18 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/FREYD_THEOREM/FAFT_Part1.vo
  • 18 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/CONSTRUCTIONS/Equalizers.vo
  • 18 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/NT/Setoid_dup2.vo
  • 18 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/FUNCTOR/Setoid_dup1.vo
  • 18 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/Limit_Adj.glob
  • 18 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/NT/YONEDA_LEMMA/Functor_dup1.vo
  • 18 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMIT_CONSTRUCTIONS/SET_Complete.vo
  • 18 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/Adj_UA.vo
  • 18 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/Limit_Adj.vo
  • 17 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/SETOID/STRUCTURE/Monoid.vo
  • 17 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMIT_CONSTRUCTIONS/HomFunctor_Continuous.vo
  • 17 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/CONSTRUCTIONS/SET_Pullback.vo
  • 17 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/NT/CatFunct.vo
  • 17 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/FUNCTOR/Comma.glob
  • 16 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/FUNCTOR/FunctorProperty.glob
  • 16 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/FREYD_THEOREM/FAFT_Part2_Proof2.vo
  • 16 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/NT/NatIso.vo
  • 15 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/FUNCTOR/Setoid_dup1.glob
  • 15 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMITS/CoLimit.glob
  • 15 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/FREYD_THEOREM/FAFT_SSC2.vo
  • 15 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMITS/FunForget_UA.vo
  • 15 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMITS/Limit.glob
  • 15 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/FUNCTOR/FunctorProperty.vo
  • 15 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/SETOID/STRUCTURE/FreeMonoid.vo
  • 15 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/NT/Category_dup2.vo
  • 15 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/FUNCTOR/Category_dup1.vo
  • 15 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/CCC/Cartesian1.glob
  • 15 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/NT/Setoid_dup2.glob
  • 14 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/FUNCTOR/Category_dup1.glob
  • 14 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/CONSTRUCTIONS/Exponents.vo
  • 14 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/CONSTRUCTIONS/SET_Exponents.vo
  • 14 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMITS/Iso_Limit.vo
  • 14 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/NT/YONEDA_LEMMA/YonedaEmbedding.vo
  • 14 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/CONSTRUCTIONS/SET_Equalizer.vo
  • 14 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/NT/Category_dup2.glob
  • 13 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/RELATIONS/Relations.vo
  • 13 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/LeftAdj_Iso.vo
  • 13 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/CONSTRUCTIONS/Pullbacks.glob
  • 13 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMITS/Comma_UA.vo
  • 13 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/SETOID/STRUCTURE/Monoid.glob
  • 13 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMITS/PULB.v
  • 13 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/FUNCTOR/FunFreeMon.vo
  • 13 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/NT/CatFunct.glob
  • 12 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMITS/Discr.vo
  • 12 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/ONE.vo
  • 12 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/NT/YONEDA_LEMMA/Functor_dup1.glob
  • 12 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/RELATIONS/CONFLUENCE/Coherence.vo
  • 12 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/RELATIONS/CONFLUENCE/Confluence.vo
  • 12 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/CONSTRUCTIONS/Exponents.glob
  • 12 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/MON.vo
  • 12 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/SETOID/Map2.vo
  • 12 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMITS/PA.v
  • 11 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/NT/Ntransformation.vo
  • 11 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMIT_CONSTRUCTIONS/SET_Complete.glob
  • 11 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/Hom_Equality.vo
  • 11 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/Adjunction1.v
  • 11 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/FUNCTOR/CAT.vo
  • 11 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/CONSTRUCTIONS/Products.vo
  • 11 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMIT_CONSTRUCTIONS/Pres_Limits.vo
  • 11 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMITS/FunForget_UA.glob
  • 11 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/CONSTRUCTIONS/SET_BinProds.vo
  • 11 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/CCC/Terminal1.vo
  • 10 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/PROD.glob
  • 10 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/CONSTRUCTIONS/SET_Pullback.glob
  • 10 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMITS/Products1.glob
  • 10 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/RELATIONS/CONFLUENCE/Coherence.glob
  • 10 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/FREYD_THEOREM/FAFT_Part1.glob
  • 10 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/SETOID/Map.vo
  • 10 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/Th_Adjoint.v
  • 10 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/SETOID/Setoid.vo
  • 10 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMIT_CONSTRUCTIONS/HomFunctor_Continuous.glob
  • 10 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/FREYD_THEOREM/FAFT_Part2_Proof1.v
  • 10 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/SETOID/Setoid_prop.vo
  • 9 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/SETOID/Map2.glob
  • 9 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/CCC/FunProd.vo
  • 9 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/FUNCTOR/PROD_proj.vo
  • 9 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/FUNCTOR/HomFunctor.vo
  • 9 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/Adj_FunFreeMon.vo
  • 9 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/Th_CoAdjoint.v
  • 9 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/SETOID/SetoidPROD.vo
  • 9 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/CONSTRUCTIONS/CCC.vo
  • 9 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/CONSTRUCTIONS/Products.glob
  • 9 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/RELATIONS/CONFLUENCE/Confluence.glob
  • 9 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMITS/Pullbacks1.v
  • 8 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/MON.glob
  • 8 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/CCC/CCC1.glob
  • 8 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/CONSTRUCTIONS/SET_Equalizer.glob
  • 8 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/CONSTRUCTIONS/SETProperty.vo
  • 8 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/NT/YONEDA_LEMMA/YonedaEmbedding.glob
  • 8 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/CONSTRUCTIONS/SET_Exponents.glob
  • 8 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/FREYD_THEOREM/FAFT_Part2_Proof2.glob
  • 8 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/FUNCTOR/Comma_proj.vo
  • 8 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMITS/Comma_UA.glob
  • 8 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/NT/YONEDA_LEMMA/Map0_dup1.vo
  • 8 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMITS/Iso_Limit.glob
  • 8 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/Dual.vo
  • 8 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/NT/Ntransformation.glob
  • 8 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/SETOID/MapProperty.vo
  • 8 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/FUNCTOR/FSC_inc.vo
  • 8 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/CCC/Diagonal.vo
  • 8 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/Hom_Equality.glob
  • 7 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/NT/HomFunctor_NT.vo
  • 7 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/HomFunctor2.v
  • 7 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMIT_CONSTRUCTIONS/Th_Limits.v
  • 7 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/SETOID/STRUCTURE/Inverses_Group.v
  • 7 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMIT_CONSTRUCTIONS/Pres_Limits.glob
  • 7 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMITS/Discr.glob
  • 7 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/FREYD_THEOREM/FAFT_SSC2.glob
  • 7 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/CONSTRUCTIONS/Binary_Products.v
  • 7 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMITS/Const.vo
  • 7 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/SET.vo
  • 7 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/CONSTRUCTIONS/SET_BinProds.glob
  • 7 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/SETOID/STRUCTURE/FreeMonoid.glob
  • 7 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMITS/Equalizers1.v
  • 7 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/CONSTRUCTIONS/SETProperty.glob
  • 7 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/CCC/FunOne.vo
  • 7 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/ONE.glob
  • 6 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/FUNCTOR/FunForget.vo
  • 6 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/SETOID/STRUCTURE/Group.vo
  • 6 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMIT_CONSTRUCTIONS/Th_Initial.v
  • 6 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/FUNCTOR/Dual_Functor.vo
  • 6 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/CCC/FunProd.v
  • 6 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/FullSubCat.vo
  • 6 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/NT/YONEDA_LEMMA/YonedaLemma.v
  • 6 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/CONSTRUCTIONS/CatProperty.v
  • 6 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/RELATIONS/CONFLUENCE/NEWMAN/Newman.vo
  • 6 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/Category.v
  • 6 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/FUNCTOR/FunFreeMon.glob
  • 6 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/RELATIONS/CONFLUENCE/TAIT/Tait.vo
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/RELATIONS/CONFLUENCE/Coherence.v
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/FUNCTOR/Comma.v
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/SETOID/BasicTypes.vo
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/FUNCTOR/Functor.v
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMITS/UniversalArrow.v
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMIT_CONSTRUCTIONS/Comma_Complete.v
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/NT/InterChangeLaw.v
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/CONSTRUCTIONS/SET_Terminal.vo
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/SETOID/Map.glob
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/Adjunction.v
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/NT/YONEDA_LEMMA/Map0_dup1.glob
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/FUNCTOR/IdCAT.vo
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/NT/CatFunct.v
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/CONSTRUCTIONS/SET_CCC.vo
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/FUNCTOR/HomFunctor.glob
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/RELATIONS/Relations.glob
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/Adj_UA.v
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/SETOID/STRUCTURE/Monoid.v
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/Dual.glob
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMITS/CoUniversalArrow.v
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMIT_CONSTRUCTIONS/HomFunctor_Continuous.v
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/CCC/Cartesian1.v
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/RELATIONS/Noetherian.vo
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/SETOID/Map.v
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/CONSTRUCTIONS/SET_Exponents.v
  • 5 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/SETOID/STRUCTURE/FreeMonoid.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/FUNCTOR/CAT.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMIT_CONSTRUCTIONS/SET_Complete.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMITS/FunForget_UA.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/SETOID/Setoid_prop.glob
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMITS/CoLimit.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/NT/Setoid_dup2.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/PROD.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMITS/Limit.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/FUNCTOR/CAT.glob
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMITS/Products1.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/FUNCTOR/PROD_proj.glob
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/MON.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/FUNCTOR/Setoid_dup1.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/Limit_Adj.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/SETOID/Setoid.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/RELATIONS/CONFLUENCE/NEWMAN/Newman.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/CONSTRUCTIONS/Equalizers.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/CONSTRUCTIONS/SET_Pullback.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/NT/NatIso.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/RELATIONS/Relations.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/NT/YONEDA_LEMMA/YonedaEmbedding.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/SETOID/Setoid.glob
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/FullSubCat.glob
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/PermCat.vo
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/FUNCTOR/FunFreeMon.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/FUNCTOR/FunctorProperty.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/RELATIONS/CONFLUENCE/TAIT/Tait.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/SETOID/Map2.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/CONSTRUCTIONS/SETProperty.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMITS/Discr.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/CONSTRUCTIONS/SET_Equalizer.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/CONSTRUCTIONS/SET_BinProds.v
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/SETOID/SetoidPROD.glob
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/CCC/Diagonal.glob
  • 4 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/ONE.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/RELATIONS/CONFLUENCE/Confluence.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMITS/Iso_Limit.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMITS/Const.glob
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/FUNCTOR/Comma_proj.glob
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/LeftAdj_Iso.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMITS/Comma_UA.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/CCC/CCC1.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/Hom_Equality.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/SETOID/SetoidPROD.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/FUNCTOR/HomFunctor.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/CONSTRUCTIONS/Pullbacks.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/Dual.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/FREYD_THEOREM/FAFT_Part2_Proof2.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/FUNCTOR/PROD_proj.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/NT/HomFunctor_NT.glob
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/FUNCTOR/FSC_inc.glob
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/NT/Ntransformation.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/SETOID/Single.vo
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/SET.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/FUNCTOR/Dual_Functor.glob
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/CONSTRUCTIONS/Exponents.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/SETOID/Setoid_prop.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/NT/Category_dup2.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMIT_CONSTRUCTIONS/Pres_Limits.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/CCC/FunOne.glob
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/FREYD_THEOREM/FAFT_Part1.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/FUNCTOR/Category_dup1.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/CONSTRUCTIONS/Products.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/SET.glob
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/RELATIONS/CONFLUENCE/TAIT/Tait.glob
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/RELATIONS/Noetherian.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/NT/YONEDA_LEMMA/Functor_dup1.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/SETOID/MapProperty.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/CCC/Terminal1.glob
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/FUNCTOR/Comma_proj.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/CCC/Diagonal.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/PermCat.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/SETOID/STRUCTURE/Group.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/FREYD_THEOREM/FAFT_SSC2.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/LIMITS/Const.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/NT/HomFunctor_NT.v
  • 3 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/FUNCTOR/FSC_inc.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/SETOID/MapProperty.glob
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/CCC/FunOne.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/FUNCTOR/FunForget.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/FullSubCat.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/FUNCTOR/Dual_Functor.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/CCC/Terminal1.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/CONSTRUCTIONS/SET_Terminal.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/CONSTRUCTIONS/CCC.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/FUNCTOR/IdCAT.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/Adj_FunFreeMon.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/FUNCTOR/FunForget.glob
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/SETOID/STRUCTURE/Group.glob
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/SETOID/Single.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/RELATIONS/Noetherian.glob
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/CONSTRUCTIONS/SET_CCC.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/SETOID/BasicTypes.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/FUNCTOR/IdCAT.glob
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/CONSTRUCTIONS/CCC.glob
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/NT/YONEDA_LEMMA/Map0_dup1.v
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/RELATIONS/CONFLUENCE/NEWMAN/Newman.glob
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/CONSTRUCTIONS/SET_Terminal.glob
  • 2 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/PermCat.glob
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/ADJUNCTION/Adj_FunFreeMon.glob
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/CATEGORY_THEORY/CATEGORY/CONSTRUCTIONS/SET_CCC.glob
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/SETOID/Single.glob
  • 1 K ../ocaml-base-compiler.4.03.0/lib/coq/user-contrib/ConCaT/SETOID/BasicTypes.glob

Uninstall 🧹

Command
opam remove -y coq-concat.8.5.0
Return code
0
Missing removes
none
Wrong removes
none

Sources are on GitHub © Guillaume Claret 🐣