CONTENTS.md

Contents of the UniMath library

The packages and files are listed here in logical order: each file depends only on files occurring earlier.

Package Foundations

• Init.v
• Preamble.v
• PartA.v
• PartB.v
• UnivalenceAxiom.v
• PartC.v
• PartD.v
• UnivalenceAxiom2.v
• Propositions.v
• Sets.v
• NaturalNumbers.v
• Tests.v
• HLevels.v
• All.v

Package MoreFoundations

• Bool.v
• Test.v
• WeakEquivalences.v
• Tactics.v
• PartA.v
• PathsOver.v
• Propositions.v
• Nat.v
• Notations.v
• AlternativeProofs.v
• DoubleNegation.v
• DecidablePropositions.v
• NullHomotopies.v
• Interval.v
• NegativePropositions.v
• Sets.v
• Orders.v
• Equivalences.v
• MoreEquivalences.v
• QuotientSet.v
• Subtypes.v
• AxiomOfChoice.v
• StructureIdentity.v
• Univalence.v
• NoInjectivePairing.v
• PartD.v
• All.v

Package Combinatorics

• StandardFiniteSets.v
• Vectors.v
• VectorsTests.v
• Lists.v
• FiniteSets.v
• KFiniteTypes.v
• KFiniteSubtypes.v
• Graph.v
• CGraph.v
• GraphPaths.v
• Equivalence_Relations.v
• WellFoundedRelations.v
• ZFstructures.v
• FiniteSequences.v
• BoundedSearch.v
• MetricTree.v
• Tests.v
• DecSet.v
• Maybe.v
• MoreLists.v
• Tuples.v
• All.v

Package Algebra

• BinaryOperations.v
• Monoids2.v
• AbelianMonoids.v
• Monoids.v
• Groups2.v
• AbelianGroups.v
• Groups.v
• GroupAction.v
• RigsAndRings.v
• RigsAndRings/Ideals.v
• Domains_and_Fields.v
• DivisionRig.v
• Apartness.v
• ConstructiveStructures.v
• Archimedean.v
• IteratedBinaryOperations.v
• Free_Monoids_and_Groups.v
• Tests.v
• Modules/Core.v
• Modules/Submodule.v
• Modules/Multimodules.v
• Modules/Examples.v
• Modules/Quotient.v
• Modules.v
• Matrix.v
• Universal/HVectors.v
• Universal/SortedTypes.v
• Universal/Signatures.v
• Universal/Algebras.v
• Universal/Terms.v
• Universal/TermAlgebras.v
• Universal/VTerms.v
• Universal/FreeAlgebras.v
• Universal/Equations.v
• Universal/EqAlgebras.v
• Universal/WTypes.v
• Universal/Examples/Nat.v
• Universal/Examples/Bool.v
• Universal/Examples/Monoid.v
• Universal/Examples/Group.v
• Universal/Examples/ListDataType.v
• Universal/Examples/Tests.v
• Universal.v
• GaussianElimination/Auxiliary.v
• GaussianElimination/Vectors.v
• GaussianElimination/Matrices.v
• GaussianElimination/RowOps.v
• GaussianElimination/Elimination.v
• GaussianElimination/Corollaries.v
• GaussianElimination/Tests.v
• All.v

Package Tactics

• EnsureStructuredProofs.v
• Utilities.v
• Monoids_Tactics.v
• Abmonoids_Tactics.v
• Groups_Tactics.v
• Nat_Tactics.v
• All.v

Package NumberSystems

• NaturalNumbersAlgebra.v
• NaturalNumbers_le_Inductive.v
• Integers.v
• RationalNumbers.v
• Tests.v
• All.v

Package SyntheticHomotopyTheory

• Coproduct.v
• Halfline.v
• AffineLine.v
• Circle.v
• Circle2.v
• Test.v
• All.v

Package PAdics

• lemmas.v
• fps.v
• frac.v
• z_mod_p.v
• padics.v
• All.v

Package OrderTheory

• Preorders.v
• Posets/Basics.v
• Posets/MonotoneFunctions.v
• Posets/PosetSum.v
• Posets/PointedPosets.v
• Posets/LiftPoset.v
• Posets/QuotientPoset.v
• Posets/Subposets.v
• Posets.v
• Posets/Examples/StandardFiniteSet.v
• Lattice/Lattice.v
• Lattice/Bounded.v
• Lattice/Complement.v
• Lattice/Distributive.v
• Lattice/Heyting.v
• Lattice/CompleteHeyting.v
• Lattice/DerivedLawsCompleteHeyting.v
• Lattice/Boolean.v
• Lattice/Examples/FromPartialOrder.v
• Lattice/Examples/Bool.v
• Lattice/Examples/Subsets.v
• Lattice/Examples/Sieves.v
• Lattice/Examples/Trivial.v
• Lattice/Examples/ScottOpen.v
• Lattice/Examples/RegularElements.v
• Prebilattice/Prebilattice.v
• Prebilattice/Interlaced.v
• Prebilattice/Distributive.v
• Prebilattice/PrebilatticeDisplayedCat.v
• Prebilattice/Product.v
• Prebilattice/Examples/FOUR.v
• OrderedSets/OrderedSets.v
• OrderedSets/WellOrderedSets.v
• DCPOs/Core/DirectedSets.v
• DCPOs/Core/Basics.v
• DCPOs/Core/WayBelow.v
• DCPOs/Basis/Continuous.v
• DCPOs/Basis/Algebraic.v
• DCPOs/Core/ScottTopology.v
• DCPOs/Core/IntrinsicApartness.v
• DCPOs/Core/ScottContinuous.v
• DCPOs/Basis/Basis.v
• DCPOs/Basis/CompactBasis.v
• DCPOs/Elements/Sharp.v
• DCPOs/Elements/Maximal.v
• DCPOs/Examples/Unit.v
• DCPOs/Examples/Propositions.v
• DCPOs/Examples/Discrete.v
• DCPOs/Examples/SubDCPO.v
• DCPOs/Examples/Fixpoints.v
• DCPOs/Examples/Equalizers.v
• DCPOs/Examples/BinaryProducts.v
• DCPOs/Examples/Products.v
• DCPOs/Examples/BinarySums.v
• DCPOs/Examples/Sums.v
• DCPOs/Examples/IdealCompletion.v
• DCPOs/Core/FubiniTheorem.v
• DCPOs/Core/CoordinateContinuity.v
• DCPOs/Examples/Exponentials.v
• DCPOs/FixpointTheorems/LeastFixpoint.v
• DCPOs/FixpointTheorems/Pataraia.v
• DCPOs/AlternativeDefinitions/Dcpo.v
• DCPOs/AlternativeDefinitions/FixedPointTheorems.v
• DCPOs.v
• All.v

Package CategoryTheory

