ยซ Up

hott 8.9 13 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.9.0       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
ocamlfind           1.9.6       A library manager for OCaml
# opam file:
opam-version: "2.0"
maintainer: "Jason Gross <jgross@mit.edu>"
homepage: "http://homotopytypetheory.org/"
bug-reports: "https://github.com/HoTT/Coq-HoTT/issues"
license: "BSD-2-Clause"
build: [
  ["bash" "-c" "./autogen.sh -skip-submodules || :"]
  ["./configure" "COQBIN=%{bin}%" "--prefix=%{prefix}%"]
  [make "-j%{jobs}%"]
]
install: [make "install"]
depends: [
  "conf-autoconf" {build}
  "ocaml"
  "ocamlfind" {build}
  "coq" {>= "8.9" & < "8.10~"}
]
authors: ["The Coq-HoTT Development Team"]
dev-repo: "git+https://github.com/HoTT/Coq-HoTT.git"
synopsis: "The Homotopy Type Theory library"
tags: ["logpath:HoTT"]
url {
  src: "https://github.com/HoTT/Coq-HoTT/archive/V8.9.tar.gz"
  checksum: "sha512=3ddb4adf11897d2a47a62144cba2f1bbbfb8ffd8613ffff66b92b3968a02c2f4cf59524ebcb83c0dc7d4aee9bc9a2f7ea283fecd3cd5ea0b3b2a15bb17607a29"
}

Lint

Command
true
Return code
0

Dry install ๐Ÿœ๏ธ

Dry install with the current Coq version:

Command
opam install -y --show-action coq-hott.8.9 coq.8.9.0
Return code
0

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

Command
true
Return code
0

Install dependencies

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

Install ๐Ÿš€

Command
opam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y -v coq-hott.8.9 coq.8.9.0
Return code
0
Duration
13 m 0 s

Installation size

