ยซ Up

hott 8.17 5 m 0 s ๐Ÿ†

Context

# Packages matching: installed
# Name                # Installed # Synopsis
base-bigarray         base
base-threads          base
base-unix             base
conf-gmp              4           Virtual package relying on a GMP lib system installation
coq                   8.17.0      The Coq Proof Assistant
coq-core              8.17.0      The Coq Proof Assistant -- Core Binaries and Tools
coq-stdlib            8.17.0      The Coq Proof Assistant -- Standard Library
coqide-server         8.17.0      The Coq Proof Assistant, XML protocol server
dune                  3.13.0      Fast, portable, and opinionated build system
ocaml                 4.14.0      The OCaml compiler (virtual package)
ocaml-base-compiler   4.14.0      Official release 4.14.0
ocaml-config          2           OCaml Switch Configuration
ocaml-options-vanilla 1           Ensure that OCaml is compiled with no special options enabled
ocamlfind             1.9.6       A library manager for OCaml
zarith                1.13        Implements arithmetic and logical operations over arbitrary-precision integers
# opam file:
opam-version: "2.0"
maintainer: [ "Jason Gross <jgross@mit.edu>" "Ali Caglayan <alizter@gmail.com>" ]
homepage: "http://homotopytypetheory.org/"
bug-reports: "https://github.com/HoTT/HoTT/issues"
license: "BSD-2-Clause"
build: [ "dune" "build" "-p" name "-j" jobs "@install" ]
install: [ "dune" "install" "-p" name ]
depends: [
  "ocaml"
  "ocamlfind" {build}
  "dune" {>= "3.5"}
  "coq" {>= "8.16.0" & < "8.18~"}
]
authors: ["The HoTT Library Development Team"]
dev-repo: "git+https://github.com/HoTT/HoTT.git"
synopsis: "The Homotopy Type Theory library"
description: """
To use the HoTT library, the following flags must be passed to coqc:
  -noinit -indices-matter
To use the HoTT library in a project, add the following to _CoqProject:
  -arg -noinit
  -arg -indices-matter
"""
tags: [ "logpath:HoTT" ]
url {
  src: "https://github.com/HoTT/HoTT/archive/refs/tags/V8.17.tar.gz"
  checksum: "sha512=0d6f713a987a8fd3006ea0bdd7a32dc0b827272a36758521736a6373aed2920ab24acd43e35ca7afc49d2ccd09a1e6d7d37ee07393c479d6e7cd39c15308ea8a"
}

Lint

Command
true
Return code
0

Dry install ๐Ÿœ๏ธ

Dry install with the current Coq version:

Command
opam install -y --show-action coq-hott.8.17 coq.8.17.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; timeout 4h opam install -y --deps-only coq-hott.8.17 coq.8.17.0
Return code
0
Duration
1 m 0 s

Install ๐Ÿš€

Command
opam list; echo; timeout 4h opam install -y -v coq-hott.8.17 coq.8.17.0
Return code
0
Duration
5 m 0 s

Installation size