• Core/Categories.v
• Core/Isos.v
• Core/Univalence.v
• Core/TwoCategories.v
• Core/TransportMorphisms.v
• Core/Functors.v
• Core/NaturalTransformations.v
• Core/Setcategories.v
• Core/EssentiallyAlgebraic.v
• Core/Prelude.v
• FunctorCategory.v
• whiskering.v
• BicatOfCatsElementary.v
• DisplayedCats/Core.v
• DisplayedCats/Isos.v
• DisplayedCats/Functors.v
• DisplayedCats/NaturalTransformations.v
• DisplayedCats/Univalence.v
• DisplayedCats/DisplayedFunctorEq.v
• DisplayedCats/Total.v
• DisplayedCats/Fiber.v
• DisplayedCats/FullyFaithfulDispFunctor.v
• opp_precat.v
• OppositeCategory/Core.v
• Groupoids.v
• ZigZag.v
• ProductCategory.v
• PrecategoryBinProduct.v
• Categories/HSET/Core.v
• CategorySum.v
• Subcategory/Core.v
• Subcategory/Full.v
• Retracts.v
• Monics.v
• Epis.v
• SplitMonicsAndEpis.v
• HomotopicalCategory.v
• Adjunctions/Core.v
• Adjunctions/AdjunctionMonics.v
• Monads/RelativeMonads.v
• Monads/RelMonads_Coreflection.v
• Monads/RelativeModules.v
• Equivalences/Core.v
• Equivalences/CompositesAndInverses.v
• Equivalences/FullyFaithful.v
• Equivalences/EquivalenceFromComp.v
• Subcategory/FullEquivalences.v
• Categories/HSET/MonoEpiIso.v
• Categories/HSET/Univalence.v
• CategoriesWithBinOps.v
• PrecategoriesWithAbgrops.v
• covyoneda.v
• Limits/Cones.v
• Limits/Equalizers.v
• Limits/Graphs/Colimits.v
• Limits/Graphs/Limits.v
• Limits/Graphs/EqDiag.v
• Limits/Coproducts.v
• Limits/Products.v
• Limits/Initial.v
• Limits/Terminal.v
• Limits/Zero.v
• Limits/BinCoproducts.v
• Limits/BinProducts.v
• Limits/Graphs/BinCoproducts.v
• Limits/Graphs/Coproducts.v
• Limits/Graphs/BinProducts.v
• Limits/Pullbacks.v
• Limits/Graphs/Initial.v
• Limits/Graphs/Terminal.v
• Limits/Graphs/Zero.v
• Limits/Graphs/Pullbacks.v
• Limits/Coequalizers.v
• Limits/Kernels.v
• Limits/Cokernels.v
• PreAdditive.v
• Limits/Pushouts.v
• Limits/Graphs/Pushouts.v
• Limits/Graphs/Equalizers.v
• Limits/Graphs/Coequalizers.v
• Limits/Graphs/Kernels.v
• Limits/Graphs/Cokernels.v
• Limits/Cats/Limits.v
• Limits/BinDirectSums.v
• Limits/FinOrdProducts.v
• Limits/FinOrdCoproducts.v
• Limits/Opp.v
• Limits/LimitIso.v
• Limits/Preservation.v
• Limits/EquivalencePreservation.v
• Limits/PreservationProperties.v
• Limits/Ends.v
• Limits/Coends.v
• Limits/PullbackConstructions.v
• RegularAndExact/RegularEpi.v
• RegularAndExact/RegularCategory.v
• RegularAndExact/RegularEpiFacts.v
• RegularAndExact/ExactCategory.v
• SubobjectClassifier/PreservesSubobjectClassifier.v
• DisplayedCats/Binproducts.v
• DisplayedCats/Fiberwise/FiberwiseTerminal.v
• DisplayedCats/Fiberwise/FiberwiseInitial.v
• DisplayedCats/Fiberwise/FiberwiseProducts.v
• DisplayedCats/Fiberwise/FiberwiseCoproducts.v
• DisplayedCats/Fiberwise/FiberwiseEqualizers.v
• DisplayedCats/Fiberwise/FiberwiseCartesianClosed.v
• DisplayedCats/Fiberwise/DependentSums.v
• DisplayedCats/Fiberwise/DependentProducts.v
• DisplayedCats/Fiberwise/FiberwiseSubobjectClassifier.v
• DisplayedCats/Codomain/FiberCod.v
• DisplayedCats/Codomain/CodDomain.v
• DisplayedCats/Codomain/CodMorphisms.v
• DisplayedCats/Codomain/CodLeftAdjoint.v
• DisplayedCats/Codomain/CodLimits.v
• DisplayedCats/Codomain/CodColimits.v
• DisplayedCats/Codomain/IteratedSlice.v
• DisplayedCats/Codomain/CodFunctor.v
• DisplayedCats/Codomain/CodSubobjectClassifier.v
• DisplayedCats/Codomain/CodRegular.v
• DisplayedCats/MonoCodomain/FiberMonoCod.v
• DisplayedCats/MonoCodomain/MonoCodFunctor.v
• DisplayedCats/MonoCodomain/Inclusion.v
• DisplayedCats/MonoCodomain/MonoCodLimits.v
• DisplayedCats/MonoCodomain/MonoCodLeftAdjoint.v
• DisplayedCats/MonoCodomain/MonoCodColimits.v
• DisplayedCats/MonoCodomain/MonoCodRightAdjoint.v
• DisplayedCats/MonoCodomain/MonoHyperdoctrine.v
• Hyperdoctrines/Hyperdoctrine.v
• Hyperdoctrines/FirstOrderHyperdoctrine.v
• Hyperdoctrines/Tripos.v
• Hyperdoctrines/GenericPredicate.v
• Hyperdoctrines/PartialEqRels/PERs.v
• Hyperdoctrines/PartialEqRels/PERMorphisms.v
• Hyperdoctrines/PartialEqRels/PERCategory.v
• Hyperdoctrines/PartialEqRels/PERConstantObjects.v
• Hyperdoctrines/PartialEqRels/PERTerminal.v
• Hyperdoctrines/PartialEqRels/PERInitial.v
• Hyperdoctrines/PartialEqRels/PERBinProducts.v
• Hyperdoctrines/PartialEqRels/PEREqualizers.v
• Hyperdoctrines/PartialEqRels/PERMonomorphisms.v
• Hyperdoctrines/PartialEqRels/PERSubobjectClassifier.v
• Hyperdoctrines/PartialEqRels/ExponentialPER.v
• Hyperdoctrines/PartialEqRels/ExponentialEval.v
• Hyperdoctrines/PartialEqRels/ExponentialLam.v
• Hyperdoctrines/PartialEqRels/ExponentialEqs.v
• Hyperdoctrines/PartialEqRels/PERExponentials.v
• Hyperdoctrines/PartialEqRels/Logic/SubobjectDispCat.v
• Hyperdoctrines/PartialEqRels/Logic/MonoEquiv.v
• Hyperdoctrines/PartialEqRels/Logic/Truth.v
• Hyperdoctrines/PartialEqRels/Logic/Falsity.v
• Hyperdoctrines/PartialEqRels/Logic/Conjunction.v
• Hyperdoctrines/PartialEqRels/Logic/Disjunction.v
• Hyperdoctrines/PartialEqRels/Logic/Implication.v
• Hyperdoctrines/PartialEqRels/Logic/Existential.v
• Hyperdoctrines/PartialEqRels/Logic/Universal.v
• Hyperdoctrines/PartialEqRels/InternalLogic.v
• Hyperdoctrines/TriposToTopos.v
• DisplayedCats/Examples/HValuedPredicates.v
• Hyperdoctrines/HValuedSets.v
• LocallyCartesianClosed/LocallyCartesianClosed.v
• DisplayedCats/Fiberwise/DualBeckChevalley.v
• DisplayedCats/Codomain/CodRightAdjoint.v
• LocallyCartesianClosed/Preservation.v
• Limits/StrictInitial.v
• Limits/DisjointBinCoproducts.v
• DisplayedCats/Codomain/ColimitProperties.v
• Limits/Examples/CategoryProductLimits.v
• Limits/StandardDiagrams.v
• Limits/Filtered.v
• IsoCommaCategory.v
• Limits/Examples/IsoCommaLimits.v
• CommaCategories.v
• Categories/Quotient.v
• Arithmetic/NNO.v
• Arithmetic/ParameterizedNNO.v
• DisplayedCats/Codomain/CodNNO.v
• Subcategory/Limits.v
• EpiFacts.v
• Categories/Type/Core.v
• Categories/Type/MonoEpiIso.v
• SimplicialSets.v
• yoneda.v
• FunctorCoalgebras.v
• precomp_fully_faithful.v
• precomp_ess_surj.v
• PrecompEquivalence.v
• UnitorsAndAssociatorsForEndofunctors.v
• PointedFunctors.v
• HorizontalComposition.v
• PointedFunctorsComposition.v
• ArrowCategory.v
• RightKanExtension.v
• coslicecat.v
• catiso.v
• DisplayedCats/CatIsoDisplayed.v
• CategoryEquality.v
• Core/PosetCat.v
• WeakEquivalences/Core.v
• WeakEquivalences/Terminal.v
• WeakEquivalences/Preservation/Binproducts.v
• WeakEquivalences/Reflection/BinProducts.v
• WeakEquivalences/Creation/BinProducts.v
• WeakEquivalences/LiftPreservation/BinProducts.v
• WeakEquivalences/Preservation/Equalizers.v
• WeakEquivalences/Reflection/Equalizers.v
• WeakEquivalences/Creation/Equalizers.v
• WeakEquivalences/LiftPreservation/Equalizers.v
• WeakEquivalences/Preservation/Pullbacks.v
• WeakEquivalences/Reflection/Pullbacks.v
• WeakEquivalences/Creation/Pullbacks.v
• WeakEquivalences/LiftPreservation/Pullbacks.v
• RezkCompletions/RezkCompletions.v
• RezkCompletions/Construction.v
• exponentials.v
• slicecat.v
• Limits/PullbacksSliceProductsEquiv.v
• Additive.v
• Abelian.v
• category_binops.v
• AbelianToAdditive.v
• Morphisms.v
• ExactCategories/ExactCategories.v
• ExactCategories/Tests.v
• ShortExactSequences.v
• AdditiveFunctors.v
• LocalizingClass.v
• UnderCategories.v
• Subobjects.v
• SubobjectClassifier/SubobjectClassifier.v
• SubobjectClassifier/SubobjectClassifierIso.v
• Quotobjects.v
• AbelianPushoutPullback.v
• PseudoElements.v
• FiveLemma.v
• LatticeObject.v
• Actions.v
• PowerObject.v
• ElementaryTopos.v
• Adjunctions/Restriction.v
• Adjunctions/Examples.v
• Subcategory/Reflective.v
• Categories/PrecategoryOfCategories.v
• Categories/CategoryOfSetCategories.v
• Categories/CategoryOfSetGroupoids.v
• Limits/Examples/CategoryOfSetcategoriesLimits.v
• Limits/Examples/CategoryOfSetGroupoidsLimits.v
• Categories/SetWith2BinOp.v
• Categories/Monoid.v
• Categories/Abmonoid.v
• Categories/Gr.v
• Categories/Abgr.v
• Categories/Rig.v
• Categories/Commrig.v
• Categories/Ring.v
• Categories/Commring.v
• Categories/Intdom.v
• Categories/Fld.v
• Categories/Module.v
• Categories/StandardCategories.v
• Categories/PreorderCategory/Core.v
• Categories/PreorderCategory/Sieves.v
• Categories/MonoidToCategory.v
• Limits/Examples/UnitCategoryLimits.v
• Categories/Type/Colimits.v
• Categories/Type/Limits.v
• Categories/Type/Structures.v
• Categories/Type/Univalence.v
• Categories/Type/NoHomsets.v
• Categories/HSET/Limits.v
• Categories/HSET/Colimits.v
• Categories/HSET/FilteredColimits.v
• Categories/HSET/Slice.v
• Categories/HSET/Structures.v
• Categories/HSET/SliceFamEquiv.v
• Categories/HSET/All.v
• Profunctors/Core.v
• Categories/HSET/SetCoends.v
• Profunctors/Examples.v
• Profunctors/Transformation.v
• Profunctors/Squares.v
• Profunctors/Collage.v
• SetValuedFunctors.v
• Categories/FinSet.v
• Categories/Woset.v
• Categories/Graph.v
• Categories/CGraph.v
• Presheaf.v
• ElementsOp.v
• elems_slice_equiv.v
• YonedaBinproducts.v
• YonedaExponentials.v
• ExponentiationLeftAdjoint.v
• GrothendieckToposes/Sieves.v
• GrothendieckToposes/Topologies.v
• GrothendieckToposes/Sites.v
• GrothendieckToposes/Sheaves.v
• GrothendieckToposes/Toposes.v
• GrothendieckToposes/Examples/TerminalSheaf.v
• GrothendieckToposes/Examples/EmptySieve.v
• GrothendieckToposes/Examples/DiscreteTopology.v
• GrothendieckToposes/Examples/IndiscreteTopology.v
• Connected.v
• LeftKanExtension.v
• Categories/CartesianCubicalSets.v
• OppositeCategory/OppositeAdjunction.v
• OppositeCategory/OppositeOfFunctorCategory.v
• Chains/Chains.v
• Chains/Cochains.v
• DisplayedCats/Examples/DispFunctorPair.v
• DisplayedCats/Examples/Opposite.v
• DisplayedCats/Fibrations.v
• DisplayedCats/Examples/Reindexing.v
• DisplayedCats/PreservesCleaving.v
• DisplayedCats/Constructions/CategoryWithStructure.v
• DisplayedCats/Constructions/DisplayedFunctorCat.v
• DisplayedCats/Constructions/FullSubcategory.v
• DisplayedCats/Constructions/Product.v
• DisplayedCats/Constructions/DisplayedSections.v
• DisplayedCats/Constructions/FunctorLift.v
• DisplayedCats/Constructions.v
• FunctorAlgebras.v
• CompletelyIterativeAlgebras.v
• Chains/Adamek.v
• Chains/CoAdamek.v
• Chains/OmegaCocontFunctors.v
• OppositeCategory/LimitsAsColimits.v
• Chains/OmegaContFunctors.v
• Chains/All.v
• Inductives/Lists.v
• Inductives/Trees.v
• Inductives/LambdaCalculus.v
• Inductives/PropositionalLogic.v
• CategoricalRecursionSchemes.v
• PointedFunctorAlgebras.v
• DisplayedCats/Equivalences.v
• DisplayedCats/EquivalenceOverId.v
• DisplayedCats/DisplayedCatEq.v
• DisplayedCats/Codomain.v
• DisplayedCats/Examples/MonoCodomain.v
• DisplayedCats/Projection.v
• DisplayedCats/SIP.v
• DisplayedCats/Examples/SetGroupoidsIsoFib.v
• DisplayedCats/Examples/SetGroupoidComprehension.v
• Monads/Monads.v
• Monads/LModules.v
• Monads/Derivative.v
• Monads/MonadAlgebras.v
• Monads/Comonads.v
• Monads/ComonadCoalgebras.v
• DisplayedCats/Limits.v
• DisplayedCats/Examples/Sigma.v
• DisplayedCats/Examples.v
• DisplayedCats/Examples/UnitalBinop.v
• DisplayedCats/Examples/CategoryOfPosets.v
• DisplayedCats/Structures/CartesianStructure.v
• DisplayedCats/Structures/StructureLimitsAndColimits.v
• DisplayedCats/Structures/StructuresSmashProduct.v
• DisplayedCats/Examples/AlgebraStructures.v
• DisplayedCats/Examples/Cartesian.v
• DisplayedCats/Examples/DCPOStructures.v
• DisplayedCats/Examples/PointedDCPOStructures.v
• DisplayedCats/Examples/PointedDCPOStrict.v
• DisplayedCats/Examples/PointedPosetStrict.v
• DisplayedCats/Examples/PointedPosetStructures.v
• DisplayedCats/Examples/PointedSetStructures.v
• DisplayedCats/Examples/PosetStructures.v
• DisplayedCats/Examples/SetStructures.v
• DisplayedCats/Examples/Arrow.v
• DisplayedCats/Examples/MonadAlgebras.v
• DisplayedCats/Examples/Three.v
• DisplayedCats/FunctorCategory.v
• DisplayedCats/Adjunctions.v
• DisplayedCats/ComprehensionC.v
• DisplayedCats/StreetFibration.v
• DisplayedCats/StreetOpFibration.v
• DisplayedCats/ReindexingForward.v
• DisplayedCats/TotalCategoryFacts.v
• DisplayedCats/TotalAdjunction.v
• Monads/KleisliCategory.v
• Monads/KTriples.v
• Monads/Kleisli.v
• Monads/KTriplesEquiv.v
• Limits/Examples/AlgebraStructuresColimits.v
• Categories/Dialgebras.v
• Categories/CatIsoInserter.v
• Categories/EilenbergMoore.v
• Categories/CoEilenbergMoore.v
• Categories/KleisliCategory.v
• Limits/Examples/EilenbergMooreLimits.v
• Elements.v
• Core.v
• Categories/Universal_Algebra/Algebras.v
• Categories/Universal_Algebra/EqAlgebras.v
• Categories/Rel.v
• Monoidal/WhiskeredBifunctors.v
• Monoidal/Categories.v
• Monoidal/StrongMonad.v
• Monoidal/Structure/Symmetric.v
• Monoidal/Structure/SymmetricDiagonal.v
• Monoidal/Structure/Closed.v
• Monoidal/Structure/Cartesian.v
• Monoidal/Functors.v
• Monoidal/FunctorCategories.v
• Monoidal/Adjunctions.v
• Monoidal/CategoriesOfMonoids.v
• Monoidal/Displayed/WhiskeredDisplayedBifunctors.v
• Monoidal/Displayed/Monoidal.v
• Monoidal/Displayed/TotalMonoidal.v
• Monoidal/Displayed/MonoidalSections.v
• Monoidal/Displayed/TransportLemmas.v
• Monoidal/Displayed/Symmetric.v
• Monoidal/Displayed/SymmetricMonoidalBuilder.v
• Monoidal/Examples/SetCartesianMonoidal.v
• Monoidal/Examples/CartesianMonoidal.v
• Monoidal/Examples/DisplayedCartesianMonoidal.v
• Monoidal/Examples/StructuresMonoidal.v
• Monoidal/Examples/EndofunctorsMonoidalElementary.v
• Monoidal/Examples/MonadsAsMonoidsElementary.v
• Monoidal/Examples/MonoidalPointedObjects.v
• Monoidal/Displayed/MonoidalFunctorLifting.v
• Monoidal/Examples/MonoidalDialgebras.v
• Monoidal/Examples/SymmetricMonoidalDialgebras.v
• Monoidal/Examples/PointedSetCartesianMonoidal.v
• Monoidal/Examples/BinopCartesianMonoidal.v
• Monoidal/Examples/SetWithSubset.v
• Monoidal/Examples/SmashProductMonoidal.v
• Monoidal/Examples/PosetsMonoidal.v
• Monoidal/Examples/Fullsub.v
• Monoidal/Examples/Relations.v
• Monoidal/Examples/Sigma.v
• Monoidal/Examples/DiagonalFunctor.v
• Monoidal/Examples/ConstantFunctor.v
• Monoidal/Comonoids/Category.v
• Monoidal/Comonoids/Tensor.v
• Monoidal/Comonoids/Monoidal.v
• Monoidal/Comonoids/Symmetric.v
• Monoidal/Comonoids/MonoidalCartesianBuilder.v
• Monoidal/Comonoids/CommComonoidsCartesian.v
• Monoidal/Comonoids/CartesianAsComonoids.v
• Monoidal/Comonoids/TransportComonoidAlongRetraction.v
• Monoidal/Examples/LiftPoset.v
• Monoidal/Examples/SymmetricMonoidalCoEilenbergMoore.v
• Monoidal/AlternativeDefinitions/MonoidalCategoriesReordered.v
• Monoidal/AlternativeDefinitions/MonoidalCategoriesTensored.v
• Monoidal/AlternativeDefinitions/EquivalenceWhiskeredNonCurriedMonoidalCategories.v
• Monoidal/AlternativeDefinitions/MonoidalCategoriesCurried.v
• Monoidal/AlternativeDefinitions/MonoidalFunctorsTensored.v
• Monoidal/AlternativeDefinitions/MonoidalFunctorsCurried.v
• Monoidal/AlternativeDefinitions/AugmentedSimplexCategory.v
• Monoidal/AlternativeDefinitions/DisplayedMonoidalTensored.v
• Monoidal/AlternativeDefinitions/DisplayedMonoidalCurried.v
• Monoidal/AlternativeDefinitions/CategoriesOfMonoids.v
• Monoidal/AlternativeDefinitions/BraidedMonoidalCategories.v
• Monoidal/AlternativeDefinitions/TotalDisplayedMonoidalCurried.v
• Monoidal/AlternativeDefinitions/MonoidalFunctorCategory.v
• Actegories/Actegories.v
• Actegories/ConstructionOfActegories.v
• Actegories/MorphismsOfActegories.v
• Actegories/ProductActegory.v
• Actegories/ProductsInActegories.v
• Actegories/CoproductsInActegories.v
• Actegories/Examples/ActionOfEndomorphismsInCATElementary.v
• Actegories/Examples/SelfActionInCATElementary.v
• Actegories/ConstructionOfActegoryMorphisms.v
• Actegories/ActionBasedStrongMonads.v
• DisplayedCats/MoreFibrations/Prefibrations.v
• DisplayedCats/MoreFibrations/CartesiannessOfComposites.v
• DisplayedCats/MoreFibrations/FibrationsCharacterisation.v
• DisplayedCats/MoreFibrations/DispCatsEquivFunctors.v
• DisplayedCats/MoreFibrations/DisplayedDisplayedCats.v
• SkewMonoidal/SkewMonoidalCategories.v
• SkewMonoidal/CategoriesOfMonoids.v
• EnrichedCats/BenabouCosmos.v
• EnrichedCats/EnrichedRelation.v
• EnrichedCats/LaxExtension.v
• EnrichedCats/Enrichment.v
• EnrichedCats/EnrichmentFunctor.v
• EnrichedCats/EnrichmentTransformation.v
• EnrichedCats/FullyFaithful.v
• EnrichedCats/EnrichmentAdjunction.v
• EnrichedCats/EnrichmentMonad.v
• EnrichedCats/Enriched/Enriched.v
• EnrichedCats/Enriched/ChangeOfBase.v
• EnrichedCats/Enriched/Opposite.v
• EnrichedCats/Enriched/UnderlyingCategory.v
• EnrichedCats/Enriched/EnrichmentEquiv.v
• EnrichedCats/Examples/SelfEnriched.v
• EnrichedCats/Limits/EnrichedTerminal.v
• EnrichedCats/Limits/EnrichedBinaryProducts.v
• EnrichedCats/Limits/EnrichedProducts.v
• EnrichedCats/Limits/EnrichedEqualizers.v
• EnrichedCats/Limits/EnrichedConicalLimits.v
• EnrichedCats/Limits/EnrichedPowers.v
• EnrichedCats/Limits/EnrichedLimits.v
• EnrichedCats/Colimits/EnrichedInitial.v
• EnrichedCats/Colimits/EnrichedBinaryCoproducts.v
• EnrichedCats/Colimits/EnrichedCoproducts.v
• EnrichedCats/Colimits/EnrichedCoequalizers.v
• EnrichedCats/Colimits/EnrichedConicalColimits.v
• EnrichedCats/Colimits/EnrichedCopowers.v
• EnrichedCats/Colimits/EnrichedColimits.v
• EnrichedCats/Colimits/CopowerFunctor.v
• EnrichedCats/Examples/SetEnriched.v
• EnrichedCats/Examples/QuantaleEnriched.v
• EnrichedCats/Examples/PosetEnriched.v
• EnrichedCats/Examples/StructureEnriched.v
• EnrichedCats/Examples/SmashStructureEnriched.v
• EnrichedCats/Examples/HomFunctor.v
• EnrichedCats/Examples/OppositeEnriched.v
• EnrichedCats/Examples/FunctorCategory.v
• EnrichedCats/Examples/Precomposition.v
• EnrichedCats/Examples/Presheaves.v
• EnrichedCats/Examples/Yoneda.v
• EnrichedCats/Examples/Tensor.v
• EnrichedCats/Bifunctors/CurriedBifunctors.v
• EnrichedCats/Bifunctors/WhiskeredBifunctors.v
• EnrichedCats/Bifunctors/CurriedTransformations.v
• EnrichedCats/Bifunctors/WhiskeredTransformations.v
• EnrichedCats/YonedaLemma.v
• EnrichedCats/Profunctors/Profunctor.v
• EnrichedCats/Profunctors/StandardProfunctors.v
• EnrichedCats/Profunctors/ProfunctorTransformations.v
• EnrichedCats/Profunctors/ProfunctorSquares.v
• EnrichedCats/Profunctors/Invertible.v
• EnrichedCats/Profunctors/Coend.v
• EnrichedCats/Profunctors/Composition/CompositionProf.v
• EnrichedCats/Profunctors/Composition/SquareComp.v
• EnrichedCats/Profunctors/Composition/Unitors.v
• EnrichedCats/Profunctors/Composition/Associators.v
• EnrichedCats/Profunctors/Composition/Whiskering.v
• EnrichedCats/Profunctors/Composition/BicatLaws.v
• EnrichedCats/Profunctors/Composition/WhiskerLaws.v
• EnrichedCats/Profunctors/Composition/OtherLaws.v
• EnrichedCats/Profunctors/Composition.v
• EnrichedCats/Profunctors/RepresentableLaws.v
• EnrichedCats/Examples/EmptyEnriched.v
• EnrichedCats/Examples/UnitEnriched.v
• EnrichedCats/Examples/FullSubEnriched.v
• EnrichedCats/Examples/ImageEnriched.v
• EnrichedCats/Examples/DialgebraEnriched.v
• EnrichedCats/Examples/SliceEnriched.v
• EnrichedCats/Examples/EilenbergMooreEnriched.v
• EnrichedCats/Examples/ProductEnriched.v
• EnrichedCats/Examples/GraphEnriched.v
• EnrichedCats/Examples/CollageEnriched.v
• EnrichedCats/Examples/ChangeOfBase.v
• EnrichedCats/RezkCompletion/PrecompFullyFaithful.v
• EnrichedCats/RezkCompletion/PrecompEssentiallySurjective.v
• EnrichedCats/RezkCompletion/EnrichedRezkCompletion.v
• EnrichedCats/RezkCompletion/RezkUniversalProperty.v
• EnrichedCats/Examples/KleisliEnriched.v
• EnrichedCats/Examples/UnivalentKleisliEnriched.v
• EnrichedCats/Examples/UnivalentKleisliMapping.v
• EnrichedCats/Limits/Examples/OppositeEnrichedLimits.v
• EnrichedCats/Limits/Examples/PosetEnrichedLimits.v
• EnrichedCats/Limits/Examples/StructureEnrichedLimits.v
• EnrichedCats/Limits/Examples/SelfEnrichedLimits.v
• EnrichedCats/Colimits/Examples/OppositeEnrichedColimits.v
• EnrichedCats/Colimits/Examples/PosetEnrichedColimits.v
• EnrichedCats/Colimits/Examples/StructureEnrichedColimits.v
• EnrichedCats/Colimits/Examples/SelfEnrichedColimits.v
• GrothendieckConstruction/TotalCategory.v
• GrothendieckConstruction/IsosInTotal.v
• GrothendieckConstruction/Projection.v
• GrothendieckConstruction/IsOpfibration.v
• GrothendieckConstruction/IsPullback.v
• TwoSidedDisplayedCats/TwoSidedDispCat.v
• TwoSidedDisplayedCats/Isos.v
• TwoSidedDisplayedCats/Univalence.v
• TwoSidedDisplayedCats/Discrete.v
• TwoSidedDisplayedCats/Total.v
• TwoSidedDisplayedCats/TwoSidedFibration.v
• TwoSidedDisplayedCats/Fiber.v
• TwoSidedDisplayedCats/DisplayedFunctor.v
• TwoSidedDisplayedCats/DisplayedNatTrans.v
• TwoSidedDisplayedCats/Strictness.v
• TwoSidedDisplayedCats/TransportLaws.v
• TwoSidedDisplayedCats/Examples/Constant.v
• TwoSidedDisplayedCats/Examples/DispCatOnTwoSidedDispCat.v
• TwoSidedDisplayedCats/Examples/TwoSidedDispCatOnDispCat.v
• TwoSidedDisplayedCats/Examples/FiberwiseProduct.v
• TwoSidedDisplayedCats/Examples/Opposites.v
• TwoSidedDisplayedCats/Examples/Arrow.v
• TwoSidedDisplayedCats/Examples/SquaresTwoCat.v
• TwoSidedDisplayedCats/Examples/Bimodules.v
• TwoSidedDisplayedCats/Examples/Comma.v
• TwoSidedDisplayedCats/Examples/IsoComma.v
• TwoSidedDisplayedCats/Examples/Lenses.v
• TwoSidedDisplayedCats/Examples/Product.v
• TwoSidedDisplayedCats/Examples/ProdOfTwosidedDispCat.v
• TwoSidedDisplayedCats/Examples/Profunctor.v
• TwoSidedDisplayedCats/Examples/Reindex.v
• TwoSidedDisplayedCats/Examples/Relations.v
• TwoSidedDisplayedCats/Examples/EnrichedRels.v
• TwoSidedDisplayedCats/Examples/Spans.v
• TwoSidedDisplayedCats/Examples/ParaTwoSidedDispCat.v
• TwoSidedDisplayedCats/Examples/StructuredCospans.v
• TwoSidedDisplayedCats/Examples/ProfunctorTwosidedDispCat.v
• DisplayedCats/Examples/StrictTwoSidedDispCat.v
• IndexedCategories/IndexedCategory.v
• IndexedCategories/IndexedFunctor.v
• IndexedCategories/IndexedTransformation.v
• IndexedCategories/FibrationToIndexedCategory.v
• IndexedCategories/CartesianToIndexedFunctor.v
• IndexedCategories/NatTransToIndexed.v
• IndexedCategories/IndexedCategoryToFibration.v
• IndexedCategories/IndexedFunctorToCartesian.v
• IndexedCategories/IndexedTransformationToTransformation.v
• IndexedCategories/OpIndexedCategory.v
• IndexedCategories/CoreIndexedCategory.v
• RepresentableFunctors/Precategories.v
• RepresentableFunctors/Bifunctor.v
• RepresentableFunctors/Representation.v
• RepresentableFunctors/RawMatrix.v
• RepresentableFunctors/DirectSum.v
• RepresentableFunctors/Test.v
• Monoidal/RezkCompletion/LiftedTensor.v
• Monoidal/RezkCompletion/LiftedTensorUnit.v
• Monoidal/RezkCompletion/LiftedUnitors.v
• Monoidal/RezkCompletion/LiftedAssociator.v
• Monoidal/RezkCompletion/LiftedMonoidal.v
• Monoidal/RezkCompletion/MonoidalRezkCompletion.v
• DaggerCategories/Categories.v
• DaggerCategories/Unitary.v
• DaggerCategories/Univalence.v
• DaggerCategories/Functors.v
• DaggerCategories/Transformations.v
• DaggerCategories/FunctorCategory.v
• DaggerCategories/Examples/Groupoids.v
• DaggerCategories/Examples/Relations.v
• DaggerCategories/Examples/Fullsub.v
• DaggerCategories/Functors/WeakEquivalences.v
• DaggerCategories/Functors/FullyFaithful.v
• DaggerCategories/Functors/Factorization.v
• DaggerCategories/Functors/Precomp.v
• DaggerCategories/CatIso.v
• MarkovCategories/MarkovCategory.v
• MarkovCategories/Determinism.v
• MarkovCategories/Univalence.v
• MarkovCategories/AlmostSurely.v
• MarkovCategories/Conditionals.v
• MarkovCategories/InformationFlowAxioms.v
• MarkovCategories/State.v
• MarkovCategories/ProbabilitySpaces.v
• MarkovCategories/Couplings.v
• All.v