Total: 65 M

  • 5 M ../ocaml-base-compiler.4.03.0/share/hott/theories/Spaces/No/Addition.vo
  • 4 M ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/Colimits/Flattening.vo
  • 2 M ../ocaml-base-compiler.4.03.0/share/hott/theories/Modalities/Topological.vo
  • 2 M ../ocaml-base-compiler.4.03.0/share/hott/theories/Modalities/Lex.vo
  • 2 M ../ocaml-base-compiler.4.03.0/share/hott/theories/Modalities/Closed.vo
  • 2 M ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/Spheres.vo
  • 2 M ../ocaml-base-compiler.4.03.0/share/hott/theories/Modalities/Nullification.vo
  • 1 M ../ocaml-base-compiler.4.03.0/share/hott/theories/Modalities/Accessible.vo
  • 1 M ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/Colimits/Pushout.vo
  • 1 M ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/implementations/binary_naturals.vo
  • 1 M ../ocaml-base-compiler.4.03.0/share/hott/theories/Modalities/Open.vo
  • 980 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Spaces/Finite.vo
  • 890 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Modalities/Fracture.vo
  • 798 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Spaces/BAut/Bool.vo
  • 754 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/TwoSphere.vo
  • 736 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories.vo
  • 695 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Category.vo
  • 688 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Grothendieck/ToSet/Morphisms.vo
  • 661 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Modalities/Modality.vo
  • 635 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/V.vo
  • 599 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Modalities/Identity.vo
  • 584 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/Truncations.vo
  • 584 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Spaces/No.vo
  • 561 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Modalities/Notnot.vo
  • 557 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Spaces/No/Core.vo
  • 555 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Modalities/ReflectiveSubuniverse.vo
  • 546 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Basics/PathGroupoids.vo
  • 531 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/Coeq.vo
  • 491 K ../ocaml-base-compiler.4.03.0/share/hott/theories/PropResizing/Nat.vo
  • 466 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Modalities/Localization.vo
  • 450 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Spaces/Card.vo
  • 441 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Types/Sum.vo
  • 424 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Types/Universe.vo
  • 399 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Tests.vo
  • 388 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Modalities/ReflectiveSubuniverse.glob
  • 386 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/Colimits/Colimit.vo
  • 384 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Adjoint.vo
  • 381 K ../ocaml-base-compiler.4.03.0/share/hott/contrib/Freudenthal.vo
  • 374 K ../ocaml-base-compiler.4.03.0/share/hott/contrib/HoTTBook.vo
  • 357 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Functor.vo
  • 354 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Category/Paths.vo
  • 344 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Spaces/Universe.vo
  • 331 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/implementations/natpair_integers.vo
  • 327 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Category/Sigma.vo
  • 312 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Category/Sigma/Univalent.vo
  • 296 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Comma.vo
  • 294 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Functor/Paths.vo
  • 280 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Types/Paths.vo
  • 276 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Idempotents.vo
  • 272 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Pseudofunctor.vo
  • 270 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/implementations/natpair_integers.glob
  • 257 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Spaces/No/Core.glob
  • 257 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Tactics/EquivalenceInduction.vo
  • 252 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Spaces/BAut.vo
  • 245 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/LaxComma/CoreLaws.vo
  • 239 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Spaces/BAut/Bool/IncoherentIdempotent.vo
  • 229 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Basics/PathGroupoids.glob
  • 225 K ../ocaml-base-compiler.4.03.0/share/hott/contrib/HoTTBookExercises.vo
  • 223 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Types/Sigma.vo
  • 221 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/Colimits/CommutativeSquares.vo
  • 213 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Pointed.vo
  • 211 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/theory/premetric.vo
  • 198 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Fibrations.vo
  • 196 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/Colimits/Colimit_Sigma.vo
  • 193 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Pseudofunctor/RewriteLaws.vo
  • 189 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Types/Prod.vo
  • 187 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Idempotents.glob
  • 176 K ../ocaml-base-compiler.4.03.0/share/hott/contrib/HoTTBookExercises.glob
  • 175 K ../ocaml-base-compiler.4.03.0/share/hott/theories/PropResizing/Nat.glob
  • 174 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/theory/premetric.glob
  • 172 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Adjoint/Pointwise.vo
  • 171 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/Suspension.vo
  • 168 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Basics/Equivalences.vo
  • 167 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Pullback.vo
  • 162 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/V.glob
  • 162 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/Flattening.vo
  • 160 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/interfaces/abstract_algebra.vo
  • 158 K ../ocaml-base-compiler.4.03.0/share/hott/theories/EquivalenceVarieties.vo
  • 155 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/InitialTerminalCategory/Pseudofunctors.vo
  • 155 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/theory/rationals.vo
  • 153 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Spaces/BAut/Cantor.vo
  • 150 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/NaturalTransformation.vo
  • 148 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Types/Sum.glob
  • 148 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/implementations/binary_naturals.glob
  • 146 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/orders/semirings.glob
  • 143 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/Colimits/Coequalizer.vo
  • 142 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Extensions.vo
  • 139 K ../ocaml-base-compiler.4.03.0/share/hott/theories/UnivalenceVarieties.vo
  • 139 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/orders/semirings.vo
  • 139 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Types/Sigma.glob
  • 138 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Adjoint/HomCoercions.vo
  • 137 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Spaces/Finite.glob
  • 135 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Category/Morphisms.vo
  • 134 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Factorization.vo
  • 133 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/LaxComma/Core.vo
  • 132 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/PseudonaturalTransformation/Core.vo
  • 131 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Comma/Core.vo
  • 128 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Adjoint/Functorial/Laws.vo
  • 127 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/implementations/field_of_fractions.vo
  • 125 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/implementations/field_of_fractions.glob
  • 121 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/interfaces/orders.vo
  • 121 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Basics/Overture.vo
  • 117 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Types/Paths.glob
  • 116 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/interfaces/canonical_names.vo
  • 114 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/Colimits/Diagram.vo
  • 114 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/theory/rationals.glob
  • 114 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Modalities/Modality.glob
  • 106 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Algebra/ooGroup.vo
  • 105 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Comma/Functorial.vo
  • 104 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Category/Morphisms.glob
  • 99 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Types/Forall.vo
  • 97 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Category/Sigma/Univalent.glob
  • 97 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/LaxComma/CoreParts.vo
  • 95 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/tactics/ring_quote.vo
  • 93 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/Circle.vo
  • 92 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/quotient.vo
  • 92 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Structure.vo
  • 91 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Basics/Equivalences.glob
  • 91 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/implementations/peano_naturals.glob
  • 91 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Types/Universe.glob
  • 91 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/implementations/peano_naturals.vo
  • 89 K ../ocaml-base-compiler.4.03.0/share/hott/theories/EquivalenceVarieties.glob
  • 88 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Factorization.glob
  • 87 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/Coeq.glob
  • 87 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Comma/ProjectionFunctors.vo
  • 85 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/Pushout.vo
  • 84 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Spaces/BAut/Rigid.vo
  • 84 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/Join.vo
  • 81 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/Suspension.glob
  • 81 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Fibrations.glob
  • 81 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/UniversalProperties.glob
  • 79 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Modalities/Localization.glob
  • 78 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/LaxComma.vo
  • 78 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Tactics/EquivalenceInduction.glob
  • 76 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/tactics/ring_pol.vo
  • 76 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Spaces/No/Addition.glob
  • 74 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/ExponentialLaws/Law2/Law.vo
  • 73 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/LaxComma/CoreLaws.glob
  • 73 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/orders/lattices.glob
  • 71 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Extensions.glob
  • 69 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Pointed.glob
  • 69 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/PseudonaturalTransformation.vo
  • 69 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/theory/rings.vo
  • 68 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/interfaces/canonical_names.glob
  • 68 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Modalities/Lex.glob
  • 66 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/orders/orders.vo
  • 66 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Types/Prod.glob
  • 65 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/orders/rings.glob
  • 64 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/ExponentialLaws/Law4/Law.vo
  • 64 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Structure/IdentityPrinciple.vo
  • 64 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/Spheres.glob
  • 64 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Comma/InducedFunctors.vo
  • 63 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/NaturalTransformation/Composition.vo
  • 62 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/theory/rings.glob
  • 61 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/theory/naturals.vo
  • 61 K ../ocaml-base-compiler.4.03.0/share/hott/theories/DProp.vo
  • 61 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Tactics.vo
  • 60 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Spaces/BAut/Bool.glob
  • 60 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Adjoint/UnitCounitCoercions.vo
  • 59 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/theory/integers.vo
  • 58 K ../ocaml-base-compiler.4.03.0/share/hott/theories/EquivGroupoids.vo
  • 58 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Basics/Overture.glob
  • 58 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Types/Forall.glob
  • 58 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Spaces/Int.vo
  • 58 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/UniversalProperties.vo
  • 58 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/SemiSimplicialSets.vo
  • 58 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/LaxComma/CoreParts.glob
  • 57 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/Colimits/Flattening.glob
  • 56 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/ExponentialLaws/Law3/Law.vo
  • 56 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/ExponentialLaws/Law4.vo
  • 56 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Functor/Composition.vo
  • 55 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Spaces/BAut.glob
  • 55 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Grothendieck/PseudofunctorToCat.vo
  • 55 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/Colimits/Colimit.glob
  • 55 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/orders/nat_int.vo
  • 55 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/Connectedness.vo
  • 54 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/theory/fields.glob
  • 53 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/orders/orders.glob
  • 53 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Yoneda.vo
  • 51 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Limits.vo
  • 51 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/theory/int_abs.vo
  • 51 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/ExponentialLaws/Law4/Functors.vo
  • 51 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/orders/rings.vo
  • 51 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Functor/Pointwise/Properties.vo
  • 51 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/NaturalTransformation/Isomorphisms.vo
  • 50 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/orders/lattices.vo
  • 50 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Basics/UniverseLevel.vo
  • 50 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Adjoint/Functorial/Laws.glob
  • 49 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Category/Paths.glob
  • 49 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/tactics/ring_quote.glob
  • 49 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Functor/Attributes.vo
  • 49 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Functor/Pointwise.vo
  • 49 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Functor/Prod.vo
  • 48 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/theory/dec_fields.glob
  • 48 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Comma/ProjectionFunctors.glob
  • 47 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Adjoint/Composition/IdentityLaws.vo
  • 47 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Types/Wtype.vo
  • 47 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/FunctorCategory.vo
  • 47 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Adjoint/HomCoercions.glob
  • 47 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/tactics/ring_pol.glob
  • 46 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Pseudofunctor/RewriteLaws.glob
  • 46 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/orders/maps.vo
  • 46 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/theory/naturals.glob
  • 46 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Types/Arrow.vo
  • 46 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/theory/groups.glob
  • 46 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/epi.vo
  • 46 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/theory/fields.vo
  • 45 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Grothendieck/PseudofunctorToCat.glob
  • 45 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Adjoint/Composition/AssociativityLaw.vo
  • 44 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/quotient.glob
  • 44 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Limits/Core.vo
  • 44 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Spaces/Nat.vo
  • 43 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/theory/dec_fields.vo
  • 43 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Comma/Core.glob
  • 43 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/ProductLaws.vo
  • 43 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Tactics/RewriteModuloAssociativity.vo
  • 42 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Modalities/Fracture.glob
  • 42 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/FunctorCategory/Morphisms.vo
  • 42 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Modalities/Accessible.glob
  • 41 K ../ocaml-base-compiler.4.03.0/share/hott/theories/EquivGroupoids.glob
  • 41 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Pseudofunctor/Identity.vo
  • 41 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Spaces/No/Negation.vo
  • 41 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Adjoint/Functorial/Core.vo
  • 41 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Pullback.glob
  • 40 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/theory/lattices.vo
  • 40 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Functor/Prod/Universal.vo
  • 40 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/interfaces/abstract_algebra.glob
  • 40 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/NaturalTransformation/Composition/Core.vo
  • 40 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Adjoint/Composition.vo
  • 40 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/orders/maps.glob
  • 39 K ../ocaml-base-compiler.4.03.0/share/hott/theories/TruncType.vo
  • 38 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Comodalities/CoreflectiveSubuniverse.vo
  • 38 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Structure/Core.vo
  • 38 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Types/Bool.vo
  • 38 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Pseudofunctor/FromFunctor.vo
  • 38 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/NaturalTransformation/Composition/Laws.vo
  • 38 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/Flattening.glob
  • 37 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Adjoint/UniversalMorphisms/Core.vo
  • 37 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Constant.vo
  • 37 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Types/Equiv.vo
  • 37 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/SetCategory/Morphisms.vo
  • 36 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/theory/lattices.glob
  • 36 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/ExponentialLaws/Law2.vo
  • 35 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/theory/nat_distance.vo
  • 35 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Adjoint/Pointwise.glob
  • 35 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/Colimits/Pushout.glob
  • 35 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Adjoint/Composition/Core.vo
  • 35 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/LaxComma/Core.glob
  • 34 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Functor/Composition/Laws.vo
  • 34 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Comma/Functorial.glob
  • 34 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Functor/Composition/Functorial.vo
  • 34 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/ExponentialLaws/Law3.vo
  • 34 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Category/Sigma/OnMorphisms.glob
  • 34 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Grothendieck/ToSet/Univalent.vo
  • 34 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/implementations/pointwise.vo
  • 34 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Functor/Sum.vo
  • 33 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/theory/apartness.vo
  • 33 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HSet.vo
  • 33 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/ExponentialLaws/Law0.vo
  • 33 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/Init/Notations.vo
  • 33 K ../ocaml-base-compiler.4.03.0/share/hott/contrib/Freudenthal.glob
  • 33 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Algebra/ooGroup.glob
  • 33 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/SetCategory.vo
  • 33 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/KanExtensions.vo
  • 32 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Adjoint/UniversalMorphisms.vo
  • 32 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Adjoint/Functorial/Parts.vo
  • 32 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/ExponentialLaws/Law4/Functors.glob
  • 32 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/interfaces/integers.vo
  • 32 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/FreeIntQuotient.vo
  • 32 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/NaturalTransformation/Composition/Laws.glob
  • 32 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/HomotopyPreCategory.vo
  • 31 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/isomorphisms/rings.vo
  • 31 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Comma/InducedFunctors.glob
  • 31 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Category/Sigma/OnMorphisms.vo
  • 31 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/ExponentialLaws/Law1/Law.vo
  • 31 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Basics/Decidable.vo
  • 31 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Spaces/Universe.glob
  • 30 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HProp.vo
  • 30 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/theory/groups.vo
  • 30 K ../ocaml-base-compiler.4.03.0/share/hott/theories/FunextVarieties.vo
  • 30 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/interfaces/rationals.vo
  • 30 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/LaxComma/Notations.vo
  • 30 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/interfaces/orders.glob
  • 29 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Functor/Composition/Functorial/Core.vo
  • 29 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/implementations/hprop_lattice.vo
  • 29 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/Program/Tactics.vo
  • 29 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/ExponentialLaws/Law1.vo
  • 29 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Types/Equiv.glob
  • 29 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/tactics/ring_tac.vo
  • 29 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/theory/integers.glob
  • 29 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/orders/naturals.vo
  • 29 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Adjoint/UnitCounit.glob
  • 29 K ../ocaml-base-compiler.4.03.0/share/hott/theories/ObjectClassifier.vo
  • 29 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Grothendieck/ToSet.vo
  • 29 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Spaces/Int.glob
  • 29 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Types/Arrow.glob
  • 29 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/NaturalTransformation/Composition/Core.glob
  • 28 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/Truncations.glob
  • 28 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Comodalities/CoreflectiveSubuniverse.glob
  • 28 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/Connectedness.glob
  • 28 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Pseudofunctor/Core.vo
  • 28 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Adjoint/UnitCounitCoercions.glob
  • 28 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Pseudofunctor/FromFunctor.glob
  • 28 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/InitialTerminalCategory/Functors.vo
  • 28 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Category/Sum.vo
  • 28 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/ExponentialLaws/Law1/Functors.vo
  • 28 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/orders/nat_int.glob
  • 28 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/theory/int_abs.glob
  • 28 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Grothendieck/ToSet/Core.vo
  • 28 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Spaces/BAut/Cantor.glob
  • 28 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/orders/integers.vo
  • 27 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Algebra/Aut.vo
  • 27 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/NaturalTransformation/Paths.vo
  • 27 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Spaces/BAut/Rigid.glob
  • 27 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/NaturalTransformation/Isomorphisms.glob
  • 27 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/isomorphisms/rings.glob
  • 27 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Types/Record.vo
  • 26 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Functor/Paths.glob
  • 26 K ../ocaml-base-compiler.4.03.0/share/hott/theories/ObjectClassifier.glob
  • 26 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Adjoint/Composition/Core.glob
  • 26 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Functor/Pointwise/Core.vo
  • 26 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/implementations/bool.vo
  • 26 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Category/Sigma/Core.glob
  • 26 K ../ocaml-base-compiler.4.03.0/share/hott/theories/UnivalenceVarieties.glob
  • 26 K ../ocaml-base-compiler.4.03.0/share/hott/theories/FunextVarieties.glob
  • 25 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Modalities/Topological.glob
  • 25 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/epi.glob
  • 25 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/ExponentialLaws/Law3/Functors.vo
  • 25 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/interfaces/naturals.vo
  • 25 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Utf8.vo
  • 25 K ../ocaml-base-compiler.4.03.0/share/hott/theories/TruncType.glob
  • 25 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/NaturalTransformation/Identity.vo
  • 24 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Adjoint/Functorial/Parts.glob
  • 24 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Adjoint/UniversalMorphisms/Core.glob
  • 24 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/Colimits/Diagram.glob
  • 24 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/orders/dec_fields.vo
  • 24 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Adjoint/Paths.vo
  • 24 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Functor/Composition/Functorial/Attributes.vo
  • 23 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/Init/Peano.vo
  • 23 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/implementations/list.vo
  • 23 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Notations.vo
  • 23 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/theory/apartness.glob
  • 23 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Adjoint/UnitCounit.vo
  • 23 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/NaturalTransformation/Core.vo
  • 23 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/Colimits/CommutativeSquares.glob
  • 22 K ../ocaml-base-compiler.4.03.0/share/hott/theories/DProp.glob
  • 22 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Basics/Trunc.vo
  • 22 K ../ocaml-base-compiler.4.03.0/share/hott/contrib/HoTTBook.glob
  • 22 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Basics/Contractible.vo
  • 22 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Category/Core.vo
  • 22 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/Pushout.glob
  • 21 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/ExponentialLaws/Tactics.vo
  • 21 K ../ocaml-base-compiler.4.03.0/share/hott/theories/BoundedSearch.vo
  • 21 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HProp.glob
  • 21 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/KanExtensions/Functors.vo
  • 21 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/GroupoidCategory/Morphisms.vo
  • 21 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Limits/Functors.vo
  • 21 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Modalities/Nullification.glob
  • 21 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/FreeIntQuotient.glob
  • 21 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/TwoSphere.glob
  • 21 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Spectra/Coinductive.vo
  • 20 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/Circle.glob
  • 20 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Types/Unit.vo
  • 20 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/Colimits/Colimit_Sigma.glob
  • 20 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Types/Bool.glob
  • 20 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/CategoryOfSections/Core.vo
  • 20 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/KanExtensions/Core.vo
  • 19 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/ChainCategory.vo
  • 19 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Functor/Prod/Core.vo
  • 19 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/ExponentialLaws/Law2/Functors.vo
  • 19 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Constant.glob
  • 19 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/NaturalTransformation/Utf8.vo
  • 19 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Structure/Core.glob
  • 19 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Functor/Prod/Functorial.vo
  • 18 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/Init/Nat.vo
  • 18 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Functor/Utf8.vo
  • 18 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/FunctorCategory/Utf8.vo
  • 18 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Basics/UniverseLevel.glob
  • 18 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Yoneda.glob
  • 18 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Functor/Prod/Universal.glob
  • 18 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Pseudofunctor/Core.glob
  • 17 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/orders/dec_fields.glob
  • 17 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Adjoint/Composition/LawsTactic.vo
  • 17 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/ProductLaws.glob
  • 17 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Structure/IdentityPrinciple.glob
  • 17 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Tactics.glob
  • 17 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/SimplicialSets.vo
  • 17 K ../ocaml-base-compiler.4.03.0/share/hott/theories/UnivalenceImpliesFunext.vo
  • 17 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/tests/ring_tac.vo
  • 17 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/NaturalTransformation/Pointwise.vo
  • 17 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/Interval.vo
  • 17 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/SetCategory/Morphisms.glob
  • 17 K ../ocaml-base-compiler.4.03.0/share/hott/theories/UnivalenceImpliesFunext.glob
  • 17 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/InitialTerminalCategory/NaturalTransformations.vo
  • 17 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/theory/additional_operations.vo
  • 17 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/NaturalTransformation/Prod.vo
  • 17 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Functor/Attributes.glob
  • 17 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Spectra/Spectrum.vo
  • 16 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/DualFunctor.vo
  • 16 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/CategoryOfSections.vo
  • 16 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/PseudonaturalTransformation/Core.glob
  • 16 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Spaces/Nat.glob
  • 16 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/implementations/list.glob
  • 16 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/Init/Peano.glob
  • 16 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/implementations/assume_rationals.vo
  • 16 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/FundamentalPreGroupoidCategory.vo
  • 16 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Category/Sigma/OnObjects.vo
  • 16 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Basics/Contractible.glob
  • 16 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/orders/sum.vo
  • 16 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Category/Sigma/Core.vo
  • 16 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HSet.glob
  • 15 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/Init/Datatypes.vo
  • 15 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Modalities/Closed.glob
  • 15 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Functor/Prod/Core.glob
  • 15 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/GroupoidCategory.vo
  • 15 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Basics/Decidable.glob
  • 15 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Functor/Pointwise/Properties.glob
  • 15 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Modalities/Open.glob
  • 15 K ../ocaml-base-compiler.4.03.0/share/hott/theories/BoundedSearch.glob
  • 15 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Types/Record.glob
  • 15 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Adjoint/Functorial/Core.glob
  • 15 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Utf8.vo
  • 15 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Category/Prod.vo
  • 15 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Cat.vo
  • 14 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/Init/Decimal.vo
  • 14 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HoTT.vo
  • 14 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Basics/Trunc.glob
  • 14 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/GroupoidCategory/Core.vo
  • 14 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/InitialTerminalCategory/Core.vo
  • 14 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Adjoint/Hom.vo
  • 14 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/Init/Nat.glob
  • 14 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Functor/Notations.vo
  • 14 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Functor/Composition/Laws.glob
  • 14 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/NaturalTransformation/Paths.glob
  • 14 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Functor/Pointwise/Core.glob
  • 14 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/HomFunctor.vo
  • 14 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/theory/additional_operations.glob
  • 13 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/FunctorCategory/Functorial.vo
  • 13 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/NaturalTransformation/Identity.glob
  • 13 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Comma/Projection.vo
  • 13 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Types/Wtype.glob
  • 13 K ../ocaml-base-compiler.4.03.0/share/hott/theories/PropResizing/Truncations.vo
  • 13 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/ExponentialLaws.vo
  • 13 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Category/Objects.vo
  • 13 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/interfaces/monad.vo
  • 13 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Category/Core.glob
  • 13 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Grothendieck/ToSet/Morphisms.glob
  • 13 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/LaxComma/Utf8.vo
  • 13 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Functorish.vo
  • 13 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/FunctorCategory/Morphisms.glob
  • 13 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/IndiscreteCategory.vo
  • 13 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/Init/Specif.vo
  • 13 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/Colimits/MappingTelescope.vo
  • 13 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Functor/Composition/Functorial/Core.glob
  • 13 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/orders/integers.glob
  • 13 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Functor/Composition/Functorial/Attributes.glob
  • 12 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Tactics/RewriteModuloAssociativity.glob
  • 12 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Cat/Core.vo
  • 12 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/InitialTerminalCategory.vo
  • 12 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Functor/Core.vo
  • 12 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/NaturalTransformation/Prod.glob
  • 12 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Spaces/Card.glob
  • 11 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/tactics/ring_tac.glob
  • 11 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/surjective_factor.vo
  • 11 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Grothendieck/ToSet/Core.glob
  • 11 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/NaturalTransformation/Composition/Functorial.vo
  • 11 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Types/Unit.glob
  • 11 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Basics/Notations.vo
  • 11 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/NaturalTransformation/Core.glob
  • 11 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Comma/Dual.vo
  • 11 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/ExponentialLaws/Tactics.glob
  • 11 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Category/Utf8.vo
  • 11 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/Colimits/Colimit_Prod.vo
  • 11 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Profunctor.vo
  • 11 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Adjoint/Paths.glob
  • 11 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/SetCategory/Functors/SetProp.vo
  • 10 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Pseudofunctor/Identity.glob
  • 10 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Modalities/Identity.glob
  • 10 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Spectra/Coinductive.glob
  • 10 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/Init/Decimal.glob
  • 10 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/orders/naturals.glob
  • 10 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Functor/Prod/Functorial.glob
  • 10 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Spaces/Cantor.vo
  • 10 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/iso.vo
  • 10 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/NaturalTransformation/Sum.vo
  • 10 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/SetCategory/Functors.vo
  • 10 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/DualFunctor.glob
  • 9 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/InitialTerminalCategory/Functors.glob
  • 9 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Grothendieck/ToCat.vo
  • 9 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/Colimits/Coequalizer.glob
  • 9 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Types/Empty.vo
  • 9 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/DependentProduct.vo
  • 9 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Category/Pi.vo
  • 9 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/NaturalTransformation/Notations.vo
  • 9 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Category/Univalent.vo
  • 9 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Spaces/BAut/Bool/IncoherentIdempotent.glob
  • 9 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/unique_choice.vo
  • 9 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/TruncImpliesFunext.vo
  • 9 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Cat/Morphisms.vo
  • 9 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/ExponentialLaws/Law2/Law.glob
  • 9 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/Init/Specif.glob
  • 9 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Functor/Composition/Core.vo
  • 9 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/FunctorCategory/Core.vo
  • 9 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Profunctor/Representable.vo
  • 9 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/FunctorCategory/Dual.vo
  • 9 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Conjugation.vo
  • 9 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Grothendieck.vo
  • 9 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/theory/nat_distance.glob
  • 9 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/ExponentialLaws/Law2/Functors.glob
  • 9 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Functor/Sum.glob
  • 9 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Adjoint/Dual.vo
  • 9 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Grothendieck/ToSet/Univalent.glob
  • 8 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/NatCategory.vo
  • 8 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Adjoint/Utf8.vo
  • 8 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/SetCategory/Core.vo
  • 8 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Category/Notations.vo
  • 8 K ../ocaml-base-compiler.4.03.0/share/hott/theories/ExcludedMiddle.vo
  • 8 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Comma/Projection.glob
  • 8 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/HomFunctor.glob
  • 8 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Conjugation.glob
  • 8 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Spaces/No/Negation.glob
  • 8 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/GroupoidCategory/Dual.vo
  • 8 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Comma/Dual.glob
  • 8 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Adjoint/Composition/AssociativityLaw.glob
  • 8 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/Join.glob
  • 8 K ../ocaml-base-compiler.4.03.0/share/hott/theories/PropResizing/Truncations.glob
  • 8 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Limits/Core.glob
  • 8 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/implementations/hprop_lattice.glob
  • 8 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Tactics/BinderApply.vo
  • 7 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Adjoint/Composition/IdentityLaws.glob
  • 7 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Basics/Utf8.vo
  • 7 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/NaturalTransformation/Pointwise.glob
  • 7 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Adjoint/Notations.vo
  • 7 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/ExponentialLaws/Law1/Functors.glob
  • 7 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Adjoint/Composition/LawsTactic.glob
  • 7 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/FundamentalPreGroupoidCategory.glob
  • 7 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/Init/Logic_Type.vo
  • 7 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/ExponentialLaws/Law0.glob
  • 7 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/CategoryOfGroupoids.vo
  • 7 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/implementations/pointwise.glob
  • 7 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/interfaces/integers.glob
  • 7 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Category/Dual.vo
  • 7 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/Init/Logic_Type.glob
  • 7 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/NaturalTransformation/Dual.vo
  • 7 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Adjoint/Hom.glob
  • 7 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/ExponentialLaws/Law3/Functors.glob
  • 7 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Functor/Composition/Core.glob
  • 7 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Modalities/Notnot.glob
  • 7 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Category/Sigma/OnObjects.glob
  • 7 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Adjoint/Functorial.vo
  • 7 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/Init/Datatypes.glob
  • 7 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Cat/Core.glob
  • 7 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Algebra/ooAction.vo
  • 7 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/InitialTerminalCategory/Notations.vo
  • 6 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Adjoint/Identity.vo
  • 6 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Comma/Utf8.vo
  • 6 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/NaturalTransformation/Composition/Functorial.glob
  • 6 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Profunctor/Core.vo
  • 6 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/unique_choice.glob
  • 6 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/FunctorCategory/Functorial.glob
  • 6 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/InitialTerminalCategory/NaturalTransformations.glob
  • 6 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/HomotopyPreCategory.glob
  • 6 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/ExponentialLaws/Law4/Law.glob
  • 6 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/surjective_factor.glob
  • 6 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/Colimits.vo
  • 6 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Functor/Dual.vo
  • 6 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Profunctor/Identity.vo
  • 6 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/ExponentialLaws/Law3/Law.glob
  • 6 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/KanExtensions/Functors.glob
  • 6 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/Interval.glob
  • 6 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Profunctor/Utf8.vo
  • 6 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/tests/ring_tac.glob
  • 6 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Algebra/Aut.glob
  • 6 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/CategoryOfSections/Core.glob
  • 6 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/SetCategory/Functors/SetProp.glob
  • 6 K ../ocaml-base-compiler.4.03.0/share/hott/theories/PropResizing/PropResizing.vo
  • 6 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/interfaces/naturals.glob
  • 6 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Tactics/EvalIn.vo
  • 5 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Category/Prod.glob
  • 5 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/GroupoidCategory/Core.glob
  • 5 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Profunctor/Notations.vo
  • 5 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/Colimits/MappingTelescope.glob
  • 5 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Functorish.glob
  • 5 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/FunctorCategory/Notations.vo
  • 5 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Category/Pi.glob
  • 5 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/KanExtensions/Core.glob
  • 5 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Tests.glob
  • 5 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/IntervalImpliesFunext.vo
  • 5 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Adjoint/Core.vo
  • 5 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/InitialTerminalCategory/Pseudofunctors.glob
  • 5 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Comma/Notations.vo
  • 5 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/FunctorCategory/Dual.glob
  • 5 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Cat/Morphisms.glob
  • 5 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/ChainCategory.glob
  • 5 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Category/Subcategory.vo
  • 5 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Category/Strict.vo
  • 5 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/IndiscreteCategory.glob
  • 5 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/DiscreteCategory.vo
  • 5 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Category/Subcategory/Full.vo
  • 5 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Category/Objects.glob
  • 5 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Functor/Core.glob
  • 5 K ../ocaml-base-compiler.4.03.0/share/hott/theories/ExcludedMiddle.glob
  • 4 K ../ocaml-base-compiler.4.03.0/share/hott/theories/NullHomotopy.vo
  • 4 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Structure/Utf8.vo
  • 4 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Limits/Functors.glob
  • 4 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Category/Subcategory/Wide.vo
  • 4 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Tactics/BinderApply.glob
  • 4 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Utf8.glob
  • 4 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/Init/Logic.vo
  • 4 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/Colimits/Colimit_Prod.glob
  • 4 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Adjoint/Dual.glob
  • 4 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Category/Sum.glob
  • 4 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Types/Empty.glob
  • 4 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Spectra/Spectrum.glob
  • 4 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Category/Dual.glob
  • 4 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories.glob
  • 4 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/ExponentialLaws/Law1/Law.glob
  • 4 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/interfaces/rationals.glob
  • 3 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/NaturalTransformation/Dual.glob
  • 3 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/InitialTerminalCategory/Core.glob
  • 3 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Structure/Notations.vo
  • 3 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/iso.glob
  • 3 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/TruncImpliesFunext.glob
  • 3 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/FunctorCategory/Core.glob
  • 3 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/implementations/assume_rationals.glob
  • 3 K ../ocaml-base-compiler.4.03.0/share/hott/theories/UnivalenceAxiom.vo
  • 3 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HoTT.glob
  • 3 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/GroupoidCategory/Morphisms.glob
  • 3 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Functor/Dual.glob
  • 3 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Misc.vo
  • 3 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Types.vo
  • 3 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/GroupoidCategory/Dual.glob
  • 3 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/interfaces/monad.glob
  • 3 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Tactics/EvalIn.glob
  • 3 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Profunctor/Representable.glob
  • 3 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Spaces/Cantor.glob
  • 3 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/NaturalTransformation/Sum.glob
  • 3 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/orders/sum.glob
  • 3 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Grothendieck/ToCat.glob
  • 2 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/SimplicialSets.glob
  • 2 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Functor/Identity.vo
  • 2 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/SemiSimplicialSets.glob
  • 2 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/Unicode/Utf8_core.vo
  • 2 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/NatCategory.glob
  • 2 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/Init/Tactics.vo
  • 2 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/DependentProduct.glob
  • 2 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/CategoryOfGroupoids.glob
  • 2 K ../ocaml-base-compiler.4.03.0/bin/hoq-config
  • 2 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Basics.vo
  • 2 K ../ocaml-base-compiler.4.03.0/share/hott/theories/NullHomotopy.glob
  • 2 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Category/Utf8.glob
  • 2 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/SetCategory/Core.glob
  • 2 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/Init/Prelude.vo
  • 2 K ../ocaml-base-compiler.4.03.0/bin/hoqtop.byte
  • 2 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Category/Univalent.glob
  • 2 K ../ocaml-base-compiler.4.03.0/share/hott/theories/PropResizing/PropResizing.glob
  • 2 K ../ocaml-base-compiler.4.03.0/bin/hoqdep
  • 2 K ../ocaml-base-compiler.4.03.0/bin/hoqtop
  • 2 K ../ocaml-base-compiler.4.03.0/bin/hoqc
  • 2 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/Init/Prelude.glob
  • 2 K ../ocaml-base-compiler.4.03.0/bin/hoqchk
  • 2 K ../ocaml-base-compiler.4.03.0/share/hott/theories/FunextAxiom.vo
  • 2 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/LaxComma/Utf8.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/NaturalTransformation.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Profunctor/Core.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Adjoint.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Category.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Adjoint/Identity.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Profunctor/Identity.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Functor.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/Program/Tactics.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/IntervalImpliesFunext.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Classes/implementations/bool.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Functor/Identity.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/NaturalTransformation/Utf8.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Category/Notations.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Comma/Utf8.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/NaturalTransformation/Notations.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Functor/Utf8.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/Unicode/Utf8_core.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Algebra/ooAction.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Functor/Notations.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/NaturalTransformation/Composition.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/Unicode/Utf8.vo
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Comma.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Category/Sigma.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Notations.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Adjoint/Composition.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Functor/Composition.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/DiscreteCategory.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/FunctorCategory/Utf8.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/FunctorCategory.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Utf8.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Structure/Utf8.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Adjoint/Utf8.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Functor/Prod.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Adjoint/Notations.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Category/Strict.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Pseudofunctor.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/GroupoidCategory.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Types.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/InitialTerminalCategory.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/HIT/Colimits.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Adjoint/Core.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/ExponentialLaws.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Profunctor.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/Init/Logic.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Functor/Composition/Functorial.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Basics.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/FunctorCategory/Notations.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Structure.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Category/Subcategory/Full.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/SetCategory.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Profunctor/Notations.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/ExponentialLaws/Law3.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/ExponentialLaws/Law2.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/ExponentialLaws/Law1.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/ExponentialLaws/Law4.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Category/Subcategory.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Functor/Pointwise.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Grothendieck/ToSet.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Profunctor/Utf8.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/Bool/Bool.vo
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/KanExtensions.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/ZArith/README.txt
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/FSets/README.txt
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/Setoids/README.txt
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/PArith/README.txt
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/Strings/README.txt
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/Arith/README.txt
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/QArith/README.txt
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/Logic/README.txt
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/Vectors/README.txt
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/Bool/README.txt
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/Structures/README.txt
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/MSets/README.txt
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/Classes/README.txt
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/NArith/README.txt
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/Wellfounded/README.txt
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/Sets/README.txt
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/Numbers/README.txt
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/Reals/README.txt
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/Sorting/README.txt
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/Relations/README.txt
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/Lists/README.txt
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Limits.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Adjoint/Functorial.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Cat.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Grothendieck.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Category/Subcategory/Wide.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/InitialTerminalCategory/Notations.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/PseudonaturalTransformation.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/LaxComma.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Adjoint/UniversalMorphisms.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Spaces/No.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/SetCategory/Functors.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Structure/Notations.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/CategoryOfSections.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/LaxComma/Notations.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Categories/Comma/Notations.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/UnivalenceAxiom.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/FunextAxiom.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Misc.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Basics/Notations.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/Unicode/Utf8.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/theories/Basics/Utf8.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/Init/Tactics.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/Init/Notations.glob
  • 1 K ../ocaml-base-compiler.4.03.0/share/hott/coq/theories/Bool/Bool.glob

Uninstall ๐Ÿงน

Command
opam remove -y coq-hott.8.9
Return code
0
Missing removes
none
Wrong removes
none