Total: 100 M

  • 8 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/Colimit_Flattening.vo
  • 7 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Torus/TorusEquivCircles.vo
  • 7 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/HomotopyGroup.vo
  • 4 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/Colimit_Pushout.vo
  • 4 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/Sequential.vo
  • 3 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Spheres.vo
  • 3 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Cubical/PathCube.vo
  • 3 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/Syllepsis.vo
  • 2 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/CayleyDickson.vo
  • 2 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/No/Addition.vo
  • 1 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups/FreeProduct.vo
  • 1 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Finite/FinSeq.vo
  • 1 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/implementations/natpair_integers.vo
  • 1 M ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories.vo
  • 1008 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/Colimit_Pushout_Flattening.vo
  • 932 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/No.vo
  • 751 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/TwoSphere.vo
  • 688 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/ExactSequence.vo
  • 687 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbSES/PullbackFiberSequence.vo
  • 656 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category.vo
  • 647 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/BlakersMassey.vo
  • 640 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/ReflectiveSubuniverse.vo
  • 621 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/ClassifyingSpace.vo
  • 567 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/Pushout.vo
  • 566 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/Coeq.vo
  • 564 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbGroups/Abelianization.vo
  • 561 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/BAut/Bool.vo
  • 541 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbSES/Core.vo
  • 501 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/PathGroupoids.vo
  • 496 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbSES/Pushout.vo
  • 495 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups/GroupCoeq.vo
  • 482 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Pointed/Loops.vo
  • 474 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Grothendieck/ToSet/Morphisms.vo
  • 469 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/PropResizing/Nat.vo
  • 468 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups/FreeGroup.vo
  • 461 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Limits/Pullback.vo
  • 454 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Comma.vo
  • 426 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Sum.vo
  • 419 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Extensions.vo
  • 415 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/Freudenthal.vo
  • 413 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Meet.vo
  • 411 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/Sum.vo
  • 400 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/No/Core.vo
  • 394 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Finite/Finite.vo
  • 384 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/Universe.vo
  • 383 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Pointed/Core.vo
  • 382 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/EMSpace.vo
  • 347 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Paths.vo
  • 340 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Card.vo
  • 335 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/Colimit.vo
  • 334 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/premetric.vo
  • 332 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint.vo
  • 321 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/SemiSimplicialSets.vo
  • 316 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Universe.vo
  • 309 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HIT/V.vo
  • 308 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbSES/SixTerm.vo
  • 304 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/rationals.vo
  • 300 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbSES/Pullback.vo
  • 296 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Adjoint.vo
  • 294 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/HSpace/Pointwise.vo
  • 293 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor.vo
  • 290 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/Suspension.vo
  • 290 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Sigma.vo
  • 275 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/Join.vo
  • 271 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/LaxComma/CoreLaws.vo
  • 269 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Sigma/Univalent.vo
  • 265 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/abstract_algebra.vo
  • 263 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/Quotient.vo
  • 263 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Equiv.vo
  • 262 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/Paths.vo
  • 252 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Pointed/pMap.vo
  • 244 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Pseudofunctor.vo
  • 241 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Analysis/Locator.vo
  • 241 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Diagrams/Cocone.vo
  • 241 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Idempotents.vo
  • 239 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Tactics/EquivalenceInduction.vo
  • 239 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/IWType.vo
  • 235 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Modality.vo
  • 233 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Paths.vo
  • 230 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Cubical/PathSquare.vo
  • 227 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups/GrpPullback.vo
  • 226 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/HSpaceS1.vo
  • 221 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Rings/Ideal.vo
  • 220 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbSES/BaerSum.vo
  • 219 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Pointed/pSusp.vo
  • 217 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/Sigma.vo
  • 212 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/BAut.vo
  • 209 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Contrib/HoTTBookExercises.vo
  • 201 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Contrib/SetoidRewrite.vo
  • 196 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/ua_third_isomorphism.vo
  • 194 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/Prod.vo
  • 188 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/MappingCylinder.vo
  • 187 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Descent.vo
  • 187 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups/Group.vo
  • 184 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Core.vo
  • 182 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Sets/Ordinals.vo
  • 181 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Rings/CRing.vo
  • 179 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/Colimit_Sigma.vo
  • 179 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Diagrams/Cone.vo
  • 177 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Diagrams/CommutativeSquares.vo
  • 174 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HIT/Flattening.vo
  • 174 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Lex.vo
  • 169 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Pseudofunctor/RewriteLaws.vo
  • 164 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Rings/ChineseRemainder.vo
  • 163 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Nat/Arithmetic.vo
  • 159 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HFiber.vo
  • 159 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbGroups/AbPushout.vo
  • 154 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups/Subgroup.vo
  • 152 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Cubical/DPathCube.vo
  • 149 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/implementations/binary_naturals.vo
  • 147 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Equivalences.vo
  • 144 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/Colimit_Coequalizer.vo
  • 144 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Rings/QuotientRing.vo
  • 144 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/orders/semirings.vo
  • 143 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/InitialTerminalCategory/Pseudofunctors.vo
  • 142 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/HSpace/Moduli.vo
  • 135 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Pointed/pFiber.vo
  • 133 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Pointwise.vo
  • 133 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Circle.vo
  • 131 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/HomCoercions.vo
  • 130 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/NatTrans.vo
  • 130 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Nat/Core.vo
  • 129 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation.vo
  • 128 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Cubical/DPath.vo
  • 127 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Contrib/HoTTBook.vo
  • 127 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Morphisms.vo
  • 125 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups/Presentation.vo
  • 125 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Metatheory/UnivalenceVarieties.vo
  • 124 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbSES/Ext.vo
  • 124 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Factorization.vo
  • 124 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Universal/Operation.vo
  • 124 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups/QuotientGroup.vo
  • 123 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/BAut/Cantor.vo
  • 123 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Finite/FinInduction.vo
  • 122 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/implementations/field_of_fractions.vo
  • 122 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/FunctorCat.vo
  • 122 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Functorial/Laws.vo
  • 121 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Rings/Z.vo
  • 113 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/canonical_names.vo
  • 111 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Yoneda.vo
  • 111 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/Cover.vo
  • 109 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/ua_second_isomorphism.vo
  • 107 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/ObjectClassifier.vo
  • 106 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/orders.vo
  • 105 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Comma/Core.vo
  • 104 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Universal/Algebra.vo
  • 103 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Tactics.vo
  • 103 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/Forall.vo
  • 103 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Structure.vo
  • 102 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/implementations/peano_naturals.vo
  • 101 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbGroups/AbelianGroup.vo
  • 100 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbGroups/Biproduct.vo
  • 99 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/ua_quotient_algebra.vo
  • 98 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Diagrams/Diagram.vo
  • 97 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Square.vo
  • 96 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/ooGroup.vo
  • 95 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Comma/Functorial.vo
  • 95 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/PseudonaturalTransformation/Core.vo
  • 94 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/tactics/ring_quote.vo
  • 91 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/LaxComma/Core.vo
  • 89 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HIT/quotient.vo
  • 88 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/Smash.vo
  • 86 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/LaxComma/CoreParts.vo
  • 85 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Finite/FinNat.vo
  • 84 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Universal/TermAlgebra.vo
  • 84 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Finite/Fin.vo
  • 83 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Localization.vo
  • 81 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Sets/Hartogs.vo
  • 81 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/ReflectiveSubuniverse.v
  • 76 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Prod.vo
  • 76 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Overture.vo
  • 75 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/ua_first_isomorphism.vo
  • 74 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Cubical/DPathSquare.vo
  • 73 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/orders/orders.vo
  • 73 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/ua_algebra.vo
  • 72 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/ua_homomorphism.vo
  • 71 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/rings.vo
  • 69 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Comma/ProjectionFunctors.vo
  • 69 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/tactics/ring_pol.vo
  • 69 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups/Lagrange.vo
  • 67 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Pointed/pTrunc.vo
  • 66 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/tests/ring_tac.vo
  • 66 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Fracture.vo
  • 65 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/WhiteheadsPrinciple.vo
  • 65 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/orders/lattices.vo
  • 65 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/orders/rings.vo
  • 64 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/EquivGpd.vo
  • 63 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law2/Law.vo
  • 63 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Topological.vo
  • 62 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Contrib/HoTTBook.v
  • 62 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Limits/Limit.vo
  • 62 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/naturals.vo
  • 62 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/DProp.vo
  • 61 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Projective.vo
  • 61 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/BAut/Rigid.vo
  • 60 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Truncations/Connectedness.vo
  • 60 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Tactics.vo
  • 59 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/Quotient/Choice.vo
  • 59 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Structure/IdentityPrinciple.vo
  • 58 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/PointedCat.vo
  • 58 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/integers.vo
  • 58 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Contrib/HoTTBookExercises.v
  • 58 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/fields.vo
  • 57 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HIT/epi.vo
  • 56 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Separated.vo
  • 55 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/orders/nat_int.vo
  • 55 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Composition.vo
  • 55 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/int_abs.vo
  • 55 K ../ocaml-base-compiler.4.14.0/lib/coq-hott/dune-package
  • 55 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/Bouquet.vo
  • 54 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Int/Spec.vo
  • 54 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Pointed/pSect.vo
  • 54 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Pointed/pHomotopy.vo
  • 54 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Sets/GCHtoAC.vo
  • 54 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ChainCategory.vo
  • 53 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/EquivGroupoids.vo
  • 53 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbSES/DirectSum.vo
  • 52 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/orders/maps.vo
  • 52 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/UnitCounitCoercions.vo
  • 51 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/ua_isomorphic.vo
  • 51 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Accessible.vo
  • 51 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Universal/Homomorphism.vo
  • 51 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/cauchy.vo
  • 50 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/Arrow.vo
  • 50 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Comma/InducedFunctors.vo
  • 50 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law4/Law.vo
  • 50 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Grothendieck/PseudofunctorToCat.vo
  • 49 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/SimplicialSets.vo
  • 49 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Notations.vo
  • 49 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Trunc.vo
  • 49 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/UniversalProperties.vo
  • 48 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/No/Core.v
  • 48 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Torus/Torus.vo
  • 47 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Int/LoopExp.vo
  • 47 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/HSpace/Core.vo
  • 47 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/Equiv.vo
  • 47 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Truncations/Core.vo
  • 47 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Pos/Core.vo
  • 47 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbGroups/Centralizer.vo
  • 47 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Pointed/pEquiv.vo
  • 46 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Yoneda.vo
  • 46 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law3/Law.vo
  • 45 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Composition.vo
  • 45 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/TwoOneCat.vo
  • 45 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Attributes.vo
  • 45 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/dec_fields.vo
  • 45 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Pointwise/Properties.vo
  • 44 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Torus/TorusHomotopy.vo
  • 44 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/ua_subalgebra.vo
  • 44 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Isomorphisms.vo
  • 43 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law4/Functors.vo
  • 43 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/LaxComma.vo
  • 43 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Prod.vo
  • 42 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Tactics/RewriteModuloAssociativity.vo
  • 42 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law4.vo
  • 42 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/ua_prod_algebra.vo
  • 42 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Pointwise.vo
  • 41 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Contrib/UniverseLevel.vo
  • 41 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Composition/AssociativityLaw.vo
  • 41 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Monoidal/MonoidalCategory.vo
  • 41 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/lattices.vo
  • 41 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Overture.v
  • 41 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/PathGroupoids.v
  • 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Composition/IdentityLaws.vo
  • 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Limits.vo
  • 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/groups.vo
  • 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ProductLaws.vo
  • 40 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Pseudofunctor/Identity.vo
  • 39 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Equiv/PathSplit.vo
  • 39 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Pos/Spec.vo
  • 39 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/Syllepsis.v
  • 39 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Monoidal.vo
  • 38 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups/Image.vo
  • 38 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Sum.vo
  • 38 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/FunctorCategory.vo
  • 38 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/PropResizing/Nat.v
  • 38 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Prod/Universal.vo
  • 37 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/apartness.vo
  • 37 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/TruncType.vo
  • 37 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups/ShortExactSequence.vo
  • 36 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/CoreflectiveSubuniverse.vo
  • 36 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Composition/Laws.vo
  • 36 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/nat_distance.vo
  • 36 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/implementations/natpair_integers.v
  • 36 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Composition.vo
  • 35 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Pseudofunctor/FromFunctor.vo
  • 35 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbGroups/AbPullback.vo
  • 35 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Functorial/Core.vo
  • 35 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/Bool.vo
  • 35 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Idempotents.v
  • 35 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HSet.vo
  • 35 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Grothendieck/ToSet.vo
  • 35 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/categories/ua_category.vo
  • 34 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Limits/Core.vo
  • 34 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Constant.vo
  • 34 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Opposite.vo
  • 34 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Composition/Core.vo
  • 34 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Composition/Laws.vo
  • 34 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/No/Negation.vo
  • 34 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/tactics/ring_tac.vo
  • 34 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups/Kernel.vo
  • 34 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/FunctorCategory/Morphisms.vo
  • 34 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Int/Core.vo
  • 34 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Extensions.v
  • 33 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Composition/Core.vo
  • 33 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Equivalences.v
  • 33 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Bifunctor.vo
  • 33 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/PseudonaturalTransformation.vo
  • 33 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/HomotopyPreCategory.vo
  • 33 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/WType.vo
  • 33 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Structure/Core.vo
  • 33 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Closed.vo
  • 33 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/implementations/pointwise.vo
  • 33 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbGroups/AbHom.vo
  • 32 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/UniversalMorphisms/Core.vo
  • 32 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/Sum.v
  • 32 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HoTT.vo
  • 32 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/isomorphisms/rings.vo
  • 32 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/implementations/bool.vo
  • 32 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/premetric.v
  • 31 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/orders/naturals.vo
  • 31 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law2.vo
  • 31 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/ua_congruence.vo
  • 31 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/BoundedSearch.vo
  • 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/SetCategory/Morphisms.vo
  • 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/integers.vo
  • 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/GraphQuotient.vo
  • 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Grothendieck/ToSet/Univalent.vo
  • 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Tactics.v
  • 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Functorial/Parts.vo
  • 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/implementations/ne_list.vo
  • 30 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Sum.vo
  • 29 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/UniversalMorphisms.vo
  • 29 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Pseudofunctor/Core.vo
  • 29 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HIT/V.v
  • 29 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Open.vo
  • 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Sigma/OnMorphisms.vo
  • 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbSES/Core.v
  • 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HIT/FreeIntQuotient.vo
  • 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Decidable.vo
  • 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbGroups/Cyclic.vo
  • 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Rings/Ideal.v
  • 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/implementations/hprop_lattice.vo
  • 28 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Pointed/Core.v
  • 27 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Universal/Congruence.vo
  • 27 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law3.vo
  • 27 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/SetCategory.vo
  • 27 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/orders/semirings.v
  • 27 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/Sigma.v
  • 27 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Composition/Functorial.vo
  • 27 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Analysis/Locator.v
  • 27 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Finite/Finite.v
  • 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Modality.v
  • 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law0.vo
  • 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Sets/GCH.vo
  • 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/orders/integers.vo
  • 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Sets/Ordinals.v
  • 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/implementations/list.vo
  • 26 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Nat/Arithmetic.v
  • 25 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/Pi1S1.vo
  • 25 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/orders/fields.vo
  • 25 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Paths.vo
  • 25 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/Sequential.v
  • 25 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Metatheory/FunextVarieties.vo
  • 25 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law1/Law.vo
  • 25 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Diagrams/ConstantDiagram.vo
  • 25 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/BAut/Bool/IncoherentIdempotent.vo
  • 25 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Hexadecimal.vo
  • 25 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/InitialTerminalCategory/Functors.vo
  • 24 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law1.vo
  • 24 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/orders/dec_fields.vo
  • 24 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Cubical/PathCube.v
  • 24 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/rationals.vo
  • 24 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Sets/AC.vo
  • 24 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups/Group.v
  • 24 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HProp.vo
  • 24 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/BlakersMassey.v
  • 23 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/KanExtensions.vo
  • 23 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Localization.v
  • 23 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Morphisms.v
  • 23 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Composition/Functorial/Attributes.vo
  • 23 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law1/Functors.vo
  • 23 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/naturals.vo
  • 23 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Tests.vo
  • 23 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups/FreeProduct.v
  • 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/implementations/binary_naturals.v
  • 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Grothendieck/ToSet/Core.vo
  • 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Pointwise/Core.vo
  • 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Nullification.vo
  • 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law3/Functors.vo
  • 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Composition/Functorial/Core.vo
  • 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Tactics.vo
  • 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/ua_setalgebra.vo
  • 22 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/UnitCounit.vo
  • 21 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Contractible.vo
  • 21 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/Paths.v
  • 21 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbGroups/AbProjective.vo
  • 21 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/HSpace/Coherent.vo
  • 21 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Pointed/pModality.vo
  • 21 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Tactics.v
  • 20 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spectra/Spectrum.vo
  • 20 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Decimal.vo
  • 20 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Identity.vo
  • 20 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/Universe.v
  • 20 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/LaxComma/CoreLaws.v
  • 20 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Core.vo
  • 20 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Universe.vo
  • 19 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Utf8.vo
  • 19 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/ExactSequence.v
  • 19 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/orders/sum.vo
  • 19 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/EncodeDecode.vo
  • 19 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Core.v
  • 19 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Paths.vo
  • 19 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/Suspension.v
  • 19 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Tactics/RewriteModuloAssociativity.v
  • 19 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Cubical/PathSquare.v
  • 19 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/DualFunctor.vo
  • 19 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/implementations/family_prod.vo
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Core.vo
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Descent.v
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Notations.vo
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/Pushout.v
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/IWType.v
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/additional_operations.vo
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Utf8.vo
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/SuccessorStructure.vo
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/implementations/peano_naturals.v
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbSES/Pullback.v
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/CategoryOfSections/Core.vo
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Induced.vo
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/ClassifyingSpace.v
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Lex.v
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups/FreeGroup.v
  • 18 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/abstract_algebra.v
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Nat/Core.v
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Metatheory/PropTrunc.vo
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbSES/Pushout.v
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/Unit.vo
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/orders/archimedean.vo
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Prod/Core.vo
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Limits/Functors.vo
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Composition/LawsTactic.vo
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbGroups/Z.vo
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/KanExtensions/Functors.vo
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups/Subgroup.v
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/rationals.v
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/CategoryOfSections.vo
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbSES/PullbackFiberSequence.v
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/No/Addition.v
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/orders/lattices.v
  • 17 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law2/Functors.vo
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/implementations/assume_rationals.vo
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/archimedean.vo
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/UniversalProperties.v
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbSES.vo
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Pointwise.vo
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Diagrams/ParallelPair.vo
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/canonical_names.v
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Utf8.vo
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/PathAny.vo
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/FundamentalPreGroupoidCategory.vo
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Tactics/EquivalenceInduction.v
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/BAut/Bool.v
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/ooAction.vo
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/EmptyCat.vo
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Aut.vo
  • 16 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/implementations/field_of_fractions.v
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Utf8.vo
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/FunctorCategory/Utf8.vo
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HIT/Interval.vo
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/InitialTerminalCategory/NaturalTransformations.vo
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Metatheory/UnivalenceImpliesFunext.vo
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/SpanPushout.vo
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Sets/Powers.vo
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Int/Equiv.vo
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Rings.vo
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Equiv/Relational.vo
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/Forall.v
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Prod.vo
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Limits/Pullback.v
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/GroupoidCategory.vo
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Adjoint.v
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/KanExtensions/Core.vo
  • 15 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Sigma/Core.vo
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Diagrams/DDiagram.vo
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Factorization.v
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/LaxComma/Notations.vo
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbGroups.vo
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/Coeq.v
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Meet.v
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Rings/CRing.v
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Prod/Functorial.vo
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/orders/orders.v
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Cat.vo
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Truncations/SeparatedTrunc.vo
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Sigma.vo
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Sigma/OnObjects.vo
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Sigma/Univalent.v
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Cubical/DPath.v
  • 14 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Notations.vo
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Finite/Fin.v
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/Prod.v
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups.vo
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbSES/BaerSum.v
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Hom.vo
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Universal/TermAlgebra.v
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Pointed/Loops.v
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Equiv.v
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Yoneda.v
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Trunc.v
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Sets/GCHtoAC.v
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/GroupoidCategory/Core.vo
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbGroups/Abelianization.v
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/rings.v
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/FunctorCategory/Functorial.vo
  • 13 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HIT/surjective_factor.vo
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/HomFunctor.vo
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Sets/Hartogs.v
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/InitialTerminalCategory/Core.vo
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Truncations/Connectedness.v
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Truncations/Core.v
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Prod.vo
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/monad.vo
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Comma/Projection.vo
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/orders/rings.v
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Nat.vo
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/ua_homomorphism.v
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/BAut.v
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Notations.v
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/EvaluationFibration.vo
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/NullHomotopy.vo
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/ua_quotient_algebra.v
  • 12 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/round.vo
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Forall.vo
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Core.vo
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Diagrams/Sequence.vo
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Cat/Core.vo
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Functorish.vo
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Comma/Core.v
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HIT/quotient.v
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/IndiscreteCategory.vo
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HIT/iso.vo
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Metatheory/TruncImpliesFunext.vo
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Objects.vo
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/PropResizing/ImpredicativeTruncation.vo
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/InitialTerminalCategory.vo
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/LaxComma/Core.v
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Pos/Core.v
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/Colimit_Prod.vo
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Grothendieck/PseudofunctorToCat.v
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Notnot.vo
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Int/Spec.v
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbGroups/Biproduct.v
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbSES/SixTerm.v
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Paths.v
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/LaxComma/Utf8.vo
  • 11 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Spheres.v
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/NatTrans.v
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Profunctor.vo
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Cantor.vo
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Pointed/pSusp.v
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HIT/unique_choice.vo
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Diagrams/Span.vo
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/Quotient/Choice.v
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/HSpace.vo
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Congruence.vo
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Accessible.v
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Datatypes.vo
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/ooGroup.v
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Sum.vo
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Circle.v
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Composition/Functorial.vo
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/Quotient.v
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Identity.vo
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/DProp.v
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/CayleyDickson.v
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Fracture.v
  • 10 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/orders/maps.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Separated.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/UnitCounit.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/LaxComma/CoreParts.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Grothendieck/ToCat.vo
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/DependentProduct.vo
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/GroupoidCategory/Morphisms.vo
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Pseudofunctor/Core.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Equiv/BiInv.vo
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/orders.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/Colimit.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Cat/Morphisms.vo
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Comma/Dual.vo
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HIT/SetCone.vo
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Cubical/DPathCube.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/tactics/ring_pol.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Pseudofunctor/RewriteLaws.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Finite.vo
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Pointed.vo
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NatCategory.vo
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Structure/Core.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws.vo
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/PseudonaturalTransformation/Core.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/dec_fields.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HFiber.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups/QuotientGroup.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Rings/Z.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Tactics/BinderApply.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Utf8.vo
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/Wedge.vo
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Contrib/SetoidRewrite.v
  • 9 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/groups.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/SetCategory/Functors/SetProp.vo
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/fields.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Diagrams/Cocone.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Finite/Tactics.vo
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/Join.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/ua_first_isomorphism.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/SetCategory/Functors.vo
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Pointed/pMap.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Profunctor/Representable.vo
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Functorial/Laws.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/FunctorCategory/Core.vo
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbGroups/AbelianGroup.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Pi.vo
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/FunctorCategory/Dual.vo
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/Arrow.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Diagrams/Cone.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/tactics/ring_quote.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Utf8.vo
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/ExcludedMiddle.vo
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/Empty.vo
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/HomotopyGroup.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Pointwise.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Composition/Core.vo
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Comma/Functorial.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups/GrpPullback.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/ua_algebra.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Univalent.vo
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/GroupoidCategory/Dual.vo
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Grothendieck.vo
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Cubical/DPathSquare.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/HomCoercions.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Yoneda.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/EquivGpd.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Comma/ProjectionFunctors.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Tactics/BinderApply.vo
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Utf8.vo
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/EMSpace.v
  • 8 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Torus/TorusEquivCircles.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Int.vo
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/naturals.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/ObjectClassifier.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Metatheory/FunextVarieties.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/Equiv.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Limits/Equalizer.vo
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Square.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/Colimit_Flattening.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/ua_second_isomorphism.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Truncations.vo
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/lattices.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Paths.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/SetCategory/Core.vo
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Universal/Operation.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Pos.vo
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/Smash.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/CategoryOfGroupoids.vo
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Universe.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Nat.vo
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Comma/InducedFunctors.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/FunctorCat.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Finite/FinSeq.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/HSpace/Core.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HIT/Flattening.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Notations.vo
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Topological.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Pseudofunctor/FromFunctor.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Composition/Laws.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Notations.vo
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbGroups/AbPushout.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Dual.vo
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/BAut/Cantor.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/ua_third_isomorphism.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/MappingCylinder.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/apartness.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Diagrams/Diagram.v
  • 7 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/EquivGroupoids.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Hexadecimal.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Int/LoopExp.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/UnitCounitCoercions.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/CoreflectiveSubuniverse.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Functorial.vo
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/InitialTerminalCategory/Notations.vo
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups/Presentation.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/Colimit_Pushout.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HoTT.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Limits/Core.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Int/Core.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Comma/Utf8.vo
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Prod.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/Bool.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Core.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Numeral.vo
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Rings/QuotientRing.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Pos/Spec.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Constant.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Projective.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HIT/epi.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Decimal.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/integers.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/HSpace/Moduli.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Notations.vo
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Rings/ChineseRemainder.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Profunctor/Core.vo
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law4/Functors.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Decidable.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Dual.vo
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/orders/nat_int.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/ua_prod_algebra.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/ua_subalgebra.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Sigma/OnMorphisms.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Card.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Identity.vo
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Finite/FinNat.v
  • 6 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Tactics/EvalIn.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Limits/Limit.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Tactics/EvalIn.vo
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/TruncType.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Universal/Homomorphism.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Profunctor/Identity.vo
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Universal/Algebra.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Profunctor/Utf8.vo
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Isomorphisms.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Dual.vo
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/FunctorCategory/Notations.vo
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/UniversalMorphisms/Core.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Pointed/pTrunc.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HSet.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Opposite.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/ua_isomorphic.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Profunctor/Notations.vo
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Attributes.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/KanExtensions/Core.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/Colimit_Sigma.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Contrib/UniverseLevel.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Comma/Notations.vo
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/BAut/Rigid.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HProp.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/cauchy.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Dual.vo
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Metatheory/Core.vo
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Sets/GCH.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Composition/Core.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Subcategory.vo
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/SetCategory/Morphisms.v
  • 5 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Metatheory/IntervalImpliesFunext.vo
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Subcategory/Full.vo
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/UnitCat.vo
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Nat.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/int_abs.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/PathAny.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbSES/Ext.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/Unit.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Contractible.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/isomorphisms/rings.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Core.vo
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/List.vo
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Sigma/Core.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HIT/FreeIntQuotient.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Structure/Utf8.vo
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Torus/Torus.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat.vo
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Composition/Laws.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Subcategory/Wide.vo
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/Cover.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ProductLaws.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Structure/IdentityPrinciple.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbSES/DirectSum.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/implementations/ne_list.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Pointed/pEquiv.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/PointedCat.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Tactics.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/DiscreteCategory.vo
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Logic.vo
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Pointed/pFiber.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/WhiteheadsPrinciple.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Metatheory/UnivalenceImpliesFunext.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Utf8.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Diagrams/CommutativeSquares.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/BoundedSearch.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Strict.vo
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Pointwise/Properties.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/FunctorCategory/Morphisms.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/PropResizing/PropResizing.vo
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Prod/Universal.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Equiv/PathSplit.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Monoidal/MonoidalCategory.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/HSpace/Pointwise.v
  • 4 K ../ocaml-base-compiler.4.14.0/doc/coq-hott/README.md
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/implementations/list.v
  • 4 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/tactics/ring_tac.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Cubical.vo
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Nullification.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/orders/fields.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Sum.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbGroups/Centralizer.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Metatheory/UnivalenceVarieties.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Structure/Notations.vo
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Induced.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Datatypes.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Paths.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/InitialTerminalCategory/Functors.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Composition/Core.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Prod/Core.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Pointwise/Core.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Utf8.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/orders/archimedean.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Closed.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types.vo
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/orders/dec_fields.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Core.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law0.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/Bouquet.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Hom.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/implementations/hprop_lattice.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Grothendieck/ToSet/Core.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Functorial/Parts.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Misc.vo
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Axioms/Univalence.vo
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Open.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Tests.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Int/Equiv.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Diagrams/Graph.vo
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ChainCategory.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Profunctor/Core.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbGroups/Cyclic.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Bifunctor.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Universal/Congruence.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/PropResizing/ImpredicativeTruncation.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Pseudofunctor/Identity.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Identity.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/HSpaceS1.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/orders/integers.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/categories/ua_category.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/TwoSphere.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Sigma/OnObjects.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Comma/Projection.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Universe.v
  • 3 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Monoidal.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/FundamentalPreGroupoidCategory.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Functorial/Core.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/BAut/Bool/IncoherentIdempotent.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups/ShortExactSequence.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Composition/LawsTactic.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Pointed/pHomotopy.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/additional_operations.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/ua_congruence.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law1/Functors.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/Colimit_Pushout_Flattening.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Paths.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/orders/naturals.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/IndiscreteCategory.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/NullHomotopy.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/nat_distance.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Finite/FinInduction.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Prod.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Composition/Functorial/Attributes.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Pointwise.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Core.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/Colimit_Coequalizer.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Paths.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Cat/Core.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/GroupoidCategory/Core.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Equiv/Relational.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/implementations/family_prod.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/DualFunctor.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbGroups/AbHom.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/TwoOneCat.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/No/Negation.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/HomotopyPreCategory.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Sets/AC.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups/Kernel.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/InitialTerminalCategory/Pseudofunctors.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/implementations/pointwise.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NatCategory.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/SetCategory/Functors/SetProp.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Objects.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Sets/Powers.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/EncodeDecode.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Pointed/pSect.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Identity.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/HomFunctor.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Limits/Functors.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/SuccessorStructure.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups/Image.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Sum.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Torus/TorusHomotopy.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Composition/Functorial/Core.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/Empty.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/InitialTerminalCategory/NaturalTransformations.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/SimplicialSets.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Composition/Core.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Tactics/Nameless.vo
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Comma/Dual.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/CategoryOfSections/Core.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/SpanPushout.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/ua_setalgebra.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Forall.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Diagrams/ConstantDiagram.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Prod/Functorial.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Pointed/pModality.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/ExcludedMiddle.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Metatheory/PropTrunc.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/GraphQuotient.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups/GroupCoeq.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Grothendieck/ToSet/Univalent.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Grothendieck/ToSet/Morphisms.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/InitialTerminalCategory/Core.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/FunctorCategory/Core.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups/Lagrange.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/DependentProduct.v
  • 2 K ../ocaml-base-compiler.4.14.0/doc/coq-hott/LICENSE.txt
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/SemiSimplicialSets.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/KanExtensions/Functors.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Pi.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HIT/Interval.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Composition/IdentityLaws.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/Freudenthal.v
  • 2 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law3/Functors.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Truncations/SeparatedTrunc.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/LaxComma/Utf8.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Sum.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law2/Law.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/WType.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/FunctorCategory/Functorial.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbGroups/AbProjective.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Dual.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law2/Functors.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/Colimit_Prod.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Equiv/BiInv.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/integers.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law4/Law.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Composition/AssociativityLaw.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Logic.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Sigma.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law3/Law.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Composition/Functorial.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Comma/Utf8.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/FunctorCategory/Dual.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Prod.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law1/Law.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Cat/Morphisms.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Functorish.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Cantor.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Dual.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbGroups/Z.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Diagrams/DDiagram.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Diagrams/Sequence.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spectra/Spectrum.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Axioms/Funext.vo
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/rationals.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HIT/surjective_factor.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/naturals.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/SetCategory/Core.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Profunctor/Representable.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Dual.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HIT/iso.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Tactics/Nameless.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/tests/ring_tac.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/orders/sum.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/List.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Metatheory/TruncImpliesFunext.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Metatheory/Core.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Univalent.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/Pi1S1.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Sum.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbGroups/AbPullback.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Dual.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/EvaluationFibration.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/implementations/assume_rationals.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/GroupoidCategory/Morphisms.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HIT/unique_choice.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/HSpace/Coherent.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Grothendieck/ToCat.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Utf8.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq-hott/opam
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/GroupoidCategory/Dual.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Limits/Equalizer.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Diagrams/ParallelPair.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/PropResizing/PropResizing.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/InitialTerminalCategory.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Numeral.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/CategoryOfGroupoids.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Notnot.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/archimedean.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Identity.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Misc.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Diagrams/Span.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Comma.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/FunctorCategory.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/SetCategory.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Profunctor/Identity.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Identity.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Composition.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Identity.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Notations.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/UnitCat.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/Wedge.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/EmptyCat.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Strict.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Grothendieck/ToSet.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbGroups.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Notations.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Metatheory/IntervalImpliesFunext.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Paths.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Sigma.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Notations.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Composition.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Grothendieck.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Notations.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/implementations/bool.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Composition.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Prod.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Utf8.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Utf8.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/round.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HIT/SetCone.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Pseudofunctor.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Utf8.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Finite/Tactics.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Aut.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/monad.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Congruence.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Utf8.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/DiscreteCategory.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/GroupoidCategory.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/LaxComma.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/ooAction.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/FunctorCategory/Utf8.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Structure.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Axioms/Univalence.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Profunctor.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/InitialTerminalCategory/Notations.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/LaxComma/Notations.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Diagrams/Graph.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Pointed.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Axioms/Funext.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Subcategory/Wide.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Comma/Notations.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Notations.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Subcategory/Full.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Rings.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law3.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbSES.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Functorial.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law2.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Core.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Structure/Utf8.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/FunctorCategory/Notations.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law1.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Limits.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Pointwise.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/KanExtensions.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law4.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Profunctor/Notations.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Profunctor/Utf8.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Composition/Functorial.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Finite.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/PseudonaturalTransformation.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Cat.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Cubical.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Subcategory.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Int.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/UniversalMorphisms.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/No.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Truncations.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/SetCategory/Functors.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/HSpace.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/CategoryOfSections.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Structure/Notations.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Pos.v
  • 1 K ../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Nat.v
  • 0 K ../ocaml-base-compiler.4.14.0/lib/coq-hott/META

Uninstall ๐Ÿงน

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