Package ModelCategories

• Retract.v
• MorphismClass.v
• Lifting.v
• WeakEquivalences.v
• WFS.v
• ModelCategory.v
• Helpers.v
• NWFS.v
• NWFSisWFS.v
• Generated/MonoidalHelpers.v
• Generated/LiftingWithClass.v
• Examples.v
• Generated/FFMonoidalStructure.v
• Generated/LNWFSHelpers.v
• Generated/LNWFSMonoidalStructure.v
• Generated/LNWFSCocomplete.v
• Generated/LNWFSClosed.v
• Generated/GenericFreeMonoid.v
• Generated/GenericFreeMonoidSequence.v
• Generated/LNWFSSmallnessReduction.v
• Generated/OneStepMonad.v
• Generated/OneStepMonadSmall.v
• Generated/SmallObjectArgument.v
• All.v

Package Bicategories

• Core/Bicat.v
• Core/Invertible_2cells.v
• Morphisms/Adjunctions.v
• Morphisms/FullyFaithful.v
• Morphisms/DiscreteMorphisms.v
• Core/Examples/OpMorBicat.v
• Morphisms/Examples/MorphismsInOp1Bicat.v
• Core/Examples/OpCellBicat.v
• Core/Unitors.v
• Core/BicategoryLaws.v
• Core/Univalence.v
• Core/TransportLaws.v
• Core/EquivToAdjequiv.v
• Core/AdjointUnique.v
• Core/UnivalenceOp.v
• Core/Discreteness.v
• Morphisms/ExtensionsAndLiftings.v
• Morphisms/InternalStreetFibration.v
• Morphisms/InternalStreetOpFibration.v
• Morphisms/Properties/ContainsAdjEquiv.v
• Morphisms/Properties/Composition.v
• Morphisms/Properties/ClosedUnderInvertibles.v
• Morphisms/Properties.v
• Core/Examples/DiscreteBicat.v
• Core/Examples/OneTypes.v
• Core/Examples/PointedOneTypesBicat.v
• Core/Examples/TwoType.v
• Core/Examples/BicatOfUnivCats.v
• Core/Examples/BicatOfCats.v
• Core/Strictness.v
• Core/Examples/StrictCats.v
• Core/Examples/Initial.v
• Core/Examples/Final.v
• Core/Examples/BicategoryFromMonoidal.v
• Core/Examples/BicategoryFromWhiskeredMonoidal.v
• Core/Examples/FibSlice.v
• Core/Examples/OpFibSlice.v
• Morphisms/Properties/AdjunctionsRepresentable.v
• Morphisms/Examples/MorphismsInBicatOfUnivCats.v
• Morphisms/Examples/FibrationsInBicatOfUnivCats.v
• Morphisms/Examples/FibrationsInStrictCats.v
• Morphisms/Examples/MorphismsInOp2Bicat.v
• DisplayedBicats/DispBicat.v
• DisplayedBicats/DispInvertibles.v
• DisplayedBicats/DispAdjunctions.v
• DisplayedBicats/DispUnivalence.v
• DisplayedBicats/CleavingOfBicat.v
• DisplayedBicats/FiberCategory.v
• DisplayedBicats/FiberBicategory/FiberBicategory1.v
• DisplayedBicats/FiberBicategory/FiberBicategory2.v
• DisplayedBicats/FiberBicategory.v
• DisplayedBicats/Examples/Sigma.v
• DisplayedBicats/Examples/DisplayedCatToBicat.v
• DisplayedBicats/Examples/FullSub.v
• DisplayedBicats/Examples/Slice.v
• DisplayedBicats/Examples/Sub1Cell.v
• DisplayedBicats/Examples/DispBicatOfDispCats.v
• DisplayedBicats/Examples/Prod.v
• DisplayedBicats/Examples/DispDepProd.v
• DisplayedBicats/Examples/LiftDispBicat.v
• DisplayedBicats/Examples/Trivial.v
• DisplayedBicats/Examples/BicatOfInvertibles.v
• DisplayedBicats/Examples/EndoMap.v
• Core/Examples/StructuredCategories.v
• DisplayedBicats/Examples/CategoriesWithStructure.v
• MonoidalCategories/MonoidalFromBicategory.v
• MonoidalCategories/EndofunctorsMonoidal.v
• MonoidalCategories/PointedFunctorsMonoidal.v
• MonoidalCategories/Actions.v
• MonoidalCategories/ConstructionOfActions.v
• MonoidalCategories/WhiskeredMonoidalFromBicategory.v
• MonoidalCategories/ActionOfEndomorphismsInBicatWhiskered.v
• MonoidalCategories/BicatOfWhiskeredMonCatsLax.v
• MonoidalCategories/BicatOfWhiskeredMonCats.v
• MonoidalCategories/EndofunctorsWhiskeredMonoidal.v
• MonoidalCategories/PointedFunctorsWhiskeredMonoidal.v
• MonoidalCategories/IdempotencePointedFunctorsWhiskeredMonoidal.v
• MonoidalCategories/ActionBasedStrength.v
• MonoidalCategories/ActionBasedStrongFunctorsMonoidal.v
• MonoidalCategories/ActionOfEndomorphismsInBicat.v
• MonoidalCategories/ActionBasedStrongFunctorCategory.v
• MonoidalCategories/ActionsFormBicategory.v
• MonoidalCategories/ActionBasedStrongFunctorsWhiskeredMonoidal.v
• MonoidalCategories/BicatOfActegories.v
• MonoidalCategories/BicatOfActionsInBicat.v
• MonoidalCategories/UnivalenceMonCat/CurriedMonoidalCategories.v
• MonoidalCategories/UnivalenceMonCat/EquivalenceWhiskeredCurried.v
• MonoidalCategories/UnivalenceMonCat/UnitLayer.v
• MonoidalCategories/UnivalenceMonCat/TensorLayer.v
• MonoidalCategories/UnivalenceMonCat/TensorUnitLayer.v
• MonoidalCategories/UnivalenceMonCat/AssociatorUnitorsLayer.v
• MonoidalCategories/UnivalenceMonCat/FinalLayer.v
• MonoidalCategories/UnivalenceMonCat/EquivalenceMonCatCurried.v
• MonoidalCategories/UnivalenceMonCat/EquivalenceMonCatNonCurried.v
• Core/Examples/Groupoids.v
• PseudoFunctors/Display/Base.v
• PseudoFunctors/Display/Map1Cells.v
• PseudoFunctors/Display/Map2Cells.v
• PseudoFunctors/Display/Identitor.v
• PseudoFunctors/Display/Compositor.v
• PseudoFunctors/Display/PseudoFunctorBicat.v
• PseudoFunctors/Display/StrictIdentitor.v
• PseudoFunctors/Display/StrictCompositor.v
• PseudoFunctors/Display/StrictPseudoFunctorBicat.v
• PseudoFunctors/PseudoFunctor.v
• PseudoFunctors/Properties.v
• PseudoFunctors/LocalEquivalenceProperties.v
• PseudoFunctors/StrictPseudoFunctor.v
• PseudoFunctors/Examples/Identity.v
• PseudoFunctors/Examples/Composition.v
• PseudoFunctors/Examples/Constant.v
• PseudoFunctors/Examples/ApFunctor.v
• PseudoFunctors/Examples/OpFunctor.v
• PseudoFunctors/Examples/CatDiag.v
• PseudoFunctors/Examples/PseudofunctorFromMonoidal.v
• PseudoFunctors/Examples/Op2OfPseudoFunctor.v
• PseudoFunctors/Examples/BicatOfCatToUnivCat.v
• PseudoFunctors/Examples/PseudoFunctorsIntoCat.v
• Transformations/PseudoTransformation.v
• Transformations/Examples/Whiskering.v
• Transformations/Examples/Unitality.v
• Transformations/Examples/Associativity.v
• Transformations/Examples/ApTransformation.v
• Transformations/Examples/PseudoTransformationIntoCat.v
• Modifications/Modification.v
• Modifications/Examples/ApModification.v
• Modifications/Examples/Unitality.v
• Modifications/Examples/Associativity.v
• Modifications/Examples/ModificationIntoCat.v
• PseudoFunctors/Representable.v
• PseudoFunctors/Yoneda.v
• PseudoFunctors/Biequivalence.v
• PseudoFunctors/Examples/StrictToPseudo.v
• PseudoFunctors/Examples/Projection.v
• MonoidalCategories/EquivalenceActegoriesAndActions.v
• PseudoFunctors/Biadjunction.v
• PseudoFunctors/UniversalArrow.v
• DisplayedBicats/DispBicatSection.v
• DisplayedBicats/Examples/PointedOneTypes.v
• DisplayedBicats/Examples/DisplayedInserter.v
• DisplayedBicats/Examples/Displayed2Inserter.v
• DisplayedBicats/Examples/Algebras.v
• DisplayedBicats/Examples/Add2Cell.v
• DisplayedBicats/Examples/ContravariantFunctor.v
• DisplayedBicats/Examples/Cofunctormap.v
• DisplayedBicats/Examples/CwF.v
• DisplayedBicats/Examples/LaxSlice.v
• DisplayedBicats/Examples/FunctorsIntoCat.v
• DisplayedBicats/Examples/Codomain.v
• DisplayedBicats/DispPseudofunctor.v
• DisplayedBicats/DispTransportLaws.v
• DisplayedBicats/UnivalenceTechniques.v
• Transformations/Examples/AlgebraMap.v
• DisplayedBicats/Examples/Monads.v
• DisplayedBicats/Examples/KleisliTriple.v
• DisplayedBicats/Examples/EnrichedCats.v
• DisplayedBicats/Examples/DispBicatOfTwoSidedDispCat.v
• DisplayedBicats/DispTransformation.v
• DisplayedBicats/DispModification.v
• DisplayedBicats/DispBiequivalence.v
• DisplayedBicats/ProductDispBiequiv.v
• DoubleCategories/Basics/DoubleCategoryBasics.v
• DoubleCategories/Basics/StrictDoubleCatBasics.v
• DoubleCategories/Core/DoubleCats.v
• DoubleCategories/Core/DoubleFunctor/Basics.v
• DoubleCategories/Core/DoubleFunctor/LeftUnitor.v
• DoubleCategories/Core/DoubleFunctor/RightUnitor.v
• DoubleCategories/Core/DoubleFunctor/Associator.v
• DoubleCategories/Core/DoubleFunctor.v
• DoubleCategories/Core/DoubleTransformation.v
• DoubleCategories/Core/BicatOfDoubleCats.v
• DoubleCategories/Core/UnivalentDoubleCats.v
• DoubleCategories/DerivedLaws/TransportLaws.v
• DoubleCategories/DerivedLaws/Variations.v
• DoubleCategories/DerivedLaws/Unitors.v
• DoubleCategories/DerivedLaws.v
• DoubleCategories/Core/InvertiblesAndEquivalences.v
• DoubleCategories/Core/CatOfStrictDoubleCats.v
• DoubleCategories/Core/CatOfPseudoDoubleCats.v
• DoubleCategories/Core/StrictDoubleCats.v
• DoubleCategories/Core/PseudoDoubleSetCats.v
• DoubleCategories/Core/SymmetricUnivalent.v
• DoubleCategories/Underlying/HorizontalBicategory.v
• DoubleCategories/Underlying/VerticalTwoCategory.v
• DoubleCategories/Underlying/VerticalTwoCategoryStrict.v
• DoubleCategories/Core/CompanionsAndConjoints.v
• DoubleCategories/Examples/UnitDoubleCat.v
• DoubleCategories/Examples/ProductDoubleCat.v
• DoubleCategories/Examples/DoubleCatOnDispCat.v
• DoubleCategories/Examples/FullSubDoubleCat.v
• DoubleCategories/Examples/OpDoubleCat.v
• DoubleCategories/Examples/RelationsDoubleCat.v
• DoubleCategories/Examples/EnrichedRelDoubleCat.v
• DoubleCategories/Examples/LaxExtensionToFunctor.v
• DoubleCategories/Examples/SquareDoubleCat.v
• DoubleCategories/Examples/SquareDoubleCatTwo.v
• DoubleCategories/Examples/Coreflections.v
• DoubleCategories/Examples/ParaDoubleCat.v
• DoubleCategories/Examples/LensesDoubleCat.v
• DoubleCategories/Examples/SpansDoubleCat.v
• DoubleCategories/Examples/KleisliDoubleCat.v
• DoubleCategories/Examples/TransposeStrict.v
• DoubleCategories/Examples/StructuredCospansDoubleCat.v
• DoubleCategories/Examples/StructuredCospansDoubleFunctor.v
• DoubleCategories/Examples/BiSetcatToDoubleCat.v
• DoubleCategories/Examples/ProfunctorDoubleCat.v
• DoubleCategories/Examples/EnrichedProfunctorDoubleCat.v
• DoubleCategories/Examples/Coalgebras.v
• DoubleCategories/Limits/DoubleTerminal.v
• DoubleCategories/AlternativeDefinitions/DoubleCatsUnfolded.v
• DoubleCategories/AlternativeDefinitions/DoubleCatsEquivalentDefinitions.v
• DoubleCategories/DoubleBicat/VerityDoubleBicat.v
• DoubleCategories/DoubleBicat/DerivedLaws.v
• DoubleCategories/DoubleBicat/UnderlyingCats.v
• DoubleCategories/Examples/TransposeDoubleBicat.v
• DoubleCategories/DoubleBicat/CellsAndSquares.v
• DoubleCategories/DoubleBicat/LocalUnivalence.v
• DoubleCategories/Examples/HorizontalDual.v
• DoubleCategories/DoubleBicat/CompanionPairs.v
• DoubleCategories/DoubleBicat/CompanionPairUnique.v
• DoubleCategories/DoubleBicat/CompanionPairAdjEquiv.v
• DoubleCategories/DoubleBicat/Conjoints.v
• DoubleCategories/DoubleBicat/GregariousEquivalence.v
• DoubleCategories/DoubleBicat/GlobalUnivalence.v
• DoubleCategories/DoubleBicat/Core.v
• DoubleCategories/Examples/SquareDoubleBicat.v
• DoubleCategories/Examples/MateDoubleBicat.v
• DoubleCategories/Examples/DoubleCatToDoubleBicat.v
• DoubleCategories/Examples/ProfunctorDoubleBicat.v
• DoubleCategories/Examples/EnrichedProfunctorDoubleBicat.v
• DisplayedBicats/Examples/MonadsLax.v
• DisplayedBicats/Examples/DispBicatOnCatToUniv.v
• PseudoFunctors/Examples/MonadInclusion.v
• PseudoFunctors/Examples/OpFunctorEnriched.v
• Monads/Examples/AdjunctionToMonad.v
• Monads/Examples/ToMonadInCat.v
• Monads/Examples/MonadsInBicatOfUnivCats.v
• Monads/Examples/MonadsInBicatOfCats.v
• Monads/Examples/MonadsInOp1Bicat.v
• Monads/Examples/MonadsInOp2Bicat.v
• Monads/Examples/MonadsInTotalBicat.v
• Monads/Examples/MonadsInBicatOfEnrichedCats.v
• Monads/DistributiveLaws.v
• Monads/MixedDistributiveLaws.v
• Monads/Examples/MonadsInMonads.v
• Monads/Examples/Composition.v
• Monads/Examples/PsfunctorOnMonad.v
• Monads/LocalEquivalenceMonad.v
• Core/Examples/Image.v
• PseudoFunctors/Examples/CorestrictImage.v
• Core/YonedaLemma.v
• Limits/Final.v
• Limits/Products.v
• Limits/Pullbacks.v
• Limits/CommaObjects.v
• Limits/Inserters.v
• Limits/IsoInserters.v
• Limits/Equifiers.v
• Limits/EilenbergMooreObjects.v
• Limits/EilenbergMooreComonad.v
• Monads/ConstructionOfAlgebras.v
• Monads/MonadToAdjunction.v
• Limits/Examples/OneTypesLimits.v
• Limits/Examples/BicatOfCatsLimits.v
• Limits/Examples/BicatOfUnivCatsLimits.v
• Limits/Examples/BicatOfEnrichedCatsLimits.v
• Limits/Examples/OpCellBicatLimits.v
• Limits/Examples/UnivGroupoidsLimits.v
• Limits/Examples/SliceBicategoryLimits.v
• Limits/Examples/TotalBicategoryLimits.v
• Limits/Examples/DispConstructionsLimits.v
• Limits/Examples/SubbicatLimits.v
• Limits/Examples/LimitsStructuredCategories.v
• MonoidalCategories/BicatOfWhiskeredMonCatsFinalObject.v
• Morphisms/Monadic.v
• MonoidalCategories/MonoidalDialgebrasInserters.v
• MonoidalCategories/BicatOfActegoriesFinalObject.v
• MonoidalCategories/MonadsAsMonoidsWhiskered.v
• Monads/Examples/MonadsInStructuredCategories.v
• Limits/ProductEquivalences.v
• Limits/PullbackFunctions.v
• Limits/PullbackEquivalences.v
• Limits/InserterEquivalences.v
• Limits/EquifierEquivalences.v
• OrthogonalFactorization/Orthogonality.v
• OrthogonalFactorization/FactorizationSystem.v
• Morphisms/Eso.v
• Morphisms/Properties/Projections.v
• Morphisms/Properties/ClosedUnderPullback.v
• Morphisms/Properties/EsoProperties.v
• Morphisms/Examples/MorphismsInOneTypes.v
• Morphisms/Examples/EsosInBicatOfUnivCats.v
• Morphisms/Examples/MorphismsInSliceBicat.v
• Morphisms/Examples/MorphismsInStructuredCat.v
• Morphisms/Examples/MorphismsInBicatOfEnrichedCats.v
• OrthogonalFactorization/EsoFactorizationSystem.v
• OrthogonalFactorization/EnrichedEsoFactorization.v
• Colimits/Initial.v
• Colimits/Coproducts.v
• Colimits/Extensive.v
• Colimits/KleisliObjects.v
• Limits/Examples/OpMorBicatLimits.v
• Colimits/Examples/OpCellBicatColimits.v
• Colimits/Examples/OneTypesColimits.v
• Colimits/Examples/BicatOfCatsColimits.v
• Colimits/Examples/BicatOfUnivCatsColimits.v
• Colimits/Examples/BicatOfEnrichedCatsColimits.v
• Colimits/Examples/SliceBicategoryColimits.v
• Colimits/CoproductEquivalences.v
• Morphisms/Properties/FromInitial.v
• Objects/CartesianObject.v
• Objects/CocartesianObject.v
• Objects/Examples/BicatOfUnivCatsObjects.v
• PseudoFunctors/Examples/ConstProduct.v
• PseudoFunctors/Examples/CurryingInBicatOfCats.v
• PseudoFunctors/PseudoFunctorLimits.v
• DisplayedBicats/DispBiadjunction.v
• PseudoFunctors/Examples/PathGroupoid.v
• DisplayedBicats/DispToFiberEquivalence.v
• DisplayedBicats/DispBuilders.v
• DisplayedBicats/Examples/MonadKtripleBiequiv.v
• DisplayedBicats/Examples/PointedGroupoid.v
• PseudoFunctors/Examples/LiftingActegories.v
• PseudoFunctors/Examples/ChangeOfBaseEnriched.v
• WkCatEnrichment/prebicategory.v
• WkCatEnrichment/Notations.v
• WkCatEnrichment/whiskering.v
• WkCatEnrichment/Cat.v
• WkCatEnrichment/internal_equivalence.v
• WkCatEnrichment/bicategory.v
• WkCatEnrichment/hcomp_bicat.v
• PseudoFunctors/Examples/Strictify.v
• PseudoFunctors/Preservation/Preservation.v
• PseudoFunctors/Preservation/BiadjunctionPreservation.v
• PseudoFunctors/Preservation/BiadjunctionPreserveProducts.v
• PseudoFunctors/Preservation/BiadjunctionPreserveInserters.v
• PseudoFunctors/Preservation/BiadjunctionPreserveEquifiers.v
• PseudoFunctors/Preservation/BiadjunctionPreserveCoproducts.v
• PseudoFunctors/Preservation/ClosedUnderEquivalence.v
• BicategoryOfBicat.v
• BicatOfBicategory.v
• DisplayedBicats/Cartesians.v
• DisplayedBicats/EquivalenceBetweenCartesians.v
• DisplayedBicats/CleavingOfBicatIsAProp.v
• DisplayedBicats/CartesianPseudoFunctor.v
• DisplayedBicats/ExamplesOfCleavings/TrivialCleaving.v
• DisplayedBicats/ExamplesOfCleavings/SliceCleaving.v
• DisplayedBicats/ExamplesOfCleavings/FunctorsIntoCatCleaving.v
• DisplayedBicats/ExamplesOfCleavings/CodomainCleaving.v
• DisplayedBicats/ExamplesOfCleavings/FibrationCleaving.v
• DisplayedBicats/ExamplesOfCleavings/OpFibrationCleaving.v
• DisplayedBicats/FiberBicategory/FunctorFromCleaving.v
• PseudoFunctors/Examples/Reindexing.v
• Logic/DisplayMapBicat.v
• DisplayedBicats/Examples/DisplayMapBicatToDispBicat.v
• DisplayedBicats/Examples/DisplayMapBicatSlice.v
• DisplayedBicats/ExamplesOfCleavings/DisplayMapBicatCleaving.v
• PseudoFunctors/Examples/PullbackFunctor.v
• PseudoFunctors/Examples/CompositionPseudoFunctor.v
• PseudoFunctors/Preservation/PullbackPreservation.v
• Limits/Examples/DisplayMapSliceLimits.v
• Colimits/Examples/DisplayMapSliceColimits.v
• DisplayedBicats/FiberBicategory/TrivialFiber.v
• DisplayedBicats/FiberBicategory/CodomainFiber.v
• DisplayedBicats/FiberBicategory/SliceFiber.v
• DisplayedBicats/FiberBicategory/DisplayMapFiber.v
• Grothendieck/FibrationToPseudoFunctor.v
• Grothendieck/PseudoFunctorToFibration.v
• Grothendieck/Unit.v
• Grothendieck/Counit.v
• Grothendieck/Biequivalence.v
• Grothendieck/FiberwiseEquiv.v
• ComprehensionCat/BicatOfCompCat/DispCatTerminal.v
• ComprehensionCat/BicatOfCompCat/FibTerminal.v
• ComprehensionCat/BicatOfCompCat/CompCat.v
• ComprehensionCat/BicatOfCompCat/FullCompCat.v
• ComprehensionCat/BicatOfCompCat.v
• ComprehensionCat/CompCatNotations.v
• ComprehensionCat/TypeFormers/UnitTypes.v
• ComprehensionCat/TypeFormers/ProductTypes.v
• ComprehensionCat/TypeFormers/EqualizerTypes.v
• ComprehensionCat/TypeFormers/Democracy.v
• ComprehensionCat/TypeFormers/SigmaTypes.v
• ComprehensionCat/TypeFormers/PiTypes.v
• ComprehensionCat/DFLCompCat.v
• ComprehensionCat/DFLCompCatNotations.v
• ComprehensionCat/ComprehensionEso.v
• ComprehensionCat/Biequivalence/DFLCompCatToFinLim.v
• ComprehensionCat/Biequivalence/FinLimToDFLCompCat.v
• ComprehensionCat/Biequivalence/Unit.v
• ComprehensionCat/Biequivalence/Counit.v
• ComprehensionCat/Biequivalence/Biequiv.v
• ComprehensionCat/LocalProperty/LocalProperties.v
• ComprehensionCat/LocalProperty/Examples.v
• ComprehensionCat/LocalProperty/CatWithProp.v
• ComprehensionCat/LocalProperty/DFLCompCatWithProp.v
• ComprehensionCat/Biequivalence/LocalProperty.v
• ComprehensionCat/Biequivalence/PiTypesBiequiv.v
• ComprehensionCat/Biequivalence/InternalLanguageTopos.v
• ComprehensionCat/SetGroupoidModel.v
• Logic/ComprehensionBicat.v
• Logic/Examples/TrivialComprehensionBicat.v
• Logic/Examples/PullbackComprehensionBicat.v
• Logic/Examples/FibrationsComprehensionBicat.v
• Logic/Examples/OpfibrationsComprehensionBicat.v
• Logic/Examples/DisplayMapComprehensionBicat.v
• Logic/Examples/FunctorsIntoCatComprehensionBicat.v
• OtherStructure/DualityInvolution.v
• OtherStructure/DualityInvolutionProperties.v
• OtherStructure/ClassifyingDiscreteOpfib.v
• OtherStructure/Exponentials.v
• OtherStructure/Cores.v
• OtherStructure/Examples/StructureBicatOfUnivCats.v
• OtherStructure/Examples/StructureOneTypes.v
• OtherStructure/Examples/StructureBicatOfEnrichedCats.v
• DisplayedBicats/DisplayedUniversalArrow.v
• DisplayedBicats/DisplayedUniversalArrowOnCat.v
• RezkCompletions/BicatToLocalUnivalentBicat.v
• RezkCompletions/RezkCompletionOfBicategory.v
• RezkCompletions/Uniqueness.v
• RezkCompletions/StructuredCats/TerminalObject.v
• RezkCompletions/StructuredCats/BinProducts.v
• RezkCompletions/StructuredCats/Pullbacks.v
• RezkCompletions/StructuredCats/Equalizers.v
• DaggerCategories/BicatOfDaggerCats.v
• All.v

