ยซ Up

hott 8.11.dev 11 m 0 s ๐Ÿ†

Context

# Packages matching: installed
# Name              # Installed # Synopsis
base-bigarray       base
base-threads        base
base-unix           base
conf-findutils      1           Virtual package relying on findutils
conf-m4             1           Virtual package relying on m4
coq                 8.11.dev    Formal proof management system
num                 1.3         The legacy Num library for arbitrary-precision integer and rational arithmetic
ocaml               4.06.1      The OCaml compiler (virtual package)
ocaml-base-compiler 4.06.1      Official 4.06.1 release
ocaml-config        1           OCaml Switch Configuration
ocamlfind           1.8.1       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/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.11" & < "8.12~"}
]
authors: ["The Coq-HoTT Development Team"]
dev-repo: "git+https://github.com/HoTT/HoTT.git"
synopsis: "The Homotopy Type Theory library"
tags: [ "logpath:HoTT" ]
url {
  src: "git+https://github.com/HoTT/HoTT.git#V8.11"
}

Lint

Command
true
Return code
0

Dry install ๐Ÿœ๏ธ

Dry install with the current Coq version:

Command
opam install -y --show-action coq-hott.8.11.dev coq.8.11.dev
Return code
0

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

Command
true
Return code
0

Install dependencies

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

Install ๐Ÿš€

Command
opam list; echo; ulimit -Sv 16000000; timeout 2h opam install -y coq-hott.8.11.dev coq.8.11.dev
Return code
0
Duration
11 m 0 s

Installation size

