# 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"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-hott.8.17 coq.8.17.0Dry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
trueopam list; echo; timeout 4h opam install -y --deps-only coq-hott.8.17 coq.8.17.0opam list; echo; timeout 4h opam install -y -v coq-hott.8.17 coq.8.17.0Total: 100 M
../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/Colimit_Flattening.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Torus/TorusEquivCircles.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/HomotopyGroup.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/Colimit_Pushout.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/Sequential.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Spheres.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Cubical/PathCube.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/Syllepsis.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/CayleyDickson.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/No/Addition.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups/FreeProduct.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Finite/FinSeq.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/implementations/natpair_integers.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/Colimit_Pushout_Flattening.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/No.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/TwoSphere.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/ExactSequence.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbSES/PullbackFiberSequence.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/BlakersMassey.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/ReflectiveSubuniverse.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/ClassifyingSpace.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/Pushout.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/Coeq.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbGroups/Abelianization.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/BAut/Bool.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbSES/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/PathGroupoids.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbSES/Pushout.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups/GroupCoeq.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Pointed/Loops.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Grothendieck/ToSet/Morphisms.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/PropResizing/Nat.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups/FreeGroup.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Limits/Pullback.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Comma.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Sum.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Extensions.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/Freudenthal.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Meet.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/Sum.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/No/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Finite/Finite.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/Universe.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Pointed/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/EMSpace.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Paths.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Card.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/Colimit.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/premetric.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/SemiSimplicialSets.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Universe.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HIT/V.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbSES/SixTerm.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/rationals.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbSES/Pullback.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Adjoint.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/HSpace/Pointwise.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/Suspension.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Sigma.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/Join.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/LaxComma/CoreLaws.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Sigma/Univalent.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/abstract_algebra.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/Quotient.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Equiv.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/Paths.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Pointed/pMap.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Pseudofunctor.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Analysis/Locator.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Diagrams/Cocone.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Idempotents.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Tactics/EquivalenceInduction.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/IWType.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Modality.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Paths.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Cubical/PathSquare.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups/GrpPullback.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/HSpaceS1.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Rings/Ideal.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbSES/BaerSum.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Pointed/pSusp.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/Sigma.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/BAut.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Contrib/HoTTBookExercises.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Contrib/SetoidRewrite.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/ua_third_isomorphism.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/Prod.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/MappingCylinder.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Descent.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups/Group.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Sets/Ordinals.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Rings/CRing.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/Colimit_Sigma.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Diagrams/Cone.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Diagrams/CommutativeSquares.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HIT/Flattening.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Lex.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Pseudofunctor/RewriteLaws.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Rings/ChineseRemainder.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Nat/Arithmetic.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HFiber.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbGroups/AbPushout.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups/Subgroup.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Cubical/DPathCube.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/implementations/binary_naturals.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Equivalences.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/Colimit_Coequalizer.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Rings/QuotientRing.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/orders/semirings.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/InitialTerminalCategory/Pseudofunctors.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/HSpace/Moduli.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Pointed/pFiber.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Pointwise.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Circle.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/HomCoercions.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/NatTrans.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Nat/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Cubical/DPath.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Contrib/HoTTBook.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Morphisms.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups/Presentation.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Metatheory/UnivalenceVarieties.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbSES/Ext.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Factorization.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Universal/Operation.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups/QuotientGroup.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/BAut/Cantor.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Finite/FinInduction.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/implementations/field_of_fractions.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/FunctorCat.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Functorial/Laws.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Rings/Z.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/canonical_names.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Yoneda.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/Cover.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/ua_second_isomorphism.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/ObjectClassifier.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/orders.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Comma/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Universal/Algebra.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Tactics.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/Forall.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Structure.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/implementations/peano_naturals.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbGroups/AbelianGroup.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbGroups/Biproduct.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/ua_quotient_algebra.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Diagrams/Diagram.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Square.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/ooGroup.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Comma/Functorial.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/PseudonaturalTransformation/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/tactics/ring_quote.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/LaxComma/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HIT/quotient.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/Smash.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/LaxComma/CoreParts.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Finite/FinNat.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Universal/TermAlgebra.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Finite/Fin.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Localization.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Sets/Hartogs.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/ReflectiveSubuniverse.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Prod.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Overture.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/ua_first_isomorphism.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Cubical/DPathSquare.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/orders/orders.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/ua_algebra.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/ua_homomorphism.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/rings.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Comma/ProjectionFunctors.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/tactics/ring_pol.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups/Lagrange.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Pointed/pTrunc.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/tests/ring_tac.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Fracture.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/WhiteheadsPrinciple.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/orders/lattices.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/orders/rings.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/EquivGpd.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law2/Law.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Topological.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Contrib/HoTTBook.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Limits/Limit.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/naturals.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/DProp.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Projective.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/BAut/Rigid.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Truncations/Connectedness.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Tactics.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/Quotient/Choice.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Structure/IdentityPrinciple.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/PointedCat.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/integers.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Contrib/HoTTBookExercises.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/fields.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HIT/epi.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Separated.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/orders/nat_int.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Composition.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/int_abs.vo../ocaml-base-compiler.4.14.0/lib/coq-hott/dune-package../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/Bouquet.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Int/Spec.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Pointed/pSect.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Pointed/pHomotopy.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Sets/GCHtoAC.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ChainCategory.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/EquivGroupoids.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbSES/DirectSum.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/orders/maps.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/UnitCounitCoercions.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/ua_isomorphic.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Accessible.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Universal/Homomorphism.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/cauchy.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/Arrow.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Comma/InducedFunctors.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law4/Law.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Grothendieck/PseudofunctorToCat.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/SimplicialSets.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Notations.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Trunc.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/UniversalProperties.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/No/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Torus/Torus.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Int/LoopExp.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/HSpace/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/Equiv.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Truncations/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Pos/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbGroups/Centralizer.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Pointed/pEquiv.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Yoneda.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law3/Law.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Composition.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/TwoOneCat.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Attributes.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/dec_fields.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Pointwise/Properties.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Torus/TorusHomotopy.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/ua_subalgebra.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Isomorphisms.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law4/Functors.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/LaxComma.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Prod.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Tactics/RewriteModuloAssociativity.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law4.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/ua_prod_algebra.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Pointwise.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Contrib/UniverseLevel.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Composition/AssociativityLaw.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Monoidal/MonoidalCategory.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/lattices.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Overture.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/PathGroupoids.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Composition/IdentityLaws.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Limits.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/groups.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ProductLaws.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Pseudofunctor/Identity.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Equiv/PathSplit.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Pos/Spec.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/Syllepsis.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Monoidal.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups/Image.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Sum.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/FunctorCategory.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/PropResizing/Nat.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Prod/Universal.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/apartness.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/TruncType.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups/ShortExactSequence.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/CoreflectiveSubuniverse.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Composition/Laws.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/nat_distance.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/implementations/natpair_integers.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Composition.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Pseudofunctor/FromFunctor.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbGroups/AbPullback.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Functorial/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/Bool.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Idempotents.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HSet.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Grothendieck/ToSet.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/categories/ua_category.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Limits/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Constant.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Opposite.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Composition/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Composition/Laws.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/No/Negation.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/tactics/ring_tac.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups/Kernel.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/FunctorCategory/Morphisms.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Int/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Extensions.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Composition/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Equivalences.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Bifunctor.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/PseudonaturalTransformation.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/HomotopyPreCategory.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/WType.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Structure/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Closed.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/implementations/pointwise.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbGroups/AbHom.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/UniversalMorphisms/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/Sum.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HoTT.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/isomorphisms/rings.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/implementations/bool.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/premetric.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/orders/naturals.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law2.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/ua_congruence.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/BoundedSearch.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/SetCategory/Morphisms.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/integers.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/GraphQuotient.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Grothendieck/ToSet/Univalent.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Tactics.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Functorial/Parts.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/implementations/ne_list.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Sum.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/UniversalMorphisms.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Pseudofunctor/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HIT/V.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Open.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Sigma/OnMorphisms.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbSES/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HIT/FreeIntQuotient.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Decidable.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbGroups/Cyclic.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Rings/Ideal.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/implementations/hprop_lattice.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Pointed/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Universal/Congruence.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law3.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/SetCategory.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/orders/semirings.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/Sigma.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Composition/Functorial.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Analysis/Locator.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Finite/Finite.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Modality.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law0.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Sets/GCH.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/orders/integers.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Sets/Ordinals.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/implementations/list.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Nat/Arithmetic.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/Pi1S1.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/orders/fields.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Paths.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/Sequential.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Metatheory/FunextVarieties.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law1/Law.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Diagrams/ConstantDiagram.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/BAut/Bool/IncoherentIdempotent.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Hexadecimal.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/InitialTerminalCategory/Functors.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law1.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/orders/dec_fields.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Cubical/PathCube.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/rationals.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Sets/AC.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups/Group.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HProp.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/BlakersMassey.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/KanExtensions.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Localization.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Morphisms.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Composition/Functorial/Attributes.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law1/Functors.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/naturals.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Tests.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups/FreeProduct.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/implementations/binary_naturals.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Grothendieck/ToSet/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Pointwise/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Nullification.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law3/Functors.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Composition/Functorial/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Tactics.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/ua_setalgebra.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/UnitCounit.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Contractible.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/Paths.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbGroups/AbProjective.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/HSpace/Coherent.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Pointed/pModality.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Tactics.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spectra/Spectrum.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Decimal.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Identity.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/Universe.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/LaxComma/CoreLaws.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Universe.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Utf8.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/ExactSequence.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/orders/sum.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/EncodeDecode.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Paths.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/Suspension.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Tactics/RewriteModuloAssociativity.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Cubical/PathSquare.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/DualFunctor.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/implementations/family_prod.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Descent.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Notations.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/Pushout.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/IWType.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/additional_operations.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Utf8.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/SuccessorStructure.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/implementations/peano_naturals.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbSES/Pullback.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/CategoryOfSections/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Induced.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/ClassifyingSpace.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Lex.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups/FreeGroup.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/abstract_algebra.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Nat/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Metatheory/PropTrunc.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbSES/Pushout.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/Unit.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/orders/archimedean.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Prod/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Limits/Functors.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Composition/LawsTactic.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbGroups/Z.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/KanExtensions/Functors.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups/Subgroup.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/rationals.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/CategoryOfSections.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbSES/PullbackFiberSequence.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/No/Addition.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/orders/lattices.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law2/Functors.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/implementations/assume_rationals.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/archimedean.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/UniversalProperties.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbSES.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Pointwise.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Diagrams/ParallelPair.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/canonical_names.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Utf8.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/PathAny.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/FundamentalPreGroupoidCategory.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Tactics/EquivalenceInduction.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/BAut/Bool.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/ooAction.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/EmptyCat.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Aut.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/implementations/field_of_fractions.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Utf8.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/FunctorCategory/Utf8.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HIT/Interval.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/InitialTerminalCategory/NaturalTransformations.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Metatheory/UnivalenceImpliesFunext.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/SpanPushout.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Sets/Powers.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Int/Equiv.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Rings.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Equiv/Relational.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/Forall.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Prod.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Limits/Pullback.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/GroupoidCategory.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Adjoint.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/KanExtensions/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Sigma/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Diagrams/DDiagram.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Factorization.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/LaxComma/Notations.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbGroups.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/Coeq.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Meet.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Rings/CRing.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Prod/Functorial.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/orders/orders.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Cat.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Truncations/SeparatedTrunc.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Sigma.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Sigma/OnObjects.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Sigma/Univalent.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Cubical/DPath.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Notations.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Finite/Fin.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/Prod.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbSES/BaerSum.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Hom.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Universal/TermAlgebra.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Pointed/Loops.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Equiv.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Yoneda.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Trunc.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Sets/GCHtoAC.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/GroupoidCategory/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbGroups/Abelianization.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/rings.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/FunctorCategory/Functorial.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HIT/surjective_factor.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/HomFunctor.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Sets/Hartogs.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/InitialTerminalCategory/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Truncations/Connectedness.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Truncations/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Prod.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/monad.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Comma/Projection.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/orders/rings.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Nat.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/ua_homomorphism.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/BAut.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Notations.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/EvaluationFibration.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/NullHomotopy.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/ua_quotient_algebra.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/round.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Forall.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Diagrams/Sequence.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Cat/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Functorish.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Comma/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HIT/quotient.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/IndiscreteCategory.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HIT/iso.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Metatheory/TruncImpliesFunext.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Objects.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/PropResizing/ImpredicativeTruncation.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/InitialTerminalCategory.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/LaxComma/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Pos/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/Colimit_Prod.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Grothendieck/PseudofunctorToCat.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Notnot.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Int/Spec.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbGroups/Biproduct.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbSES/SixTerm.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Paths.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/LaxComma/Utf8.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Spheres.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/NatTrans.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Profunctor.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Cantor.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Pointed/pSusp.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HIT/unique_choice.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Diagrams/Span.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/Quotient/Choice.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/HSpace.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Congruence.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Accessible.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Datatypes.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/ooGroup.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Sum.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Circle.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Composition/Functorial.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/Quotient.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Identity.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/DProp.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/CayleyDickson.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Fracture.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/orders/maps.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Separated.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/UnitCounit.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/LaxComma/CoreParts.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Grothendieck/ToCat.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/DependentProduct.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/GroupoidCategory/Morphisms.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Pseudofunctor/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Equiv/BiInv.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/orders.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/Colimit.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Cat/Morphisms.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Comma/Dual.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HIT/SetCone.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Cubical/DPathCube.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/tactics/ring_pol.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Pseudofunctor/RewriteLaws.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Finite.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Pointed.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NatCategory.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Structure/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/PseudonaturalTransformation/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/dec_fields.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HFiber.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups/QuotientGroup.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Rings/Z.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Tactics/BinderApply.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Utf8.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/Wedge.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Contrib/SetoidRewrite.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/groups.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/SetCategory/Functors/SetProp.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/fields.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Diagrams/Cocone.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Finite/Tactics.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/Join.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/ua_first_isomorphism.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/SetCategory/Functors.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Pointed/pMap.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Profunctor/Representable.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Functorial/Laws.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/FunctorCategory/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbGroups/AbelianGroup.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Pi.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/FunctorCategory/Dual.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/Arrow.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Diagrams/Cone.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/tactics/ring_quote.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Utf8.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/ExcludedMiddle.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/Empty.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/HomotopyGroup.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Pointwise.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Composition/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Comma/Functorial.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups/GrpPullback.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/ua_algebra.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Univalent.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/GroupoidCategory/Dual.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Grothendieck.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Cubical/DPathSquare.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/HomCoercions.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Yoneda.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/EquivGpd.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Comma/ProjectionFunctors.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Tactics/BinderApply.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Utf8.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/EMSpace.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Torus/TorusEquivCircles.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Int.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/naturals.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/ObjectClassifier.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Metatheory/FunextVarieties.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/Equiv.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Limits/Equalizer.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Square.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/Colimit_Flattening.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/ua_second_isomorphism.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Truncations.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/lattices.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Paths.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/SetCategory/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Universal/Operation.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Pos.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/Smash.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/CategoryOfGroupoids.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Universe.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Nat.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Comma/InducedFunctors.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/FunctorCat.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Finite/FinSeq.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/HSpace/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HIT/Flattening.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Notations.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Topological.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Pseudofunctor/FromFunctor.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Composition/Laws.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Notations.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbGroups/AbPushout.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Dual.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/BAut/Cantor.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/ua_third_isomorphism.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/MappingCylinder.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/apartness.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Diagrams/Diagram.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/EquivGroupoids.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Hexadecimal.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Int/LoopExp.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/UnitCounitCoercions.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/CoreflectiveSubuniverse.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Functorial.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/InitialTerminalCategory/Notations.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups/Presentation.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/Colimit_Pushout.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HoTT.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Limits/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Int/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Comma/Utf8.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Prod.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/Bool.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Numeral.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Rings/QuotientRing.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Pos/Spec.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Constant.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Projective.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HIT/epi.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Decimal.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/integers.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/HSpace/Moduli.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Notations.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Rings/ChineseRemainder.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Profunctor/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law4/Functors.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Decidable.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Dual.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/orders/nat_int.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/ua_prod_algebra.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/ua_subalgebra.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Sigma/OnMorphisms.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Card.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Identity.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Finite/FinNat.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Tactics/EvalIn.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Limits/Limit.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Tactics/EvalIn.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/TruncType.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Universal/Homomorphism.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Profunctor/Identity.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Universal/Algebra.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Profunctor/Utf8.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Isomorphisms.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Dual.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/FunctorCategory/Notations.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/UniversalMorphisms/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Pointed/pTrunc.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HSet.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Opposite.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/ua_isomorphic.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Profunctor/Notations.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Attributes.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/KanExtensions/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/Colimit_Sigma.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Contrib/UniverseLevel.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Comma/Notations.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/BAut/Rigid.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HProp.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/cauchy.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Dual.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Metatheory/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Sets/GCH.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Composition/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Subcategory.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/SetCategory/Morphisms.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Metatheory/IntervalImpliesFunext.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Subcategory/Full.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/UnitCat.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Nat.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/int_abs.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/PathAny.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbSES/Ext.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/Unit.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Contractible.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/isomorphisms/rings.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Core.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/List.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Sigma/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HIT/FreeIntQuotient.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Structure/Utf8.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Torus/Torus.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Composition/Laws.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Subcategory/Wide.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/Cover.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ProductLaws.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Structure/IdentityPrinciple.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbSES/DirectSum.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/implementations/ne_list.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Pointed/pEquiv.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/PointedCat.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Tactics.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/DiscreteCategory.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Logic.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Pointed/pFiber.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/WhiteheadsPrinciple.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Metatheory/UnivalenceImpliesFunext.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Utf8.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Diagrams/CommutativeSquares.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/BoundedSearch.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Strict.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Pointwise/Properties.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/FunctorCategory/Morphisms.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/PropResizing/PropResizing.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Prod/Universal.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Equiv/PathSplit.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Monoidal/MonoidalCategory.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/HSpace/Pointwise.v../ocaml-base-compiler.4.14.0/doc/coq-hott/README.md../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/implementations/list.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/tactics/ring_tac.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Cubical.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Nullification.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/orders/fields.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Sum.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbGroups/Centralizer.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Metatheory/UnivalenceVarieties.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Structure/Notations.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Induced.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Datatypes.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Paths.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/InitialTerminalCategory/Functors.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Composition/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Prod/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Pointwise/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Utf8.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/orders/archimedean.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Closed.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/orders/dec_fields.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law0.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/Bouquet.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Hom.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/implementations/hprop_lattice.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Grothendieck/ToSet/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Functorial/Parts.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Misc.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Axioms/Univalence.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Open.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Tests.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Int/Equiv.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Diagrams/Graph.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ChainCategory.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Profunctor/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbGroups/Cyclic.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Bifunctor.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Universal/Congruence.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/PropResizing/ImpredicativeTruncation.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Pseudofunctor/Identity.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Identity.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/HSpaceS1.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/orders/integers.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/categories/ua_category.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/TwoSphere.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Sigma/OnObjects.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Comma/Projection.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Universe.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Monoidal.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/FundamentalPreGroupoidCategory.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Functorial/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/BAut/Bool/IncoherentIdempotent.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups/ShortExactSequence.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Composition/LawsTactic.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Pointed/pHomotopy.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/additional_operations.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/ua_congruence.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law1/Functors.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/Colimit_Pushout_Flattening.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Paths.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/orders/naturals.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/IndiscreteCategory.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/NullHomotopy.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/theory/nat_distance.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Finite/FinInduction.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Prod.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Composition/Functorial/Attributes.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Pointwise.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/Colimit_Coequalizer.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Paths.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Cat/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/GroupoidCategory/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Equiv/Relational.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/implementations/family_prod.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/DualFunctor.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbGroups/AbHom.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/TwoOneCat.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/No/Negation.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/HomotopyPreCategory.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Sets/AC.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups/Kernel.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/InitialTerminalCategory/Pseudofunctors.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/implementations/pointwise.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NatCategory.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/SetCategory/Functors/SetProp.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Objects.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Sets/Powers.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/EncodeDecode.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Pointed/pSect.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Identity.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/HomFunctor.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Limits/Functors.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/SuccessorStructure.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups/Image.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Sum.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Torus/TorusHomotopy.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Composition/Functorial/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/Empty.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/InitialTerminalCategory/NaturalTransformations.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/SimplicialSets.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Composition/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Tactics/Nameless.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Comma/Dual.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/CategoryOfSections/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/SpanPushout.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/ua_setalgebra.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Forall.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Diagrams/ConstantDiagram.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Prod/Functorial.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Pointed/pModality.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/ExcludedMiddle.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Metatheory/PropTrunc.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/GraphQuotient.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups/GroupCoeq.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Grothendieck/ToSet/Univalent.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Grothendieck/ToSet/Morphisms.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/InitialTerminalCategory/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/FunctorCategory/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups/Lagrange.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/DependentProduct.v../ocaml-base-compiler.4.14.0/doc/coq-hott/LICENSE.txt../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/SemiSimplicialSets.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/KanExtensions/Functors.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Pi.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HIT/Interval.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Composition/IdentityLaws.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/Freudenthal.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law3/Functors.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Truncations/SeparatedTrunc.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/LaxComma/Utf8.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Sum.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law2/Law.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types/WType.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/FunctorCategory/Functorial.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbGroups/AbProjective.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Dual.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law2/Functors.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Colimits/Colimit_Prod.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Equiv/BiInv.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/integers.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law4/Law.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Composition/AssociativityLaw.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Logic.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Sigma.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law3/Law.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Composition/Functorial.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Comma/Utf8.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/FunctorCategory/Dual.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Prod.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law1/Law.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Cat/Morphisms.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Functorish.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Cantor.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Dual.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbGroups/Z.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Diagrams/DDiagram.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Diagrams/Sequence.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spectra/Spectrum.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Axioms/Funext.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/rationals.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HIT/surjective_factor.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/naturals.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/SetCategory/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Profunctor/Representable.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Dual.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HIT/iso.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Tactics/Nameless.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/tests/ring_tac.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/orders/sum.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/List.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Metatheory/TruncImpliesFunext.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Metatheory/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Univalent.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/Pi1S1.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Sum.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbGroups/AbPullback.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Dual.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/EvaluationFibration.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/implementations/assume_rationals.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/GroupoidCategory/Morphisms.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HIT/unique_choice.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/HSpace/Coherent.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Grothendieck/ToCat.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Utf8.v../ocaml-base-compiler.4.14.0/lib/coq-hott/opam../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/GroupoidCategory/Dual.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Limits/Equalizer.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Diagrams/ParallelPair.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/PropResizing/PropResizing.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/InitialTerminalCategory.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics/Numeral.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/CategoryOfGroupoids.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Notnot.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/archimedean.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Identity.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Misc.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Diagrams/Span.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Comma.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/FunctorCategory.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/SetCategory.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Profunctor/Identity.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Modalities/Identity.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Composition.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Identity.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Notations.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/UnitCat.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Groups.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/Wedge.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/EmptyCat.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Strict.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Grothendieck/ToSet.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbGroups.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Notations.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Metatheory/IntervalImpliesFunext.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/WildCat/Paths.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Sigma.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Notations.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Composition.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Grothendieck.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Notations.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/implementations/bool.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Composition.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Prod.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Utf8.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/NaturalTransformation/Utf8.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/round.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/HIT/SetCone.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Pseudofunctor.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Utf8.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Finite/Tactics.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Aut.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Classes/interfaces/monad.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Congruence.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Utf8.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/DiscreteCategory.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/GroupoidCategory.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Types.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/LaxComma.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/ooAction.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Basics.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/FunctorCategory/Utf8.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Structure.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Axioms/Univalence.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Profunctor.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/InitialTerminalCategory/Notations.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/LaxComma/Notations.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Diagrams/Graph.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Pointed.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Axioms/Funext.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Subcategory/Wide.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Comma/Notations.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Notations.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Subcategory/Full.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/Rings.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law3.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Algebra/AbSES.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Functorial.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law2.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/Core.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Structure/Utf8.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/FunctorCategory/Notations.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law1.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Limits.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Pointwise.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/KanExtensions.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/ExponentialLaws/Law4.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Profunctor/Notations.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Profunctor/Utf8.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Functor/Composition/Functorial.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Finite.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/PseudonaturalTransformation.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Cat.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Cubical.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Category/Subcategory.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Int.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Adjoint/UniversalMorphisms.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/No.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Truncations.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/SetCategory/Functors.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Homotopy/HSpace.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/CategoryOfSections.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Categories/Structure/Notations.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Pos.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/HoTT/Spaces/Nat.v../ocaml-base-compiler.4.14.0/lib/coq-hott/METAopam remove -y coq-hott.8.17