Package Ktheory

• GrothendieckGroup.v
• All.v

Package Topology

• Prelim.v
• Filters.v
• Topology.v
• CategoryTop.v
• All.v

Package RealNumbers

• Prelim.v
• Fields.v
• Sets.v
• NonnegativeRationals.v
• NonnegativeReals.v
• Reals.v
• DedekindCuts.v
• DecidableDedekindCuts.v
• All.v

Package SubstitutionSystems

• Notation.v
• Signatures.v
• BinSumOfSignatures.v
• SumOfSignatures.v
• BinProductOfSignatures.v
• SubstitutionSystems.v
• SimplifiedHSS/SubstitutionSystems.v
• SignaturesEquivRelativeStrength.v
• GeneralizedSubstitutionSystems.v
• MonadsFromSubstitutionSystems.v
• SimplifiedHSS/MonadsFromSubstitutionSystems.v
• GenMendlerIteration.v
• GenMendlerIteration_alt.v
• ActionScenarioForGenMendlerIteration_alt.v
• ApplicationsGenMendlerIteration_alt.v
• LiftingInitial.v
• SimplifiedHSS/LiftingInitial.v
• LiftingInitial_alt.v
• SimplifiedHSS/LiftingInitial_alt.v
• ModulesFromSignatures.v
• SimplifiedHSS/ModulesFromSignatures.v
• LamSignature.v
• Lam.v
• SimplifiedHSS/Lam.v
• SignatureExamples.v
• SignatureCategory.v
• SubstitutionSystems_Summary.v
• SimplifiedHSS/SubstitutionSystems_Summary.v
• LamHSET.v
• SimplifiedHSS/LamHSET.v
• BindingSigToMonad.v
• SimplifiedHSS/BindingSigToMonad.v
• LamFromBindingSig.v
• SimplifiedHSS/LamFromBindingSig.v
• MLTT79.v
• SimplifiedHSS/MLTT79.v
• FromBindingSigsToMonads_Summary.v
• SimplifiedHSS/FromBindingSigsToMonads_Summary.v
• SortIndexing.v
• MonadsMultiSorted.v
• MonadsMultiSorted_alt.v
• MultiSortedBindingSig.v
• MultiSorted.v
• MultiSortedMonadConstruction.v
• SimplifiedHSS/MultiSortedMonadConstruction.v
• MultiSorted_alt.v
• MultiSortedMonadConstruction_alt.v
• SimplifiedHSS/MultiSortedMonadConstruction_alt.v
• MonadicSubstitution_alt.v
• SimplifiedHSS/MonadicSubstitution_alt.v
• STLC.v
• SimplifiedHSS/STLC.v
• STLC_alt.v
• SimplifiedHSS/STLC_alt.v
• CCS.v
• SimplifiedHSS/CCS.v
• CCS_alt.v
• SimplifiedHSS/CCS_alt.v
• PCF_alt.v
• SimplifiedHSS/PCF_alt.v
• ActionBasedStrengthOnHomsInBicat.v
• EquivalenceSignaturesWithActegoryMorphisms.v
• EquivalenceLaxLineatorsHomogeneousCase.v
• SigmaMonoids.v
• ConstructionOfGHSS.v
• BindingSigToMonad_actegorical.v
• ContinuitySignature/GeneralLemmas.v
• ContinuitySignature/CommutingOfOmegaLimitsAndCoproducts.v
• ContinuitySignature/ContinuityOfMultiSortedSigToFunctor.v
• ContinuitySignature/MultiSortedSignatureFunctorEquivalence.v
• ContinuitySignature/InstantiateHSET.v
• MultiSorted_actegorical.v
• MultiSortedMonadConstruction_actegorical.v
• MultiSortedMonadConstruction_coind_actegorical.v
• MultiSortedEmbeddingIndCoindHSET.v
• UntypedForests.v
• Forests.v
• STLC_actegorical.v
• STLC_actegorical_abstractcat.v
• All.v