Total: 93 M

  • 10 M ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/Torus/TorusEquivCircles.vo
  • 8 M ../ocaml-base-compiler.4.06.1/share/hott/theories/Homotopy/HomotopyGroup.vo
  • 5 M ../ocaml-base-compiler.4.06.1/share/hott/theories/HIT/Spheres.vo
  • 4 M ../ocaml-base-compiler.4.06.1/share/hott/theories/Homotopy/CayleyDickson.vo
  • 4 M ../ocaml-base-compiler.4.06.1/share/hott/theories/Colimits/Colimit_Flattening.vo
  • 3 M ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/BAut/Bool.vo
  • 3 M ../ocaml-base-compiler.4.06.1/share/hott/theories/Cubical/PathCube.vo
  • 2 M ../ocaml-base-compiler.4.06.1/share/hott/theories/Homotopy/ClassifyingSpace.vo
  • 2 M ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/No/Addition.vo
  • 1 M ../ocaml-base-compiler.4.06.1/share/hott/theories/Colimits/Colimit_Pushout.vo
  • 1004 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Colimits/Colimit_Pushout_Flattening.vo
  • 851 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Homotopy/BlakersMassey.vo
  • 754 K ../ocaml-base-compiler.4.06.1/share/hott/theories/HIT/TwoSphere.vo
  • 732 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Category.vo
  • 712 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories.vo
  • 671 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Homotopy/EMSpace.vo
  • 669 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Grothendieck/ToSet/Morphisms.vo
  • 659 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Algebra/AbelianGroup.vo
  • 658 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Modalities/ReflectiveSubuniverse.vo
  • 598 K ../ocaml-base-compiler.4.06.1/share/hott/theories/HIT/V.vo
  • 591 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Homotopy/Suspension.vo
  • 555 K ../ocaml-base-compiler.4.06.1/share/hott/theories/HIT/Coeq.vo
  • 537 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Colimits/Pushout.vo
  • 531 K ../ocaml-base-compiler.4.06.1/share/hott/theories/PropResizing/Nat.vo
  • 524 K ../ocaml-base-compiler.4.06.1/share/hott/theories/WildCat/Sum.vo
  • 520 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Basics/PathGroupoids.vo
  • 518 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Homotopy/HSpaceS1.vo
  • 517 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/No.vo
  • 454 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/No/Core.vo
  • 449 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/Card.vo
  • 444 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/Finite.vo
  • 433 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Types/Sum.vo
  • 428 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Types/Universe.vo
  • 420 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Limits/Pullback.vo
  • 419 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/Universe.vo
  • 404 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Adjoint.vo
  • 403 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Extensions.vo
  • 400 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Pointed/Loops.vo
  • 372 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/implementations/natpair_integers.vo
  • 364 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Modalities/ReflectiveSubuniverse.glob
  • 360 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Category/Paths.vo
  • 355 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Category/Sigma.vo
  • 339 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Category/Sigma/Univalent.vo
  • 327 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Functor.vo
  • 292 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Colimits/Quotient.vo
  • 278 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Comma.vo
  • 278 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/BAut.vo
  • 277 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Homotopy/Join.vo
  • 273 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/interfaces/abstract_algebra.vo
  • 272 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Diagrams/Cocone.vo
  • 270 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Pseudofunctor.vo
  • 270 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/implementations/natpair_integers.glob
  • 269 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Types/Paths.vo
  • 268 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/BAut/Cantor.vo
  • 263 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Idempotents.vo
  • 260 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Tactics/EquivalenceInduction.vo
  • 259 K ../ocaml-base-compiler.4.06.1/share/hott/contrib/HoTTBook.vo
  • 258 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/No/Core.glob
  • 252 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Functor/Paths.vo
  • 250 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/LaxComma/CoreLaws.vo
  • 245 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Modalities/Modality.vo
  • 239 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Basics/PathGroupoids.glob
  • 234 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Cubical/PathSquare.vo
  • 232 K ../ocaml-base-compiler.4.06.1/share/hott/theories/WildCat/Equiv.vo
  • 231 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Modalities/Descent.vo
  • 228 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/theory/ua_third_isomorphism.vo
  • 220 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Homotopy/Freudenthal.vo
  • 219 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Diagrams/CommutativeSquares.vo
  • 214 K ../ocaml-base-compiler.4.06.1/share/hott/contrib/HoTTBookExercises.vo
  • 213 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/theory/premetric.vo
  • 204 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Types/Sigma.vo
  • 202 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Diagrams/Cone.vo
  • 200 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Pointed/pSusp.vo
  • 199 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Colimits/Colimit_Sigma.vo
  • 186 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Pseudofunctor/RewriteLaws.vo
  • 185 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Basics/Equivalences.vo
  • 183 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Types/Prod.vo
  • 182 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Colimits/MappingCylinder.vo
  • 177 K ../ocaml-base-compiler.4.06.1/share/hott/contrib/HoTTBookExercises.glob
  • 177 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Fibrations.vo
  • 175 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/theory/premetric.glob
  • 174 K ../ocaml-base-compiler.4.06.1/share/hott/theories/PropResizing/Nat.glob
  • 170 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Colimits/Colimit.vo
  • 164 K ../ocaml-base-compiler.4.06.1/share/hott/theories/HIT/Flattening.vo
  • 163 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/implementations/binary_naturals.vo
  • 163 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Idempotents.glob
  • 160 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Basics/Overture.vo
  • 156 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/NaturalTransformation.vo
  • 154 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Cubical/DPathCube.vo
  • 154 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Extensions.glob
  • 154 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Metatheory/UnivalenceVarieties.vo
  • 153 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/InitialTerminalCategory/Pseudofunctors.vo
  • 151 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Types/Sum.glob
  • 150 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/theory/rationals.vo
  • 149 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Adjoint/Functorial/Laws.vo
  • 149 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/implementations/binary_naturals.glob
  • 148 K ../ocaml-base-compiler.4.06.1/share/hott/theories/HIT/V.glob
  • 147 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Adjoint/HomCoercions.vo
  • 146 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/orders/semirings.glob
  • 146 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Modalities/Lex.vo
  • 144 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Adjoint/Pointwise.vo
  • 144 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/Finite.glob
  • 138 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/orders/semirings.vo
  • 136 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/BAut/Rigid.vo
  • 135 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Cubical/DPath.vo
  • 135 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Factorization.vo
  • 135 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/LaxComma/Core.vo
  • 134 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Category/Morphisms.vo
  • 134 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Types/Sigma.glob
  • 130 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Algebra/Group.vo
  • 130 K ../ocaml-base-compiler.4.06.1/share/hott/theories/HIT/Circle.vo
  • 129 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Algebra/Subgroup.vo
  • 126 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Colimits/Colimit_Coequalizer.vo
  • 126 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/interfaces/canonical_names.vo
  • 125 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/implementations/field_of_fractions.glob
  • 125 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Comma/Core.vo
  • 122 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/implementations/field_of_fractions.vo
  • 120 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/theory/ua_second_isomorphism.vo
  • 119 K ../ocaml-base-compiler.4.06.1/share/hott/theories/WildCat/Core.vo
  • 117 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Types/Paths.glob
  • 117 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Cubical/PathCube.glob
  • 114 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/theory/rationals.glob
  • 113 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/interfaces/orders.vo
  • 113 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Algebra/ooGroup.vo
  • 111 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Diagrams/Diagram.vo
  • 109 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Colimits/Pushout.glob
  • 108 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Modalities/Modality.glob
  • 108 K ../ocaml-base-compiler.4.06.1/share/hott/theories/WildCat/FunctorCat.vo
  • 107 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/theory/ua_quotient_algebra.vo
  • 106 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Homotopy/BlakersMassey.glob
  • 105 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/PseudonaturalTransformation/Core.vo
  • 104 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Types/Forall.vo
  • 101 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Category/Morphisms.glob
  • 99 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Category/Sigma/Univalent.glob
  • 99 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Comma/Functorial.vo
  • 97 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/LaxComma/CoreParts.vo
  • 97 K ../ocaml-base-compiler.4.06.1/share/hott/theories/HIT/Coeq.glob
  • 96 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/tactics/ring_quote.vo
  • 95 K ../ocaml-base-compiler.4.06.1/share/hott/theories/HIT/quotient.vo
  • 94 K ../ocaml-base-compiler.4.06.1/share/hott/theories/WildCat/Yoneda.vo
  • 93 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Cubical/PathSquare.glob
  • 93 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Structure.vo
  • 92 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Basics/Equivalences.glob
  • 92 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Types/Universe.glob
  • 91 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/implementations/peano_naturals.glob
  • 91 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/LaxComma.vo
  • 91 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Homotopy/Smash.vo
  • 89 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/BAut/Bool/IncoherentIdempotent.vo
  • 89 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Modalities/Localization.vo
  • 89 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/implementations/peano_naturals.vo
  • 87 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Modalities/Separated.vo
  • 85 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Modalities/Descent.glob
  • 81 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/theory/ua_first_isomorphism.vo
  • 81 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/interfaces/ua_algebra.vo
  • 81 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Modalities/Localization.glob
  • 81 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/UniversalProperties.glob
  • 80 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Comma/ProjectionFunctors.vo
  • 79 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Tactics/EquivalenceInduction.glob
  • 78 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/interfaces/canonical_names.glob
  • 77 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/theory/ua_homomorphism.vo
  • 76 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/No/Addition.glob
  • 76 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Cubical/DPathSquare.vo
  • 73 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/LaxComma/CoreLaws.glob
  • 73 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/orders/lattices.glob
  • 73 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Modalities/Fracture.vo
  • 71 K ../ocaml-base-compiler.4.06.1/share/hott/theories/WildCat/EquivGpd.vo
  • 71 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/theory/rings.vo
  • 70 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Modalities/Lex.glob
  • 70 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Homotopy/Suspension.glob
  • 70 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Modalities/Topological.vo
  • 69 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/NaturalTransformation/Composition.vo
  • 68 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/orders/orders.vo
  • 68 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Limits/Limit.vo
  • 68 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/tactics/ring_pol.vo
  • 68 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Cubical/DPath.glob
  • 67 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/ExponentialLaws/Law2/Law.vo
  • 65 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/orders/rings.glob
  • 65 K ../ocaml-base-compiler.4.06.1/share/hott/theories/HIT/Spheres.glob
  • 65 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Types/Prod.glob
  • 64 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Structure/IdentityPrinciple.vo
  • 64 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/theory/naturals.vo
  • 64 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Fibrations.glob
  • 64 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/interfaces/abstract_algebra.glob
  • 64 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Pointed/Loops.glob
  • 64 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Factorization.glob
  • 63 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Adjoint/UnitCounitCoercions.vo
  • 63 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/Torus/TorusHomotopy.vo
  • 62 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/theory/rings.glob
  • 61 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Functor/Composition.vo
  • 60 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/theory/integers.vo
  • 60 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/BAut/Bool.glob
  • 60 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Limits/Pullback.glob
  • 59 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Types/Forall.glob
  • 59 K ../ocaml-base-compiler.4.06.1/share/hott/theories/DProp.vo
  • 59 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Basics/Overture.glob
  • 59 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/theory/ua_quotient_algebra.glob
  • 58 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/orders/rings.vo
  • 57 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Pointed/pSusp.glob
  • 57 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Modalities/Accessible.vo
  • 57 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Truncations/Connectedness.vo
  • 56 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/LaxComma/CoreParts.glob
  • 56 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/SemiSimplicialSets.vo
  • 56 K ../ocaml-base-compiler.4.06.1/share/hott/theories/WildCat/Core.glob
  • 56 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/Torus/Torus.vo
  • 55 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Tactics.vo
  • 55 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/theory/ua_isomorphic.vo
  • 55 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/theory/fields.glob
  • 55 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/orders/nat_int.vo
  • 55 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Algebra/Group.glob
  • 55 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/theory/int_abs.vo
  • 55 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Comma/InducedFunctors.vo
  • 54 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/orders/lattices.vo
  • 54 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Grothendieck/PseudofunctorToCat.vo
  • 53 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/orders/orders.glob
  • 53 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Yoneda.vo
  • 53 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Functor/Pointwise/Properties.vo
  • 53 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Functor/Pointwise.vo
  • 53 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/ExponentialLaws/Law4/Law.vo
  • 53 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Adjoint/Composition.vo
  • 52 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/orders/maps.vo
  • 52 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Functor/Attributes.vo
  • 52 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/UniversalProperties.vo
  • 51 K ../ocaml-base-compiler.4.06.1/share/hott/theories/WildCat/Prod.vo
  • 51 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Functor/Prod.vo
  • 51 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Cubical/DPathCube.glob
  • 51 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/ExponentialLaws/Law4.vo
  • 50 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/ExponentialLaws/Law3/Law.vo
  • 50 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/NaturalTransformation/Isomorphisms.vo
  • 50 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Adjoint/Functorial/Laws.glob
  • 50 K ../ocaml-base-compiler.4.06.1/share/hott/theories/WildCat/TwoOneCat.vo
  • 50 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Basics/Trunc.vo
  • 50 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Category/Paths.glob
  • 50 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Truncations/Core.vo
  • 49 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Pointed/pTrunc.vo
  • 49 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Adjoint/Composition/AssociativityLaw.vo
  • 49 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/tactics/ring_quote.glob
  • 49 K ../ocaml-base-compiler.4.06.1/share/hott/theories/HIT/epi.vo
  • 48 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Comma/ProjectionFunctors.glob
  • 48 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Algebra/QuotientGroup.vo
  • 48 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/theory/dec_fields.glob
  • 48 K ../ocaml-base-compiler.4.06.1/share/hott/theories/WildCat/Equiv.glob
  • 48 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Types/Equiv.vo
  • 48 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/theory/groups.glob
  • 47 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/tactics/ring_pol.glob
  • 47 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/theory/fields.vo
  • 47 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Adjoint/HomCoercions.glob
  • 47 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/ExponentialLaws/Law4/Functors.vo
  • 46 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Pseudofunctor/RewriteLaws.glob
  • 46 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Homotopy/Smash.glob
  • 46 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/theory/ua_homomorphism.glob
  • 46 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/theory/naturals.glob
  • 46 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/PseudonaturalTransformation.vo
  • 46 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Types/Wtype.vo
  • 46 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Adjoint/Composition/IdentityLaws.vo
  • 45 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Grothendieck/PseudofunctorToCat.glob
  • 45 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Types/Arrow.vo
  • 45 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/FunctorCategory.vo
  • 45 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/Nat.vo
  • 45 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/Int/LoopExp.vo
  • 45 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/theory/ua_subalgebra.vo
  • 45 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/theory/ua_second_isomorphism.glob
  • 45 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/ProductLaws.vo
  • 44 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Basics/UniverseLevel.vo
  • 44 K ../ocaml-base-compiler.4.06.1/share/hott/theories/HIT/quotient.glob
  • 44 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/Pos/Core.vo
  • 44 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Homotopy/CayleyDickson.glob
  • 44 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Homotopy/WhiteheadsPrinciple.vo
  • 43 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/theory/dec_fields.vo
  • 43 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Algebra/AbelianGroup.glob
  • 43 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Pseudofunctor/Identity.vo
  • 43 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/theory/ua_prod_algebra.vo
  • 43 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/theory/lattices.vo
  • 42 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Adjoint/Functorial/Core.vo
  • 42 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Colimits/Colimit_Flattening.glob
  • 42 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Modalities/Fracture.glob
  • 42 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Comma/Core.glob
  • 42 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/NaturalTransformation/Composition/Laws.vo
  • 42 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Colimits/Quotient.glob
  • 41 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Limits.vo
  • 41 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Equiv/PathSplit.vo
  • 41 K ../ocaml-base-compiler.4.06.1/share/hott/theories/TruncType.vo
  • 41 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/NaturalTransformation/Composition/Core.vo
  • 41 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Functor/Prod/Universal.vo
  • 41 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/theory/ua_third_isomorphism.glob
  • 41 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/theory/groups.vo
  • 40 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Modalities/CoreflectiveSubuniverse.vo
  • 40 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/BAut.glob
  • 40 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/orders/maps.glob
  • 40 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Cubical/DPathSquare.glob
  • 39 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Homotopy/ClassifyingSpace.glob
  • 39 K ../ocaml-base-compiler.4.06.1/share/hott/theories/WildCat/EquivGpd.glob
  • 39 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Functor/Composition/Laws.vo
  • 39 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/Pos/Core.glob
  • 39 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Adjoint/Functorial/Parts.vo
  • 38 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Homotopy/Join.glob
  • 38 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Tactics/RewriteModuloAssociativity.vo
  • 38 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Adjoint/Composition/Core.vo
  • 38 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Types/Bool.vo
  • 38 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Pseudofunctor/FromFunctor.vo
  • 38 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Constant.vo
  • 38 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/LaxComma/Notations.vo
  • 38 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/ExponentialLaws/Law2.vo
  • 38 K ../ocaml-base-compiler.4.06.1/share/hott/theories/HIT/Flattening.glob
  • 38 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/theory/apartness.vo
  • 37 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/theory/nat_distance.vo
  • 37 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/Int/LoopExp.glob
  • 37 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/FunctorCategory/Morphisms.vo
  • 37 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Structure/Core.vo
  • 37 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Homotopy/EMSpace.glob
  • 37 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Limits/Core.vo
  • 37 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/categories/ua_category.vo
  • 36 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/theory/ua_first_isomorphism.glob
  • 36 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/theory/lattices.glob
  • 36 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/implementations/pointwise.vo
  • 36 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/Int/Spec.vo
  • 36 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/No/Negation.vo
  • 35 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Adjoint/Pointwise.glob
  • 35 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Adjoint/UniversalMorphisms/Core.vo
  • 35 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Pointed/pEquiv.vo
  • 34 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/LaxComma/Core.glob
  • 34 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Comma/Functorial.glob
  • 34 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Functor/Composition/Functorial.vo
  • 34 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Category/Sigma/OnMorphisms.glob
  • 34 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Modalities/Closed.vo
  • 34 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Colimits/Colimit_Pushout.glob
  • 34 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/ExponentialLaws/Law3.vo
  • 34 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Functor/Sum.vo
  • 34 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/isomorphisms/rings.vo
  • 34 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Grothendieck/ToSet/Univalent.vo
  • 34 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/SetCategory/Morphisms.vo
  • 33 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Algebra/ooGroup.glob
  • 33 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/Init/Notations.vo
  • 33 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Modalities/Separated.glob
  • 33 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Algebra/Subgroup.glob
  • 33 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/HomotopyPreCategory.vo
  • 33 K ../ocaml-base-compiler.4.06.1/share/hott/theories/ObjectClassifier.vo
  • 33 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/implementations/hprop_lattice.vo
  • 33 K ../ocaml-base-compiler.4.06.1/share/hott/theories/HIT/FreeIntQuotient.vo
  • 33 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/interfaces/integers.vo
  • 32 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/interfaces/ua_congruence.vo
  • 32 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/implementations/bool.vo
  • 32 K ../ocaml-base-compiler.4.06.1/share/hott/theories/HSet.vo
  • 32 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/tactics/ring_tac.vo
  • 32 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/ExponentialLaws/Law4/Functors.glob
  • 32 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Algebra/Aut.vo
  • 32 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/NaturalTransformation/Composition/Laws.glob
  • 32 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Category/Sigma/OnMorphisms.vo
  • 32 K ../ocaml-base-compiler.4.06.1/share/hott/theories/WildCat/Opposite.vo
  • 31 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Homotopy/Pi1S1.vo
  • 31 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/orders/naturals.vo
  • 31 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Colimits/Colimit.glob
  • 31 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/Int/Spec.glob
  • 31 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Adjoint/UniversalMorphisms.vo
  • 31 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Comma/InducedFunctors.glob
  • 31 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Types/Equiv.glob
  • 31 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/Int/Core.vo
  • 31 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/Universe.glob
  • 31 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Truncations/Connectedness.glob
  • 30 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/SetCategory.vo
  • 30 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Modalities/Accessible.glob
  • 30 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Pseudofunctor/Core.vo
  • 30 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Basics/Decidable.vo
  • 30 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/interfaces/orders.glob
  • 29 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/implementations/ne_list.vo
  • 29 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Modalities/Open.vo
  • 29 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/theory/integers.glob
  • 29 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/interfaces/rationals.vo
  • 29 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Adjoint/UnitCounit.glob
  • 29 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Types/Arrow.glob
  • 29 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Colimits/MappingCylinder.glob
  • 29 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Diagrams/ConstantDiagram.vo
  • 29 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/NaturalTransformation/Composition/Core.glob
  • 28 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/Pos/Spec.vo
  • 28 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/ExponentialLaws/Law1.vo
  • 28 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Adjoint/UnitCounitCoercions.glob
  • 28 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/theory/ua_prod_algebra.glob
  • 28 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Grothendieck/ToSet.vo
  • 28 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Basics/Trunc.glob
  • 28 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/KanExtensions.vo
  • 28 K ../ocaml-base-compiler.4.06.1/share/hott/theories/WildCat/NatTrans.vo
  • 28 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Pseudofunctor/FromFunctor.glob
  • 28 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Modalities/CoreflectiveSubuniverse.glob
  • 28 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/ExponentialLaws/Law0.vo
  • 28 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Metatheory/FunextVarieties.vo
  • 28 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/orders/nat_int.glob
  • 28 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/theory/int_abs.glob
  • 28 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/implementations/list.vo
  • 28 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Diagrams/Cocone.glob
  • 28 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/BAut/Cantor.glob
  • 27 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/InitialTerminalCategory/Functors.vo
  • 27 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Truncations/Core.glob
  • 27 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/BAut/Rigid.glob
  • 27 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/Program/Tactics.vo
  • 27 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Category/Sum.vo
  • 27 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/NaturalTransformation/Isomorphisms.glob
  • 27 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/isomorphisms/rings.glob
  • 27 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Tests.vo
  • 27 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Functor/Composition/Functorial/Core.vo
  • 27 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/NaturalTransformation/Paths.vo
  • 27 K ../ocaml-base-compiler.4.06.1/share/hott/theories/ObjectClassifier.glob
  • 26 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Utf8.vo
  • 26 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Pointed/pMap.vo
  • 26 K ../ocaml-base-compiler.4.06.1/share/hott/theories/WildCat/Yoneda.glob
  • 26 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Adjoint/Composition/Core.glob
  • 26 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Pointed/pFiber.vo
  • 26 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Diagrams/Cone.glob
  • 26 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Pointed/Core.vo
  • 26 K ../ocaml-base-compiler.4.06.1/share/hott/theories/HIT/Circle.glob
  • 26 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/ExponentialLaws/Law1/Law.vo
  • 26 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/orders/integers.vo
  • 26 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Category/Sigma/Core.glob
  • 26 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Metatheory/FunextVarieties.glob
  • 26 K ../ocaml-base-compiler.4.06.1/share/hott/theories/WildCat/Prod.glob
  • 26 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/Torus/TorusEquivCircles.glob
  • 26 K ../ocaml-base-compiler.4.06.1/share/hott/theories/TruncType.glob
  • 25 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Grothendieck/ToSet/Core.vo
  • 25 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Homotopy/HomotopyGroup.glob
  • 25 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/NaturalTransformation/Identity.vo
  • 25 K ../ocaml-base-compiler.4.06.1/share/hott/theories/HIT/epi.glob
  • 25 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Notations.vo
  • 25 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/ExponentialLaws/Law1/Functors.vo
  • 25 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Adjoint/UnitCounit.vo
  • 25 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/interfaces/naturals.vo
  • 25 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Functor/Composition/Functorial/Attributes.vo
  • 25 K ../ocaml-base-compiler.4.06.1/share/hott/theories/PathAny.glob
  • 25 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/orders/dec_fields.vo
  • 25 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Homotopy/HSpace.vo
  • 25 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/ExponentialLaws/Law3/Functors.vo
  • 24 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Functor/Paths.glob
  • 24 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Adjoint/Functorial/Parts.glob
  • 24 K ../ocaml-base-compiler.4.06.1/share/hott/theories/HProp.vo
  • 24 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Modalities/Topological.glob
  • 24 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spectra/Coinductive.vo
  • 24 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Adjoint/UniversalMorphisms/Core.glob
  • 24 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/interfaces/ua_algebra.glob
  • 24 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Functor/Pointwise/Core.vo
  • 24 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Modalities/Nullification.vo
  • 23 K ../ocaml-base-compiler.4.06.1/share/hott/theories/HoTT.vo
  • 23 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/theory/apartness.glob
  • 23 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Basics/Contractible.vo
  • 23 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Metatheory/UnivalenceVarieties.glob
  • 23 K ../ocaml-base-compiler.4.06.1/share/hott/theories/BoundedSearch.vo
  • 23 K ../ocaml-base-compiler.4.06.1/share/hott/contrib/HoTTBook.glob
  • 23 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/theory/ua_subalgebra.glob
  • 22 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/NaturalTransformation/Core.vo
  • 22 K ../ocaml-base-compiler.4.06.1/share/hott/theories/DProp.glob
  • 22 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Diagrams/Diagram.glob
  • 22 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/Init/Decimal.vo
  • 22 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/tests/ring_tac.vo
  • 22 K ../ocaml-base-compiler.4.06.1/share/hott/theories/WildCat/Type.vo
  • 22 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/Init/Peano.vo
  • 22 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/ChainCategory.vo
  • 22 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Diagrams/CommutativeSquares.glob
  • 21 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/interfaces/ua_setalgebra.vo
  • 21 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Category/Core.vo
  • 21 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spectra/Spectrum.vo
  • 21 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/NaturalTransformation/Utf8.vo
  • 21 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Functor/Prod/Core.vo
  • 21 K ../ocaml-base-compiler.4.06.1/share/hott/theories/HIT/TwoSphere.glob
  • 21 K ../ocaml-base-compiler.4.06.1/share/hott/theories/HIT/FreeIntQuotient.glob
  • 20 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/ExponentialLaws/Tactics.vo
  • 20 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Functor/Utf8.vo
  • 20 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Adjoint/Paths.vo
  • 20 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/SimplicialSets.vo
  • 20 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/implementations/ne_list.glob
  • 20 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/FunctorCategory/Utf8.vo
  • 20 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Pointed/pType.vo
  • 20 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/Int/Core.glob
  • 20 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Types/Bool.glob
  • 20 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Colimits/Colimit_Sigma.glob
  • 19 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Types/Unit.vo
  • 19 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Pointed/pHomotopy.vo
  • 19 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/CategoryOfSections/Core.vo
  • 19 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/ExponentialLaws/Law2/Functors.vo
  • 19 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/theory/ua_isomorphic.glob
  • 19 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Constant.glob
  • 19 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/KanExtensions/Functors.vo
  • 19 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/Init/Nat.vo
  • 19 K ../ocaml-base-compiler.4.06.1/share/hott/theories/HProp.glob
  • 19 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/theory/additional_operations.vo
  • 19 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/DualFunctor.vo
  • 19 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/Pos/Spec.glob
  • 18 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Structure/Core.glob
  • 18 K ../ocaml-base-compiler.4.06.1/share/hott/theories/WildCat/EmptyCat.vo
  • 18 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/implementations/family_prod.vo
  • 18 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Basics/Contractible.glob
  • 18 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Basics/UniverseLevel.glob
  • 18 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Equiv/Relational.vo
  • 18 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Functor/Prod/Universal.glob
  • 18 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Yoneda.glob
  • 18 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/implementations/list.glob
  • 18 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/NaturalTransformation/Prod.vo
  • 18 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Pointed/pEquiv.glob
  • 18 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/orders/sum.vo
  • 18 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Pseudofunctor/Core.glob
  • 17 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Limits/Functors.vo
  • 17 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/orders/dec_fields.glob
  • 17 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Diagrams/ParallelPair.vo
  • 17 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/implementations/assume_rationals.vo
  • 17 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/ProductLaws.glob
  • 17 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Metatheory/UnivalenceImpliesFunext.glob
  • 17 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Structure/IdentityPrinciple.glob
  • 17 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/NaturalTransformation/Pointwise.vo
  • 17 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Tactics.glob
  • 17 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/KanExtensions/Core.vo
  • 17 K ../ocaml-base-compiler.4.06.1/share/hott/theories/WildCat/Induced.vo
  • 17 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Metatheory/UnivalenceImpliesFunext.vo
  • 17 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Utf8.vo
  • 17 K ../ocaml-base-compiler.4.06.1/share/hott/theories/HIT/Interval.vo
  • 17 K ../ocaml-base-compiler.4.06.1/share/hott/theories/PathAny.vo
  • 17 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Adjoint/Composition/LawsTactic.vo
  • 17 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/SetCategory/Morphisms.glob
  • 17 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Functor/Prod/Functorial.vo
  • 17 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/InitialTerminalCategory/NaturalTransformations.vo
  • 17 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Functor/Attributes.glob
  • 16 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/FundamentalPreGroupoidCategory.vo
  • 16 K ../ocaml-base-compiler.4.06.1/share/hott/theories/WildCat/FunctorCat.glob
  • 16 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/PseudonaturalTransformation/Core.glob
  • 16 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Diagrams/DDiagram.vo
  • 16 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Category/Sigma/Core.vo
  • 16 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Limits/Limit.glob
  • 16 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/Nat.glob
  • 16 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/CategoryOfSections.vo
  • 16 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/Init/Peano.glob
  • 16 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Functor/Notations.vo
  • 16 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Category/Sigma/OnObjects.vo
  • 16 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Adjoint/Hom.vo
  • 15 K ../ocaml-base-compiler.4.06.1/share/hott/theories/HSet.glob
  • 15 K ../ocaml-base-compiler.4.06.1/share/hott/theories/WildCat/Sigma.vo
  • 15 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Functor/Prod/Core.glob
  • 15 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/Init/Datatypes.vo
  • 15 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Basics/Decidable.glob
  • 15 K ../ocaml-base-compiler.4.06.1/share/hott/theories/BoundedSearch.glob
  • 15 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Functor/Pointwise/Properties.glob
  • 15 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Cat.vo
  • 15 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Adjoint/Functorial/Core.glob
  • 15 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/GroupoidCategory.vo
  • 14 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Equiv/Relational.glob
  • 14 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Equiv/PathSplit.glob
  • 14 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/Init/Decimal.glob
  • 14 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/FunctorCategory/Functorial.vo
  • 14 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/Torus/Torus.glob
  • 14 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/NaturalTransformation/Paths.glob
  • 14 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/Init/Nat.glob
  • 14 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Functor/Composition/Laws.glob
  • 14 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Pointed/pTrunc.glob
  • 14 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/GroupoidCategory/Core.vo
  • 14 K ../ocaml-base-compiler.4.06.1/share/hott/theories/WildCat/Forall.vo
  • 14 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Types/Wtype.glob
  • 14 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Functor/Pointwise/Core.glob
  • 14 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/theory/additional_operations.glob
  • 14 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Category/Prod.vo
  • 14 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/InitialTerminalCategory/Core.vo
  • 13 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/interfaces/monad.vo
  • 13 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/NaturalTransformation/Identity.glob
  • 13 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Category/Objects.vo
  • 13 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Colimits/SpanPushout.vo
  • 13 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Homotopy/WhiteheadsPrinciple.glob
  • 13 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Colimits/SpanPushout.glob
  • 13 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Basics/Notations.vo
  • 13 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Grothendieck/ToSet/Morphisms.glob
  • 13 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/HomFunctor.vo
  • 13 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Category/Core.glob
  • 13 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/FunctorCategory/Morphisms.glob
  • 13 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/ExponentialLaws.vo
  • 13 K ../ocaml-base-compiler.4.06.1/share/hott/theories/WildCat/NatTrans.glob
  • 13 K ../ocaml-base-compiler.4.06.1/share/hott/theories/HIT/surjective_factor.vo
  • 13 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Functor/Composition/Functorial/Core.glob
  • 13 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/orders/integers.glob
  • 13 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/Init/Specif.vo
  • 13 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/LaxComma/Utf8.vo
  • 13 K ../ocaml-base-compiler.4.06.1/share/hott/theories/PropResizing/ImpredicativeTruncation.vo
  • 13 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Functor/Composition/Functorial/Attributes.glob
  • 13 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Functorish.vo
  • 12 K ../ocaml-base-compiler.4.06.1/share/hott/theories/WildCat/Opposite.glob
  • 12 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Comma/Projection.vo
  • 12 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Functor/Core.vo
  • 12 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Tactics/RewriteModuloAssociativity.glob
  • 12 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Diagrams/Sequence.vo
  • 12 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Cat/Core.vo
  • 12 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Modalities/Nullification.glob
  • 12 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/InitialTerminalCategory.vo
  • 12 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/IndiscreteCategory.vo
  • 12 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/Int/Equiv.glob
  • 12 K ../ocaml-base-compiler.4.06.1/share/hott/theories/HIT/iso.vo
  • 12 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/NaturalTransformation/Prod.glob
  • 12 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Pointed/Core.glob
  • 12 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Colimits/Colimit_Pushout_Flattening.glob
  • 12 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/Card.glob
  • 12 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Profunctor.vo
  • 12 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Homotopy/HSpaceS1.glob
  • 11 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/tactics/ring_tac.glob
  • 11 K ../ocaml-base-compiler.4.06.1/share/hott/theories/WildCat/TwoOneCat.glob
  • 11 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Metatheory/TruncImpliesFunext.vo
  • 11 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Colimits/Colimit_Prod.vo
  • 11 K ../ocaml-base-compiler.4.06.1/share/hott/theories/HIT/unique_choice.vo
  • 11 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Types/Unit.glob
  • 11 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/NaturalTransformation/Composition/Functorial.vo
  • 11 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/Cantor.vo
  • 11 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/NaturalTransformation/Core.glob
  • 11 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Grothendieck/ToSet/Core.glob
  • 11 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Algebra/Congruence.vo
  • 11 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/ExponentialLaws/Tactics.glob
  • 11 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Algebra/QuotientGroup.glob
  • 11 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Pseudofunctor/Identity.glob
  • 11 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Algebra/Z.vo
  • 10 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spectra/Coinductive.glob
  • 10 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Diagrams/Span.vo
  • 10 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/interfaces/ua_congruence.glob
  • 10 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/Int/Equiv.vo
  • 10 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Category/Utf8.vo
  • 10 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/NaturalTransformation/Sum.vo
  • 10 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/orders/naturals.glob
  • 10 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/SetCategory/Functors/SetProp.vo
  • 10 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Functor/Prod/Functorial.glob
  • 10 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/DualFunctor.glob
  • 10 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/SetCategory/Functors.vo
  • 10 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Comma/Dual.vo
  • 10 K ../ocaml-base-compiler.4.06.1/share/hott/theories/HIT/SetCone.vo
  • 10 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/GroupoidCategory/Morphisms.vo
  • 10 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/implementations/family_prod.glob
  • 9 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/InitialTerminalCategory/Functors.glob
  • 9 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Algebra/ooAction.vo
  • 9 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Grothendieck/ToCat.vo
  • 9 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/DependentProduct.vo
  • 9 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Profunctor/Representable.vo
  • 9 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Category/Pi.vo
  • 9 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Functor/Composition/Core.vo
  • 9 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/NatCategory.vo
  • 9 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Cat/Morphisms.vo
  • 9 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Types/Empty.vo
  • 9 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/Init/Specif.glob
  • 9 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/ExponentialLaws/Law2/Law.glob
  • 9 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/BAut/Bool/IncoherentIdempotent.glob
  • 9 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Category/Univalent.vo
  • 9 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/NaturalTransformation/Notations.vo
  • 9 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Modalities/Notnot.vo
  • 9 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Equiv/BiInv.vo
  • 9 K ../ocaml-base-compiler.4.06.1/share/hott/theories/PropResizing/ImpredicativeTruncation.glob
  • 9 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/theory/nat_distance.glob
  • 9 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/categories/ua_category.glob
  • 9 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/FunctorCategory/Dual.vo
  • 9 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/ExponentialLaws/Law2/Functors.glob
  • 9 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Functor/Sum.glob
  • 9 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Grothendieck/ToSet/Univalent.glob
  • 8 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Adjoint/Paths.glob
  • 8 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/FunctorCategory/Core.vo
  • 8 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Diagrams/DDiagram.glob
  • 8 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Pointed/pMap.glob
  • 8 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Comma/Projection.glob
  • 8 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Grothendieck.vo
  • 8 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/No/Negation.glob
  • 8 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Pointed.vo
  • 8 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Adjoint/Utf8.vo
  • 8 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Adjoint/Dual.vo
  • 8 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Adjoint/Composition/AssociativityLaw.glob
  • 8 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Comma/Dual.glob
  • 8 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Limits/Equalizer.vo
  • 8 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Modalities/Closed.glob
  • 8 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Category/Notations.vo
  • 8 K ../ocaml-base-compiler.4.06.1/share/hott/theories/ExcludedMiddle.vo
  • 8 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Modalities/Identity.vo
  • 8 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Limits/Core.glob
  • 8 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/HomFunctor.glob
  • 8 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/implementations/hprop_lattice.glob
  • 8 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Adjoint/Composition/IdentityLaws.glob
  • 8 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/GroupoidCategory/Dual.vo
  • 8 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/SetCategory/Core.vo
  • 8 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Modalities/Open.glob
  • 7 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/Init/Logic_Type.vo
  • 7 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Colimits/Colimit_Coequalizer.glob
  • 7 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/ExponentialLaws/Law1/Functors.glob
  • 7 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/NaturalTransformation/Pointwise.glob
  • 7 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/FundamentalPreGroupoidCategory.glob
  • 7 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Adjoint/Composition/LawsTactic.glob
  • 7 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Pointed/pFiber.glob
  • 7 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/ExponentialLaws/Law0.glob
  • 7 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/interfaces/integers.glob
  • 7 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Basics/Utf8.vo
  • 7 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Homotopy/Wedge.vo
  • 7 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Pointed/pHomotopy.glob
  • 7 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/CategoryOfGroupoids.vo
  • 7 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Adjoint/Notations.vo
  • 7 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Tactics/BinderApply.vo
  • 7 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/implementations/pointwise.glob
  • 7 K ../ocaml-base-compiler.4.06.1/share/hott/theories/WildCat/Forall.glob
  • 7 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/Init/Logic_Type.glob
  • 7 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Truncations.vo
  • 7 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Adjoint/Hom.glob
  • 7 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/ExponentialLaws/Law3/Functors.glob
  • 7 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Category/Sigma/OnObjects.glob
  • 7 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Category/Dual.vo
  • 7 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/Init/Datatypes.glob
  • 7 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Functor/Composition/Core.glob
  • 7 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Cat/Core.glob
  • 7 K ../ocaml-base-compiler.4.06.1/share/hott/theories/WildCat/Induced.glob
  • 6 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Adjoint/Identity.vo
  • 6 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Adjoint/Functorial.vo
  • 6 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Homotopy/Freudenthal.glob
  • 6 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/NaturalTransformation/Composition/Functorial.glob
  • 6 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/InitialTerminalCategory/Notations.vo
  • 6 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/Torus/TorusHomotopy.glob
  • 6 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/FunctorCategory/Functorial.glob
  • 6 K ../ocaml-base-compiler.4.06.1/share/hott/theories/HIT/unique_choice.glob
  • 6 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Pointed/pType.glob
  • 6 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Comma/Utf8.vo
  • 6 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/NaturalTransformation/Dual.vo
  • 6 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/HomotopyPreCategory.glob
  • 6 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Profunctor/Core.vo
  • 6 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/InitialTerminalCategory/NaturalTransformations.glob
  • 6 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/ExponentialLaws/Law4/Law.glob
  • 6 K ../ocaml-base-compiler.4.06.1/share/hott/theories/HIT/surjective_factor.glob
  • 6 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/ExponentialLaws/Law3/Law.glob
  • 6 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/tests/ring_tac.glob
  • 6 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/KanExtensions/Functors.glob
  • 6 K ../ocaml-base-compiler.4.06.1/share/hott/theories/WildCat/Type.glob
  • 6 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/interfaces/naturals.glob
  • 6 K ../ocaml-base-compiler.4.06.1/share/hott/theories/HIT/Interval.glob
  • 6 K ../ocaml-base-compiler.4.06.1/share/hott/theories/WildCat/Sigma.glob
  • 6 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Functor/Dual.vo
  • 6 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Limits/Equalizer.glob
  • 5 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Profunctor/Identity.vo
  • 5 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Tactics/EvalIn.vo
  • 5 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Category/Prod.glob
  • 5 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/GroupoidCategory/Core.glob
  • 5 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/SetCategory/Functors/SetProp.glob
  • 5 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Homotopy/HSpace.glob
  • 5 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Profunctor/Utf8.vo
  • 5 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Functorish.glob
  • 5 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Diagrams/Graph.vo
  • 5 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Category/Pi.glob
  • 5 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Algebra/Aut.glob
  • 5 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/KanExtensions/Core.glob
  • 5 K ../ocaml-base-compiler.4.06.1/share/hott/theories/WildCat/UnitCat.vo
  • 5 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/CategoryOfSections/Core.glob
  • 5 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Diagrams/Sequence.glob
  • 5 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/FunctorCategory/Notations.vo
  • 5 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/InitialTerminalCategory/Pseudofunctors.glob
  • 5 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/FunctorCategory/Dual.glob
  • 5 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Profunctor/Notations.vo
  • 5 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Cat/Morphisms.glob
  • 5 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/ChainCategory.glob
  • 5 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/interfaces/ua_setalgebra.glob
  • 5 K ../ocaml-base-compiler.4.06.1/share/hott/theories/HoTT.glob
  • 5 K ../ocaml-base-compiler.4.06.1/share/hott/theories/PropResizing/PropResizing.vo
  • 5 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Adjoint/Core.vo
  • 5 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Comma/Notations.vo
  • 5 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Category/Strict.vo
  • 5 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/IndiscreteCategory.glob
  • 5 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Diagrams/ConstantDiagram.glob
  • 5 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Functor/Core.glob
  • 5 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Category/Objects.glob
  • 5 K ../ocaml-base-compiler.4.06.1/share/hott/theories/ExcludedMiddle.glob
  • 5 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Tests.glob
  • 4 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Metatheory/Core.vo
  • 4 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Metatheory/IntervalImpliesFunext.vo
  • 4 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Category/Subcategory.vo
  • 4 K ../ocaml-base-compiler.4.06.1/share/hott/theories/NullHomotopy.vo
  • 4 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/DiscreteCategory.vo
  • 4 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Limits/Functors.glob
  • 4 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Category/Subcategory/Full.vo
  • 4 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/Init/Logic.vo
  • 4 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Equiv/BiInv.glob
  • 4 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Structure/Utf8.vo
  • 4 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Tactics/BinderApply.glob
  • 4 K ../ocaml-base-compiler.4.06.1/share/hott/theories/WildCat/Sum.glob
  • 4 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spectra/Spectrum.glob
  • 4 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Category/Subcategory/Wide.vo
  • 4 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Adjoint/Dual.glob
  • 4 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Category/Sum.glob
  • 4 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Colimits/Colimit_Prod.glob
  • 4 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Types/Empty.glob
  • 4 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/ExponentialLaws/Law1/Law.glob
  • 4 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Utf8.glob
  • 4 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Category/Dual.glob
  • 4 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories.glob
  • 4 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/interfaces/rationals.glob
  • 3 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Metatheory/TruncImpliesFunext.glob
  • 3 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/InitialTerminalCategory/Core.glob
  • 3 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/FunctorCategory/Core.glob
  • 3 K ../ocaml-base-compiler.4.06.1/share/hott/theories/WildCat.vo
  • 3 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/NaturalTransformation/Dual.glob
  • 3 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/NatCategory.glob
  • 3 K ../ocaml-base-compiler.4.06.1/share/hott/theories/HIT/iso.glob
  • 3 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/implementations/assume_rationals.glob
  • 3 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Cubical.vo
  • 3 K ../ocaml-base-compiler.4.06.1/share/hott/theories/WildCat/Paths.vo
  • 3 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/Int.vo
  • 3 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Structure/Notations.vo
  • 3 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/Cantor.glob
  • 3 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/GroupoidCategory/Morphisms.glob
  • 3 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Homotopy/Pi1S1.glob
  • 3 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Functor/Dual.glob
  • 3 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/GroupoidCategory/Dual.glob
  • 3 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Types.vo
  • 3 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/interfaces/monad.glob
  • 3 K ../ocaml-base-compiler.4.06.1/share/hott/theories/UnivalenceAxiom.vo
  • 3 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Tactics/EvalIn.glob
  • 3 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Profunctor/Representable.glob
  • 3 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Misc.vo
  • 3 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/orders/sum.glob
  • 3 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Homotopy/Wedge.glob
  • 3 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/SimplicialSets.glob
  • 3 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/NaturalTransformation/Sum.glob
  • 3 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Grothendieck/ToCat.glob
  • 2 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/SemiSimplicialSets.glob
  • 2 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Functor/Identity.vo
  • 2 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/Unicode/Utf8_core.vo
  • 2 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Diagrams/ParallelPair.glob
  • 2 K ../ocaml-base-compiler.4.06.1/bin/hoq-config
  • 2 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/DependentProduct.glob
  • 2 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/CategoryOfGroupoids.glob
  • 2 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/Init/Tactics.vo
  • 2 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/Pos.vo
  • 2 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Tactics/Nameless.vo
  • 2 K ../ocaml-base-compiler.4.06.1/share/hott/theories/NullHomotopy.glob
  • 2 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Basics.vo
  • 2 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Category/Utf8.glob
  • 2 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Diagrams/Span.glob
  • 2 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/SetCategory/Core.glob
  • 2 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/Init/Prelude.vo
  • 2 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Category/Univalent.glob
  • 2 K ../ocaml-base-compiler.4.06.1/bin/hoqtop.byte
  • 2 K ../ocaml-base-compiler.4.06.1/bin/hoqidetop
  • 2 K ../ocaml-base-compiler.4.06.1/bin/hoqdep
  • 2 K ../ocaml-base-compiler.4.06.1/bin/hoqtop
  • 2 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/Init/Prelude.glob
  • 2 K ../ocaml-base-compiler.4.06.1/bin/hoqc
  • 2 K ../ocaml-base-compiler.4.06.1/bin/hoqchk
  • 2 K ../ocaml-base-compiler.4.06.1/share/hott/theories/PropResizing/PropResizing.glob
  • 2 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/LaxComma/Utf8.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Modalities/Notnot.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/NaturalTransformation.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/FunextAxiom.vo
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Profunctor/Core.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Adjoint.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Category.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/WildCat/UnitCat.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Algebra/Z.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Adjoint/Identity.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Profunctor/Identity.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Metatheory/IntervalImpliesFunext.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Functor.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/Program/Tactics.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Algebra/Congruence.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/HIT/SetCone.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Modalities/Identity.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Classes/implementations/bool.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Functor/Identity.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/NaturalTransformation/Utf8.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Metatheory/Core.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Category/Notations.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Comma/Utf8.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/NaturalTransformation/Notations.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Functor/Utf8.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/WildCat/EmptyCat.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/Unicode/Utf8_core.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Functor/Notations.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/NaturalTransformation/Composition.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/WildCat/Paths.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Comma.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Category/Sigma.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Notations.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/WildCat.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/Unicode/Utf8.vo
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Adjoint/Composition.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Functor/Composition.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/DiscreteCategory.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Algebra/ooAction.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/FunctorCategory/Utf8.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/FunctorCategory.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Utf8.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Structure/Utf8.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Adjoint/Utf8.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Functor/Prod.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Tactics/Nameless.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Adjoint/Notations.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Category/Strict.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Pseudofunctor.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/GroupoidCategory.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/InitialTerminalCategory.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Adjoint/Core.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Types.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/ExponentialLaws.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Diagrams/Graph.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Profunctor.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/Init/Logic.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Pointed.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Functor/Composition/Functorial.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Basics.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/FunctorCategory/Notations.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Structure.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Category/Subcategory/Full.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/SetCategory.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Profunctor/Notations.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/ExponentialLaws/Law3.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/ExponentialLaws/Law2.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/ExponentialLaws/Law1.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/ExponentialLaws/Law4.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Category/Subcategory.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Functor/Pointwise.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Grothendieck/ToSet.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Profunctor/Utf8.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/KanExtensions.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/ZArith/README.txt
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/FSets/README.txt
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/Setoids/README.txt
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/PArith/README.txt
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/Strings/README.txt
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/Arith/README.txt
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/QArith/README.txt
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/Logic/README.txt
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/Vectors/README.txt
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/Bool/README.txt
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/Structures/README.txt
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/MSets/README.txt
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/Classes/README.txt
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/NArith/README.txt
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/Wellfounded/README.txt
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/Sets/README.txt
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/Numbers/README.txt
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/Reals/README.txt
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/Sorting/README.txt
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/Relations/README.txt
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/Lists/README.txt
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Limits.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/Bool/Bool.vo
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Cubical.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Adjoint/Functorial.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Cat.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Grothendieck.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Category/Subcategory/Wide.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/InitialTerminalCategory/Notations.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/PseudonaturalTransformation.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/LaxComma.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Adjoint/UniversalMorphisms.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/No.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/Int.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/SetCategory/Functors.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Structure/Notations.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/CategoryOfSections.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/LaxComma/Notations.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Categories/Comma/Notations.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/UnivalenceAxiom.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/FunextAxiom.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Truncations.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Spaces/Pos.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Misc.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Basics/Notations.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/Unicode/Utf8.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/theories/Basics/Utf8.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/Init/Tactics.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/Init/Notations.glob
  • 1 K ../ocaml-base-compiler.4.06.1/share/hott/coq/theories/Bool/Bool.glob

Uninstall ๐Ÿงน

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