Package Folds

• UnicodeNotations.v
• folds_precat.v
• from_precats_to_folds_and_back.v
• folds_isomorphism.v
• folds_pre_2_cat.v
• All.v

Package HomologicalAlgebra

• Triangulated.v
• Complexes.v
• KA.v
• TranslationFunctors.v
• MappingCone.v
• MappingCylinder.v
• KAPreTriangulated.v
• KATriangulated.v
• CohomologyComplex.v
• All.v

Package AlgebraicGeometry

• Topology.v
• SheavesOfRings.v
• Spec.v
• All.v

Package Paradoxes

• GirardsParadox.v
• All.v

Package Induction

• FunctorAlgebras_legacy.v
• FunctorCoalgebras_legacy.v
• PolynomialFunctors.v
• PolynomialAlgebras2Cells.v
• ImpredicativeInductiveSets.v
• M/Core.v
• M/Limits.v
• M/Uniqueness.v
• W/Core.v
• W/Wtypes.v
• W/WtypesAsW.v
• W/Fibered.v
• W/Naturals.v
• W/Uniqueness.v
• M/Chains.v
• M/ComputationalM.v
• All.v

Package AlgebraicTheories

• FiniteSetSkeleton.v
• IndexedSetCategory.v
• AlgebraicTheoryCategoryCore.v
• AlgebraicTheories.v
• AlgebraicTheoryMorphisms.v
• AlgebraicTheoryCategory.v
• AlgebraCategoryCore.v
• Algebras.v
• AlgebraMorphisms.v
• AlgebraCategory.v
• LambdaCalculus.v
• LambdaTheoryCategoryCore.v
• LambdaTheories.v
• LambdaTheoryMorphisms.v
• LambdaTheoryCategory.v
• PresheafCategoryCore.v
• Presheaves.v
• PresheafMorphisms.v
• PresheafCategory.v
• Examples/EndomorphismTheory.v
• Examples/FreeObjectTheory.v
• Examples/FreeMonoidTheory.v
• Examples/FreeTheory.v
• Examples/LambdaCalculus.v
• Examples/OnePointTheory.v
• Examples/Plus1Presheaf.v
• Examples/ProjectionsTheory.v
• Examples/TheoryAlgebra.v
• Examples/ExtensionsTheory.v
• AlgebraicTheoryToLawvereTheory.v
• AlgebraicTheoryToMonoid.v
• Combinators.v
• CategoryOfRetracts.v
• OriginalRepresentationTheorem.v
• RepresentationTheorem.v
• FundamentalTheorem/SurjectivePrecomposition.v
• FundamentalTheorem/CommonUtilities/KaroubiEnvelope.v
• FundamentalTheorem/CommonUtilities/MonoidActions.v
• FundamentalTheorem/AlgebraToTheory.v
• All.v

Package Semantics

• LinearLogic/LinearNonLinear.v
• LinearLogic/LafontCategory.v
• LinearLogic/LinearCategory.v
• LinearLogic/LinearCategoryEilenbergMooreAdjunction.v
• LinearLogic/LinearToLinearNonLinear.v
• LinearLogic/RelationalModel.v
• LinearLogic/LiftingModel.v
• EnrichedEffectCalculus/EECModel.v
• EnrichedEffectCalculus/ContinuationModel.v
• EnrichedEffectCalculus/CopowerModel.v
• All.v