Library UniMath.All

Library UniMath.Algebra.AbelianGroups

• 1. Basic definitions
  • • Construction of the trivial abgr consisting of one element given by unit.
    • Abelian group structure on morphism between abelian groups
• 2. Subobjects
• 3. Kernels
  • Kernel as abelian group
  • The inclusion Kernel f --> X is a morphism of abelian groups
  • Image of f is a subgroup
• 4. Quotient objects
• 5. Direct products
• 6. Abelian group of fractions of an abelian unitary monoid
• 7. Abelian group of fractions and abelian monoid of fractions
• 8. Canonical homomorphism to the abelian group of fractions
• 9. Abelian group of fractions in the case when all elements are cancelable
• 10. Relations on the abelian group of fractions
• 11. Relations and the canonical homomorphism to abgrdiff

Library UniMath.Algebra.AbelianMonoids

• 1. Basic definitions
  • • • Construction of the trivial abmonoid consisting of one element given by unit.
      • Abelian monoid structure on homsets
• 2. Subobjects
• 3. Quotient objects
• 4. Direct products
• 5. Monoid of fractions of an abelian monoid
• 6. Canonical homomorphism to the monoid of fractions
• 7. Abelian monoid of fractions in the case when elements of the localization submonoid are cancelable
• 8. Relations on the abelian monoid of fractions
• 9. Relations and canonical homomorphism to abmonoidfrac

Library UniMath.Algebra.Apartness

• Definition of appartness relation
  • Apartness
  • Tight apartness
  • Operations and apartness

Library UniMath.Algebra.Archimedean

• Archimedean property
  • Preamble
  • The standard function from the natural numbers to a monoid
  • relation
  • Archimedean property in a monoid
  • Archimedean property in a group
  • Archimedean property in a rig
  • Archimedean property in a ring
  • Archimedean property in a field
  • Archimedean property in a constructive field

Library UniMath.Algebra.BinaryOperations

• 1. Unary operations
• 2. Binary operations
• 2.1. General definitions
  • • • Transfer of binary operations relative to weak equivalences
• 2.2. Standard conditions on one binary operation on a set
• 2.3. Elements with inverses
• 2.4. Group operations
• 2.5. Standard conditions on a pair of binary operations on a set
  • • • Transfer properties of binary operations relative to weak equivalences
• 3. Sets with one binary operation
• 3.1. General definitions
• 3.2. Functions compatible with a binary operation (homomorphism) and their properties
  • • • (X = Y) ≃ (binopiso X Y)
      • hfiber and binop
• 3.3. Transport of properties of a binary operation
• 3.4. Subobject
• 3.5. Relations compatible with a binary operation and quotient objects
• 3.6. Relations inversely compatible with a binary operation
• 3.7. Homomorphisms and relations
• 3.8. Quotient relations
• 3.9. Direct products
• 4. Sets with two binary operations
• 4.1. General definitions
• 4.2. Functions compatible with a pair of binary operation (homomorphisms) and their properties
  • • • X = Y ≃ (X ≃ Y)
• 4.3. Transport of properties of a pair of binary operations
• 4.4. Subobjects
• 4.5. Quotient objects
• 4.6. Direct products
• 5. Infinitary operations

Library UniMath.Algebra.ConstructiveStructures

• Definition of appartness relationConstructive Algebraic Structures
  • Predicats in a rig with a tight appartness relation
  • Constructive rig with division
  • Constructive commutative rig with division
  • Constructive Field

Library UniMath.Algebra.DivisionRig

• Division Rig
  • Definition of a DivRig
  • Definition of a Commutative DivRig

Library UniMath.Algebra.Domains_and_Fields

• Algebra I. Part E. Integral domains and fields. Vladimir Voevodsky. Aug. 2011 - .
  • Contents
  • Preamble
  • Standard Algebraic Structures (cont.) Integral domains and Fileds.
    • Integral domains
      • General definitions
      • (X = Y) ≃ (ringiso X Y)
      • Computational lemmas for integral domains
      • Multiplicative submonoid of non-zero elements
      • Relations similar to "greater" on integral domains
    • Ring units (i.e. multilicatively invertible elements)
    • Fields
      • Main definitions
      • (X = Y) ≃ (ringiso X Y)
      • Field of fractions of an integral domain with decidable equality
      • Canonical homomorphism to the field of fractions
    • Relations similar to "greater" on fields of fractions
      • Description of the field of fractions as the ring of fractions with respect to the submonoid of "positive" elements
      • Definition and properties of "greater" on the field of fractions
      • Relations and the canonical homomorphism to the field of fractions

Library UniMath.Algebra.Free_Monoids_and_Groups

• • Contents

Library UniMath.Algebra.GroupAction

• Group actions
  • Definitions
  • Applications of univalence
  • Torsors
  • Applications of univalence

Library UniMath.Algebra.Groups

• Algebra I. Part C. Groups, abelian groups. Vladimir Voevodsky. Aug. 2011 - .

Library UniMath.Algebra.Groups2

• 1. Basic definitions
  • • Construction of the trivial group consisting of one element given by unit.
• 2. Computation lemmas for groups
• 3. Relations on groups
• 4. Subobjects
• 5. Quotient objects
• 6. Cosets
• 7. Normal Subgroups
• 8. Direct products
• 9. Group of invertible elements in a monoid

Library UniMath.Algebra.IteratedBinaryOperations

Library UniMath.Algebra.Matrix

• Matrices
  • Contents
  • Vectors
    • Standard conditions on one binary operation
    • Standard conditions on a pair of binary operations
    • Structures
  • Matrices
    • Standard conditions on one binary operation
    • Structures
    • Matrix rig

Library UniMath.Algebra.Modules

Library UniMath.Algebra.Monoids

• Algebra I. Part B. Monoids, abelian monoids. Vladimir Voevodsky. Aug. 2011 - .

Library UniMath.Algebra.Monoids2

• 1. Basic definitions
  • • • Construction of the trivial monoid consisting of one element given by unit.
• 2. Functions between monoids compatible with structures (homomorphisms) and their properties
• 3. Subobjects
• 4. Kernels
• 5. Quotient objects
• 6. Cosets
• 7. Direct products

Library UniMath.Algebra.RigsAndRings

• Algebra I. Part D. Rigs and rings. Vladimir Voevodsky. Aug. 2011 - .
  • Preamble
  • Standard Algebraic Structures (cont.)
    • Rigs - semirings with 1, 0 and x * 0 = 0 * x = 0
      • General definitions
      • Homomorphisms of rigs (rig functions)
      • (X = Y) ≃ (rigiso X Y)
      • Relations similar to "greater" or "greater or equal" on rigs
      • Subobjects
      • Quotient objects
      • Direct products
      • Opposite rigs
      • Nonzero rigs
    • Commutative rigs
      • General definitions
      • (X = Y) ≃ (rigiso X Y)
      • Relations similar to "greater" on commutative rigs
      • Subobjects
      • Quotient objects
      • Direct products
      • Opposite commutative rigs
    • Rings
      • General definitions
      • Homomorphisms of rings
      • (X = Y) ≃ (ringiso X Y)
      • Computation lemmas for rings
      • Relations compatible with the additive structure on rings
      • Relations compatible with the multiplicative structure on rings
      • Relations "inversely compatible" with the multiplicative structure on rings
      • Relations on rings and ring homomorphisms
      • Subobjects
      • Quotient objects
      • Direct products
      • Opposite rings
      • Ring of differences associated with a rig
      • Canonical homomorphism to the ring associated with a rig (ring of differences)
      • Relations similar to "greater" or "greater or equal" on the ring associated with a rig
      • Relations and the canonical homomorphism to the ring associated with a rig (ring of differences)
    • Commutative rings
      • General definitions
      • (X = Y) ≃ (ringiso X Y)
      • Computational lemmas for commutative rings
      • Subobjects
      • Quotient objects
      • Direct products
      • Opposite commutative rings
      • Commutative rigs to commutative rings
      • Rings of fractions
      • Canonical homomorphism to the ring of fractions
      • Ring of fractions in the case when all elements which are being inverted are cancelable
      • Relations similar to "greater" or "greater or equal" on the rings of fractions
      • Relations and the canonical homomorphism to the ring of fractions

Library UniMath.Algebra.Tests

Library UniMath.Algebra.Universal

• Universal algebra: signatures, algebras and terms

Library UniMath.Algebra.GaussianElimination.Auxiliary

• Matrices
• Logic
• Naturals
• Standard finite sets
• Rings, fields
• Rationals. Commented out to respect import dependency ordering. Could be downstreamed or removed.
• Maybe

Library UniMath.Algebra.GaussianElimination.Corollaries

Library UniMath.Algebra.GaussianElimination.Elimination

• Key definitions, and main goal theorem
• Leading entries
• Pivot-selection
• Gaussian elimination

Library UniMath.Algebra.GaussianElimination.Matrices

• Matrices
• Arbitrary types
• Arbitary rigs
• Commutative rigs
• Matrices representing permutations

Library UniMath.Algebra.GaussianElimination.RowOps

• Matrices

Library UniMath.Algebra.GaussianElimination.Tests

Library UniMath.Algebra.GaussianElimination.Vectors

• Matrices
• Vectors in arbitrary types
• Basic vector algebra over rigs
• Total sums of vectors
• Pulse functions

Library UniMath.Algebra.Modules.Core

• 1. Modules
  • 1.1. A module constructor that takes a left action satisfying four axioms
• 2. R-module morphisms
  • 2.1. Linearity
  • 2.2. Module morphisms
  • 2.3 R-module homomorphisms form an R-module
  • 2.4. Isomorphisms

Library UniMath.Algebra.Modules.Examples

• 1. The identity multimodule morphism
• 2. Constructing a module from a ring morphism
• 3. The zero module

Library UniMath.Algebra.Modules.Multimodules

• • 1. Multimodules
• 2. Multimodule morphisms
  • 2.1. Multilinearity
  • 2.2. Multimodule morphisms
• 3. Properties of the ring actions

Library UniMath.Algebra.Modules.Quotient

• 1. Preliminaries
  • 1.1. Equivalence relations on a module that are closed under the module structure
  • 1.2. Construction of an appropriate equivalence relation from a submodule
• 2. The quotient module and its universal property
  • 2.1. The module
  • 2.2. The universal property
• Universal property in terms of submodules

Library UniMath.Algebra.Modules.Submodule

• 1. Subobjects of modules
• 2. Kernels
• 3. Images

Library UniMath.Algebra.RigsAndRings.Ideals

• Ideals
  • Contents
    • Left ideals (lideal)
    • Right ideals (rideal)
    • Two-sided ideals (ideal)
    • The above notions for commutative rigs
  • Kernel ideal
  • Unit ideal
  • Prime ideal
  • Localization at a prime ideal

Library UniMath.Algebra.Universal.Algebras

• Algebra for a given signature.
  • Basic definitions.
  • Helper for building an algebra starting from a simple signature.
  • Homomorphisms of algebras.
  • Identity and composition of homomorphisms.
  • The unit algebra and the proof it is final.
  • Helpers for working with curried functions
  • Algebras with hSets as carriers

Library UniMath.Algebra.Universal.Algebras_eq

Library UniMath.Algebra.Universal.Congruences

Library UniMath.Algebra.Universal.DisplayedAlgebras

Library UniMath.Algebra.Universal.EqAlgebras

• Varieties.

Library UniMath.Algebra.Universal.Equations

• Equations over a signature and equational theories
  • Equations.
  • Notations for equations.
  • Equation systems.
  • Equational specifications.

Library UniMath.Algebra.Universal.FreeAlgebras

• Free algebras.

Library UniMath.Algebra.Universal.HVecRel

Library UniMath.Algebra.Universal.HVectors

• Heterogeneous vectors.
  • Basic definitions.
    • Constructors.
    • Notations.
    • Projections.
    • Some identities for computing hel.
    • Weak equivalence with functions.
  • Level-1 heterogeneous vectors.
    • Miscellanea of operations on level-1 hvecs.
    • Map involving level-1 hvecs.
  • Level-2 heterogeneous vectors.
  • Functions from hvecs and their curried variants.
    • An hvec made up of sets is an hSet

Library UniMath.Algebra.Universal.Signatures

• Signatures for universal algebra.

Library UniMath.Algebra.Universal.SortedTypes

• Sorted types.

Library UniMath.Algebra.Universal.SubAlgebras

Library UniMath.Algebra.Universal.TermAlgebras

• The ground term algebra and the proof it is initial.

Library UniMath.Algebra.Universal.Terms

• Terms for a given signature.
  • Definition of oplist (operations list).
    • The opexec and oplistexec functions.
    • The stackconcatenate function.
    • The oplistsplit function.
  • Terms and related constructors and destructors.
    • The vecoplist2oplist and oplist2vecoplist functions
  • Constructors and destuctors.
    • Term normalization
    • Miscellanea properties for terms.
  • Term induction.
    • Term induction step
    • Immediate applications of term induction
  • Notations for ground terms.
    • Helpers for working with curried functions.

Library UniMath.Algebra.Universal.VTerms

• • Variables and terms with variables
  • Helpers for working with curried functions

Library UniMath.Algebra.Universal.WTypes

• Algebra, functor algebras and w-types.

Library UniMath.Algebra.Universal.Examples.Bool

• Example on booleans.
  • Algebra structure over type bool.
  • Boolean ground terms.
  • Booleans terms and semantics for boolean formulae.

Library UniMath.Algebra.Universal.Examples.Group

• Example on groups.

Library UniMath.Algebra.Universal.Examples.ListDataType

• Example of lists

Library UniMath.Algebra.Universal.Examples.Monoid

• Example on monoids.

Library UniMath.Algebra.Universal.Examples.Nat

• Example on natural numbers

Library UniMath.Algebra.Universal.Examples.Tests

• Several tests for univeral algebra operations.

Library UniMath.AlgebraicGeometry.SheavesOfRings

Library UniMath.AlgebraicGeometry.Spec

• • Contents
  • Zariski topology
  • Structure sheaf
    • Sections
    • Restriction of a section
    • Definition of the structure sheaf

Library UniMath.AlgebraicGeometry.Topology

Library UniMath.AlgebraicTheories.AlgebraCategory

• 1. Univalence
• 2. Algebras are fibered over theories
• 3. A characterization of iso's of algebras
• 4. Algebra pullback functor along an algebraic theory morphism

Library UniMath.AlgebraicTheories.AlgebraCategoryCore

• 1. The dependent product category of theories and algebras
  • 1.1. The full category of algebra data
    • 1.1.1. Temporary accessors
  • 1.2. The full category of algebras
    • 1.2.1. A lemma about algebras
• 2. The category of algebras

Library UniMath.AlgebraicTheories.AlgebraMorphisms

• 1. The definition of algebra morphisms
  • • 1.1.2. The property of the morphisms

Library UniMath.AlgebraicTheories.AlgebraicTheories

• 1. The definition of algebraic theories
• 2. Some useful definitions and their properties

Library UniMath.AlgebraicTheories.AlgebraicTheoryCategory

• 1. A characterization of iso's of algebraic theories
• 2. Univalence
• 3. Limits

Library UniMath.AlgebraicTheories.AlgebraicTheoryCategoryCore

• 1. The category of algebraic theories
  • 1.1. The category of algebraic theory data
    • 1.1.1. Temporary accessors
  • 1.2. The category of algebraic theories
    • 1.2.2. A lemma about algebraic theories

Library UniMath.AlgebraicTheories.AlgebraicTheoryMorphisms

• 1. The definition of algebraic theory morphisms
• 2. An equality lemma

Library UniMath.AlgebraicTheories.AlgebraicTheoryToLawvereTheory

• 1. The functor from algebraic theories to setcategories
• 2. The equivalence between two types of presheaves

Library UniMath.AlgebraicTheories.AlgebraicTheoryToMonoid

• 1. The construction of the monoid
• 2. The embedding into the Lawvere theory

Library UniMath.AlgebraicTheories.Algebras

• 1. The definition of algebras
• 2. An equality lemma
• 3. Some properties of algebras
• 4. A lemma about the interplay between the algebra action and vectors

Library UniMath.AlgebraicTheories.CategoryOfRetracts

• 1. The category of retracts
• 2. The terminal object
• 3. Fixpoints
• 4. Binary products
  • 4.1 Some properties of the power objects, defined via binary products
• 5. Exponential objects
• 6. Every object is a retract of λ x, x

Library UniMath.AlgebraicTheories.Combinators

• 1. The tactics
• 2. Compose
• 3. Pair
• 4. Pair arrow
• 5. Pair projections
• 6. Union arrow ('match')
• 7. Union injections
• 8. Evaluation of a curried function
• 9. Curry
• 10. Uncurry
• 11. N-tuple
• 12. N-tuple arrow
• 13. N-tuple projection

Library UniMath.AlgebraicTheories.FiniteSetSkeleton

Library UniMath.AlgebraicTheories.IndexedSetCategory

• 1. The definition of the category
• 2. Univalence
• 3. Limits

Library UniMath.AlgebraicTheories.LambdaCalculus

• 1. The data of the λ-calculus
• 2. Properties and operations derived from the data
• 3. A definition of the λ-calculus with compatibility between the pieces of data
• 4. Properties derived from the full λ-calculus
  • 4.1. Properties of rect
  • 4.2. Properties of subst subst_var

Library UniMath.AlgebraicTheories.LambdaTheories

• 1. The definition of λ-theories
• 2. The definition of β-equality
• 3. The definiiton of η-equality
• 4. Lemmas on the interaction of abs with subst
• 5. The definition and properties of app and beta_equality
• 6. A characterization of app and abs in terms of app' and one

Library UniMath.AlgebraicTheories.LambdaTheoryCategory

• 1. A characterization of iso's of λ-theories
• 2. Univalence
• 3. Limits

Library UniMath.AlgebraicTheories.LambdaTheoryCategoryCore

• 1. The category of λ-theories
  • 1.1. The category of λ-theory data
    • 1.1.1. Temporary accessors
  • 1.2. The category of λtheories
    • 1.2.1. A lemma about λ-theories

Library UniMath.AlgebraicTheories.LambdaTheoryMorphisms

• 1. The definition of λ-theory morphisms lambda_theory_morphism

Library UniMath.AlgebraicTheories.OriginalRepresentationTheorem

• 1. The endomorphism theory
  • 1.1. An explicit description of its operations
• 2. The isomorphism
• 3. The right inverse

Library UniMath.AlgebraicTheories.PresheafCategory

• 1. Univalence
• 2. Fibration
• 3. Limits
• 4. Terminal object
• 5. Binary products
• 6. Products

Library UniMath.AlgebraicTheories.PresheafCategoryCore

• 1. The dependent product category of theories and presheaves
  • 1.1. The full category of presheaf data
    • 1.1.1. Temporary accessors
  • 1.2. The full category of presheaves
    • 1.2.1. A lemma about presheaves
• 2. The category of presheaves

Library UniMath.AlgebraicTheories.PresheafEquivalence

• 1. The equivalence between R and K
• 2. The fully faithful functor from LL to K
• 2.1. The isomorphism between the composed functor and the embedding from L1 to K
• 3. The equivalence

Library UniMath.AlgebraicTheories.PresheafMorphisms

• 1. The definition of a presheaf morphism
• 3. An equality lemma

Library UniMath.AlgebraicTheories.Presheaves

• 1. The definition of a presheaf
• 2. The presheaf given by the algebraic theory itself

Library UniMath.AlgebraicTheories.ReflexiveObjects

Library UniMath.AlgebraicTheories.RepresentationTheorem

• 1. A proof that the object (theory_presheaf) can be exponentiated
• 2. A construction of the lambda endomorphism theory of theory_presheaf
• 3. An isomorphism between the two λ-theories
• 4. The right inverse

Library UniMath.AlgebraicTheories.RepresentationTheoremsRelation

• 1. The diagram
• 2. The isomorphism between the reflexive objects
• 3. The endomorphism theory has no left inverse

Library UniMath.AlgebraicTheories.Examples.EmptyPresheaf

• 1. The empty presheaf

Library UniMath.AlgebraicTheories.Examples.EndomorphismTheory

• 1. The definition of the endomorphism algebraic theory
• 2. The definition of the endomorphism λ-theory
• 3. A characterization of the endomorphism theories with β-equality
• 4. A characterization of the endomorphism theories with η-equality
• 5. The endomorphism theory of a set
• 6. The morphism between endomorphism theories

Library UniMath.AlgebraicTheories.Examples.ExtensionsTheory

• 1. The theory of extensions
• 2. The category of T_A-algebras is equivalent to A / T-alg
• 3. Every morphism F: T -> T' factors through T(F^*(T'_0))

Library UniMath.AlgebraicTheories.Examples.FreeMonoidTheory

• 1. The definition of the algebraic theory
• 2. The functor from monoids to algebras
• 3. Constructing a monoid from an algebra
• 4. The equivalence

Library UniMath.AlgebraicTheories.Examples.FreeObjectTheory

• 1. The free object theory
• 2. The functor from objects of C to algebras for this theory

Library UniMath.AlgebraicTheories.Examples.FreeTheory

• 1. The free functor
• 2. The forgetful functor
• 3. The adjunction
• 4. The equivalence between algebras and coslices

Library UniMath.AlgebraicTheories.Examples.LambdaCalculus

• 1. The algebraic theory of the λ-calculus
• 2. The λ-theory of the λ-calculus
• 3. The λ-theory has β-equality

Library UniMath.AlgebraicTheories.Examples.OnePointTheory

• 1. The definition of the one point theory
• 2. The only algebra of the one point theory is the unit type

Library UniMath.AlgebraicTheories.Examples.Plus1Presheaf

• 1. The definition of the plus 1 presheaf

Library UniMath.AlgebraicTheories.Examples.ProjectionsTheory

• 1. The definition of the projections theory
• 2. The definition of a T-algebra structure on every set

Library UniMath.AlgebraicTheories.Examples.PuncturedTheory

• 1. The punctured theory
• 2. The embedding and pullback
• 3. The lifting of T*-algebras to T-algebras
• 4. The isomorphism that shows we have a retraction for T_0 nonempty

Library UniMath.AlgebraicTheories.Examples.TheoryAlgebra

• 1. The T-algebra structure
• 2. It is the free algebra on n generators

Library UniMath.AlgebraicTheories.FundamentalTheorem.AlgebraToTheory

• 1. The construction of the monoid
• 2. The construction of the λ-theory with β-equality

Library UniMath.AlgebraicTheories.FundamentalTheorem.SurjectivePrecomposition

Library UniMath.AlgebraicTheories.FundamentalTheorem.CommonUtilities.MonoidActions

• 1. The category of monoid action data and its objects
• 2. The category of monoid actions
• 3. The definition of a right M-action
• 4. The definition of a morphism of M-actions
• 5. The terminal M-action
• 6. The binary product of M-actions
• 7. The exponential M-action
• 8. A characterization of isomorphisms
• 9. An isomorphism between the set of global elements and the set of fixpoints of a monoid action
• 10. Restriction of scalars
• 11. Extension of scalars
  • 11.1. Extension of scalars preserves monoid monoid action
  • 11.2. Extension of scalars preserves the terminal
  • 11.3. Extension of scalars preserves binary products

Library UniMath.Bicategories.BicatOfBicategory

• Bicategories

Library UniMath.Bicategories.BicategoryOfBicat

• Bicategories

Library UniMath.Bicategories.Colimits.CoproductEquivalences

Library UniMath.Bicategories.Colimits.Coproducts

Library UniMath.Bicategories.Colimits.Extensive

Library UniMath.Bicategories.Colimits.Initial

• Biinitial object in a bicategory

Library UniMath.Bicategories.Colimits.KleisliObjects

Library UniMath.Bicategories.Colimits.Examples.BicatOfCatsColimits

Library UniMath.Bicategories.Colimits.Examples.BicatOfEnrichedCatsColimits

• 1. Kleisli objects

Library UniMath.Bicategories.Colimits.Examples.BicatOfUnivCatsColimits

Library UniMath.Bicategories.Colimits.Examples.DisplayMapSliceColimits

Library UniMath.Bicategories.Colimits.Examples.OneTypesColimits

Library UniMath.Bicategories.Colimits.Examples.OpCellBicatColimits

Library UniMath.Bicategories.Colimits.Examples.SliceBicategoryColimits

Library UniMath.Bicategories.ComprehensionCat.BicatOfCompCat

Library UniMath.Bicategories.ComprehensionCat.CompCatNotations

• 1. Notations for comprehension categories
• 2. Notations and accessors for functors of comprehension categories
• 3. Terms in comprehension categories

Library UniMath.Bicategories.ComprehensionCat.ComprehensionEso

Library UniMath.Bicategories.ComprehensionCat.DFLCompCat

• 1. The bicategory of DFL comprehension categories
• 2. This bicategory is univalent
• 3. Builders and accessors
• 4. Invertible 2-cells
• 5. The adjoint equivalence coming from democracy
• 6. Adjoint equivalences of DFL comprehension categories

Library UniMath.Bicategories.ComprehensionCat.DFLCompCatNotations

• 1. Terms and displayed morphisms
• 2. Operations on democracy
• 3. Operations on extensional identity types
• 4. Operations on sigma types

Library UniMath.Bicategories.ComprehensionCat.SetGroupoidModel

• 1. The univalent comprehension category of setgroupoids
• 2. The univalent comprehension category of setgroupoids with split isofibrations

Library UniMath.Bicategories.ComprehensionCat.BicatOfCompCat.CompCat

• 1. Comprehension functors
• 2. Comprehension natural transformations
• 3. The displayed bicategory of comprehension categories
• 4. The univalence of this displayed bicategory
• 5. Builders and accessors
• 6. Comparison
• 7. Adjoint equivalences

Library UniMath.Bicategories.ComprehensionCat.BicatOfCompCat.DispCatTerminal

• 1. The bicategory of categories with a terminal object and a displayed category
• 2. Builders and accessors
• 3. Adjoint equivalences

Library UniMath.Bicategories.ComprehensionCat.BicatOfCompCat.FibTerminal

• 1. The bicategory of categories with a terminal object and a fibration
• 2. Builders and accessors
• 3. Adjoint equivalences

Library UniMath.Bicategories.ComprehensionCat.BicatOfCompCat.FullCompCat

• 1. The bicategory of full comprehension categories
• 2. The univalence of the bicategory of full comprehension categories
• 3. Builders and accessors
• 4. Adjoint equivalences

Library UniMath.Bicategories.ComprehensionCat.Biequivalence.Biequiv

Library UniMath.Bicategories.ComprehensionCat.Biequivalence.Counit

• 1. The morphism of the counit
• 2. The naturality of the counit
• 3. The data of the counit
• 4. The laws of the counit
• 5. The counit
• 6. The counit is an adjoint equivalence

Library UniMath.Bicategories.ComprehensionCat.Biequivalence.DFLCompCatToFinLim

• 1. The action on objects
• 2. The action on morphisms
• 3. The action on 2-cells
• 4. The identitor and compositor
• 5. The data of the pseudofunctor
• 6. The laws of the pseudofunctor
• 7. The pseudofunctor from DFL comprehension categories to categories with finite limits

Library UniMath.Bicategories.ComprehensionCat.Biequivalence.FinLimToDFLCompCat

• 1. The action on objects
• 2. The action on morphisms
• 3. The action on 2-cells
• 4. The identitor and compositor
• 5. The data
• 6. The laws
• 7. The pseudofunctor from categories with finite limits to DFL comprehension categories

Library UniMath.Bicategories.ComprehensionCat.Biequivalence.InternalLanguageTopos

• 1. The internal language of pretoposes
• 2. The internal language of ∏-pretoposes
• 3. The internal language of pretoposes with natural numbers
• 4. The internal language of elementary toposes
• 5. The internal language of elementary toposes with an NNO

Library UniMath.Bicategories.ComprehensionCat.Biequivalence.LocalProperty

• 1. The extended pseudofunctor from categories to comprehension categories
• 2. The extended pseudofunctor from comprehension categories to categories
• 3. The unit
• 4. The counit
• 5. The displayed biequivalence

Library UniMath.Bicategories.ComprehensionCat.Biequivalence.PiTypesBiequiv

• 1. Lemmas on equivalences and locally cartesian closed categories
• 2. The extended pseudofunctor from categories to comprehension categories
• 3. The extended pseudofunctor from comprehension categories to categories
• 4. The unit
• 5. The counit
• 6. The displayed biequivalence

Library UniMath.Bicategories.ComprehensionCat.Biequivalence.Unit

• 1. The morphism of the unit
• 2. The naturality of the unit
• 3. The laws of the unit
• 4. The unit
• 5. The unit is a pointwise adjoint equivalence

Library UniMath.Bicategories.ComprehensionCat.LocalProperty.CatWithProp

• 1. The displayed bicategory arising from a categorical property
• 2. The univalence of this bicategory
• 3. Displayed adjoint equivalences in this bicategory

Library UniMath.Bicategories.ComprehensionCat.LocalProperty.DFLCompCatWithProp

• 1. The displayed bicategory of DFL comprehension categories with fiberwise structure
• 2. Properties of this displayed bicategory
• 3. Adjoint equivalences

Library UniMath.Bicategories.ComprehensionCat.LocalProperty.Examples

• 1. Conjunction of local properties
• 2. Subproperties of local properties
• 3. Strict initial objects
• 4. Stable binary coproducts
• 5. Disjoint binary coproducts
• 6. Regularity
• 7. Exactness
• 8. Pretoposes
• 9. Subobject classifiers
• 10. Elementary toposes
• 11. Parameterized natural number objects
• 12. Arithmetic universes
• 13. Elementary toposes with a natural numbers object

Library UniMath.Bicategories.ComprehensionCat.LocalProperty.LocalProperties

• 1. Properties of categories
• 2. Fiberwise versions of properties
• 3. Local properties

Library UniMath.Bicategories.ComprehensionCat.TypeFormers.Democracy

• 1. Democratic full comprehension categories
• 2. Functors that preserve democracy
• 3. The displayed bicategory of democratic full comprehension categories
• 4. The univalence of this displayed bicategory

Library UniMath.Bicategories.ComprehensionCat.TypeFormers.EqualizerTypes

• 1. The displayed bicategory of equalizer types
• 2. The univalence of this displayed bicategory
• 3. Equalizer types for comprehension categories
• 4. Equalizer types for full comprehension categories
• 5. Adjoint equivalences

Library UniMath.Bicategories.ComprehensionCat.TypeFormers.PiTypes

• 1. Preliminaries on pi-types
• 2. Dependent products for morphisms that are isomorphic to projections
• 3. Builders for dependent products
• 4. Uniqueness of dependent products
• 5. Preservation of dependent products
• 6. Examples of functors that preserve dependent products
  • 6.1. Functors that preserve all dependent products
  • 6.2. The identity
  • 6.3. Composition
• 7. The displayed bicategory of pi-types
• 8. This displayed bicategory is univalent
• 9. Pi-types for DFL full comprehension categories
• 10. Adjoint equivalences

Library UniMath.Bicategories.ComprehensionCat.TypeFormers.ProductTypes

• 1. The displayed bicategory of product types
• 2. The univalence of this displayed bicategory
• 3. Product types for comprehension categories
• 4. Product types for full comprehension categories
• 5. Adjoint equivalences

Library UniMath.Bicategories.ComprehensionCat.TypeFormers.SigmaTypes

• 1. The displayed bicategory of sigma types
• 2. The univalence of this displayed bicategory
• 3. Sigma types for comprehension categories
• 4. Adjoint equivalences

Library UniMath.Bicategories.ComprehensionCat.TypeFormers.UnitTypes

• 1. The displayed bicategory of unit types
• 2. The univalence of this displayed bicategory
• 3. Unit types for comprehension categories
• 4. Unit types for full comprehension categories
• 5. Adjoint equivalences
• 6. Strong unit types

Library UniMath.Bicategories.Core.AdjointUnique

Library UniMath.Bicategories.Core.Bicat

• Bicategories
  • Definition of prebicategory
    • Data
  • Laws
  • Bicategories
  • Invertible 2-cells
  • Derived laws
  • Interchange law
  • Homs are categories
  • Functor structure on horizontal composition.
  • Chaotic bicat
  • Associators and unitors are isos.
  • Functor structure on associators and unitors.
  • Precomposition functor
  • Postcomposition functor
  • Notations.

Library UniMath.Bicategories.Core.BicategoryLaws

Library UniMath.Bicategories.Core.Discreteness

Library UniMath.Bicategories.Core.EquivToAdjequiv

Library UniMath.Bicategories.Core.Invertible_2cells

• More on invertible 2cells
  • Inverse 2cell of a composition
  • Two-cells that are isomorphisms

Library UniMath.Bicategories.Core.Strictness

• Strict bicategories

Library UniMath.Bicategories.Core.TransportLaws

Library UniMath.Bicategories.Core.Unitors

• Bicategories
  • Examples of laws derived by reversing morphisms or cells.

Library UniMath.Bicategories.Core.Univalence

• Univalence for bicategories
  • J rule for locally univalent bicategories
  • J rule for globally univalent bicategories
  • Application of J:
  • Adjoint equivalences in a globally univalent bicategory form a bigroupoid

Library UniMath.Bicategories.Core.UnivalenceOp

• Univalence for opposite bicategories

Library UniMath.Bicategories.Core.YonedaLemma

• Yoneda Lemma

Library UniMath.Bicategories.Core.Examples.BicatOfCats

• Bicategory of 1-categories

Library UniMath.Bicategories.Core.Examples.BicatOfUnivCats

• Bicategory of 1-categories

Library UniMath.Bicategories.Core.Examples.BicategoryFromMonoidal

Library UniMath.Bicategories.Core.Examples.BicategoryFromWhiskeredMonoidal

Library UniMath.Bicategories.Core.Examples.DiscreteBicat

• 1. The discrete bicategory
• 2. The discrete bicategory is discrete
• 3. Global univalence of the discrete bicategory

Library UniMath.Bicategories.Core.Examples.FibSlice

Library UniMath.Bicategories.Core.Examples.Final

• • Final bicategory and proof that it's univalent.

Library UniMath.Bicategories.Core.Examples.Groupoids

Library UniMath.Bicategories.Core.Examples.Image

Library UniMath.Bicategories.Core.Examples.Initial

• • Initial bicategory and proof that it's univalent.

Library UniMath.Bicategories.Core.Examples.OneTypes

Library UniMath.Bicategories.Core.Examples.OpCellBicat

• • op2 bicategory.

Library UniMath.Bicategories.Core.Examples.OpFibSlice

Library UniMath.Bicategories.Core.Examples.OpMorBicat

Library UniMath.Bicategories.Core.Examples.PointedOneTypesBicat

Library UniMath.Bicategories.Core.Examples.StrictCats

• Bicategory of strict categories

Library UniMath.Bicategories.Core.Examples.StructuredCategories

• 8. Locally Cartesian closed categories

Library UniMath.Bicategories.Core.Examples.TwoType

Library UniMath.Bicategories.DaggerCategories.BicatOfDaggerCats

Library UniMath.Bicategories.DisplayMapCat.BicatOfDisplayMapCat

• Bicategory of Display Map Categories
  • Bicategory
  • Pseudofunctor into the Bicategory of Full Comprehension Categories

Library UniMath.Bicategories.DisplayMapCat.DispBicatOfDisplayMapCat

• Bicategory of Display Map Categories
  • Displayed Bicategory of Display Map Categories
    • Coercions
    • Univalence
  • Displayed Bicategory of Display Map Categories with Terminal object in base
    • Coercions
    • Univalence of disp_bicat_terminal_display_map_cat.
  • Pseudofunctor from the bicategory of display map categories with terminal objects into the bicategory of full comprehension categories.
    • Pseudofunctor Data
    • Pseudofunctor Laws

Library UniMath.Bicategories.DisplayedBicats.CartesianPseudoFunctor

Library UniMath.Bicategories.DisplayedBicats.Cartesians

Library UniMath.Bicategories.DisplayedBicats.CleavingOfBicat

Library UniMath.Bicategories.DisplayedBicats.CleavingOfBicatIsAProp

Library UniMath.Bicategories.DisplayedBicats.DispAdjunctions

• Internal adjunction in displayed bicategories
• Definitions and properties of displayed adjunctions
  • Displayed left adjoints
    • Data & laws for left adjoints
    • Laws for equivalences
    • Packaged
  • Identity is a displayed adjoint
• Classification of internal adjunctions in the total category

Library UniMath.Bicategories.DisplayedBicats.DispBiadjunction

• • Triangles
  • Data
  • Total biadjunction.

Library UniMath.Bicategories.DisplayedBicats.DispBicat

• Displayed bicategories
  • Displayed bicategories.
  • Transport of displayed cells.
  • Definition of displayed bicategories.
  • Operations on bicategories
  • Data projections
  • Laws
  • Invertible displayed 2-cells.
  • Derived laws
  • Total bicategory of a displayed bicategory
  • Displayed left and right unitors coincide on the identity
  • Useful properties
  • Notations.

Library UniMath.Bicategories.DisplayedBicats.DispBicatSection

Library UniMath.Bicategories.DisplayedBicats.DispBiequivalence

• • Data
  • Total biequivalence.

Library UniMath.Bicategories.DisplayedBicats.DispBuilders

Library UniMath.Bicategories.DisplayedBicats.DispInvertibles

• Displayed invertible 2-cells
  • Being a displayed invertible 2-cell is a proposition
  • Classification of invertible 2-cells in the total bicategory
    • If a 2-cell is invertible in the total category, then it is invertible in the base category
    • If a 2-cell is invertible in the total category, then it is invertible in the fiber
    • If the displayed 2-cell is invertible, then the corresponding 2-cell in the total bicategory is also invertible.

Library UniMath.Bicategories.DisplayedBicats.DispModification

• • Definition of displayed modifications
    • Data
    • Data

Library UniMath.Bicategories.DisplayedBicats.DispPseudofunctor

• • Definition of displayed pseudofunctor
    • Data
    • Properties
    • Disp pseudofunct
  • Identity
  • Composition

Library UniMath.Bicategories.DisplayedBicats.DispToFiberEquivalence

• Displayed biequivalences give rise to equivalences on the fiber.

Library UniMath.Bicategories.DisplayedBicats.DispTransformation

• • Definition of displayed transformation.
    • Data
    • Properties
    • Displayed transformation
  • Identity
  • Composition

Library UniMath.Bicategories.DisplayedBicats.DispTransportLaws

Library UniMath.Bicategories.DisplayedBicats.DispUnivalence

• Internal adjunction in displayed bicategories

Library UniMath.Bicategories.DisplayedBicats.DisplayedUniversalArrow

Library UniMath.Bicategories.DisplayedBicats.DisplayedUniversalArrowOnCat

Library UniMath.Bicategories.DisplayedBicats.EquivalenceBetweenCartesians

Library UniMath.Bicategories.DisplayedBicats.FiberBicategory

Library UniMath.Bicategories.DisplayedBicats.FiberCategory

• Fiber category of a displayed bicategory whose displayed 2-cells form a

Library UniMath.Bicategories.DisplayedBicats.ProductDispBiequiv

• 1. The product of displayed pseudofunctors
• 2. The product of displayed biequivalences

Library UniMath.Bicategories.DisplayedBicats.UnivalenceTechniques

Library UniMath.Bicategories.DisplayedBicats.Examples.Add2Cell

Library UniMath.Bicategories.DisplayedBicats.Examples.Algebras

Library UniMath.Bicategories.DisplayedBicats.Examples.BicatOfInvertibles

Library UniMath.Bicategories.DisplayedBicats.Examples.Codomain

Library UniMath.Bicategories.DisplayedBicats.Examples.Cofunctormap

• Bicategories

Library UniMath.Bicategories.DisplayedBicats.Examples.ContravariantFunctor

• Bicategories

Library UniMath.Bicategories.DisplayedBicats.Examples.CwF

• Bicategories

Library UniMath.Bicategories.DisplayedBicats.Examples.DispBicatOfDispCats

• Bicategories

Library UniMath.Bicategories.DisplayedBicats.Examples.DispBicatOfTwoSidedDispCat

Library UniMath.Bicategories.DisplayedBicats.Examples.DispBicatOnCatToUniv

Library UniMath.Bicategories.DisplayedBicats.Examples.DispDepProd

Library UniMath.Bicategories.DisplayedBicats.Examples.DisplayMapBicatSlice

Library UniMath.Bicategories.DisplayedBicats.Examples.DisplayMapBicatToDispBicat

Library UniMath.Bicategories.DisplayedBicats.Examples.Displayed2Inserter

Library UniMath.Bicategories.DisplayedBicats.Examples.DisplayedCatToBicat

Library UniMath.Bicategories.DisplayedBicats.Examples.DisplayedInserter

Library UniMath.Bicategories.DisplayedBicats.Examples.EndoMap

Library UniMath.Bicategories.DisplayedBicats.Examples.EnrichedCats

• 1. The displayed bicategory
• 2. Local univalence
• 3. Global univalence
• 4. Accessors for the bicategory of enriched categories
• 5. The category of quantale enriched categories

Library UniMath.Bicategories.DisplayedBicats.Examples.FullSub

• Bicategories

Library UniMath.Bicategories.DisplayedBicats.Examples.FunctorsIntoCat

Library UniMath.Bicategories.DisplayedBicats.Examples.KleisliTriple

Library UniMath.Bicategories.DisplayedBicats.Examples.LaxSlice

Library UniMath.Bicategories.DisplayedBicats.Examples.LiftDispBicat

• 1. The lift of a displayed bicategory
• 2. Invertible 2-cells in the lift
• 3. Adjoints equivalences in the lift
• 4. The univalence of the lift
• 5. Properties of the lift

Library UniMath.Bicategories.DisplayedBicats.Examples.MonadKtripleBiequiv

• Biequivalence between Monads and Ktriples
  • Miscellanea
  • Basic monadic constructions built from a Ktriple.
  • Pseudofunctor Ktriples to Monads.

Library UniMath.Bicategories.DisplayedBicats.Examples.Monads

Library UniMath.Bicategories.DisplayedBicats.Examples.MonadsLax

Library UniMath.Bicategories.DisplayedBicats.Examples.PointedGroupoid

Library UniMath.Bicategories.DisplayedBicats.Examples.PointedOneTypes

Library UniMath.Bicategories.DisplayedBicats.Examples.Prod

• Bicategories
  • Direct product of two displayed structures over a bicategory.

Library UniMath.Bicategories.DisplayedBicats.Examples.Sigma

• Bicategories

Library UniMath.Bicategories.DisplayedBicats.Examples.Slice

Library UniMath.Bicategories.DisplayedBicats.Examples.Sub1Cell

Library UniMath.Bicategories.DisplayedBicats.Examples.Trivial

• • Trivial display.

Library UniMath.Bicategories.DisplayedBicats.Examples.CategoriesWithStructure.BinProducts

Library UniMath.Bicategories.DisplayedBicats.Examples.CategoriesWithStructure.Equalizers

Library UniMath.Bicategories.DisplayedBicats.Examples.CategoriesWithStructure.FiniteLimits

Library UniMath.Bicategories.DisplayedBicats.Examples.CategoriesWithStructure.Pullbacks

Library UniMath.Bicategories.DisplayedBicats.Examples.CategoriesWithStructure.SubobjectClassifier

Library UniMath.Bicategories.DisplayedBicats.Examples.CategoriesWithStructure.Terminal

Library UniMath.Bicategories.DisplayedBicats.ExamplesOfCleavings.CodomainCleaving

Library UniMath.Bicategories.DisplayedBicats.ExamplesOfCleavings.DisplayMapBicatCleaving

Library UniMath.Bicategories.DisplayedBicats.ExamplesOfCleavings.FibrationCleaving

Library UniMath.Bicategories.DisplayedBicats.ExamplesOfCleavings.FunctorsIntoCatCleaving

Library UniMath.Bicategories.DisplayedBicats.ExamplesOfCleavings.OpFibrationCleaving

Library UniMath.Bicategories.DisplayedBicats.ExamplesOfCleavings.SliceCleaving

Library UniMath.Bicategories.DisplayedBicats.ExamplesOfCleavings.TrivialCleaving

Library UniMath.Bicategories.DisplayedBicats.FiberBicategory.CodomainFiber

Library UniMath.Bicategories.DisplayedBicats.FiberBicategory.DisplayMapFiber

Library UniMath.Bicategories.DisplayedBicats.FiberBicategory.FiberBicategory1

• Bicategories

Library UniMath.Bicategories.DisplayedBicats.FiberBicategory.FiberBicategory2

• Bicategories

Library UniMath.Bicategories.DisplayedBicats.FiberBicategory.FunctorFromCleaving

Library UniMath.Bicategories.DisplayedBicats.FiberBicategory.SliceFiber

Library UniMath.Bicategories.DisplayedBicats.FiberBicategory.TrivialFiber

Library UniMath.Bicategories.DoubleCategories.DerivedLaws

Library UniMath.Bicategories.DoubleCategories.AlternativeDefinitions.DoubleCatsEquivalentDefinitions

• Double Categories
• 1. The map from unfolded double categories to double categories
• 2. The inverse
• 3. It forms an equivalence

Library UniMath.Bicategories.DoubleCategories.AlternativeDefinitions.DoubleCatsUnfolded

• Double Categories
  • Contents :

Library UniMath.Bicategories.DoubleCategories.Basics.DoubleCategoryBasics

• 1. Horizontal identities
• 2. Horizontal composition
• 3. Left unitor
• 4. Right unitor
• 5. Associator
• 6. Triangle and pentagon laws

Library UniMath.Bicategories.DoubleCategories.Basics.StrictDoubleCatBasics

• 1. Laws for strict double categories
• 2. Horizontal identities/composition forms a set
• 3. Preservation of horizontal identities
• 4. Preservation of horizontal composition
• 5. The identity preserves identities and composition
• 6. The composition preserves identities and composition

Library UniMath.Bicategories.DoubleCategories.Core.BicatOfDoubleCats

• 1. Two-sided displayed categories with identities
• 2. Two-sided displayed categories with horizontal composition
• 3. Two-sided displayed categories with identities and horizontal composition
• 4. Two-sided displayed categories with left unitors
• 5. Two-sided displayed categories with right unitors
• 6. Two-sided displayed categories with associators
• 7. Two-sided displayed categories with unitors and associators
• 8. Displayed bicategory of double categories

Library UniMath.Bicategories.DoubleCategories.Core.CatOfPseudoDoubleCats

• 1. Preliminary definitions
• 2. Displayed category that adds the left unitor
• 3. Displayed category that adds the right unitor
• 4. Displayed category that adds the associator
• 5. Displayed category that adds the unitors and associator
• 6. The category of pseudo double setcategories

Library UniMath.Bicategories.DoubleCategories.Core.CatOfStrictDoubleCats

• 1. The displayed category of horizontal identities
• 2. The displayed categoryes of horizontal compositions
• 3. The displayed category of horizontal identities and compositions
• 4. The category of strict double categories

Library UniMath.Bicategories.DoubleCategories.Core.CompanionsAndConjoints

• 1. Companion pairs
• 2. Conjoints

Library UniMath.Bicategories.DoubleCategories.Core.DoubleCats

• 1. Double categories
• 2. Accessors for double categories
  • 2.1. The vertical category
  • 2.2. Horizontal morphisms
  • 2.3. Squares
  • 2.4. Functoriality of horizontal identities
  • 2.5. Functoriality of horizontal composition
  • 2.6. Left unitor
  • 2.7. Right unitor
  • 2.8. Associator
  • 2.9. Triangle and pentagon equations
• 3. Builder for double categories
• 4. Squares and equalities
• 5. Flat double categories

Library UniMath.Bicategories.DoubleCategories.Core.DoubleFunctor

Library UniMath.Bicategories.DoubleCategories.Core.DoubleTransformation

• 1. Preservation of the identity
• 2. Preservation of composition
• 3. Examples of double transformations

Library UniMath.Bicategories.DoubleCategories.Core.InvertiblesAndEquivalences

• 1. Invertible 2-cells
• 2. Adjoint equivalences

Library UniMath.Bicategories.DoubleCategories.Core.PseudoDoubleSetCats

• 1. Pseudo double setcategories
• 2. Accessors for pseudo double setcategories
• 3. Builder for pseudo double setcategories

Library UniMath.Bicategories.DoubleCategories.Core.StrictDoubleCats

• 1. Strict double categories
• 2. Accessors for double categories
  • 2.1. The vertical category
  • 2.2. Horizontal morphisms
  • 2.3. Squares
  • 2.4. Transporting squares
  • 2.5. Laws for squares
  • 2.6. Functoriality of horizontal identities
  • 2.7. Functoriality of horizontal composition
  • 2.8. Laws for horizontal composition
  • 2.9. Transport laws
• 3. Builder for strict double categories
• 4. Strict functors for strict double categories
• 5. Accessors for strict double functors
• 6. Builder for strict double functors

Library UniMath.Bicategories.DoubleCategories.Core.SymmetricUnivalent

• 1. The horizontal category
• 2. The 2-sided displayed category of vertical morphisms and squares
• 3. A useful lemma for `idtoiso`
• 4. Horizontal identities
• 5. Horizontal composition
• 6. The left unitor
• 7. The right unitor
• 8. The associator
• 9. The triangle and pentagon equations
• 10. The dual double category
• 11. Symmetric univalence for double categories

Library UniMath.Bicategories.DoubleCategories.Core.UnivalentDoubleCats

• 1. Univalent double categories
• 2. Accessors for univalent double categories
• 3. Builder for double categories
• 4. Lax functors for double categories
• 5. Accessors for lax functors
• 6. Builder for lax functors
• 7. Strong double functors
• 8. Double transformations
• 9. Accessors for double transformations
• 10. Builder for double transformations

Library UniMath.Bicategories.DoubleCategories.Core.DoubleFunctor.Associator

Library UniMath.Bicategories.DoubleCategories.Core.DoubleFunctor.Basics

• 1. Preservation of the identity
• 2. Preservation of composition
• 3. Preservation of the unitors and associators
• 4. The identity double functor

Library UniMath.Bicategories.DoubleCategories.Core.DoubleFunctor.LeftUnitor

Library UniMath.Bicategories.DoubleCategories.Core.DoubleFunctor.RightUnitor

Library UniMath.Bicategories.DoubleCategories.DerivedLaws.TransportLaws

Library UniMath.Bicategories.DoubleCategories.DerivedLaws.Unitors

• 1. Derived laws regarding horizontal composition
• 2. Derived laws for the pentagon and triangle
• 3. Derived laws for the unitors on the identity

Library UniMath.Bicategories.DoubleCategories.DerivedLaws.Variations

• 1. Variations of the double category laws
• 2. Laws involving identities and globular iso squares
• 3. Variations of the laws of lax double functors

Library UniMath.Bicategories.DoubleCategories.DoubleBicat.CellsAndSquares

• 1. Maps from cells to squares
• 2. The conditions that cells can be expressed as certain squares
• 3. Verity double bicategories in which vertical cells are the same as squares
• 3.1. Identity squares and vertical cells
• 3.2. Composition of squares and vertical cells
• 3.3. Invertible squares and vertical cells
• 4. Verity double bicategories in which horizontal cells are the same as squares
• 4.1. Identity squares and horizontal cells
• 4.2. Composition of squares and horizontal cells
• 4.3. Invertible squares and horizontal cells

Library UniMath.Bicategories.DoubleCategories.DoubleBicat.CompanionPairAdjEquiv

• 1. Cells between companion pairs
• 2. Invertible 2-cells between companions
• 3. Companions of adjoint equivalences
• 4. Vertical equivalences in Verity double bicategories with all companions

Library UniMath.Bicategories.DoubleCategories.DoubleBicat.CompanionPairUnique

• 1. Squares between companion pairs
• 2. The square is invertible
• 3. Preservation of the unit and counit
• 4. Consequences of the uniqueness

Library UniMath.Bicategories.DoubleCategories.DoubleBicat.CompanionPairs

• 1. Definition of companion pairs
• 2. Identity companion pairs
• 3. Composition of companion pairs
• 4. Verity double bicategories with all companion pairs
• 5. Companions of horizontal morphisms

Library UniMath.Bicategories.DoubleCategories.DoubleBicat.Conjoints

• 1. Definition of conjoints
• 2. Conjoints and companions
• 3. Identity conjoints
• 4. Composition of companion pairs
• 5. Verity double bicategories with all conjoints

Library UniMath.Bicategories.DoubleCategories.DoubleBicat.Core

Library UniMath.Bicategories.DoubleCategories.DoubleBicat.DerivedLaws

• 1. Laws regarding the left unitor and composition
• 2. Laws regarding the right unitor and composition
• 3. Laws regarding the associator
• 4. Laws regarding whiskering 2-cells
• 5. Equality laws for whiskering
• 6. Operations on globular squares
• 7. Composing corners

Library UniMath.Bicategories.DoubleCategories.DoubleBicat.GlobalUnivalence

• 1. Horizontally globally univalent Verity double bicategories
• 3. Globally univalent Verity double bicategories
• 4. Gregarious univalent Verity double bicategories
• 5. Horizontally globally univalent to gregarious univalent
• 6. Equivalence of horizontal global univalence and gregarious univalence

Library UniMath.Bicategories.DoubleCategories.DoubleBicat.GregariousEquivalence

• 1. Gregarious equivalences
• 2. The identity is a gregarious equivalence
• 3. Identities to gregarious equivalences
• 4. Horizontal gregarious equivalences
• 5. Being a horizontal gregarious equivalence is a proposition
• 6. Adjoint equivalences and gregarious equivalences

Library UniMath.Bicategories.DoubleCategories.DoubleBicat.LocalUnivalence

• 1. Local horizontal univalence
• 2. Local horizontal univalence via squares
• 3. Equivalence between the different local horizontal univalence conditions
• 4. Local vertical univalence
• 5. Local vertical univalence via squares
• 6. Equivalence between the different local vertical univalence conditions
• 7. Locally univalent vertical bicategories

Library UniMath.Bicategories.DoubleCategories.DoubleBicat.UnderlyingCats

• 1. The underlying horizontal bicategory
• 2. The underlying vertical bicategory
• 3. The underlying horizontal hom-category
• 4. The underlying vertical hom-category
• 5. The underlying category of squares and horizontal cylinders
• 6. The underlying category of squares and vertical cylinders
• 7. The underlying category of vertical morphisms and squares
• 8. The underlying category of horizontal morphisms and squares

Library UniMath.Bicategories.DoubleCategories.DoubleBicat.VerityDoubleBicat

• 1. Bicategories with squares
• 2. Horizontal and vertical bicategory with squares
• 3. Horizontal identity squares and verizontal composition of squares
• 4. Whiskering operations
• 5. Identity and composition laws for whiskering (items (i)-(v) in Verity)
• 6. Laws relating composition and identity squares (items (ix) and (x) in Verity)
• 7. Laws about cylinders (items (vi)-(vii) in Verity)
• 8. Verity double bicategories
• 9. Unfolded versions of the laws for Verity double bicategories

Library UniMath.Bicategories.DoubleCategories.Examples.BiSetcatToDoubleCat

• 1. The underlying category
• 2. The 2-sided displayed category of 1-cells
• 3. Horizontal identities
• 4. Horizontal composition
• 5. The unitors and associators
• 6. The pentagon and triangle equation
• 7. The double category corresponding to a bicategory
• 8. The pseudo double setcategory corresponding to a bicategory

Library UniMath.Bicategories.DoubleCategories.Examples.Coalgebras

• 1. Basic definitions
• 2. The 2-sided displayed category
• 3. Builders and accessors for horizontal morphisms
• 4. Builders and accessors for squares
• 5. Horizontal identities
• 6. Horizontal composition
• 7. Globular isomorphism squares
• 8. The left unitor
• 9. The right unitor
• 10. The associator
• 11. The coherences
• 12. The double category of coalgebras of a lax double functor
• 13. The univalence of the double category of coalgebra
• 14. The univalent double category of coalgebras of a lax double functor
• 15. Flatness of the double category of coalgebras

Library UniMath.Bicategories.DoubleCategories.Examples.Coreflections

• 1. Coreflections in a 2-category
• 2. The displayed category of adjunctions
• 3. The displayed category of coreflections
• 4. The double category of coreflections
• 5. Lemmas for calculation
• 6. Companions and conjoints

Library UniMath.Bicategories.DoubleCategories.Examples.DoubleCatOnDispCat

• 1. The double category
• 2. Properties of this double category
• 3. Univalence and strictness

Library UniMath.Bicategories.DoubleCategories.Examples.DoubleCatToDoubleBicat

• 1. The vertical bicategory
• 2. The whiskering operations
• 3. The laws of the Verity double bicategory
• 4. The Verity double bicategory coming from a pseudo double category
• 5. The univalence of this Verity double bicategory
• 6. Companions and conjoints

Library UniMath.Bicategories.DoubleCategories.Examples.EnrichedProfunctorDoubleBicat

• 1. The 2-sided displayed category of the Verity bicategory of enriched profunctors
• 2. The vertical bicategory of enriched profunctors
• 3. The whiskering operations
• 4. More laws
• 5. The Verity double bicategory of enriched categories and profunctors
• 6. 2-cells versus squares
• 7. Companion pairs of profunctors
• 8. Vertical invertible 2-cells of enriched profunctors
• 9. The local univalence of the Verity double bicategory of squares
• 10. The global univalence of the Verity double bicategory of squares

Library UniMath.Bicategories.DoubleCategories.Examples.EnrichedProfunctorDoubleCat

• 1. The 2-sided displayed category of quantale enriched profunctors
• 2. Horizontal identities
• 3. Horizontal composition
• 4. The unitors and associators
• 5. The double category of quantale enriched profunctors
• 6. Companions and conjoints

Library UniMath.Bicategories.DoubleCategories.Examples.EnrichedRelDoubleCat

• 1. Horizontal identities
• 2. Horizontal composition
• 3. Unitors and associators
• 4. The double category of enriched relations
• 5. Companion pairs and conjoints

Library UniMath.Bicategories.DoubleCategories.Examples.FullSubDoubleCat

• 1. The full sub double category
• 2. Properties of this double category
• 3. Univalence and strictness

Library UniMath.Bicategories.DoubleCategories.Examples.HorizontalDual

• 1. The data of the horizontal dual
• 2. Whiskering operations
• 3. Laws of the horizontal dual
• 4. The horizontal dual
• 5. Vertical cells and squares
• 6. The local univalence of the dual

Library UniMath.Bicategories.DoubleCategories.Examples.KleisliDoubleCat

• 1. Horizontal operations
• 2. The Kleisli double category
• 3. The strict Kleisli double category

Library UniMath.Bicategories.DoubleCategories.Examples.LaxExtensionToFunctor

• 1. Every lax extension gives rise to a lax double functor
• 2. Every lax double functor gives rise to a lax extension
• 3. Equivalence between lax double functors and functors with a lax extension

Library UniMath.Bicategories.DoubleCategories.Examples.LensesDoubleCat

• 1. The horizontal identity
• 2. Horizontal composition
• 3. Unitors and associators
• 4. The double category
• 5. The strict double category

Library UniMath.Bicategories.DoubleCategories.Examples.MateDoubleBicat

• 1. The bicategory of left adjoints
• 2. The data of the double bicategory of mates
• 3. The laws
• 4. The double bicategory of mates
• 5. 2-cells coincide with certain mates
• 6. Companion pairs
• 7. Vertical invertible 2-cells
• 8. The local univalence of the Verity double bicategory of mates
• 9. Vertical adjoint equivalences
• 10. The global univalence of the Verity double bicategory of mates

Library UniMath.Bicategories.DoubleCategories.Examples.OpDoubleCat

• 1. Vertical opposites of double categories
• 1.1. Horizontal identity in the vertical opposite
• 1.2. Horizontal composition in the vertical opposite
• 1.3. Unitors and associators
• 1.4. Triangle and pentagon
• 1.5. The vertical opposite
• 2. Horizontal opposites of double categories
• 2.1. Horizontal identity in the horizontal opposite
• 2.2. Horizontal composition in the horizontal opposite
• 2.3. Unitors and associators
• 2.4. Triangle and pentagon
• 2.5. The horizontal opposite

Library UniMath.Bicategories.DoubleCategories.Examples.ParaDoubleCat

• 1. Horizontal identities
• 2. Horizontal composition
• 3. The unitors and associators
• 4. The triangle and pentagon equations
• 5. The double category of parametrized morphisms
• 6. Parametrized morphisms and isomorphisms

Library UniMath.Bicategories.DoubleCategories.Examples.ProductDoubleCat

• 1. Horizontal identity and composition
• 2. Unitors and associator
• 3. The triangle and pentagon
• 4. The product of double categories
• 5. Projections
• 6. Pairing
• 7. Pairing of double transformations
• 8. Products of double categories

Library UniMath.Bicategories.DoubleCategories.Examples.ProfunctorDoubleBicat

• 1. The 2-sided displayed category of the Verity bicategory of profunctors
• 2. The vertical bicategory of profunctors
• 3. The whiskering operations
• 4. More laws
• 5. The Verity double bicategory of univalent categories and profunctors
• 6. 2-cells versus squares
• 7. Companion pairs of profunctors
• 8. Vertical invertible 2-cells of profunctors
• 9. The local univalence of the Verity double bicategory of squares
• 10. The global univalence of the Verity double bicategory of squares

Library UniMath.Bicategories.DoubleCategories.Examples.ProfunctorDoubleCat

• 1. Horizontal identity
• 2. Horizontal composition
• 3. Unitors and associators
• 4. Triangle and pentagon
• 5. The univalent pseudo double category of profunctors
• 6. Companions and conjoints

Library UniMath.Bicategories.DoubleCategories.Examples.RelationsDoubleCat

• 1. Relations valued in propositions
• 1.1. Horizontal identities
• 1.2. Horizontal composition
• 1.3. The unitors and associators
• 1.4. The triangle and pentagon equations
• 1.5. The double category of relations valued in propositions
• 1.6. Companions and conjoints
• 2. Relations valued in sets
• 2.1. Horizontal identities
• 2.2. Horizontal composition
• 2.3. The unitors and associators
• 2.4. The triangle and pentagon equations
• 2.5. The double category of relations
• 2.6. Companions and conjoints

Library UniMath.Bicategories.DoubleCategories.Examples.SpansDoubleCat

• 1. Horizontal identities
• 2. Horizontal composition
• 3. The unitors and associators
• 4. The triangle and pentagon equations
• 5. The double category of spans

Library UniMath.Bicategories.DoubleCategories.Examples.SquareDoubleBicat

• 1. The data of the double bicategory of squares
• 2. The laws
• 3. The double bicategory of squares
• 4. 2-cells coincide with certain squares
• 5. Companion pairs
• 6. Vertical invertible 2-cells
• 7. The local univalence of the Verity double bicategory of squares
• 8. Vertical adjoint equivalences
• 9. The global univalence of the Verity double bicategory of squares

Library UniMath.Bicategories.DoubleCategories.Examples.SquareDoubleCat

• 1. Horizontal operations
• 2. The square double category
• 3. The strict square double category

Library UniMath.Bicategories.DoubleCategories.Examples.SquareDoubleCatTwo

• 1. Horizontal operations
• 2. The square double category of a 2-category
• 3. The square pseudo double setcategory of a 2-setcategory

Library UniMath.Bicategories.DoubleCategories.Examples.StructuredCospansDoubleCat

• 1. Horizontal identities
• 2. Horizontal composition
• 3. The unitors and associators
• 4. The triangle and pentagon equations
• 5. The double category of structured cospans

Library UniMath.Bicategories.DoubleCategories.Examples.StructuredCospansDoubleFunctor

• 1. Preservation of horizontal identities
• 2. Preservation of horizontal composition
• 3. The coherences
• 4. The double functors between the double categories of structured cospans
• 5. Conditions under which this double functor is strong

Library UniMath.Bicategories.DoubleCategories.Examples.TransposeDoubleBicat

• 1. The 2-sided displayed category of the transpose
• 2. The vertical bicategory of the transpose
• 3. The whiskering operations
• 4. The transpose of a Verity double bicategory

Library UniMath.Bicategories.DoubleCategories.Examples.TransposeStrict

• 1. The precategory
• 2. The 2-sided displayed category
• 3. The horizontal identity
• 4. Horizontal composition
• 5. Double category laws
• 6. The dual double category

Library UniMath.Bicategories.DoubleCategories.Examples.UnitDoubleCat

• 1. Horizontal operations of the unit double category
• 2. The unit double category
• 3. Functors to the unit double category
• 4. Transformations to the unit double category
• 5. The unit double category is a terminal object

Library UniMath.Bicategories.DoubleCategories.Limits.DoubleTerminal

• 1. Terminal objects in double categories
• 2. Accessors and builders
• 3. Terminal object in the double category of relations
• 4. Terminal object in the double category of enriched relations
• 5. Terminal object in the double category of spans

Library UniMath.Bicategories.DoubleCategories.Underlying.HorizontalBicategory

• 1. The data of the horizontal bicategory
• 2. The laws of the horizontal bicategory
• 3. The horizontal bicategory
• 4. Local univalence of the bicategory

Library UniMath.Bicategories.DoubleCategories.Underlying.VerticalTwoCategory

• 1. The underlying vertical category
• 2. The data of the vertical 2-category
• 3. The laws of the vertical 2-category
• 4. The vertical 2-category of a pseudo double category

Library UniMath.Bicategories.DoubleCategories.Underlying.VerticalTwoCategoryStrict

• 1. The underlying category
• 2. The data of the 2-category
• 3. The laws of the 2-category
• 4. The underlying vertical 2-category

Library UniMath.Bicategories.Grothendieck.Biequivalence

Library UniMath.Bicategories.Grothendieck.Counit

Library UniMath.Bicategories.Grothendieck.FiberwiseEquiv

Library UniMath.Bicategories.Grothendieck.FibrationToPseudoFunctor

Library UniMath.Bicategories.Grothendieck.PseudoFunctorToFibration

Library UniMath.Bicategories.Grothendieck.Unit

Library UniMath.Bicategories.Limits.CommaObjects

Library UniMath.Bicategories.Limits.EilenbergMooreComonad

Library UniMath.Bicategories.Limits.EilenbergMooreObjects

Library UniMath.Bicategories.Limits.EquifierEquivalences

Library UniMath.Bicategories.Limits.Equifiers

Library UniMath.Bicategories.Limits.Final

• Bifinal object in a bicategory

Library UniMath.Bicategories.Limits.InserterEquivalences

Library UniMath.Bicategories.Limits.Inserters

Library UniMath.Bicategories.Limits.IsoInserters

Library UniMath.Bicategories.Limits.ProductEquivalences

Library UniMath.Bicategories.Limits.Products

Library UniMath.Bicategories.Limits.PullbackEquivalences

Library UniMath.Bicategories.Limits.PullbackFunctions

Library UniMath.Bicategories.Limits.Pullbacks

Library UniMath.Bicategories.Limits.Examples.BicatOfCatsLimits

Library UniMath.Bicategories.Limits.Examples.BicatOfEnrichedCatsLimits

Library UniMath.Bicategories.Limits.Examples.BicatOfUnivCatsLimits

Library UniMath.Bicategories.Limits.Examples.DispConstructionsLimits

Library UniMath.Bicategories.Limits.Examples.DisplayMapSliceLimits

Library UniMath.Bicategories.Limits.Examples.LimitsStructuredCategories

Library UniMath.Bicategories.Limits.Examples.OneTypesLimits

Library UniMath.Bicategories.Limits.Examples.OpCellBicatLimits

Library UniMath.Bicategories.Limits.Examples.OpMorBicatLimits

Library UniMath.Bicategories.Limits.Examples.SliceBicategoryLimits

Library UniMath.Bicategories.Limits.Examples.SubbicatLimits

Library UniMath.Bicategories.Limits.Examples.TotalBicategoryLimits

Library UniMath.Bicategories.Limits.Examples.UnivGroupoidsLimits

Library UniMath.Bicategories.Logic.ComprehensionBicat

Library UniMath.Bicategories.Logic.DisplayMapBicat

Library UniMath.Bicategories.Logic.Examples.DisplayMapComprehensionBicat

Library UniMath.Bicategories.Logic.Examples.FibrationsComprehensionBicat

Library UniMath.Bicategories.Logic.Examples.FunctorsIntoCatComprehensionBicat

Library UniMath.Bicategories.Logic.Examples.OpfibrationsComprehensionBicat

Library UniMath.Bicategories.Logic.Examples.PullbackComprehensionBicat

Library UniMath.Bicategories.Logic.Examples.TrivialComprehensionBicat

Library UniMath.Bicategories.Modifications.Modification

• Modifications between pseudo transformations

Library UniMath.Bicategories.Modifications.Examples.ApModification

Library UniMath.Bicategories.Modifications.Examples.Associativity

Library UniMath.Bicategories.Modifications.Examples.ModificationIntoCat

Library UniMath.Bicategories.Modifications.Examples.Unitality

Library UniMath.Bicategories.Monads.ConstructionOfAlgebras

Library UniMath.Bicategories.Monads.DistributiveLaws

Library UniMath.Bicategories.Monads.LocalEquivalenceMonad

• 1. Action on objects
• 2. Action on morphisms
• 3. The functor
• 4. The functor is faithful
• 5. The functor is full
• 6. The functor is essentially surjective
• 7. The adjoint equivalence

Library UniMath.Bicategories.Monads.MixedDistributiveLaws

Library UniMath.Bicategories.Monads.MonadToAdjunction

Library UniMath.Bicategories.Monads.Examples.AdjunctionToMonad

Library UniMath.Bicategories.Monads.Examples.Composition

Library UniMath.Bicategories.Monads.Examples.MonadsInBicatOfCats

Library UniMath.Bicategories.Monads.Examples.MonadsInBicatOfEnrichedCats

Library UniMath.Bicategories.Monads.Examples.MonadsInBicatOfUnivCats

Library UniMath.Bicategories.Monads.Examples.MonadsInMonads

Library UniMath.Bicategories.Monads.Examples.MonadsInOp1Bicat

Library UniMath.Bicategories.Monads.Examples.MonadsInOp2Bicat

Library UniMath.Bicategories.Monads.Examples.MonadsInStructuredCategories

Library UniMath.Bicategories.Monads.Examples.MonadsInTotalBicat

Library UniMath.Bicategories.Monads.Examples.PsfunctorOnMonad

Library UniMath.Bicategories.Monads.Examples.ToMonadInCat

Library UniMath.Bicategories.MonoidalCategories.ActionBasedStrength

Library UniMath.Bicategories.MonoidalCategories.ActionBasedStrongFunctorCategory

Library UniMath.Bicategories.MonoidalCategories.ActionBasedStrongFunctorsMonoidal

Library UniMath.Bicategories.MonoidalCategories.ActionBasedStrongFunctorsWhiskeredMonoidal

Library UniMath.Bicategories.MonoidalCategories.ActionOfEndomorphismsInBicat

Library UniMath.Bicategories.MonoidalCategories.ActionOfEndomorphismsInBicatWhiskered

Library UniMath.Bicategories.MonoidalCategories.Actions

Library UniMath.Bicategories.MonoidalCategories.ActionsFormBicategory

Library UniMath.Bicategories.MonoidalCategories.BicatOfActegories

Library UniMath.Bicategories.MonoidalCategories.BicatOfActegoriesFinalObject

Library UniMath.Bicategories.MonoidalCategories.BicatOfActionsInBicat

Library UniMath.Bicategories.MonoidalCategories.BicatOfWhiskeredMonCats

Library UniMath.Bicategories.MonoidalCategories.BicatOfWhiskeredMonCatsFinalObject

Library UniMath.Bicategories.MonoidalCategories.BicatOfWhiskeredMonCatsLax

Library UniMath.Bicategories.MonoidalCategories.ConstructionOfActions

Library UniMath.Bicategories.MonoidalCategories.EndofunctorsMonoidal

Library UniMath.Bicategories.MonoidalCategories.EndofunctorsWhiskeredMonoidal

Library UniMath.Bicategories.MonoidalCategories.EquivalenceActegoriesAndActions

Library UniMath.Bicategories.MonoidalCategories.IdempotencePointedFunctorsWhiskeredMonoidal

Library UniMath.Bicategories.MonoidalCategories.MonadsAsMonoidsWhiskered

Library UniMath.Bicategories.MonoidalCategories.MonoidalDialgebrasInserters

Library UniMath.Bicategories.MonoidalCategories.MonoidalFromBicategory

• • • Going into the opposite direction of UniMath.Bicategories.Core.Examples.BicategoryFromMonoidal

Library UniMath.Bicategories.MonoidalCategories.PointedFunctorsMonoidal

Library UniMath.Bicategories.MonoidalCategories.PointedFunctorsWhiskeredMonoidal

Library UniMath.Bicategories.MonoidalCategories.WhiskeredMonoidalFromBicategory

• • • Going into the opposite direction of UniMath.Bicategories.Core.Examples.BicategoryFromWhiskeredMonoidal

Library UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.AssociatorUnitorsLayer

Library UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.CurriedMonoidalCategories

Library UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.EquivalenceMonCatCurried

Library UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.EquivalenceMonCatNonCurried

Library UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.EquivalenceWhiskeredCurried

Library UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.FinalLayer

Library UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.TensorLayer

Library UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.TensorUnitLayer

Library UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.UnitLayer

Library UniMath.Bicategories.Morphisms.Adjunctions

• Internal adjunctions and adjoint equivalences
  • Definitions of internal adjunctions
    • Data & laws for left adjoints
    • Laws for equivalences
    • Packaged

Library UniMath.Bicategories.Morphisms.DiscreteMorphisms

Library UniMath.Bicategories.Morphisms.Eso

Library UniMath.Bicategories.Morphisms.ExtensionsAndLiftings

Library UniMath.Bicategories.Morphisms.FullyFaithful

Library UniMath.Bicategories.Morphisms.InternalStreetFibration

Library UniMath.Bicategories.Morphisms.InternalStreetOpFibration

Library UniMath.Bicategories.Morphisms.Monadic

Library UniMath.Bicategories.Morphisms.Properties

Library UniMath.Bicategories.Morphisms.Examples.EsosInBicatOfUnivCats

Library UniMath.Bicategories.Morphisms.Examples.FibrationsInBicatOfUnivCats

Library UniMath.Bicategories.Morphisms.Examples.FibrationsInStrictCats

Library UniMath.Bicategories.Morphisms.Examples.MorphismsInBicatOfEnrichedCats

• 1. Faithful 1-cells
• 2. Fully faithful 1-cells
• 3. Conservative 1-cells
• 4. Discrete 1-cells
• 5. Enriched adjunctions

Library UniMath.Bicategories.Morphisms.Examples.MorphismsInBicatOfUnivCats

Library UniMath.Bicategories.Morphisms.Examples.MorphismsInOneTypes

Library UniMath.Bicategories.Morphisms.Examples.MorphismsInOp1Bicat

Library UniMath.Bicategories.Morphisms.Examples.MorphismsInOp2Bicat

Library UniMath.Bicategories.Morphisms.Examples.MorphismsInSliceBicat

Library UniMath.Bicategories.Morphisms.Examples.MorphismsInStructuredCat

Library UniMath.Bicategories.Morphisms.Properties.AdjunctionsRepresentable

Library UniMath.Bicategories.Morphisms.Properties.ClosedUnderInvertibles

Library UniMath.Bicategories.Morphisms.Properties.ClosedUnderPullback

Library UniMath.Bicategories.Morphisms.Properties.Composition

Library UniMath.Bicategories.Morphisms.Properties.ContainsAdjEquiv

Library UniMath.Bicategories.Morphisms.Properties.EsoProperties

Library UniMath.Bicategories.Morphisms.Properties.FromInitial

Library UniMath.Bicategories.Morphisms.Properties.Projections

Library UniMath.Bicategories.Objects.CartesianObject

Library UniMath.Bicategories.Objects.CocartesianObject

Library UniMath.Bicategories.Objects.Examples.BicatOfUnivCatsObjects

Library UniMath.Bicategories.OrthogonalFactorization.EnrichedEsoFactorization

• 1, The left and right class of the factorization system
• 2. Image factorization
• 3. Lifts of 1-cells
• 4. Lifts of 2-cells
• 5. Uniqueness of lifts of 2-cells
• 6. Fully faithful 1-cells are closed under invertible 2-cells
• 7. The factorization system
• 8. Essentially surjective+fully faithful implies adjoint equivalence

Library UniMath.Bicategories.OrthogonalFactorization.EsoFactorizationSystem

Library UniMath.Bicategories.OrthogonalFactorization.FactorizationSystem

• 1. Factorizations
• 2. Orthogonal factorization systems
• 3. Builder for orthogonal factorization systems
• 4. Projections for orthogonal factorization systems
• 5. Properties of orthogonal factorization systems

Library UniMath.Bicategories.OrthogonalFactorization.Orthogonality

• 1. Orthogonality
• 2. Constructing orthogonal morphisms
• 3. Projections of orthogonal morphisms
  • 3.1. Lifting property for for 1-cells
  • 3.2. Lifting property for for 2-cells
  • 3.3. Lifting property for for equalities

Library UniMath.Bicategories.OtherStructure.ClassifyingDiscreteOpfib

Library UniMath.Bicategories.OtherStructure.Cores

Library UniMath.Bicategories.OtherStructure.DualityInvolution

• 1. Data of duality involutions
• 2. Counit of duality involution
• 3. Laws of duality involutions
• 4. Duality involutions
• 5. Accessors for the laws of duality involutions

Library UniMath.Bicategories.OtherStructure.DualityInvolutionProperties

• 1. Transposes of duality involutions
• 2. Duality involutions are local equivalences

Library UniMath.Bicategories.OtherStructure.Exponentials

Library UniMath.Bicategories.OtherStructure.Examples.StructureBicatOfEnrichedCats

Library UniMath.Bicategories.OtherStructure.Examples.StructureBicatOfUnivCats

Library UniMath.Bicategories.OtherStructure.Examples.StructureOneTypes

Library UniMath.Bicategories.PseudoFunctors.Biadjunction

Library UniMath.Bicategories.PseudoFunctors.Biequivalence

• Biequivalence

Library UniMath.Bicategories.PseudoFunctors.LocalEquivalenceProperties

• 1. Action on 1-cells and 2-cells
• 2. Unit and counit
• 3. Functoriality of the action on 2-cells
• 4. Action on invertible 2-cells
• 5. Identitor and compositor
• 6. Pseudofunctor laws

Library UniMath.Bicategories.PseudoFunctors.Properties

• 1. Local equivalences
• 2. Projections for local equivalences
• 3. Local weak equivalences
• 4. Essentially surjective pseudofunctors
• 5. Weak equivalences of bicategories

Library UniMath.Bicategories.PseudoFunctors.PseudoFunctor

• Pseudofunctors on bicategories
• Pseudo functors.
  • Pseudo-functors

Library UniMath.Bicategories.PseudoFunctors.PseudoFunctorLimits

Library UniMath.Bicategories.PseudoFunctors.Representable

• Representable pseudofunctor, pseudotransformation, and modifications

Library UniMath.Bicategories.PseudoFunctors.StrictPseudoFunctor

• Strict pseudofunctors on bicategories
• Strict pseudo functors.
  • Strict pseudo-functors

Library UniMath.Bicategories.PseudoFunctors.UniversalArrow

Library UniMath.Bicategories.PseudoFunctors.Yoneda

• Yoneda embedding

Library UniMath.Bicategories.PseudoFunctors.Display.Base

Library UniMath.Bicategories.PseudoFunctors.Display.Compositor

Library UniMath.Bicategories.PseudoFunctors.Display.Identitor

Library UniMath.Bicategories.PseudoFunctors.Display.Map1Cells

Library UniMath.Bicategories.PseudoFunctors.Display.Map2Cells

Library UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat

Library UniMath.Bicategories.PseudoFunctors.Display.StrictCompositor

Library UniMath.Bicategories.PseudoFunctors.Display.StrictIdentitor

Library UniMath.Bicategories.PseudoFunctors.Display.StrictPseudoFunctorBicat

Library UniMath.Bicategories.PseudoFunctors.Examples.ApFunctor

Library UniMath.Bicategories.PseudoFunctors.Examples.BicatOfCatToUnivCat

Library UniMath.Bicategories.PseudoFunctors.Examples.CatDiag

Library UniMath.Bicategories.PseudoFunctors.Examples.ChangeOfBaseEnriched

Library UniMath.Bicategories.PseudoFunctors.Examples.Composition

Library UniMath.Bicategories.PseudoFunctors.Examples.CompositionPseudoFunctor

Library UniMath.Bicategories.PseudoFunctors.Examples.ConstProduct

Library UniMath.Bicategories.PseudoFunctors.Examples.Constant

Library UniMath.Bicategories.PseudoFunctors.Examples.CorestrictImage

Library UniMath.Bicategories.PseudoFunctors.Examples.CurryingInBicatOfCats

Library UniMath.Bicategories.PseudoFunctors.Examples.Identity

Library UniMath.Bicategories.PseudoFunctors.Examples.LiftingActegories

Library UniMath.Bicategories.PseudoFunctors.Examples.MonadInclusion

Library UniMath.Bicategories.PseudoFunctors.Examples.Op2OfPseudoFunctor

Library UniMath.Bicategories.PseudoFunctors.Examples.OpFunctor

Library UniMath.Bicategories.PseudoFunctors.Examples.OpFunctorEnriched

Library UniMath.Bicategories.PseudoFunctors.Examples.PathGroupoid

Library UniMath.Bicategories.PseudoFunctors.Examples.Projection

Library UniMath.Bicategories.PseudoFunctors.Examples.PseudoFunctorsIntoCat

Library UniMath.Bicategories.PseudoFunctors.Examples.PseudofunctorFromMonoidal

• • • Going into the opposite direction

Library UniMath.Bicategories.PseudoFunctors.Examples.PullbackFunctor

Library UniMath.Bicategories.PseudoFunctors.Examples.Reindexing

Library UniMath.Bicategories.PseudoFunctors.Examples.StrictToPseudo

Library UniMath.Bicategories.PseudoFunctors.Examples.Strictify

Library UniMath.Bicategories.PseudoFunctors.Preservation.BiadjunctionPreservation

Library UniMath.Bicategories.PseudoFunctors.Preservation.BiadjunctionPreserveCoproducts

Library UniMath.Bicategories.PseudoFunctors.Preservation.BiadjunctionPreserveEquifiers

Library UniMath.Bicategories.PseudoFunctors.Preservation.BiadjunctionPreserveInserters

Library UniMath.Bicategories.PseudoFunctors.Preservation.BiadjunctionPreserveProducts

Library UniMath.Bicategories.PseudoFunctors.Preservation.ClosedUnderEquivalence

Library UniMath.Bicategories.PseudoFunctors.Preservation.Preservation

Library UniMath.Bicategories.PseudoFunctors.Preservation.PullbackPreservation

Library UniMath.Bicategories.RezkCompletions.BicatToLocalUnivalentBicat

Library UniMath.Bicategories.RezkCompletions.DisplayedRezkCompletions

Library UniMath.Bicategories.RezkCompletions.RezkCompletionOfBicategory

Library UniMath.Bicategories.RezkCompletions.Uniqueness

• 1. An equality lemma for the type `functor_from A`
• 2. Two initial functors from a type are equal
• 3. Two Rezk completions are equal

Library UniMath.Bicategories.RezkCompletions.StructuredCats.BinProducts

Library UniMath.Bicategories.RezkCompletions.StructuredCats.Equalizers

Library UniMath.Bicategories.RezkCompletions.StructuredCats.FiniteLimits

Library UniMath.Bicategories.RezkCompletions.StructuredCats.Pullbacks

Library UniMath.Bicategories.RezkCompletions.StructuredCats.SubobjectClassifier

Library UniMath.Bicategories.RezkCompletions.StructuredCats.Terminal

Library UniMath.Bicategories.Transformations.PseudoTransformation

Library UniMath.Bicategories.Transformations.Examples.AlgebraMap

Library UniMath.Bicategories.Transformations.Examples.ApTransformation

Library UniMath.Bicategories.Transformations.Examples.Associativity

Library UniMath.Bicategories.Transformations.Examples.PseudoTransformationIntoCat

Library UniMath.Bicategories.Transformations.Examples.Unitality

Library UniMath.Bicategories.Transformations.Examples.Whiskering

Library UniMath.Bicategories.WkCatEnrichment.Cat

Library UniMath.Bicategories.WkCatEnrichment.Notations

Library UniMath.Bicategories.WkCatEnrichment.bicategory

Library UniMath.Bicategories.WkCatEnrichment.hcomp_bicat

Library UniMath.Bicategories.WkCatEnrichment.internal_equivalence

Library UniMath.Bicategories.WkCatEnrichment.prebicategory

• • Final packing and projections.
  • Basics on identities and inverses
    • The othoter triangle identity.

Library UniMath.Bicategories.WkCatEnrichment.whiskering

Library UniMath.CategoryTheory.Abelian

• Abelian categories
  • Contents
• Definition of Abelian categories
  • Data1
  • Data2
  • Every monic is kernel of its cokernel
  • Every epi is a cokernel of its kernel
  • AbelianData
  • Abelian categories
• isMonic f -> isEpi f -> is_z_isomorphism f
• Pullbacks of monics and pushouts of epis
  • Pullbacks of monics
  • Pushouts of epis
• Equalizers and Coequalizers
  • Equalizers
  • Coequalizers
• Pushouts and pullbacks
• Monic kernels and Epi cokernels
  • KernelArrow of Monic x --> y = (to_Zero A) --> x
  • CokernelArrow of Epi x --> y = y --> (to_Zero A)
  • KernelArrow = FromZero ⇒ isMonic
  • CokernelArrow = ToZero ⇒ isEpi
• Factorization of morphisms
  • Kernels, Cokernels, CoImage, and Image
  • Construction of the morphism CoIm f --> Im f
  • f = (x --> CoIm f) · (CoIm f --> Im f) · (Im f --> y)
  • CoIm f --> Im f is an isomorphism.
  • f = Epi ((x --> CoIm f) · (CoIm f --> Im f)) · Monic (Im f --> y)
  • f = Epi ((x --> CoIm f)) · Monic ((CoIm f --> Im f) · (Im f --> y))
• A Abelian -> A^op Abelian, Abelian_opp

Library UniMath.CategoryTheory.AbelianPushoutPullback

• Pushout of a Monic is Monic, Pullback of an Epi is Epi
  • Introduction
  • Pushout of a Monic is Monic
  • Pushout of Monic is Pullback
  • Pullback of an Epi is Epi
  • Pullback of Epi is Pushout

Library UniMath.CategoryTheory.AbelianToAdditive

• AbelianPreCat is CategoryWithAdditiveStructure
  • Contents
• AbelianPreCat is CategoryWithAdditiveStructure.
  • Preliminaries
  • AbelianPreCat is CategoryWithAdditiveStructure

Library UniMath.CategoryTheory.Actions

• Actions
  • Contents
  • Structures on morphisms
    • Endomorphisms and the endomorphism monoid
    • The endomorphism ring in an additive category
  • Algebraic structures as categories
    • Lemmas about categories with one object
    • Monoids
      • Monoids as categories (monoid_weq_contr_category)
      • Monoid morphisms as functors (monoid_fun_weq_functor)
    • Groups
      • Groups as groupoids
      • Group morphisms as functors
  • Actions
    • As homomorphisms
      • Monoid (group) actions
      • Ring actions
    • As functors
      • Equivariant maps (intertwiners)
      • Monoid (group) actions
      • Ring actions
  • Theory
    • Translation groupoid (translation_groupoid)

Library UniMath.CategoryTheory.Additive

• Additive categories.
• Contents
• Definition of additive categories
• Quotient is additive
• Kernels, Equalizers, Cokernels, and Coequalizers in CategoryWithAdditiveStructure categories
  • Introduction
  • Correspondence between Cokernels and Coeqalizers
• Sum and in to BinDirectSum is Monic
• Monics and Epis in an additive category
• Miscellaneous results about pre- and postcomposition in an additive category

Library UniMath.CategoryTheory.AdditiveFunctors

• Additive functors
  • Contents
• Definition of additive functor
  • isAdditiveFunctor
  • Additive functor
  • Basics of additive functors
• Additive functor preserves BinDirectSums
  • F preserves IdIn1, IdIn2, IdUnit1, IdUnit2, and Id of BinDirectSum
• Additive criteria
  • Preserves unel
  • Commutes with binop
• The functor QuotcategoryFunctor is additive
• Equivalences of additive categories

Library UniMath.CategoryTheory.All

Library UniMath.CategoryTheory.ArrowCategory

• Arrow categories
  • Contents
  • Definition
  • As a comma category

Library UniMath.CategoryTheory.BicatOfCatsElementary

Library UniMath.CategoryTheory.CategoricalRecursionSchemes

Library UniMath.CategoryTheory.CategoriesWithBinOps

• • Precategories such that spaces of morphisms have a binary operation

Library UniMath.CategoryTheory.CategoryEquality

• • Equality of precategories

Library UniMath.CategoryTheory.CategorySum

Library UniMath.CategoryTheory.CommaCategories

Library UniMath.CategoryTheory.CompletelyIterativeAlgebras

Library UniMath.CategoryTheory.Connected

Library UniMath.CategoryTheory.Core

• 8. A displayed category for the core

Library UniMath.CategoryTheory.ElementaryTopos

Library UniMath.CategoryTheory.Elements

Library UniMath.CategoryTheory.ElementsOp

Library UniMath.CategoryTheory.EpiFacts

Library UniMath.CategoryTheory.Epis

• Epis
  • Contents
• Definition of Epis
• Construction of the subcategory consisting of all epis.
• In functor categories epis can be constructed from pointwise epis

Library UniMath.CategoryTheory.ExponentiationLeftAdjoint

Library UniMath.CategoryTheory.FiveLemma

• FiveLemma
  • Contents
  • FiveLemma
  • Introduction
  • Rows
    • Objects for a row
    • Differentials for a row
    • Composition of consecutive differentials is 0
    • Row is exact
    • Define row for FiveLemma
  • Morphism of FiveRows
    • Morphisms in the morphism
    • Commutativity of the squares
    • Morphism of rows
  • Introduction
  • Introduction
  • Introduction
  • Construction of the first row
  • Construction of the second row
  • Construction of the morphism between rows
  • FiveLemma for short exact sequences

Library UniMath.CategoryTheory.FunctorAlgebras

• • Category of algebras of an endofunctor
  • This category is saturated if the base category is
  • Lambek's lemma: If (A,a) is an initial F-algebra then a is an iso
  • The natural numbers are intial for X ↦ 1 + X

Library UniMath.CategoryTheory.FunctorCategory

• Functor (pre)categories
  • Contents
  • Functor category [C, D]
    • The data of the functor precategory
    • Above data forms a precategory

Library UniMath.CategoryTheory.FunctorCoalgebras

• The category of coalgebras is univalent

Library UniMath.CategoryTheory.Groupoids

• Groupoids
  • Contents
  • Definitions
  • Lemmas
  • Subgroupoids
  • Discrete categories

Library UniMath.CategoryTheory.HomotopicalCategory

• HomotopicalCategory
  • Contents

Library UniMath.CategoryTheory.HorizontalComposition

• • currying functorial composition

Library UniMath.CategoryTheory.IsoCommaCategory

Library UniMath.CategoryTheory.LatticeObject

• Definition of lattice objects and bounded lattice objects
• Definition of sublattice objects

Library UniMath.CategoryTheory.LeftKanExtension

Library UniMath.CategoryTheory.LocalizingClass

• Localizing class
• Localizing class and localization of categories.
  • Localizing classes
    • Identities and compositions are in the subset of morphisms
      • Squares
    • Completion to squares
      • Pre- and post switch
      • Post switch
    • Pre- and postcomposition with morphisms in the subset
    • Localizing class
  • Roofs
  • Coroofs
  • RoofTop
  • Composition of roofs
  • Definition of the localization
  • Universal property

Library UniMath.CategoryTheory.Monics

• Monics
  • Contents
• Definition of Monics
• Construction of the subcategory consisting of all monics.
• In functor categories monics can be constructed from pointwise monics

Library UniMath.CategoryTheory.Morphisms

• Some general constructions
  • Contensts
• Pair of morphisms
  • Morphism
  • MorphismPair
• MorphismPair and opposite categories
• ShortShortExactData
  • Data for ShortShortExact
• ShortShortExactData and opposite categories

Library UniMath.CategoryTheory.PointedFunctorAlgebras

Library UniMath.CategoryTheory.PointedFunctors

Library UniMath.CategoryTheory.PointedFunctorsComposition

Library UniMath.CategoryTheory.PowerObject

Library UniMath.CategoryTheory.PreAdditive

• Definition of preadditive categories.
  • Contents
• Definition of a PreAdditive precategory
• Zero and unit
• Inverses and composition
• KernelIn, CokernelOut, and Binary Operations
  • Introduction
• Quotient of homsets
  • Here are some random results copied from category_abgr.v.
  • Composition of morphisms
    • Some lemmas
    • Morphisms to elements of groups
    • Composition of morphisms in the quotient precategory
      • Structure for composition
      • Composition for quotient category
  • Some equations on linearity, compositions, and binops
  • Construction of the Quotcategory
  • Quotient precategory of PreAdditive is PreAdditive
  • The canonical functor to Quotcategory
  • If PA has a zero object, then so does Quotcategory of PA

Library UniMath.CategoryTheory.PrecategoriesWithAbgrops

• • Precategories with homsets abelian groups (abgrops).

Library UniMath.CategoryTheory.PrecategoryBinProduct

• Binary product of (pre)categories
  • Contents :

Library UniMath.CategoryTheory.PrecompEquivalence

Library UniMath.CategoryTheory.Presheaf

• Define some standard presheaves
• Definition of the subobject classifier in a presheaf.

Library UniMath.CategoryTheory.ProductCategory

• • Functors
    • Families of functors (family_functor)
    • Projections (pr_functor)
    • Delta functor (delta_functor)
    • Tuple functor (tuple_functor)
  • Equivalence between functors into components and functors into product

Library UniMath.CategoryTheory.PseudoElements

• Pseudo elements
  • Contents
  • Introduction
  • Definition of pseudo elements
    • Pseudo fiber
  • Basics of pseudo elements
  • Pseudo element criterias
    • Zero criteria
    • isMonic criteria
    • isEpi criteria
    • isExact criteria
    • Difference criteria
      • Data for Difference
      • Difference criteria
    • Pullback using pseudo elements

Library UniMath.CategoryTheory.Quotobjects

• Quotobjects
• Definition of quotient objects

Library UniMath.CategoryTheory.RightKanExtension

• Definition of global right Kan extension as right adjoint to precomposition
• Construction of right Kan extensions when the target category has limits

Library UniMath.CategoryTheory.SetValuedFunctors

Library UniMath.CategoryTheory.ShortExactSequences

• Short exact sequences
  • Contents
• Introduction
• Definition of short exact sequences
  • Transform isExact to isExact' and isExact' to isExact
  • Short Short Exact
  • Remark
  • LeftShortExact
  • RightShortExact
  • ShortExact
• ShortShortExact criteria
  • ShortShortExact implies isCoequalizer.
  • From isCokernel to ShortShortExact
• Correspondence of shortexact in A an A^op
• LeftShortExact and RightShortExact from a ShortShortExact with extra properties
• Correspondence between ShortShortExact and ShortExact
  • Construction of ShortExact from ShortShortExact
  • ShortShortExact from data of ShortExact
• ShortShortExact from isKernel and isCokernel
  • Introduction
• LeftShortExact (resp. RightShortExact) construction for derived functors
  • Introduction
  • LeftShortExact containing an equalizer
  • RightShortExact containing a coequalizer

Library UniMath.CategoryTheory.SimplicialSets

• Homotopy theory of simplicial sets.

Library UniMath.CategoryTheory.SplitMonicsAndEpis

• Split monics, split epis
  • Contents
  • Split monomorphisms

Library UniMath.CategoryTheory.Subobjects

• Definition of the category of subobjects (monos) of c
• Definition of subobjects as equivalence classes of monos

Library UniMath.CategoryTheory.UnderCategories

• Morphism of tips induces a functor

Library UniMath.CategoryTheory.UnitorsAndAssociatorsForEndofunctors

Library UniMath.CategoryTheory.YonedaBinproducts

Library UniMath.CategoryTheory.YonedaExponentials

Library UniMath.CategoryTheory.ZigZag

Library UniMath.CategoryTheory.category_binops

• • Equivalence between isomorphisms and binopisos

Library UniMath.CategoryTheory.catiso

• Isomorphism of (pre)categories
• Construction of a map (catiso A B) -> (A = B)

Library UniMath.CategoryTheory.coslicecat

• Coslice categories
  • Contents:
• Definition of coslice categories
  • Isos in coslice categories

Library UniMath.CategoryTheory.covyoneda

• Covariant Yoneda functor
  • On objects
  • On morphisms
  • Functorial properties of the yoneda assignments
  • covyoneda lemma: natural transformations from covyoneda C c to F
  • The covyoneda embedding is fully faithful

Library UniMath.CategoryTheory.elems_slice_equiv

• Proof that PreShv ∫P ≃ PreShv C / P
  • Construction of the functor from PreShv ∫P to PreShv C / P
  • Construction of the functor from PreShv C / P to PreShv ∫P
  • Construction of the natural isomorphism from (slice_to_PreShv ∙ PreShv_to_slice) to the identity functor
  • Construction of the natural isomorphism from the identity functor to (PreShv_to_slice ∙ slice_to_PreShv)
  • The equivalence of the categories PreShv ∫P and PreShv C / P

Library UniMath.CategoryTheory.exponentials

• 1. Definition of exponentials
• 2. Accessors
• 3. Preservation
• Preservation of exponentials by functors
• 4. Transport along an adjoint equivalence
• 5. Exponentials are independent of the choice of the binary products

Library UniMath.CategoryTheory.opp_precat

• The opposite precategory of a precategory
• The opposite functor

Library UniMath.CategoryTheory.precomp_ess_surj

• Lengthy preparation for the main result of this file
  • Section variables
  • Specification of preimage G of a functor F
    • G on objects
    • Preparation for G on morphisms
    • G on morphisms
  • G is the preimage of F under _ O H
• Precomposition with an ess. surj. and f. f. functor is ess. surj.

Library UniMath.CategoryTheory.precomp_fully_faithful

• Precomposition with an essentially surjective functor is faithful.
• Precomposition with an essentially surjective and full functor is full
• Precomposition with an essentially surjective and full functor is fully faithful

Library UniMath.CategoryTheory.slicecat

• Definition of slice categories
  • Isos in slice categories
  • Monics in slice categories
  • Epis in slice categories
• Proof that C/x is a univalent_category if C is.
• A morphism x --> y in the base category induces a functor between C/x and C/y
• Colimits in slice categories
• Moving between Binary products in slice categories and Pullbacks in base category
• Binary coproducts in slice categories of categories with binary coproducts
• Coproducts in slice categories of categories with coproducts
  • Pullbacks

Library UniMath.CategoryTheory.whiskering

• Whiskering
  • Contents :
• Whiskering: Composition of a natural transformation with a functor

Library UniMath.CategoryTheory.yoneda

• Yoneda functor
  • On objects
  • On morphisms
  • Functorial properties of the yoneda assignments
  • Yoneda lemma: natural transformations from yoneda C c to F
  • The Yoneda embedding is fully faithful

Library UniMath.CategoryTheory.Actegories.Actegories

Library UniMath.CategoryTheory.Actegories.ActionBasedStrongMonads

Library UniMath.CategoryTheory.Actegories.ConstructionOfActegories

Library UniMath.CategoryTheory.Actegories.ConstructionOfActegoryMorphisms

Library UniMath.CategoryTheory.Actegories.CoproductsInActegories

Library UniMath.CategoryTheory.Actegories.MorphismsOfActegories

Library UniMath.CategoryTheory.Actegories.ProductActegory

Library UniMath.CategoryTheory.Actegories.ProductsInActegories

Library UniMath.CategoryTheory.Actegories.Examples.ActionOfEndomorphismsInCATElementary

Library UniMath.CategoryTheory.Actegories.Examples.SelfActionInCATElementary

Library UniMath.CategoryTheory.Adjunctions.AdjunctionMonics

Library UniMath.CategoryTheory.Adjunctions.Core

• Adjunctions
• Identity functor is a left adjoint
• Construction of an adjunction from some partial data (Theorem 2 (iv) of Chapter IV.1 of
• Construction of an adjunction from some partial data
• Post-composition with a left adjoint is a left adjoint
• Post-composition with a right adjoint is a right adjoint
• Definition of the maps on hom-types
• Proof that those maps are inverse to each other
• Proof of the equations (naturality squares) of the adjunction
• Adjunction defined from a natural isomorphism on homsets (F A --> B) ≃ (A --> G B)
• Weak equivalence between adjunctions F -| G and natural weqs of homsets (F A --> B) ≃ (A --> G B)
  • Lemmas about adjunctions

Library UniMath.CategoryTheory.Adjunctions.Examples

• • 1. Adjunctions between delta functors and (co)product functors
  • 1.1. The adjunction between the binary delta and product functor
  • 1.2. The adjunction between the general delta and product functor
  • 1.3. The adjunction between the binary coproduct and delta functor
  • 1.4. The adjunction between the general coproduct and delta functor
  • 2. Swapping of arguments in functor categories
  • 3. Adjunctions are closed under natural isomorphism
  • 4. The adjunction between the constant initial and terminal functors

Library UniMath.CategoryTheory.Adjunctions.Restriction

• Restriction of an adjuction to an equivalence
  • Contents
  • Restriction of an adjunction to an equivalence

Library UniMath.CategoryTheory.Arithmetic.NNO

Library UniMath.CategoryTheory.Arithmetic.ParameterizedNNO

• 1. Parameterized NNOs
• 2. Accessors
• 3. Every parameterized NNO is an NNO
• 4. Uniqueness of parameterized NNOs
• 5. Preservation of parameterized NNOs
• 6. Examples of functors that preserve parameterized NNOs
• 7. Independence of the choice of binary products

Library UniMath.CategoryTheory.Categories.AbelianGroup

• 1. The univalent category of abelian groups
• 2. The additive structure
  • 2.1. The abelian group structure on homsets
  • 2.2. The preadditive structure
  • 2.3. The zero object
  • 2.4. Direct sums
  • 2.5. The additive structure
• 3. Kernels and Cokernels
  • 3.1. Kernels
    • Composition Kernel f --> X --> Y is the zero arrow
    • KernelIn morphism
    • Kernels
  • 3.2. Cokernels
    • Subgroup gives an equivalence relation.
    • Construction of the quotient abelian group Y/(Im f)
    • The canonical morphism Y --> Y/(Im f)
    • CokernelOut
    • Cokernels
• 4. Monics are inclusions and Epis are surjections
  • 4.1. Epis are surjections
  • 4.2. Monics are inclusions
• 5. Monics are kernels of their cokernels and epis are cokernels of their kernels
  • 5.1. Monics are Kernels
  • 5.2. Epis are Cokernels
• 6. The category of abelian groups is an abelian category
• 7. An elementwise criterion for isKernel

Library UniMath.CategoryTheory.Categories.AbelianMonoid

• 1. The univalent category of abelian monoids

Library UniMath.CategoryTheory.Categories.CGraph

• Category of correspondence graphs
  • Precategory of precgraphs.
  • Category of cgraphs.
  • Forgetful functor.

Library UniMath.CategoryTheory.Categories.CartesianCubicalSets

Library UniMath.CategoryTheory.Categories.CatIsoInserter

Library UniMath.CategoryTheory.Categories.CategoryOfSetCategories

• 1. The category of strict categories
• 2. Isomorphisms of strict categories
• 3. The univalence of the category of strict categories

Library UniMath.CategoryTheory.Categories.CategoryOfSetGroupoids

• 1. Groupoids whose objects form a set
• 2. The category of setgroupoids
• 3. Isomorphisms
• 4. The univalent category of setgroupoids

Library UniMath.CategoryTheory.Categories.CoEilenbergMoore

Library UniMath.CategoryTheory.Categories.Commrig

• Category of commrigs
  • Contents
• Precategory of commrigs
• Category of commrigs
  • (rigiso X Y) ≃ (z_iso X Y)
  • Category of commrigs

Library UniMath.CategoryTheory.Categories.Commring

• Category of commrings
  • Contents
• Category of commrings
• Category of commrings
  • (ringiso X Y) ≃ (z_iso X Y)
  • Category of commrings

Library UniMath.CategoryTheory.Categories.Dialgebras

Library UniMath.CategoryTheory.Categories.EilenbergMoore

Library UniMath.CategoryTheory.Categories.FinSet

• The category of finite sets
  • Contents:
  • The univalent category FinSet of finite sets/types
  • (Co)limits
    • Colimits
      • Binary coproducts
    • Limits
      • Binary products

Library UniMath.CategoryTheory.Categories.Fld

• Category of flds
  • Contents
• Precategory of flds
• Category of flds
  • (rigiso X Y) ≃ (z_iso X Y)
  • Category of flds

Library UniMath.CategoryTheory.Categories.Graph

• Bicategory of graphs
  • Precategory of pregraphs.
  • Category of graphs.

Library UniMath.CategoryTheory.Categories.Group

• 1. The univalent category of groups

Library UniMath.CategoryTheory.Categories.Intdom

• Category of intdoms
  • Contents
• Precategory of intdoms
• Category of intdoms
  • (rigiso X Y) ≃ (iso X Y)
  • Category of intdoms

Library UniMath.CategoryTheory.Categories.KleisliCategory

Library UniMath.CategoryTheory.Categories.Magma

• 1. The category of magmas
  • 1.1. Magmas
  • 1.2. Magma morphisms
• 2. The category of abelian magmas
• 3. The category of semigroups
• 4. The category of unital magmas
• 5. The category of monoids
• 6. The category of abelian monoids
• 7. The category of groups
• 8. The category of abelian groups

Library UniMath.CategoryTheory.Categories.Module

• 1. Univalence
• 2. The zero object

Library UniMath.CategoryTheory.Categories.ModuleCore

• 1. The category of R-modules

Library UniMath.CategoryTheory.Categories.Monoid

• 1. The univalent category of monoids
• 2. The free and forgetful functors
  • 2.1. The Forgetful functor
  • 2.2. The Free functor
  • 2.3. The adjunction

Library UniMath.CategoryTheory.Categories.MonoidToCategory

• 1. The functor from monoids to categories
  • 1.2. Fully faithful
• 2. The equivalence between presheaves and monoid actions

Library UniMath.CategoryTheory.Categories.PrecategoryOfCategories

Library UniMath.CategoryTheory.Categories.Quotient

• 1. Definition of a congruence relation mor_cong_rel C on a category C
• 2. Definition of the quotient category mor_quot_category

Library UniMath.CategoryTheory.Categories.Rel

Library UniMath.CategoryTheory.Categories.Rig

• Rigs category
  • Contents
• Precategory of rigs
• Category of rigs
  • (rigiso X Y) ≃ (iso X Y)
  • Category of rigs

Library UniMath.CategoryTheory.Categories.Ring

• Rings category
  • Contents
• Precategory of rings
• Category of rings
  • (ringiso X Y) ≃ (z_iso X Y)
  • Category of rings

Library UniMath.CategoryTheory.Categories.SetWith2BinOp

• Category of setswith2binops
  • Contents
• Precategory of setwith2binops
• Category of setwith2binops
  • (twobinopiso X Y) ≃ (iso X Y)
  • Category of setwith2binops

Library UniMath.CategoryTheory.Categories.StandardCategories

• Standard categories
  • Contents:
  • The path/fundamental groupoid of a type
    • Characterization of discrete categories
  • The discrete univalent_category on n objects (cat_n)
  • The category with one object (unit_category)
  • The category with no objects (empty_category)

Library UniMath.CategoryTheory.Categories.Woset

• The category of well-ordered sets with order preserving morphisms
• The category of well-ordered sets with arbitrary functions as morphisms

Library UniMath.CategoryTheory.Categories.HSET.All

Library UniMath.CategoryTheory.Categories.HSET.Colimits

• Colimits in HSET
  • Contents
  • General colimits ColimsHSET
  • Binary coproducs BinCoproductsHSET
  • General indexed coproducs CoproductsHSET
    • Binary coproducts from colimits BinCoproductsHSET_from_Colims
    • Pushouts from colimits PushoutsHSET_from_Colims
  • Initial object InitialHSET
    • Initial object from colimits InitialHSET_from_Colims

Library UniMath.CategoryTheory.Categories.HSET.Core

• Category of hSets
  • Contents:
  • Category HSET of hSets (hset_category)
  • Some particular HSETs

Library UniMath.CategoryTheory.Categories.HSET.FilteredColimits

• Filtered Colimits of Sets.

Library UniMath.CategoryTheory.Categories.HSET.Limits

• Limits in HSET
  • Contents
  • General limits
    • Alternate definition using cats/limits
  • Binary products (BinProductsHSET)
    • Binary products from limits (BinProductsHSET_from_Lims)
  • General indexed products (ProductsHSET)
  • Terminal object TerminalHSET
    • Terminal object from general limits TerminalHSET_from_Lims
  • Pullbacks PullbacksHSET
• Elements of pullbacks of sets
  • • Pullbacks from general limits PullbacksHSET_from_Lims
    • Pullbacks of arrows from unit as inverse images
  • Equalizers from general limits EqualizersHSET_from_Lims

Library UniMath.CategoryTheory.Categories.HSET.MonoEpiIso

• Characterizations of monos, epis, and isos in HSET
  • Contents
  • Points as global elements
  • Monomorphisms are exactly injective functions MonosAreInjective_HSET
  • Epimorphisms are exactly surjective functions EpisAreSurjective_HSET
  • Equivalence between isomorphisms and weak equivalences of two hSets.

Library UniMath.CategoryTheory.Categories.HSET.SetCoends

• 1. Coends of profunctors
• 2. Accessors for coends of profunctors

Library UniMath.CategoryTheory.Categories.HSET.Slice

• Slices of HSET
  • Contents
  • Locally cartesian closed structure
    • Terminal object (Terminal_HSET_slice)
    • Binary products (BinProducts_HSET_slice)
    • General indexed products (Products_HSET_slice)
    • Exponentials (Exponentials_HSET_slice)
  • Colimits
    • Binary coproducts (BinCoproducts_HSET_slice)
  • The forgetful functor HSET/X --> HSET is a left adjoint

Library UniMath.CategoryTheory.Categories.HSET.SliceFamEquiv

Library UniMath.CategoryTheory.Categories.HSET.Structures

• Other structures in HSET
  • Contents
  • Natural numbers object (NNO_HSET)
  • Exponentials (Exponentials_HSET)
  • Construction of exponentials for functors into HSET
  • Kernel pairs (kernel_pair_HSET)
  • Effective epis (EffectiveEpis_HSET)
  • Split epis with axiom of choice (SplitEpis_HSET)
  • Forgetful functor to type_precat
  • Subobject classifier

Library UniMath.CategoryTheory.Categories.HSET.Univalence

• HSET is a univalent_category (is_univalent_HSET)
  • HSET is a univalent_category.

Library UniMath.CategoryTheory.Categories.KaroubiEnvelope.Core

• 1. The definition of a karoubi envelope
• 2. Functors on C are equivalent to functors on the setcategory Karoubi envelope

Library UniMath.CategoryTheory.Categories.KaroubiEnvelope.RezkCompletion

• 1. The packaging of the Rezk completion

Library UniMath.CategoryTheory.Categories.KaroubiEnvelope.SetKaroubi

• 1. The setcategory Karoubi envelope and its embedding of C
  • 1.1. The objects and morphisms and their constructors and accessors
  • 1.2. The category
  • 1.3. The embedding
  • 1.4. Every idempotent in the setcategory karoubi envelope splits
  • 1.5. Every object of the setcategory karoubi envelope is a retract of an element of C
  • 1.6. The bundling of the above into a term of set_karoubi_envelope
• 3. The alternative definition, using the presheaf category
  • 3.1. The equivalence between the two definitions
• 4. The formations of the opposite category and the Karoubi envelope commute
• 5. The Karoubi envelope construction gives a monad on the category of setcategories

Library UniMath.CategoryTheory.Categories.KaroubiEnvelope.UnivalentKaroubi

• 1. The univalent Karoubi envelope
  • 1.1. The category
  • 1.2. The fully faithful embedding
  • 1.3. Every idempotent in the karoubi envelope splits
  • 1.4. Every object of the karoubi envelope is a retract of an element of C
  • 1.5. The bundling of the above into a term of univalent_karoubi_envelope
  • 1.6. Another proof of the splitting

Library UniMath.CategoryTheory.Categories.PreorderCategory.Core

• 1. The category over a preorder
• 2. Univalence

Library UniMath.CategoryTheory.Categories.PreorderCategory.Sieves

• 1. The equivalence
  • 1.1. The construction of a subtype from a sieve
  • 1.2. The construction of a sieve from a subtype
  • 1.3. The construction of a sieve from a sieve yields the same sieve again
  • 1.4. The construction of a subtype from a subtype yields the same subtype again

Library UniMath.CategoryTheory.Categories.Type.Colimits

• Colimits in the precategory of types
  • Contents:
  • Initial object (InitialType)

Library UniMath.CategoryTheory.Categories.Type.Core

• The precategory of types
  • Contents:
  • The precategory of types of a fixed universe
  • Hom functors
  • As a bifunctor hom_functor
  • Covariant cov_hom_functor
  • Contravariant contra_hom_functor

Library UniMath.CategoryTheory.Categories.Type.Limits

• Limits in the precategory of types
  • Contents:
  • Terminal object (TerminalType)

Library UniMath.CategoryTheory.Categories.Type.MonoEpiIso

• Characterizations of monos, epis, and isos in type_precat
  • Contents
  • Injective functions are monic InjectivesAreMonic_type

Library UniMath.CategoryTheory.Categories.Type.NoHomsets

Library UniMath.CategoryTheory.Categories.Type.Structures

• Other structures in type_precat
  • Contents
  • Exponentials
    • Exponential functor

Library UniMath.CategoryTheory.Categories.Type.Univalence

• Near-univalence of type_precat

Library UniMath.CategoryTheory.Categories.Universal_Algebra.Algebras

• The univalent category of algebras over a signature.

Library UniMath.CategoryTheory.Categories.Universal_Algebra.EqAlgebras

• The univalent category of equational algebras over an equational specification.

Library UniMath.CategoryTheory.Chains.Adamek

• Adámek's theorem
• Adámek's theorem for constructing initial algebras of omega-cocontinuous functors

Library UniMath.CategoryTheory.Chains.All

Library UniMath.CategoryTheory.Chains.Chains

• Chains
  • Definition of (ω-)cocontinuous functors

Library UniMath.CategoryTheory.Chains.CoAdamek

• Adámek's theorem

Library UniMath.CategoryTheory.Chains.Cochains

• Cochains
  • Definition of (ω-)continuous functors

Library UniMath.CategoryTheory.Chains.OmegaCocontFunctors

• ω-cocontinuous functors
• Examples of (omega) cocontinuous functors
  • Left adjoints preserve colimits
  • The identity functor is (omega) cocontinuous
  • The constant functor is omega cocontinuous
  • Functor composition preserves omega cocontinuity
  • Functor iteration preserves (omega)-cocontinuity
  • A pair of functors (F,G) : A * B -> C * D is omega cocontinuous if F and G are
  • A functor F : A -> product_category I B is (omega-)cocontinuous if each F_i : A -> B_i is
  • A family of functor F^I : A^I -> B^I is omega cocontinuous if each F_i is
  • The bindelta functor C -> C^2 mapping x to (x,x) is omega cocontinuous
  • The generalized delta functor C -> C^I is omega cocontinuous
  • The functor "+ : C^2 -> C" is cocontinuous
  • The functor "+ : C^I -> C" is cocontinuous
  • Binary coproduct of functors: F + G : C -> D is omega cocontinuous
  • Coproduct of families of functors: + F_i : C -> D is omega cocontinuous
  • Constant product functors: C -> C, x |-> a * x and x |-> x * a are cocontinuous
  • The functor "* : C^2 -> C" is omega cocontinuous
  • Binary product of functors: F * G : C -> D is omega cocontinuous
  • Direct proof that the precomposition functor is cocontinuous
  • Precomposition functor is cocontinuous using construction of right Kan extensions
• Swapping of functor category arguments
• The forgetful functor from Set/X to Set preserves colimits

Library UniMath.CategoryTheory.Chains.OmegaContFunctors

• ω-cocontinuous functors
  • Right adjoints preserve limits
  • Identity preserves limits
  • Constant functors
  • Composition of omega (continuous) functors
  • Functor iteration preserves (omega)-continuity
  • Binary product of functors: F * G : C -> D is omega continuous
• If a functor is part of an equivalence of categories,
  • Post composition with a right adjoint is continuous
  • Direct proof that the precomposition functor is continuous
  • A pair of functors (F,G) : A * B -> C * D is omega continuous if F and G are
  • A functor F : A -> product_category I B is (omega-)continuous if each F_i : A -> B_i is
• • The functor "+ : C^I -> C" is continuous is equivalently with saying that coproducts commute with limits
  • Coproduct of families of functors: + F_i : C -> D is omega continuous given coproducts in D distribute over limits

Library UniMath.CategoryTheory.Core.Categories

• Categories
  • Contents :
• Definition of a precategory
  • precategory_data
  • Axioms of a precategory

Library UniMath.CategoryTheory.Core.EssentiallyAlgebraic

• • Precategories in style of essentially algebraic cats

Library UniMath.CategoryTheory.Core.Functors

• Functors
  • Contents:
• Functors : Morphisms of precategories
  • Functors preserve isomorphisms
  • Functors and idtoiso
  • Functors preserve inverses
  • Conservative functors
  • Composition of functors, identity functors
    • Composition
    • Identity functor
    • Constant functor
  • Fully faithful functors
    • Fully faithful functors reflect isos
  • (Split) essentially surjective functors
  • Faithful functors
  • Full functors
  • Fully faithful is the same as full and faithful
  • Image on objects of a functor

Library UniMath.CategoryTheory.Core.Isos

• Isomorphisms
  • Contents
  • Properties of isomorphisms
  • Equivalence relation identifying isomorphic objects
  • Isomorphisms in a category z_iso
  • Properties of 0-isomorphisms

Library UniMath.CategoryTheory.Core.NaturalTransformations

• Natural transformations
  • Contents
  • Definition of natural transformations
  • Identity natural transformation
  • Composition of natural transformations
  • Natural isomorphisms

Library UniMath.CategoryTheory.Core.PosetCat

• 1. Posetal categories
• 2. Every posetal category is a poset
• 3. Every poset is a posetal category
• 4. Equivalence between posetal categories and posets

Library UniMath.CategoryTheory.Core.Prelude

• Prelude for category theory

Library UniMath.CategoryTheory.Core.Setcategories

• Setcategories: Precategories whose objects and morphisms are sets
  • Contents

Library UniMath.CategoryTheory.Core.TransportMorphisms

• Lemmas on transport of morphisms
  • • Transport source and target of a morphism
    • Transport a morphism using funextfun
    • Transport of is_iso
    • Induced precategories

Library UniMath.CategoryTheory.Core.TwoCategories

• 1. Definition of 2-categories
• 2. Accessors for the data
• 4. Projections of the laws
• 5. 2-categories
• 6. Derived laws
• 7. 2-setcategories
• 8. Univalent 2-categories
• 9. Hom-categories

Library UniMath.CategoryTheory.Core.Univalence

• Univalent categories (AKA saturated categories)
  • Contents
  • Univalent categories: idtoiso is an equivalence
  • Definition of isotoid
  • Properties of idtoiso and isotoid

Library UniMath.CategoryTheory.DaggerCategories.CatIso

Library UniMath.CategoryTheory.DaggerCategories.Categories

Library UniMath.CategoryTheory.DaggerCategories.FunctorCategory

Library UniMath.CategoryTheory.DaggerCategories.Functors

Library UniMath.CategoryTheory.DaggerCategories.Transformations

Library UniMath.CategoryTheory.DaggerCategories.Unitary

Library UniMath.CategoryTheory.DaggerCategories.Univalence

Library UniMath.CategoryTheory.DaggerCategories.Examples.Fullsub

Library UniMath.CategoryTheory.DaggerCategories.Examples.Groupoids

Library UniMath.CategoryTheory.DaggerCategories.Examples.Relations

Library UniMath.CategoryTheory.DaggerCategories.Functors.Factorization

Library UniMath.CategoryTheory.DaggerCategories.Functors.FullyFaithful

Library UniMath.CategoryTheory.DaggerCategories.Functors.Precomp

• • • G on objects
    • Preparation for G on morphisms
    • G on morphisms
  • G is the preimage of F under _ O H

Library UniMath.CategoryTheory.DaggerCategories.Functors.WeakEquivalences

Library UniMath.CategoryTheory.DisplayedCats.Adjunctions

• Naturality of homset bijections
• homset_conj_inv and homset_conj' are weak equivalences.
• The right adjoint functor of a displayed adjunction preserves cartesian morphisms.

Library UniMath.CategoryTheory.DisplayedCats.Binproducts

• • analogously for terminal objects

Library UniMath.CategoryTheory.DisplayedCats.CatIsoDisplayed

Library UniMath.CategoryTheory.DisplayedCats.Codomain

• The slice displayed category
  • The displayed codomain
• Cleaving for codomain
• Isos in the codomain
• The univalence

Library UniMath.CategoryTheory.DisplayedCats.ComprehensionC

• Displayed Category from a category with display maps
• Definition of a cartesian displayed functor

Library UniMath.CategoryTheory.DisplayedCats.Constructions

Library UniMath.CategoryTheory.DisplayedCats.Core

• Displayed categories
  • Definition
  • Utility lemmas
• Functors

Library UniMath.CategoryTheory.DisplayedCats.DisplayMapCat

• Display Map Category
  • Display Map
  • Display Map Category
    • Proofs about isomorphisms
    • Bit of univalence
  • Inclusion Functor
  • Functor between Display Map Classes
  • Functor between Display Map Categories
    • Define how functor `F` acts on the Display Map Category
  • Natural Transformation
  • Corresponding Comprehension Category
  • Pseudo Map corresponding to a functor between Display Map Categories
  • Transformation corresponding to a natural transformation between functors between display map categories

Library UniMath.CategoryTheory.DisplayedCats.DisplayedCatEq

Library UniMath.CategoryTheory.DisplayedCats.DisplayedFunctorEq

Library UniMath.CategoryTheory.DisplayedCats.EquivalenceOverId

• 8. Equivalences over the identity and equivalences

Library UniMath.CategoryTheory.DisplayedCats.Equivalences

• • Contents:
• General definition of displayed adjunctions and equivalences
  • Lemmas on the triangle identities
• Constructions on and of displayed equivalences
  • Full + faithful + ess split => equivalence
    • Utility lemmas from fullness+faithfulness
• Displayed equivalences and adjunctions over identity
  • Adjunctions
  • Displayed equivalences over id (adjoint and quasi)
  • Lemmas on the triangle identities
• Constructions on and of displayed equivalences over identity
  • Full + faithful + ess split => equivalence
    • Utility lemmas from fullness+faithfulness
    • Converse functor
  • Inverses and composition of adjunctions/equivalences
  • Induced adjunctions/equivalences of fiber precats

Library UniMath.CategoryTheory.DisplayedCats.Examples

• Examples
• Displayed category of groups
  • The displayed arrow category
  • Objects with N-action
  • Elements of sets

Library UniMath.CategoryTheory.DisplayedCats.Fiber

• Fiber categories
  • Univalence
  • Fiber functors

Library UniMath.CategoryTheory.DisplayedCats.Fibrations

• Isofibrations
• Fibrations
  • (Cloven) fibration
  • Weak fibration
  • Connection with isofibrations
  • Uniqueness of cartesian lifts
  • Functor from discrete fibrations to presheaves
    • Functor on objects
    • Functor on morphisms
    • Functor properties
  • Functor from presheaves to discrete fibrations
    • Functor on objects
    • Functor on morphisms
    • Functor properties
• Split fibrations

Library UniMath.CategoryTheory.DisplayedCats.FullyFaithfulDispFunctor

• 1. Fully faithful displayed functors reflect isomorphisms
• 2. The identity is fully faithful

Library UniMath.CategoryTheory.DisplayedCats.FunctorCategory

• Functor category as a displayed category
  • Base category.
  • Step 1
  • Step 2
  • Step 3
  • Step 4

Library UniMath.CategoryTheory.DisplayedCats.Functors

• • Functors over functors between bases
  • Composite and identity functors.
  • Action of functors on z_isos.
  • Properties of functors

Library UniMath.CategoryTheory.DisplayedCats.Isos

• • Isomorphisms (and lemmas)
  • More utility lemmas

Library UniMath.CategoryTheory.DisplayedCats.Limits

Library UniMath.CategoryTheory.DisplayedCats.NaturalTransformations

• • Displayed Natural Transformations

Library UniMath.CategoryTheory.DisplayedCats.PreservesCleaving

• 1. Preservation of cleavings
• 2. Examples of functors that preserve cleavings

Library UniMath.CategoryTheory.DisplayedCats.Projection

Library UniMath.CategoryTheory.DisplayedCats.ReindexingForward

Library UniMath.CategoryTheory.DisplayedCats.SIP

• The Structure Identity Principle
• The Structure Identity Principle
  • The data and properties according to HoTT book, chapter 9.8
  • A displayed precategory from the data
  • Displayed category from SIP data is univalent
  • The conclusion of SIP: total category is univalent

Library UniMath.CategoryTheory.DisplayedCats.StreetFibration

Library UniMath.CategoryTheory.DisplayedCats.StreetOpFibration

Library UniMath.CategoryTheory.DisplayedCats.Total

• Total Categories and Total Functors
  • Definition and forgetful functor
  • Isomorphisms and saturation
  • idtoiso in the total category
  • Total functors of displayed functors

Library UniMath.CategoryTheory.DisplayedCats.TotalAdjunction

Library UniMath.CategoryTheory.DisplayedCats.TotalCategoryFacts

Library UniMath.CategoryTheory.DisplayedCats.Univalence

• • Saturation: displayed univalent categories

Library UniMath.CategoryTheory.DisplayedCats.Codomain.CodColimits

• 1. Initial object in the slice
• 2. Binary coproducts in the slice
• 3. Coequalizers in the slice

Library UniMath.CategoryTheory.DisplayedCats.Codomain.CodDomain

• 1. The domain functor
• 2. The domain functor is a left adjoint

Library UniMath.CategoryTheory.DisplayedCats.Codomain.CodFunctor

• 1. Displayed functor between codomain displayed categories
• 2. Displayed natural transformation between codomain displayed categories
• 3. Cartesianness of the displayed functor
• 4. Preservation of limits
• 5. Preservation of colimits
• 6. Naturality for the slice of terminal objects

Library UniMath.CategoryTheory.DisplayedCats.Codomain.CodLeftAdjoint

• 1. The left adjoint
• 2. The unit
• 3. The counit
• 4. The triangle equalities
• 5. The adjunction
• 6. The Beck-Chevalley condition
• 7. Dependent sums for the codomain

Library UniMath.CategoryTheory.DisplayedCats.Codomain.CodLimits

• 1. Preservation of limits by substitution
• 2. Fiberwise terminal objects
• 3. Fiberwise binary products
• 4. Fiberwise equalizers

Library UniMath.CategoryTheory.DisplayedCats.Codomain.CodMorphisms

Library UniMath.CategoryTheory.DisplayedCats.Codomain.CodNNO

• 1. Basic definitions
• 2. The universal mapping property
• 3. Parameterized natural numbers object in the slice category
• 4. Stability under substitution
• 5. Preservation by the pseudofunctoriality of the arrow category

Library UniMath.CategoryTheory.DisplayedCats.Codomain.CodRegular

• 1. Regular epimorphisms in the slice category
• 2. Regular categories are closed under slicing
• 3. Preservation of regular epimorphisms by the pullback functor
• 4. Preservation of regular epimorphisms by the codomain functor
• 5. Exactness of the slice category

Library UniMath.CategoryTheory.DisplayedCats.Codomain.CodRightAdjoint

• 1. The Beck-Chevalley condition
• 2. Dependent products in a locally cartesian closed category

Library UniMath.CategoryTheory.DisplayedCats.Codomain.CodSubobjectClassifier

• 1. The universal property
• 2. The subobject classifier
• 3. Preservation of subobject classifiers by the pullback functor
• 4. The functor on the arrow category preserves subobject classifiers

Library UniMath.CategoryTheory.DisplayedCats.Codomain.ColimitProperties

• 1. Strict initial objects in the slice category
• 2. Disjoint binary coproducts in the slice
• 3. Stable binary coproducts in the slice
• 4. Preservation of colimits by the arrow functor

Library UniMath.CategoryTheory.DisplayedCats.Codomain.FiberCod

• 1. Accessors for the fiber of the codomain
• 2. Builders for the fiber of the codomain
• 3. Standard objects and morphisms in the codomain
• 4. Calculations for codomain fiber
• 5. The fiber of terminal objects

Library UniMath.CategoryTheory.DisplayedCats.Codomain.IteratedSlice

• 1. Iterated slice categories
• 2. Pullbacks in iterated slice categories
• 3. Preservation of colimits by pullback in the iterated slice

Library UniMath.CategoryTheory.DisplayedCats.Constructions.CategoryWithStructure

• 1. Displayed category from structure on objects and compatibility on morphisms

Library UniMath.CategoryTheory.DisplayedCats.Constructions.DisplayedFunctorCat

• 1. The displayed functor category
• 2. The characterization of displayed isomorphisms

Library UniMath.CategoryTheory.DisplayedCats.Constructions.DisplayedSections

• 1. Displayed sections and their accessors
• 2. Displayed natural transformations and their accessors
• 3. The category

Library UniMath.CategoryTheory.DisplayedCats.Constructions.FullSubcategory

• 1. The construction of the full subcategory as a displayed category
• 2. Univalence
• 3. Shortcuts for just the resulting total category
• 4. The truncation functor

Library UniMath.CategoryTheory.DisplayedCats.Constructions.FunctorLift

• 1. The construction of functors via lifting
• 2. The special case where F is the identity
  • 2.1. The construction of a section from a displayed section
  • 2.2. The construction of a natural transformation from a morphism
  • 2.3. The functor from displayed sections to the functor category

Library UniMath.CategoryTheory.DisplayedCats.Constructions.Product

• 1. The product displayed category
• Products of displayed (pre)categories
• 2. A characterization of displayed isomorphism
• 3. Univalence
• 4. The projecton displayed functors

Library UniMath.CategoryTheory.DisplayedCats.Examples.AlgebraStructures

Library UniMath.CategoryTheory.DisplayedCats.Examples.Arrow

Library UniMath.CategoryTheory.DisplayedCats.Examples.Cartesian

• 1. One can consider any category as a displayed category over the unit category
  • 1.1. Univalence of the category over the unit category
• 2. The cartesian product as a displayed category over the first component
  • 2.1 The cartesian product creates limits
• 3. The arrow category
• 4. A direct definition of the product category as a displayed category
• 4.1. This cartesian has limits as well

Library UniMath.CategoryTheory.DisplayedCats.Examples.CategoryOfPosets

Library UniMath.CategoryTheory.DisplayedCats.Examples.DCPOStructures

Library UniMath.CategoryTheory.DisplayedCats.Examples.DispFunctorPair

• 1. The maps back and forth
• 2. The equivalence

Library UniMath.CategoryTheory.DisplayedCats.Examples.HValuedPredicates

• 1. The displayed category of H-valued predicates
• 2. Properties of this displayed category
• 3. The hyperdoctrine of H-valued predicates
• 4. Logic of H-valued predicates
• 4.1. Fiberwise terminal object
• 4.2. Fiberwise initial object
• 4.3. Fiberwise binary products
• 4.4. Fiberwise binary coproducts
• 4.5. Fiberwise exponentials
• 4.6. Dependent products
• 4.7. Dependent sums
• 5. The first-order hyperdoctrine of H-valued predicates
• 6. Comprehension category of H-valued predicates
• 7. The tripos of H-valued predicates
• 8. The comprehension category of H-valued predicates is not necessarily full

Library UniMath.CategoryTheory.DisplayedCats.Examples.MonadAlgebras

Library UniMath.CategoryTheory.DisplayedCats.Examples.MonoCodomain

• 1. The displayed category of monomorphisms
• 2. Pullback squares are cartesian
• 3. Cleaving for codomain of monomorphisms
• 4. Isos in the codomain
• 5. The univalence
• 6. Accessors for monomorphisms

Library UniMath.CategoryTheory.DisplayedCats.Examples.Opposite

Library UniMath.CategoryTheory.DisplayedCats.Examples.PointedDCPOStrict

Library UniMath.CategoryTheory.DisplayedCats.Examples.PointedDCPOStructures

Library UniMath.CategoryTheory.DisplayedCats.Examples.PointedPosetStrict

Library UniMath.CategoryTheory.DisplayedCats.Examples.PointedPosetStructures

Library UniMath.CategoryTheory.DisplayedCats.Examples.PointedSetStructures

Library UniMath.CategoryTheory.DisplayedCats.Examples.PosetStructures

Library UniMath.CategoryTheory.DisplayedCats.Examples.Reindexing

• • Reindexing
  • A functor of displayed categories from reindexing

Library UniMath.CategoryTheory.DisplayedCats.Examples.SetGroupoidComprehension

• 1. The total category of an isofibration
• 2. The comprehension functor
• 3. Some transport lemmas that we need
• 4. The comprehension functor is Cartesian
• 5. Comprehension for split isofibrations

Library UniMath.CategoryTheory.DisplayedCats.Examples.SetGroupoidsIsoFib

• 1. Displayed categories that represent setgroupoids
• 2. Properties of displayed setgroupoids
• 3. The data of the displayed category of displayed setgroupoids
• 4. Transport lemmas
• 5. Verification of the axioms
• 6. This displayed category is univalent
  • 6.1. Isos of displayed setgroupoids
  • 6.2. Proof of univalence
• 7. The displayed category of isofibrations
• 8. A cleaving for the displayed category of isofibrations
• 9. The displayed category of split isofibrations
• 10. A cleaving for the displayed category of split isofibrations

Library UniMath.CategoryTheory.DisplayedCats.Examples.SetStructures

Library UniMath.CategoryTheory.DisplayedCats.Examples.Sigma

• Sigmas of displayed (pre)categories
  • Transport and isomorphism lemmas
  • Univalence
    • Characterization of the isos of sigma_disp_cat
    • The univalence proof

Library UniMath.CategoryTheory.DisplayedCats.Examples.StrictTwoSidedDispCat

• 1. The data of the displayed category of 2-sided displayed categories
• 2. Transport lemmas for this displayed category
• 3. The laws
• 4. The displayed category of strict 2-sided displayed categories
• 5. The proof that it is univalent
  • 5.1. Characterization of the isomorphisms
  • 5.2. The actual proof of univalence

Library UniMath.CategoryTheory.DisplayedCats.Examples.Three

Library UniMath.CategoryTheory.DisplayedCats.Examples.UnitalBinop

Library UniMath.CategoryTheory.DisplayedCats.Fiberwise.DependentProducts

• 1. The Beck-Chevalley condition for right adjoints
• 2. Dependent products
• 3. Accessors for dependent products
• 4. Preservation of dependent products by functors between fibrations
• 5. Examples of functors that preserve dependent products

Library UniMath.CategoryTheory.DisplayedCats.Fiberwise.DependentSums

• 1. The natural transformation from the left Beck-Chevalley condition
• 2. Fibrations with dependent sums
• 3. Accessors for dependent sums
• 4. Preservation of dependent sums by functors between fibrations

Library UniMath.CategoryTheory.DisplayedCats.Fiberwise.DualBeckChevalley

Library UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseCartesianClosed

• 1. Fiberwise exponentials
• 2, Accessors
• 3. Specialized builder for fibrations that land in posets
• 4. Distributivity of products and coproducts

Library UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseCoproducts

• 1. Fiberwise products
• 2. Preservation of fiberwise coproducts

Library UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseEqualizers

• 1. Fiberwise products
• 2. Preservation of fiberwise equalizers

Library UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseInitial

• 1. Fiberwise initial objects
• 2. Preservation of fiberwise initial objects

Library UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseProducts

• 1. Fiberwise products
• 2. Preservation of fiberwise products

Library UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseSubobjectClassifier

• 1. Fiberwise subobject classifiers
• 2. Preservation of fiberwise subobject classifiers

Library UniMath.CategoryTheory.DisplayedCats.Fiberwise.FiberwiseTerminal

• 1. Fiberwise terminal objects
• 2. Right adjoint from fiberwise terminal objects
• 3. Preservation of fiberwise terminal objects

Library UniMath.CategoryTheory.DisplayedCats.MonoCodomain.FiberMonoCod

• 1. Accessors for the fiber of the codomain of monomorphisms
• 2. Builders for the fiber of the codomain of monomorphisms
• 3. Standard objects and morphisms in the codomain of monomorphisms

Library UniMath.CategoryTheory.DisplayedCats.MonoCodomain.Inclusion

• 1. The displayed functor
• 2. The fiber functor
• 3. From the slice category to the slice category of monomorphisms

Library UniMath.CategoryTheory.DisplayedCats.MonoCodomain.MonoCodColimits

• 1. Initial object in the slice of monomorphisms
• 2. Binary coproducts in the slice of monomorphisms

Library UniMath.CategoryTheory.DisplayedCats.MonoCodomain.MonoCodFunctor

• 1. Displayed functor between displayed categories of monomorphisms
• 2. Conditions for which this functor is a weak equivalence
• 3. Properties of the fiber functor

Library UniMath.CategoryTheory.DisplayedCats.MonoCodomain.MonoCodLeftAdjoint

• 1. Interpretation of the existential quantifier
• 2. Stability

Library UniMath.CategoryTheory.DisplayedCats.MonoCodomain.MonoCodLimits

• 1. Fiberwise terminal objects
• 2. Fiberwise binary products

Library UniMath.CategoryTheory.DisplayedCats.MonoCodomain.MonoCodRightAdjoint

• 1. Preservation of monomorphisms by dependent products
• 2. Rules for universal quantification
• 3. Stability under substitution for the universal quantifier
• 4. The universal quantifier
• 5. Introduction/elimination rules for the implication
• 6. Stability under substitution for the implication
• 7. The implication

Library UniMath.CategoryTheory.DisplayedCats.MonoCodomain.MonoHyperdoctrine

• 1. The preorder hyperdoctrine of monomorphisms in a category
• 2. The hyperdoctrine of monomorphisms in a univalent category

Library UniMath.CategoryTheory.DisplayedCats.MoreFibrations.CartesiannessOfComposites

Library UniMath.CategoryTheory.DisplayedCats.MoreFibrations.DispCatsEquivFunctors

Library UniMath.CategoryTheory.DisplayedCats.MoreFibrations.DisplayedDisplayedCats

Library UniMath.CategoryTheory.DisplayedCats.MoreFibrations.FibrationsCharacterisation

Library UniMath.CategoryTheory.DisplayedCats.MoreFibrations.Prefibrations

• Prefibrations

Library UniMath.CategoryTheory.DisplayedCats.Structures.CartesianStructure

Library UniMath.CategoryTheory.DisplayedCats.Structures.StructureLimitsAndColimits

Library UniMath.CategoryTheory.DisplayedCats.Structures.StructuresSmashProduct

Library UniMath.CategoryTheory.EnrichedCats.BenabouCosmos

• 1. Benabou cosmos
• 2. Accessors
• 3. Quantales

Library UniMath.CategoryTheory.EnrichedCats.EnrichedRelation

• 1. Enriched relations
• 2. Identity and composition of enriched relations
• 3. Order on enriched relations
• 4. Squares of enriched relations
• 5. Associators and unitors
• 6. Identity squares
• 7. Composition of squares
• 8. Converses of enriched relations
• 9. Companion pairs of enriched relations
• 10. Conjoints of enriched relations
• 11. Calculational lemmas
• 12. Basic properties of the order of enriched relations

Library UniMath.CategoryTheory.EnrichedCats.Enrichment

Library UniMath.CategoryTheory.EnrichedCats.EnrichmentAdjunction

Library UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor

• 1. Functors with enrichments
• 2. Properties for enriched functors
  • 2.1. Fully faithful functors
  • 2.2. Weak equivalences
• 4. The composition of enriched functors
• 5. The constant functor
• 6. Lemmas for pre- and postcomposition

Library UniMath.CategoryTheory.EnrichedCats.EnrichmentMonad

Library UniMath.CategoryTheory.EnrichedCats.EnrichmentTransformation

Library UniMath.CategoryTheory.EnrichedCats.FullyFaithful

• 1. Composition of fully faithful functors
• 2. Fully faithful functors are closed under natural isomorphism
• 3. Factorization of fully faithful functors

Library UniMath.CategoryTheory.EnrichedCats.LaxExtension

• 1. Definition of lax extensions
• 2. Builder and equality
• 3. Functors with a lax extension
• 4. Properties of lax extensions

Library UniMath.CategoryTheory.EnrichedCats.YonedaLemma

• 1. The inverse of the Yoneda embedding
• 2. The strong Yoneda lemma

Library UniMath.CategoryTheory.EnrichedCats.Bifunctors.CurriedBifunctors

• 1. Curried bifunctors
• 2. Accessors
• 3. Equivalences with functors from the tensor

Library UniMath.CategoryTheory.EnrichedCats.Bifunctors.CurriedTransformations

• 1. Curried transformations between bifunctors
• 2. Equivalence with enriched natural transformations

Library UniMath.CategoryTheory.EnrichedCats.Bifunctors.WhiskeredBifunctors

• 1. Definition of whiskered bifunctors
• 2. Accessors for whiskered bifunctors
• 3. Equivalence with functors from the tensor

Library UniMath.CategoryTheory.EnrichedCats.Bifunctors.WhiskeredTransformations

• 1. Whiskered transformations between bifunctors
• 2. Equivalence with enriched natural transformations

Library UniMath.CategoryTheory.EnrichedCats.Colimits.CopowerFunctor

Library UniMath.CategoryTheory.EnrichedCats.Colimits.EnrichedBinaryCoproducts

Library UniMath.CategoryTheory.EnrichedCats.Colimits.EnrichedCoequalizers

Library UniMath.CategoryTheory.EnrichedCats.Colimits.EnrichedColimits

Library UniMath.CategoryTheory.EnrichedCats.Colimits.EnrichedConicalColimits

Library UniMath.CategoryTheory.EnrichedCats.Colimits.EnrichedCopowers

Library UniMath.CategoryTheory.EnrichedCats.Colimits.EnrichedCoproducts

Library UniMath.CategoryTheory.EnrichedCats.Colimits.EnrichedInitial

Library UniMath.CategoryTheory.EnrichedCats.Colimits.Examples.OppositeEnrichedColimits

Library UniMath.CategoryTheory.EnrichedCats.Colimits.Examples.PosetEnrichedColimits

Library UniMath.CategoryTheory.EnrichedCats.Colimits.Examples.SelfEnrichedColimits

Library UniMath.CategoryTheory.EnrichedCats.Colimits.Examples.StructureEnrichedColimits

Library UniMath.CategoryTheory.EnrichedCats.Enriched.ChangeOfBase

Library UniMath.CategoryTheory.EnrichedCats.Enriched.Enriched

• Enriched categories
  • Contents
  • Definition
    • Enriched functors
    • Composition of enriched functors

Library UniMath.CategoryTheory.EnrichedCats.Enriched.EnrichmentEquiv

Library UniMath.CategoryTheory.EnrichedCats.Enriched.Opposite

Library UniMath.CategoryTheory.EnrichedCats.Enriched.UnderlyingCategory

Library UniMath.CategoryTheory.EnrichedCats.Examples.ChangeOfBase

Library UniMath.CategoryTheory.EnrichedCats.Examples.CollageEnriched

• 1. The underlying category
• 2. The enrichment
• 3. The underlying category
• 4. The underlying category is univalent
• 5. The left inclusion
• 6. The right inclusion
• 7. The square of the collage

Library UniMath.CategoryTheory.EnrichedCats.Examples.DialgebraEnriched

Library UniMath.CategoryTheory.EnrichedCats.Examples.EilenbergMooreEnriched

Library UniMath.CategoryTheory.EnrichedCats.Examples.EmptyEnriched

Library UniMath.CategoryTheory.EnrichedCats.Examples.FullSubEnriched

Library UniMath.CategoryTheory.EnrichedCats.Examples.FunctorCategory

Library UniMath.CategoryTheory.EnrichedCats.Examples.GraphEnriched

• 1. The graph of an enriched profunctor
• 2. Accessors and builders for objects and morphisms
• 3. The enriched hom object
• 4. Operations for the enrichment
• 5. Laws for the enrichment
• 6. The enrichment for the graph
• 7. The first projection
• 8. The second projection
• 9. The square of the graph

Library UniMath.CategoryTheory.EnrichedCats.Examples.HomFunctor

Library UniMath.CategoryTheory.EnrichedCats.Examples.ImageEnriched

Library UniMath.CategoryTheory.EnrichedCats.Examples.KleisliEnriched

• 1. Data of the enrichment
• 2. The laws of the enrichment
• 3. The enrichment
• 4. Enriched functors from the Kleisli category
• 5. Natural transformations from the Kleisli category

Library UniMath.CategoryTheory.EnrichedCats.Examples.OppositeEnriched

Library UniMath.CategoryTheory.EnrichedCats.Examples.PosetEnriched

Library UniMath.CategoryTheory.EnrichedCats.Examples.Precomposition

Library UniMath.CategoryTheory.EnrichedCats.Examples.Presheaves

• 1. Hom objects of presheaves
• 2. The identity for the enrichment
• 3. Composition for the enrichment
• 4. Global elements versus natural transformations
• 5. Laws of the enrichment
• 6. Enrichment for the presheaf category

Library UniMath.CategoryTheory.EnrichedCats.Examples.ProductEnriched

Library UniMath.CategoryTheory.EnrichedCats.Examples.QuantaleEnriched

• 1. Builder for categories enriched over quantales
• 2. The objects in a quantale enriched univalent category form a set
• 3. Builder for functors of categories enriched over quantales
• 4. Properties of quantale enriched functors
• 5. Equality of natural transformation for quantale enriched categories
• 6. Builder for quantale enriched profunctors
• 7. Properties of quantale enriched profunctors
• 8. Properties of quantale enriched transformations

Library UniMath.CategoryTheory.EnrichedCats.Examples.SelfEnriched

Library UniMath.CategoryTheory.EnrichedCats.Examples.SetEnriched

Library UniMath.CategoryTheory.EnrichedCats.Examples.SliceEnriched

Library UniMath.CategoryTheory.EnrichedCats.Examples.SmashStructureEnriched

Library UniMath.CategoryTheory.EnrichedCats.Examples.StructureEnriched

Library UniMath.CategoryTheory.EnrichedCats.Examples.Tensor

• 1. The data of the tensor
• 2. The axioms
• 3. The tensor of enriched categories

Library UniMath.CategoryTheory.EnrichedCats.Examples.UnitEnriched

Library UniMath.CategoryTheory.EnrichedCats.Examples.UnivalentKleisliEnriched

Library UniMath.CategoryTheory.EnrichedCats.Examples.UnivalentKleisliMapping

• 1. Enriched functors from the univalent Kleisli category
• 2. Enriched transformations from the univalent Kleisli category
• 3. Uniqueness of 2-cells from the univalent Kleisli category

Library UniMath.CategoryTheory.EnrichedCats.Examples.Yoneda

Library UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedBinaryProducts

Library UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedConicalLimits

Library UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedEqualizers

Library UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedLimits

• 1. Cones of enriched limits
• 2. Limits in an enriched category
• 3. Being a limit is a proposition *
• 4. Some accessors for enriched limits
• 5. Enriched limits are unique up to isomorphism
• 6. Uniqueness of enriched limits
• 7. Instances of limits
• 7.1. Powers as limits
• 7.2. Conical limits as limits

Library UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedPowers

Library UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedProducts

Library UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedTerminal

Library UniMath.CategoryTheory.EnrichedCats.Limits.Examples.OppositeEnrichedLimits

Library UniMath.CategoryTheory.EnrichedCats.Limits.Examples.PosetEnrichedLimits

Library UniMath.CategoryTheory.EnrichedCats.Limits.Examples.SelfEnrichedLimits

Library UniMath.CategoryTheory.EnrichedCats.Limits.Examples.StructureEnrichedLimits

Library UniMath.CategoryTheory.EnrichedCats.Profunctors.Coend

• 1. Construction of the coend of an enriched profunctor
• 2. Accessors

Library UniMath.CategoryTheory.EnrichedCats.Profunctors.Composition

Library UniMath.CategoryTheory.EnrichedCats.Profunctors.Invertible

• 1. Invertible profunctor transformations
• 2. The inverse transformation
• 3. The identity type of enriched profunctors

Library UniMath.CategoryTheory.EnrichedCats.Profunctors.Profunctor

• 1. Enriched profunctors
• 2. Accessors
• 3. Equivalence with whiskered bifunctors
• 4. Action on morphisms in the underlying category

Library UniMath.CategoryTheory.EnrichedCats.Profunctors.ProfunctorSquares

• 1. Squares of enriched profunctors
• 2. Accessors/builders for squares of enriched profunctors
• 3. Squares and transformations
• 4. Examples of squares of enriched profunctors
  • 4.1. Horizontal identity square
  • 4.2. Vertical identity square
  • 4.3. Horizontal composition of squares
• 4.4. Up whiskering
• 4.5. Down whiskering
• 4.6. Left whiskering
• 4.7. Right whiskering
  • 4.8. Companion pairs
  • 4.9. Conjoints

Library UniMath.CategoryTheory.EnrichedCats.Profunctors.ProfunctorTransformations

• 1. Transformations between enriched profunctors
• 2. Equivalence with the usual definition
• 3. Standard transformations of profunctors
  • 3.1. The identity
  • 3.2. Composition
• 4. Extra laws

Library UniMath.CategoryTheory.EnrichedCats.Profunctors.RepresentableLaws

• 1. Laws for the left representable
• 2. Laws for the right representable

Library UniMath.CategoryTheory.EnrichedCats.Profunctors.StandardProfunctors

• 1. Identity profunctor
• 2. Representable profunctors
  • 2.1. Left representable
  • 2.2. Right representable
• 3. Precomposition with enriched functors

Library UniMath.CategoryTheory.EnrichedCats.Profunctors.Composition.Associators

• 1. The right associator
  • 1.1. Action on objects
  • 1.2. The data
  • 1.3. The laws
  • 1.4. The right associator as a transformation
• 2. The right associator
  • 2.1. Action on objects
  • 2.2. The data

Library UniMath.CategoryTheory.EnrichedCats.Profunctors.Composition.BicatLaws

• 1. Naturality for the associator
• 2. The triangle law
• 3. The pentagon law

Library UniMath.CategoryTheory.EnrichedCats.Profunctors.Composition.CompositionProf

• 1. The functor over which we take the coend
• 2. The coend used to define composition
• 3. The left action
• 4. The right action
• 5. The data
• 6. The laws
• 7. Composition of enriched profunctors
• 8. Additional laws for action on morphisms

Library UniMath.CategoryTheory.EnrichedCats.Profunctors.Composition.OtherLaws

• 1. The interchange law
• 2. Cylinder laws for the left unitor
• 3. Cylinder laws for the right unitor
• 4. Cylinder laws for the associator
• 5. Composition and whiskering
• 6. Saturation of the Verity double bicategory of enriched profunctors

Library UniMath.CategoryTheory.EnrichedCats.Profunctors.Composition.SquareComp

• 1. The data
• 2. The laws
• 3. Composition of squares

Library UniMath.CategoryTheory.EnrichedCats.Profunctors.Composition.Unitors

• 1. The left unitor
  • 1.1. The morphism of the left unitor
  • 1.2. Naturality of the left unitor
  • 1.3. The left unitor as a transformation
  • 1.4. The inverse of the left unitor
• 2. The right unitor
  • 2.1. The morphism of the right unitor
  • 2.2. Naturality of the right unitor
  • 2.3. The right unitor as a transformation
  • 2.4. The inverse of the right unitor

Library UniMath.CategoryTheory.EnrichedCats.Profunctors.Composition.WhiskerLaws

• 1. Up whiskering and composition
• 2. Down whiskering and composition
• 3. Up whiskering and identities
• 4. Swapping whiskering
• 5. Composition of squares and whiskering

Library UniMath.CategoryTheory.EnrichedCats.Profunctors.Composition.Whiskering

• 1. Right whiskering
• 2. Left whiskering

Library UniMath.CategoryTheory.EnrichedCats.RezkCompletion.EnrichedRezkCompletion

• 1. The Rezk completion and its enrichment
• 2. The weak equivalence
• 3. Bundled version

Library UniMath.CategoryTheory.EnrichedCats.RezkCompletion.PrecompEssentiallySurjective

• 1. Action on objects
• 2. Action on morphisms
• 3. The enrichment
• 4. The commutativity
• 5. Essential surjectivity

Library UniMath.CategoryTheory.EnrichedCats.RezkCompletion.PrecompFullyFaithful

• 1. Faithfulness
• 2. Fullness

Library UniMath.CategoryTheory.EnrichedCats.RezkCompletion.RezkUniversalProperty

• 1. Universal property of the Rezk completion
• 2. Accessors for the universal property of the Rezk completion

Library UniMath.CategoryTheory.Equivalences.CompositesAndInverses

• Composition and inverses of (adjoint) equivalences of precategories
  • Contents
  • Equivalences
  • Composition
  • Inverses

Library UniMath.CategoryTheory.Equivalences.Core

• • Equivalence of categories
  • Contents:
• Sloppy equivalence of categories
• Equivalence of (pre)categories
• Adjointification of a sloppy equivalence
  • One triangle equality is enough
  • Adjointification
• Being an adjoint equivalence is closed under isomorphism
• Identity functor is an adjoint equivalence
• Equivalence of categories yields equivalence of object types
• From full faithfullness and ess surj to equivalence

Library UniMath.CategoryTheory.Equivalences.EquivalenceFromComp

• 1. F* is an equivalence
• 2. F'* is an equivalence

Library UniMath.CategoryTheory.Equivalences.FullyFaithful

• Fully faithful functors and equivalences
  • Contents :
  • Fully faithful functor from an equivalence
  • Functor from an equivalence is essentially surjective
  • Fully faithful essentially surjective functors preserve all hProps on hom-types

Library UniMath.CategoryTheory.ExactCategories.ExactCategories

• Exact categories
  • Contents

Library UniMath.CategoryTheory.ExactCategories.Tests

Library UniMath.CategoryTheory.GrothendieckConstruction.IsOpfibration

Library UniMath.CategoryTheory.GrothendieckConstruction.IsPullback

Library UniMath.CategoryTheory.GrothendieckConstruction.IsosInTotal

Library UniMath.CategoryTheory.GrothendieckConstruction.Projection

Library UniMath.CategoryTheory.GrothendieckConstruction.TotalCategory

Library UniMath.CategoryTheory.GrothendieckToposes.Sheaves

• 1. The sheaf properties
  • 1.1. The natural transformation property
  • 1.2. The equalizer property
  • 1.3. The elementary property
• 2. The equivalences
  • 2.1. The first implies the second
  • 2.2. The second implies the third
  • 2.3. The third implies the first
  • 2.4. The implications the other way around
• 3. Sheaves
  • 3.1. The category of sheaves
  • 3.2. Sheaves
  • 3.3. Sheaf morphisms

Library UniMath.CategoryTheory.GrothendieckToposes.Sieves

• 1. Sieves
• 2. Pullback of sieves
• 3. Selected morphisms

Library UniMath.CategoryTheory.GrothendieckToposes.Sites

• 1. Sites
• 2. Covering sieves

Library UniMath.CategoryTheory.GrothendieckToposes.Topologies

• 1. The property for a collection of sieves of being a topology
• 2. Grothendieck topologies

Library UniMath.CategoryTheory.GrothendieckToposes.Toposes

• 1. The property of being a Grothendieck topos
• 2. Grothendieck toposes
• 3. The recursion and induction principles

Library UniMath.CategoryTheory.GrothendieckToposes.Examples.DiscreteTopology

• 1. The discrete site
• 2. The sheaf category is equivalent to the unit category
  • 2.1. The contractibility of F X
  • 2.2. The equivalence

Library UniMath.CategoryTheory.GrothendieckToposes.Examples.EmptySieve

• 1. The empty sieve

Library UniMath.CategoryTheory.GrothendieckToposes.Examples.IndiscreteTopology

• 1. The indiscrete site
• 2. Any presheaf is a sheaf

Library UniMath.CategoryTheory.GrothendieckToposes.Examples.TerminalSheaf

• 1. The terminal sheaf

Library UniMath.CategoryTheory.Hyperdoctrines.FirstOrderHyperdoctrine

• 1. First-order hyperdoctrines
• 2. The truth formula
• 3. The falsity formula
• 4. Conjunction
• 5. Weakening of hypotheses
• 6. Disjunction
• 7. Implication
• 8. Universal quantification
• 9. Existential quantification
• 10. Equality
• 11. Derived rules for equality
• 12. Derived connectives
• 12.1. Bi-implication
• 12.2. Negation
• 13. A tactic for simplifying goals in the internal language of first-order hyperdoctrines

Library UniMath.CategoryTheory.Hyperdoctrines.GenericPredicate

• 1. Definition of generic predicates in first-order hyperdoctrines

Library UniMath.CategoryTheory.Hyperdoctrines.HValuedSets

• 1. The topos of H-valued sets
• 2. Accessors and builders for H-valued sets
• 3. Accessors and builders for morphisms of H-valued sets

Library UniMath.CategoryTheory.Hyperdoctrines.Hyperdoctrine

• 1. Structure of hyperdoctrines
• 2. Accessors for types in a hyperdoctrine
• 3. Accessors for terms in a hyperdoctrine
• 3.1. Substitution on terms
• 3.2. Terms for the unit type
• 3.3. Terms for the binary product type
• 4. Formulas in a hyperdoctrine
• 5. Proof terms in a hyperdoctrine
• 6. Equality of formulas
• 7. Substitution on formulas in a hyperdoctrine

Library UniMath.CategoryTheory.Hyperdoctrines.Tripos

• 1. Tripos
• 2. Some substitutions necessary to define weak triposes
• 3. The definition of weak triposes
• 4. Every tripos is a weak tripos

Library UniMath.CategoryTheory.Hyperdoctrines.TriposToTopos

Library UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.ExponentialEqs

• 1. Basic material that is useful in the remainder of the file
• 2. The beta-rule
• 3. The eta-rule

Library UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.ExponentialEval

• 1. The formula of the evaluation morphism
• 2. The laws of the evaluation morphism
• 3. The evaluation morphism

Library UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.ExponentialLam

• 1. The formula defining abstraction
• 2. Accessors
• 3. The image
• 4. Lambda abstraction

Library UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.ExponentialPER

• 1. Functions of partial setoids via the powerset
• 2. Accessors
• 3. Pointwise equality of partial setoid functions
• 4. The partial setoid of functions
• 5. Accessors for the partial equivalence relation of functions

Library UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.InternalLogic

Library UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERBinProducts

• 1. The first projection
• 2. The second projection
• 3. Pairing partial setoid morphisms
• 4. The uniqueness
• 5. Binary products of partial setoids
• 6. Preservation of binary products by the constant object functor

Library UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERCategory

• 1. The identity morphism
• 2. The composition of morphisms of partial setoids
• 3. The category of partial setoids

Library UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERConstantObjects

• 1. Every term gives a partial setoid morphism
• 2. The constant object functor

Library UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PEREqualizers

• 1. The equalizer partial setoid
• 2. Accessors for the partial equivalence relation of the equalizer
• 3. The inclusion of the equalizer
• 4. The universal property of the equalizer
• 4.1. The map from the universal property
• 4.2. Uniqueness of the morphism
• 5. Equalizers of partial setoids

Library UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERExponentials

Library UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERInitial

• 1. The initial partial setoid
• 2. The morphism from the initial partial setoid and its uniqueness
• 3. The initial object
• 4. This initial object is strict

Library UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERMonomorphisms

• 1. Formulas to monomorphisms
• 1.1. The partial setoid
• 1.2. Accessors for the partial equivalence relation
• 1.3. The inclusion
• 1.4. The proof that it is monic
• 2. Proofs to commuting triangles
• 2.1. The morphism from a proof
• 2.2. Proof of commutativity
• 3. The displayed functor from formulas to monomorphisms
• 4. The displayed functor is fully faithful
• 5. The displayed functor is split essentially surjective
• 6. Identifying terms using monomorphisms

Library UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERMorphisms

• 1. Laws of partial setoid morphisms
• 2. Partial setoid morphisms
• 3. Accessors for partial setoid morphisms

Library UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERSubobjectClassifier

• 1. The partial setoid representing the subobject classifier
• 2. Accessors for the partial equivalence relation
• 3. The map representing truth
• 4. The universal mapping property of the subobject classifier
• 4.1. Maps to the subobject classifier
• 4.2. The map gives rise to a pullback square
• 4.3. Uniqueness
• 5. The subobject classifier of partial setoids

Library UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERTerminal

• 1. Morphism to the terminal object
• 2. Uniqueness of the morphism to the terminal object
• 3. The terminal object
• 4. Preservation of terminal objects by the constant object functor

Library UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.PERs

• 1. Partial equivalence relations
• 2. Partial setoids
• 3. Every type is a partial setoid with equality
• 4. The product of partial setoids

Library UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.Logic.Conjunction

• 1. The formula
• 2. Elimination rules
• 3. Introduction rule
• 4. Stability under substitution
• 5. Fiberwise binary products

Library UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.Logic.Disjunction

• 1. The formula
• 2. Introduction rules
• 3. Elimination rule
• 4. Stability under substitution
• 5. Fiberwise binary coproducts

Library UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.Logic.Existential

• 1. The formula
• 2. Introduction rule
• 3. Elimination rule
• 4. Stability under substitution
• 5. Dependent sums

Library UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.Logic.Falsity

• 1. The formula
• 2. Elimination rule
• 3. Stability under substitution
• 4. The fiberwise initial object

Library UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.Logic.Implication

• 1. The formula
• 2. Elimination rule
• 3. Introduction rule
• 4. Stability under substitution
• 5. Fiberwise exponentials

Library UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.Logic.MonoEquiv

• 1. Subobjects to monomorphisms
• 2. The action on morphisms
• 3. The displayed functor
• 4. Fully faithfulness
• 5. Split essential surjectivity

Library UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.Logic.SubobjectDispCat

• 1. Subobjects of partial setoids
• 2. Accessors for subobjects of partial setoids
• 3. Morphisms between subobjects of partial setoids
• 4. The displayed category of subobjects
• 5. This displayed category is univalent
• 6. The cleaving

Library UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.Logic.Truth

• 1. The formula
• 2. Introduction rule
• 3. Stability under substitution
• 4. The fiberwise terminal object

Library UniMath.CategoryTheory.Hyperdoctrines.PartialEqRels.Logic.Universal

• 1. The formula
• 2. The elimination rule
• 3. The introduction rule
• 4. Dependent products of subobjects

Library UniMath.CategoryTheory.IdempotentsAndSplitting.Fullsub

Library UniMath.CategoryTheory.IdempotentsAndSplitting.FunctorCategory

Library UniMath.CategoryTheory.IdempotentsAndSplitting.Retracts

• 1. Retractions
• 2. Idempotents and split idempotents
  • 2.1. Split idempotent implies idempotent
  • 2.2. In a univalent category, being split idempotent is a mere proposition
• 3. Functors
  • 3.1. Retractions are preserved by functors
  • 3.2. Idempotents are preserved by functors
  • 3.3. Split idempotents are preserved by functors

Library UniMath.CategoryTheory.IdempotentsAndSplitting.Set

Library UniMath.CategoryTheory.IndexedCategories.CartesianToIndexedFunctor

Library UniMath.CategoryTheory.IndexedCategories.CoreIndexedCategory

Library UniMath.CategoryTheory.IndexedCategories.FibrationToIndexedCategory

Library UniMath.CategoryTheory.IndexedCategories.IndexedCategory

Library UniMath.CategoryTheory.IndexedCategories.IndexedCategoryToFibration

Library UniMath.CategoryTheory.IndexedCategories.IndexedFunctor

Library UniMath.CategoryTheory.IndexedCategories.IndexedFunctorToCartesian

Library UniMath.CategoryTheory.IndexedCategories.IndexedTransformation

Library UniMath.CategoryTheory.IndexedCategories.IndexedTransformationToTransformation

Library UniMath.CategoryTheory.IndexedCategories.NatTransToIndexed

Library UniMath.CategoryTheory.IndexedCategories.OpIndexedCategory

Library UniMath.CategoryTheory.Inductives.LambdaCalculus

Library UniMath.CategoryTheory.Inductives.Lists

• Lists as the colimit of a chain given by the list functor: F(X) = 1 + A * X
• Equivalence with lists as iterated products

Library UniMath.CategoryTheory.Inductives.PropositionalLogic

• • Contents

Library UniMath.CategoryTheory.Inductives.Trees

• Binary trees
  • Flattening of a tree into a list

Library UniMath.CategoryTheory.Limits.BinBiproducts

Library UniMath.CategoryTheory.Limits.BinCoproducts

• Definition of binary coproduct of objects in a precategory
• Proof that coproducts are unique when the precategory C is a univalent_category
• Binary coproducts from colimits
• Coproducts over bool from binary coproducts
  • Construction of isBinCoproduct from an isomorphism to BinCoproduct.

Library UniMath.CategoryTheory.Limits.BinDirectSums

• Direct definition of binary direct sum using preadditive categories.
  • Contents
  • Composition of IndAr
• BinDirectSums in quotient of PreAdditive category

Library UniMath.CategoryTheory.Limits.BinProducts

• Direct implementation of binary products
  • Contents
  • Definition of binary products
  • Binary products from limits (BinProducts_from_Lims)
  • Definition of binary product functor (binproduct_functor)
  • Definition of a binary product structure on a functor category
  • Construction of BinProduct from an isomorphism to BinProduct.
  • Equivalent universal property: (C --> A) × (C --> B) ≃ (C --> A × B)
  • Terminal object as the unit (up to isomorphism) of binary products

Library UniMath.CategoryTheory.Limits.Coends

• 1. Coedges
• 2. Coends
• 3. Accessors for coends
• 4. Construction of coends from coproducts and coequalizers

Library UniMath.CategoryTheory.Limits.Coequalizers

Library UniMath.CategoryTheory.Limits.Cokernels

• Direct definition of cokernels
  • Contents
• Definition of cokernels
• Correspondence of cokernels and coequalizers
  • Coequalizer from Cokernel
  • Cokernel from Coequalizer
• Cokernels up to iso
• Cokernel of epi · morphism
  • Introduction
• CokernelOut of equal, not necessarily definitionally equal, morphisms is iso

Library UniMath.CategoryTheory.Limits.Cones

Library UniMath.CategoryTheory.Limits.Coproducts

• Definition of indexed coproducts of objects in a precategory
• The coproduct functor: C^I -> C
• Coproducts lift to functor categories
• Coproducts from colimits

Library UniMath.CategoryTheory.Limits.DisjointBinCoproducts

• 1. Disjoint binary coproducts
• 2. Stable binary coproducts
• 3. Characterization of stable binary coproducts

Library UniMath.CategoryTheory.Limits.Ends

Library UniMath.CategoryTheory.Limits.Equalizers

• • Definition
  • Proof that the equalizer arrow is monic (EqualizerArrowisMonic)
  • Alternative universal property

Library UniMath.CategoryTheory.Limits.EquivalencePreservation

• 1. Equivalences and limits (backward preservation)
• 2. Equivalences and colimits (forward preservation)
• 3. Equivalences and limits (forward preservation)
• 4. Equivalences and colimits (backward preservation)

Library UniMath.CategoryTheory.Limits.Filtered

• Filtered Categories *
• *
• Definition of filtered categories and compact/finitely presentable *
• objects. Two definitions of filtered categories are given, *
• is_filtered *
• is_filtered_alt *
• and a proof that they are equivalent is given in weq_filtered. *
• *
• Contents *
• 1) Filtered categories *
• 2) Compact objects *
• 3) Properties *
• 4) Equivalence between is_filtered and is_filtered_alt. *
• *

Library UniMath.CategoryTheory.Limits.FinOrdCoproducts

Library UniMath.CategoryTheory.Limits.FinOrdProducts

Library UniMath.CategoryTheory.Limits.Initial

• Being initial is a property in a (saturated/univalent) category
• Construction of initial object in a functor category

Library UniMath.CategoryTheory.Limits.Kernels

• Direct implementation of kernels
  • Contents
• Correspondence of kernels and equalizers
  • Equalizer from Kernel
  • Kernel from Equalizer
• Kernel up to isomorphism
• Kernel of morphism · monic
  • Introduction
• KernelIn of equal, not necessarily definitionally equal, morphisms is iso
• Transports of kernels

Library UniMath.CategoryTheory.Limits.LimitIso

• 1. Binary products on isomorphisc cones
• 2. Equalizers on isomorphic cones
• 3. Binary coproducts on isomorphic cocones

Library UniMath.CategoryTheory.Limits.Opp

• Duality between C and C^op
  • Contents
• Translation of structures from C^op to C
  • Monic and Epi
  • Initial, Terminal, and Zero
  • Equality on ZeroArrows
  • Equalizers and Coequalizers
  • Kernels and Cokernels
  • Pushouts and pullbacks
  • BinProducts and BinCoproducts
• Translation of structures from C to C^op
  • Monic and Epi
  • Initial, Terminal, and Zero
  • Equality on ZeroArrows
  • Equalizers and Coequalizers
  • Kernels and Cokernels
  • Pushouts and pullbacks
  • BinProducts and BinCoproducts

Library UniMath.CategoryTheory.Limits.Preservation

Library UniMath.CategoryTheory.Limits.PreservationProperties

• 1. Preservation and natural isomorphisms
• 2. Preservation and equivalences in the arrow bicategory
• 3. Preservation of binary products and equalizers from pullbacks
• 4. Preservation of pullbacks via binary products and equalizers

Library UniMath.CategoryTheory.Limits.Products

• Definition of indexed products of objects in a precategory
• The product functor: C^I -> C
• Products lift to functor categories
• Products from limits
  • Construction of Product from an isomorphism to Product.

Library UniMath.CategoryTheory.Limits.PullbackConstructions

• 1. Equalizers from pullbacks and products
• 2. Equalizers from pullbacks and a terminal object
• 3. Pullback of a product

Library UniMath.CategoryTheory.Limits.Pullbacks

• Criteria for existence of pullbacks.
• A square isomorphic to a pullback is a pullback (case 1)
• Pullback of identities
• A fully faithful functor reflects limits
• A fully faithful and essentially surjective functor preserves pullbacks
• Pullbacks in functor categories
• Construction of binary products from pullbacks
• Pullbacks in functor_precategory
• Swapping pullbacks

Library UniMath.CategoryTheory.Limits.PullbacksSliceProductsEquiv

• Proof that the types of binary products in C/Z and pullbacks of pairs of arrows to Z in C are equivalent
  • equivalence of function taking proof of isPullback to proof of isBinProduct
  • equivalence of function taking proof of isBinProduct to proof of isPullback
  • pullback_to_slice_binprod is invertible
  • slice_binprod_to_pullback is invertible
  • function taking the type of all binary products in C / Z
  • function taking the type of all pullbacks of functions to Z in C
  • binprod_to_pullback is invertible
  • pullback_to_binprod is invertible
  • the equivalence of the types of binary products in C/Z

Library UniMath.CategoryTheory.Limits.Pushouts

Library UniMath.CategoryTheory.Limits.StandardDiagrams

• Standard graphs and diagrams.

Library UniMath.CategoryTheory.Limits.StrictInitial

• 1. Strict initial objects
• 2. Strictness is preserved under isomorphism
• 3. Stability of strict initial objects
• 4. Monics from strict initial objects

Library UniMath.CategoryTheory.Limits.Terminal

• Construction of terminal object in a functor category

Library UniMath.CategoryTheory.Limits.Zero

• • Transport of ZeroArrow

Library UniMath.CategoryTheory.Limits.Cats.Limits

Library UniMath.CategoryTheory.Limits.Examples.AlgebraStructuresColimits

Library UniMath.CategoryTheory.Limits.Examples.CategoryOfSetGroupoidsLimits

• 1. The terminal setgroupoid

Library UniMath.CategoryTheory.Limits.Examples.CategoryOfSetcategoriesLimits

Library UniMath.CategoryTheory.Limits.Examples.CategoryProductLimits

Library UniMath.CategoryTheory.Limits.Examples.EilenbergMooreLimits

Library UniMath.CategoryTheory.Limits.Examples.IsoCommaLimits

Library UniMath.CategoryTheory.Limits.Examples.UnitCategoryLimits

Library UniMath.CategoryTheory.Limits.Graphs.BinCoproducts

• Definition of binary coproduct of objects in a precategory
• Proof that coproducts are unique when the precategory C is a univalent_category

Library UniMath.CategoryTheory.Limits.Graphs.BinProducts

Library UniMath.CategoryTheory.Limits.Graphs.Coequalizers

• Coequalizers defined in terms of colimits
  • Contents
• Definition of coequalizers in terms of colimits
  • Coequalizers to coequalizers
  • Connections to other colimits
• Definitions coincide
  • isCoequalizers
  • Coequalizers

Library UniMath.CategoryTheory.Limits.Graphs.Cokernels

• Cokernels defined in terms of colimits.
  • Contents
• Definition of cokernels in terms of colimits
  • Coincides with the direct definiton

Library UniMath.CategoryTheory.Limits.Graphs.Colimits

• Definition of colimits
• Defines colimits in functor categories when the target has colimits
  • Left adjoints preserve colimits

Library UniMath.CategoryTheory.Limits.Graphs.Coproducts

• 1. The graph
• 2. The construction

Library UniMath.CategoryTheory.Limits.Graphs.Diagrams

Library UniMath.CategoryTheory.Limits.Graphs.EqDiag

Library UniMath.CategoryTheory.Limits.Graphs.Equalizers

• Equalizers defined in terms of limits
  • Contents
• Definition of equalizers in terms of limits
  • Equalizers to equalizers
  • Connections to other limits
• Definitions coincide
  • isEqualizers
  • Equalizers

Library UniMath.CategoryTheory.Limits.Graphs.Initial

• • Maps between initial as special colimit and direct definition

Library UniMath.CategoryTheory.Limits.Graphs.Kernels

• Kernels defined in terms of limits
  • Contents
• Definition of kernels in terms of limits
  • Maps between Kernels as limits and direct definition.

Library UniMath.CategoryTheory.Limits.Graphs.Limits

• Definition of limits
• Limits in functor categories
  • Right adjoints preserve limits
• Definition of limits via colimits

Library UniMath.CategoryTheory.Limits.Graphs.Pullbacks

• • Maps between pullbacks as special limits and

Library UniMath.CategoryTheory.Limits.Graphs.Pushouts

• Pushouts defined in terms of colimits
  • Contents
• Definition of pushouts in terms of colimits
  • Pushouts to Pushouts
  • Connections to other colimits
• Definitions coincide
  • isPushout
  • Pushout

Library UniMath.CategoryTheory.Limits.Graphs.Terminal

• • Maps between terminal as a special limit and direct definition

Library UniMath.CategoryTheory.Limits.Graphs.Zero

• Zero Objects
  • Contents
• Definition of zero using limits and colimits
• Zero coincides with the direct definition
  • isZero
  • Zero
  • Arrows

Library UniMath.CategoryTheory.LocallyCartesianClosed.LocallyCartesianClosed

• 1. Locally cartesian closed categories
• 2. The slices of locally cartesian closed categories are cartesian closed
• 3. Some properties of locally Cartesian closed categories

Library UniMath.CategoryTheory.LocallyCartesianClosed.Preservation

• 1. Structure preserving functors between LCCCs
• 2. The identity is structure preserving
• 3. The composition is structure preserving

Library UniMath.CategoryTheory.MarkovCategories.AlmostSurely

Library UniMath.CategoryTheory.MarkovCategories.Conditionals

• 1. Definition of markov_category_with_conditionals
• 2. Accessors
• 3. Bayesian inverses
• 4. Consequences and derived information flow axioms

Library UniMath.CategoryTheory.MarkovCategories.Couplings

Library UniMath.CategoryTheory.MarkovCategories.Determinism

• 2. Examples and Properties

Library UniMath.CategoryTheory.MarkovCategories.InformationFlowAxioms

• 1. Definition of the Information Flow Axioms
• 2. Accessors
• 3. Consequences of Causality

Library UniMath.CategoryTheory.MarkovCategories.MarkovCategory

• Projections (marginals)

Library UniMath.CategoryTheory.MarkovCategories.ProbabilitySpaces

Library UniMath.CategoryTheory.MarkovCategories.State

Library UniMath.CategoryTheory.MarkovCategories.Univalence

Library UniMath.CategoryTheory.Monads.ComonadCoalgebras

Library UniMath.CategoryTheory.Monads.Comonads

• Definition and lemmas for cobind
• Helper lemma for showing two comonads are equal
• Alternate (equivalent) definition of Comonad
• Equivalence of Comonad and Comonad'

Library UniMath.CategoryTheory.Monads.Derivative

• Definition of distributive laws for Monads and composition of Monads
• Definition of the "Maybe" monad (coproduct with a fixed object)

Library UniMath.CategoryTheory.Monads.KTriples

• Kleisli Triples

Library UniMath.CategoryTheory.Monads.KTriplesEquiv

Library UniMath.CategoryTheory.Monads.Kleisli

• Equivalence of the types of KleisliMonad and "monoidal" monads

Library UniMath.CategoryTheory.Monads.KleisliCategory

Library UniMath.CategoryTheory.Monads.LModules

• Definition of module
• Monad category

Library UniMath.CategoryTheory.Monads.MonadAlgebras

Library UniMath.CategoryTheory.Monads.Monads

• Definition and lemmas for bind
• Operations for monads based on binary coproducts
• Substitution operation for monads
• Helper lemma for showing two monads are equal
• Alternate (equivalent) definition of Monad
• Equivalence of Monad and Monad'

Library UniMath.CategoryTheory.Monads.RelMonads_Coreflection

• Postcomposition of a relative monad with a coreflection
  • Proof of the monad axioms of the composed data
  • Postcomposition of a monad morphism with a coreflection
  • Postcomposing a monad with the right adjoint of a coreflection
  • Postcomposing a monad morphism with the right adjoint of a coreflection

Library UniMath.CategoryTheory.Monads.RelativeModules

• Modules over relative monads
  • Miscellanea
  • Definition of module over a relative monad.
  • Packing the full structure of Relative Module together.
  • Functoriality of Modules
  • Morphisms of modules over a fixe relative monad.
  • Category of modules over a fixed relative monad.
  • Tautological module

Library UniMath.CategoryTheory.Monads.RelativeMonads

• Definition of relative monads

Library UniMath.CategoryTheory.Monoidal.Adjunctions

Library UniMath.CategoryTheory.Monoidal.Categories

Library UniMath.CategoryTheory.Monoidal.CategoriesForQuantum

Library UniMath.CategoryTheory.Monoidal.CategoriesOfMonoids

Library UniMath.CategoryTheory.Monoidal.FunctorCategories

Library UniMath.CategoryTheory.Monoidal.Functors

Library UniMath.CategoryTheory.Monoidal.StrongMonad

Library UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors

Library UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.AugmentedSimplexCategory

Library UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.BraidedMonoidalCategories

• • Contents:
• Braidings
• Hexagon equations.
• Braided monoidal categories
  • Accessors

Library UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.CategoriesOfMonoids

Library UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.DisplayedMonoidalCurried

Library UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.DisplayedMonoidalTensored

Library UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.EquivalenceWhiskeredNonCurriedMonoidalCategories

Library UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesCurried

Library UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesReordered

Library UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored

Library UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorCategory

Library UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsCurried

Library UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsTensored

Library UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.TotalDisplayedMonoidalCurried

Library UniMath.CategoryTheory.Monoidal.Comonoids.CartesianAsComonoids

Library UniMath.CategoryTheory.Monoidal.Comonoids.Category

Library UniMath.CategoryTheory.Monoidal.Comonoids.CommComonoidsCartesian

Library UniMath.CategoryTheory.Monoidal.Comonoids.Monoidal

Library UniMath.CategoryTheory.Monoidal.Comonoids.MonoidalCartesianBuilder

Library UniMath.CategoryTheory.Monoidal.Comonoids.Symmetric

Library UniMath.CategoryTheory.Monoidal.Comonoids.Tensor

Library UniMath.CategoryTheory.Monoidal.Comonoids.TransportComonoidAlongRetraction

Library UniMath.CategoryTheory.Monoidal.Displayed.Monoidal

Library UniMath.CategoryTheory.Monoidal.Displayed.MonoidalFunctorLifting

Library UniMath.CategoryTheory.Monoidal.Displayed.MonoidalSections

Library UniMath.CategoryTheory.Monoidal.Displayed.Symmetric

Library UniMath.CategoryTheory.Monoidal.Displayed.SymmetricMonoidalBuilder

Library UniMath.CategoryTheory.Monoidal.Displayed.TotalMonoidal

Library UniMath.CategoryTheory.Monoidal.Displayed.TransportLemmas

Library UniMath.CategoryTheory.Monoidal.Displayed.WhiskeredDisplayedBifunctors

Library UniMath.CategoryTheory.Monoidal.Examples.BinopCartesianMonoidal

Library UniMath.CategoryTheory.Monoidal.Examples.CartesianMonoidal

Library UniMath.CategoryTheory.Monoidal.Examples.ConstantFunctor

Library UniMath.CategoryTheory.Monoidal.Examples.DiagonalFunctor

Library UniMath.CategoryTheory.Monoidal.Examples.DisplayedCartesianMonoidal

Library UniMath.CategoryTheory.Monoidal.Examples.EndofunctorsMonoidalElementary

Library UniMath.CategoryTheory.Monoidal.Examples.Fullsub

Library UniMath.CategoryTheory.Monoidal.Examples.LiftPoset

Library UniMath.CategoryTheory.Monoidal.Examples.MonadsAsMonoidsElementary

Library UniMath.CategoryTheory.Monoidal.Examples.MonoidalDialgebras

Library UniMath.CategoryTheory.Monoidal.Examples.MonoidalPointedObjects

Library UniMath.CategoryTheory.Monoidal.Examples.PointedSetCartesianMonoidal

Library UniMath.CategoryTheory.Monoidal.Examples.PosetsMonoidal

Library UniMath.CategoryTheory.Monoidal.Examples.Relations

Library UniMath.CategoryTheory.Monoidal.Examples.SetCartesianMonoidal

Library UniMath.CategoryTheory.Monoidal.Examples.SetWithSubset

Library UniMath.CategoryTheory.Monoidal.Examples.Sigma

Library UniMath.CategoryTheory.Monoidal.Examples.SmashProductMonoidal

Library UniMath.CategoryTheory.Monoidal.Examples.StructuresMonoidal

Library UniMath.CategoryTheory.Monoidal.Examples.SymmetricMonoidalCoEilenbergMoore

Library UniMath.CategoryTheory.Monoidal.Examples.SymmetricMonoidalDialgebras

Library UniMath.CategoryTheory.Monoidal.RezkCompletion.LiftedAssociator

Library UniMath.CategoryTheory.Monoidal.RezkCompletion.LiftedMonoidal

Library UniMath.CategoryTheory.Monoidal.RezkCompletion.LiftedTensor

Library UniMath.CategoryTheory.Monoidal.RezkCompletion.LiftedTensorUnit

Library UniMath.CategoryTheory.Monoidal.RezkCompletion.LiftedUnitors

Library UniMath.CategoryTheory.Monoidal.RezkCompletion.MonoidalRezkCompletion

Library UniMath.CategoryTheory.Monoidal.Structure.Cartesian

Library UniMath.CategoryTheory.Monoidal.Structure.Closed

Library UniMath.CategoryTheory.Monoidal.Structure.Symmetric

Library UniMath.CategoryTheory.Monoidal.Structure.SymmetricDiagonal

Library UniMath.CategoryTheory.OppositeCategory.Core

Library UniMath.CategoryTheory.OppositeCategory.LimitsAsColimits

Library UniMath.CategoryTheory.OppositeCategory.OppositeAdjunction

Library UniMath.CategoryTheory.OppositeCategory.OppositeEquivalence

Library UniMath.CategoryTheory.OppositeCategory.OppositeOfFunctorCategory

Library UniMath.CategoryTheory.Profunctors.Collage

• 1. The collage of a profunctor
• 2. The collage is univalent
• 3. The inclusions into the collage
• 4. The squares from the collage

Library UniMath.CategoryTheory.Profunctors.Core

• Profunctors
  • Contents
  • Definition
  • Dinatural transformations
    • Dinatural transformation from a natural transformation
  • (Co)ends
    • Wedges
    • Ends
      • Accessors/coercions
    • Cowedges
    • Coends

Library UniMath.CategoryTheory.Profunctors.Examples

• 1. The constant profunctor
• 2. The identity profunctor
• 3. Representable profunctors
• 4. Precomposition of a profunctor with functors
• 5. Product of profunctors
• 6. Composition of profunctors

Library UniMath.CategoryTheory.Profunctors.Squares

• 1. Squares of profunctors
• 2. Builder for squares of profunctors
• 3. Transformations to squares
• 4. Standard profunctor squares
  • 4.1. Identity squares
  • 4.2. Composition of squares
  • 4.3. Whiskering operations
• 4.4. Unitors and associators
• 4.5. Companion pairs
• 4.6. Conjoints

Library UniMath.CategoryTheory.Profunctors.Transformation

• 1. Natural transformations between profunctors
• 2. Builder for natural transformations between profunctors
• 3. Equality of natural transformations between profunctors
• 4. Natural isomorphisms between profunctors
• 5. Standard natural transformations between profunctors
• 5.1. Identity and composition
• 5.2. Left unitor
• 5.3. Right unitor
• 5.4. Associator
• 5.5. Inverse laws
• 5.6. Whiskering
• 6. Equality of profunctors

Library UniMath.CategoryTheory.RegularAndExact.ExactCategory

• 1. Internal relations
• 2. The relation on morphisms from an internal relation
• 3. Properties of internal relations
  • 3.1. Internal reflexivity
  • 3.2. Internal symmetry
  • 3.3. Internal transitivity
• 3.4. Internal equivalence relations
• 4. Effective internal equivalence relations
• 5. Exact categories

Library UniMath.CategoryTheory.RegularAndExact.RegularCategory

• 1. Coequalizers of kernel pairs
• 2. Regular categories
• 3. Morphisms between kernel pairs (Lemma 2.1.2 in Borceux)
• 4. Factorization in regular categories

Library UniMath.CategoryTheory.RegularAndExact.RegularEpi

• 1. Regular epimorphisms
• 2. Regular epimorphisms are closed under isomorphism
• 3. Regular epis are epimorphisms
• 4. Preservation of regular epimorphisms
• 5. Preservation of regular epimorphisms along chosen pullbacks
• 6. Preservation of regular epimorphisms by identity and composition

Library UniMath.CategoryTheory.RegularAndExact.RegularEpiFacts

• 1. Isomorphisms are regular epimorphisms
• 2. Regular epimorphisms versus effective epimorphisms
• 3. Regular epimorphisms versus strong epimorphisms
• 4. Strong epimorphisms versus extremal epimorphisms
• 5. Regular epimorphisms versus extremal epimorphisms

Library UniMath.CategoryTheory.RepresentableFunctors.Bifunctor

Library UniMath.CategoryTheory.RepresentableFunctors.DirectSum

• • • direct sums

Library UniMath.CategoryTheory.RepresentableFunctors.Precategories

• • • make a precategory

Library UniMath.CategoryTheory.RepresentableFunctors.RawMatrix

• • raw matrices

Library UniMath.CategoryTheory.RepresentableFunctors.Representation

Library UniMath.CategoryTheory.RepresentableFunctors.Test

Library UniMath.CategoryTheory.RezkCompletions.Construction

• 2. The construction of the Rezk completion and the embedding F

Library UniMath.CategoryTheory.RezkCompletions.RezkCompletions

• 1. The definition and accessors of a Rezk completion
• 2. The definition an initial functor from a category
  • 2.1. The proof that for an initial functor F, any functor G is the identity if F ∙ G = F
• 3. The equivalence between the covariant functor categories
  • 3.1. The proof that F is the initial functor from A
• 4. The equivalence between the contravariant functor categories

Library UniMath.CategoryTheory.SkewMonoidal.CategoriesOfMonoids

Library UniMath.CategoryTheory.SkewMonoidal.SkewMonoidalCategories

Library UniMath.CategoryTheory.Subcategory.Core

• • Sub(pre)categories
  • Contents :
  • Definitions
    • A sub-precategory forms a precategory.
    • (Inclusion) functor from a sub-precategory to the ambient precategory
  • Subcategories
  • Restriction of a functor to a subcategory

Library UniMath.CategoryTheory.Subcategory.Full

• • Full sub(pre)categories
  • Contents
  • The inclusion of a full subcategory is fully faithful
    • Fullness
    • Faithfulness
  • The (full) image of a functor
  • Given a functor F : C -> D, we obtain a functor F : C -> Img(F)
    • Morphisms in the full subprecat are equiv to morphisms in the precategory
    • Image factorization C -> Img(F) -> D
  • Any full subprecategory of a univalent_category is a univalent_category.
    • Isos in the full subcategory are equivalent to isos in the precategory
    • From Identity in the subcategory to isos in the category
    • Decomp of map from id in the subcat to isos in the subcat via isos in ambient precat
    • The aforementioned decomposed map is a weak equivalence
  • Proof of the targeted theorem: full subcats of cats are cats

Library UniMath.CategoryTheory.Subcategory.FullEquivalences

Library UniMath.CategoryTheory.Subcategory.Limits

• • (Co)limits in full subprecategories
• C has (co)limits of shape F,
• C' : ob C → UU is a proposition on the objects of C, and
• C' is closed under the formation of (co)limits of shape F,
• precategory_object_from_sub_precategory_object
• precategory_morphism_from_sub_precategory_morphism
• precategory_morphisms_in_subcat
• precategory_object_in_subcat.
  • Contents
  • The subcategory inclusion reflects limits
  • Limits
    • Terminal objects
    • Binary products
    • General limits
  • Colimits
    • Initial objects
    • Binary coproducts

Library UniMath.CategoryTheory.Subcategory.Reflective

• Reflective subcategories
  • Contents

Library UniMath.CategoryTheory.SubobjectClassifier.Operations

• 1. Falsity
• 2. Conjunction
• 3. Disjunction
• 4. Implication

Library UniMath.CategoryTheory.SubobjectClassifier.PreservesSubobjectClassifier

• 1. Preserving subobject classifiers
• 2. Preservation of chosen subobject classifiers
• 3. Preservation of subobject classifiers via isomorphisms
• 4. Preservation of subobject classifiers is independent of the choice of terminal object

Library UniMath.CategoryTheory.SubobjectClassifier.SubobjectClassifier

• Subobject classifiers
  • Contents
  • Definition
  • Accessors

Library UniMath.CategoryTheory.SubobjectClassifier.SubobjectClassifierIso

• 1. Isomorphisms between subobject classifiers
• 2. Being isomorphic to subobject classifiers
• 3. Independence of terminal object

Library UniMath.CategoryTheory.TwoSidedDisplayedCats.Discrete

Library UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedFunctor

Library UniMath.CategoryTheory.TwoSidedDisplayedCats.DisplayedNatTrans

Library UniMath.CategoryTheory.TwoSidedDisplayedCats.Fiber

Library UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos

Library UniMath.CategoryTheory.TwoSidedDisplayedCats.Strictness

• 1. Strict 2-sided displayed categories
• 2. The total category of a strict 2-sided displayed category
• 3. Equality of 2-sided displayed functors

Library UniMath.CategoryTheory.TwoSidedDisplayedCats.Total

Library UniMath.CategoryTheory.TwoSidedDisplayedCats.TransportLaws

• 1. Identity, inverse, and composition
• 2. Composition in a strict 2-sided displayed category
• 3. A special law for composition assuming strictness
• 4. Transporting along paths of objects

Library UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat

• 1.1. Definition of two-sided displayed categories

Library UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedFibration

Library UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence

Library UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.Arrow

Library UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.Bimodules

Library UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.Comma

Library UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.Constant

Library UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.DispCatOnTwoSidedDispCat

Library UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.EnrichedRels

• 1. The data
• 2. The 2-sided displayed category
• 3. Univalence

Library UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.FiberwiseProduct

Library UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.IsoComma

Library UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.Lenses

• 1. Definition via two-sided displayed categories
• 2. Discreteness and univalence
• 3. Builders and accessors
• 4. Identity and composition of lenses
• 5. Identity and composition laws of lenses

Library UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.Opposites

• 1. The vertical opposite
• 1.1. The construction of the 2-sided displayed category
• 1.2. Isos in the vertical opposite
• 1.3. The univalence of the vertical opposite
• 2. The horizontal opposite
• 2.1. The construction of the 2-sided displayed category
• 2.2. Isos in the horizontal opposite
• 2.3. The univalence of the horizontal opposite

Library UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.ParaTwoSidedDispCat

• 1. The 2-sided displayed category of parametrized morphisms
• 2. Univalence
• 3. Builders and accessors
• 4. Isomorphisms of parametrized morphisms
• 5. The identity parametrized morphism
• 6. The composition of parametrized morphisms
• 7. The left unitor of parametrized morphisms
• 8. The right unitor of parametrized morphisms
• 9. The associator of parametrized morphisms
• 10. Companions and conjoints

Library UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.ProdOfTwosidedDispCat

Library UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.Product

Library UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.Profunctor

Library UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.ProfunctorTwosidedDispCat

• 1. The data of the 2-sided displayed category
• 2. Transport laws for this 2-sided displayed category
• 3. The 2-sided displayed category of profunctors
• 4. Isomorphisms of profunctors
• 5. It is a univalent 2-sided displayed category

Library UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.Reindex

Library UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.Relations

Library UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.Spans

• 1. The definition
• 2. The univalence
• 3. Builders and accessors
• 4. Isomorphisms of spans
• 5. The identity spans
• 6. The composition of spans
• 7. The left unitor of spans
• 8. The right unitor of spans
• 9. The associator of spans
• 10. Companions and conjoints

Library UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.SquaresTwoCat

• 1. Definition via two-sided displayed categories
• 2. Univalence and strictness

Library UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.StructuredCospans

• 1. The 2-sided displayed category of structured cospans
• 2. Builders and accessors for structured cospans
• 3. The univalence of the 2-sided displayed category of structured cospans
• 4. Isos of structured cospans
• 5. The identity structured cospans
• 6. The composition of structured cospans
• 7. The left unitor of structured cospans
• 8. The right unitor of structured cospans
• 9. The associator of structured cospans
• 10. Companions and conjoints
• 11. Functors on structured cospans

Library UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.TwoSidedDispCatOnDispCat

• 1. The 2-sided displayed category
• 2. Isomorphisms in this 2-sided displayed category
• 3. Properties of this 2-sided displayed category

Library UniMath.CategoryTheory.WeakEquivalences.Core

Library UniMath.CategoryTheory.WeakEquivalences.Initial

Library UniMath.CategoryTheory.WeakEquivalences.Mono

Library UniMath.CategoryTheory.WeakEquivalences.Terminal

Library UniMath.CategoryTheory.WeakEquivalences.Creation.BinProducts

Library UniMath.CategoryTheory.WeakEquivalences.Creation.Equalizers

Library UniMath.CategoryTheory.WeakEquivalences.Creation.Pullbacks

Library UniMath.CategoryTheory.WeakEquivalences.LiftPreservation.BinProducts

Library UniMath.CategoryTheory.WeakEquivalences.LiftPreservation.Equalizers

Library UniMath.CategoryTheory.WeakEquivalences.LiftPreservation.Pullbacks

Library UniMath.CategoryTheory.WeakEquivalences.LiftPreservation.SubobjectClassifier

Library UniMath.CategoryTheory.WeakEquivalences.Preservation.Bincoproducts

Library UniMath.CategoryTheory.WeakEquivalences.Preservation.Binproducts

Library UniMath.CategoryTheory.WeakEquivalences.Preservation.Equalizers

Library UniMath.CategoryTheory.WeakEquivalences.Preservation.NNO

Library UniMath.CategoryTheory.WeakEquivalences.Preservation.Pullbacks

Library UniMath.CategoryTheory.WeakEquivalences.Preservation.SubobjectClassifier

Library UniMath.CategoryTheory.WeakEquivalences.Reflection.BinProducts

Library UniMath.CategoryTheory.WeakEquivalences.Reflection.Equalizers

Library UniMath.CategoryTheory.WeakEquivalences.Reflection.Pullbacks

Library UniMath.CategoryTheory.WeakEquivalences.Reflection.SubobjectClassifier

Library UniMath.Combinatorics.BoundedSearch

Library UniMath.Combinatorics.CGraph

• Correspondence graphs
  • Precgraphs.
  • Cgraph morphisms.
  • Equality of cgraph morphisms
  • Weak equivalence between CGraphs and Graphs

Library UniMath.Combinatorics.DecSet

• Decidable sets.

Library UniMath.Combinatorics.Equivalence_Relations

Library UniMath.Combinatorics.FiniteSequences

• Finite sequences
  • Contents
  • Vectors
  • Matrices
  • Sequences
    • Definitions
    • Lemmas

Library UniMath.Combinatorics.FiniteSets

• Finite sets. Vladimir Voevodsky . Apr. - Sep. 2011.
  • Preamble
  • Sets with a given number of elements.
    • Structure of a set with n elements on X defined as a term in ⟦ n ⟧ ≃ X.
    • The property of X to have n elements
  • General finite sets.
    • Finite structure.
    • Finite types.

Library UniMath.Combinatorics.Graph

• Bicategory of graphs
  • Pregraphs.
  • Graphs.
  • Graph morphisms.

Library UniMath.Combinatorics.GraphPaths

Library UniMath.Combinatorics.KFiniteSubtypes

• Kfinite Subtypes

Library UniMath.Combinatorics.KFiniteTypes

Library UniMath.Combinatorics.Lists

• Lists
• Lists over an arbitrary type

Library UniMath.Combinatorics.Maybe

• A simple implementation of the maybe/option monad which does not require category theory.

Library UniMath.Combinatorics.MetricTree

• Metric trees
  • Definitions

Library UniMath.Combinatorics.MoreLists

• Additional definitions, lemmas and notations for lists.
  • Notations for lists.
  • Proofs that cons is injective on both arguments.
  • Several properties for the length of a list.
  • Miscellanea of properties and definitions.
  • The drop operation and related properties.
  • The prefix_remove operation and related properties.

Library UniMath.Combinatorics.StandardFiniteSets

• Standard finite sets . Vladimir Voevodsky . Apr. - Sep. 2011 .
  • Preamble
  • Standard finite sets stn .
  • "Boundary" maps dni : stn n -> stn ( S n ) and their properties.
  • The order-preserving functions sni n i : stn (S n) -> stn n that take the value i twice.
  • Weak equivalences between standard finite sets and constructions on these sets
    • The weak equivalence from stn n to the complement of a point j in stn ( S n ) defined by dni j
    • Weak equivalence from coprod ( stn n ) unit to stn ( S n ) defined by dni i
    • Weak equivalences from stn n for n = 0 , 1 , 2 to empty , unit and bool ( see also the section on nelstruct in finitesets.v ).
    • Weak equivalence between the coproduct of stn n and stn m and stn ( n + m )
    • Weak equivalence from the total space of a family stn ( f x ) over stn n to stn ( stnsum n f )
    • Weak equivalence between the direct product of stn n and stn m and stn n * m
    • Weak equivalences between decidable subsets of stn n and stn x
    • Weak equivalences between hfibers of functions from stn n over isolated points and stn x
    • Weak equivalence between stn n -> stn m and stn ( natpower m n ) ( uses functional extensionality )
    • Weak equivalence from the space of functions of a family stn ( f x ) over stn n to stn ( stnprod n f ) ( uses functional extensionality )
    • Weak equivalence between ( stn n ) ≃ ( stn n ) and stn ( factorial n ) ( uses functional extensionality )
  • Standard finite sets satisfy weak axiom of choice
  • Weak equivalence class of stn n determines n .

Library UniMath.Combinatorics.Tests

• • Test computations.

Library UniMath.Combinatorics.Tuples

• 1. A way to append one element to a tuple
• 2. A couple of lemmas about the elements of an extended tuple
• 3. A lemma specifying when extend_tuple is equal to another tuple
• 4. The tactics

Library UniMath.Combinatorics.Vectors

• Vectors as iterated products.
  • Lemmata about standard finite sets.
  • Vectors.
    • Constructors.
    • Notations.
    • Projections.
    • Some identities for computing el.
    • Extensionality.
    • Weak equivalence with functions.
    • Induction.
    • Map, fold and append.
    • Fusion laws.
    • Other operations on vecs.

Library UniMath.Combinatorics.VectorsTests

• Tests for vectors as iterated products.

Library UniMath.Combinatorics.WellFoundedRelations

Library UniMath.Combinatorics.ZFstructures

Library UniMath.Folds.UnicodeNotations

Library UniMath.Folds.folds_isomorphism

• Definition of FOLDS precat isomorphisms
• Lemmas about FOLDS isomorphisms
• A FOLDS isomorphism is determined by the first family of isos
• Identity FOLDS isomorphism
• Inverse of a FOLDS isomorphism
• Composition of FOLDS isomorphisms
• From isomorphisms to FOLDS isomorphisms
• from FOLDS isomorphism to isomorphism
• from FOLDS isos to isos and back, and the other way round

Library UniMath.Folds.folds_pre_2_cat

• The definition of a FOLDS pre-3-category
  • Objects and a dependent type of morphisms
  • Identity, composition, and equality, given through predicates
  • E is an "equality", i.e. a congruence and equivalence
  • The axioms for identity
  • The axioms for composition
  • A FOLDS pre-3-category is a package of
• FOLDS-2-precategories
• FOLDS-2-isomorphisms
• In FOLDS-2-precats, folds_iso f g <-> E f g
• Univalent FOLDS-2-precategory
• FOLDS precategories
• Univalent FOLDS pre-2-category is a FOLDS precategory
• FOLDS precategory implies univalence

Library UniMath.Folds.folds_precat

• The definition of a FOLDS precategory
  • Objects and a dependent type of morphisms
  • Identity and composition, given through predicates
  • The axioms for identity
• Some lemmas about FOLDS precategories

Library UniMath.Folds.from_precats_to_folds_and_back

• From precategories to FOLDS precategories
• From FOLDS precategories to precategories
• From FOLDS precats to precats to FOLDS precats
• From precats to FOLDS precats to precats
• Some lemmas to pass from comp to compose and back
• Some lemmas to pass from id to identity and back

Library UniMath.Foundations.All

Library UniMath.Foundations.HLevels

• HLevel(n) is of hlevel n+1
  • Weak equivalence between identity types in HLevel and U
  • Hlevel of path spaces
    • The case n = 0
    • The case n = S n'
  • The lemma itself
  • HLevel
• Main theorem: HLevel n is of hlevel S n
  • Aside: Univalence for predicates and hlevels

Library UniMath.Foundations.Init

Library UniMath.Foundations.NaturalNumbers

• Natural numbers and their properties. Vladimir Voevodsky. Apr. - Sep. 2011
  • Contents
  • Preamble
  • Equality and inequality on nat
    • Basic properties of paths on nat and the proofs of isdeceq and isaset for nat.
    • S : nat -> nat is a decidable inclusion.
  • Inequalities on nat.
    • Boolean "less or equal" and "greater or equal" on nat.
    • Semi-boolean "greater" on nat or natgth
    • Semi-boolean "less" on nat or natlth
    • Semi-boolean "less or equal " on nat or natleh
    • Semi-boolean "greater or equal" on nat or natgeh.
    • Simple implications between comparisons
    • Comparison alternatives
    • Mixed transitivities
    • Two comparisons and S
    • Comparision alternatives and S
  • Some properties of plus on nat
    • The structure of the additive abelian monoid on nat
    • Addition and comparisons
    • Comparisons and n -> n + 1
    • Two comparisons and n -> n + 1
    • Comparision alternatives and n -> n + 1
    • Cancellation properties of plus on nat
    • Some properties of minus on nat
    • Comparisons and n -> n - 1
    • Basic algebraic properties of mul on nat.
    • Cancellation properties of mul on nat
    • Multiplication and comparisons
    • Division with a remainder on nat
    • Exponentiation natpower n m ("n to the power m") on nat
    • Factorial on nat
  • The order-preserving functions di i : nat -> nat whose image is the complement of one element i.
  • The order-preserving functions si i : nat -> nat that take the value i twice.

Library UniMath.Foundations.PartA

• Univalent Foundations, Part A
  • Contents
  • Preamble
    • Imports
  • Some standard constructions not using identity types (paths)
    • Canonical functions from empty and to unit
    • Functions from unit corresponding to terms
    • Identity functions and function composition, curry and uncurry
    • Definition of binary operation
    • Iteration of an endomorphism
    • Basic constructions related to the adjoint evaluation function X -> ((X -> Y) -> Y)
    • Pairwise direct products
    • Negation and double negation
    • Logical equivalence
  • Paths and operations on paths
    • Associativity of function composition and mutual invertibility of curry/uncurry
    • Composition of paths and inverse paths
    • Direct product of paths
    • The function maponpaths between paths types defined by a function between ambient types
    • maponpaths for the identity functions and compositions of functions
    • Homotopy between sections
    • Equality between functions defines a homotopy
    • maponpaths for a function homotopic to the identity
    • maponpaths in the case of a projection p with a section s
    • Fibrations and paths - the transport functions
    • A series of lemmas about paths and total2
    • Lemmas about transport adapted from the HoTT library and the HoTT book
    • Homotopies between families and the total spaces
  • First fundamental notions
    • Contractibility iscontr
    • Homotopy fibers hfiber
    • The functions between the hfibers of homotopic functions over the same point
    • Paths in homotopy fibers
    • Coconuses: spaces of paths that begin coconusfromt or end coconustot at a given point
    • The total paths space of a type - two definitions
    • Coconus of a function: the total space of the family of h-fibers
  • Weak equivalences
    • Basics - isweq and weq
    • Weak equivalences and paths spaces (more results in further sections)
    • Adjointness property of a weak equivalence and its inverse
    • Transport functions are weak equivalences
    • Weak equivalences between contractible types (one implication)
    • unit and contractibility
    • Homotopy equivalence is a weak equivalence
    • Some weak equivalences
    • The 2-out-of-3 property of weak equivalences
    • Any function between contractible types is a weak equivalence
    • Composition of weak equivalences
    • The 2-out-of-6 (two-out-of-six) property of weak equivalences
    • Pairwise direct products of weak equivalences
    • Weak equivalence of a type and its direct product with the unit
    • Associativity of total2 as a weak equivalence
    • Associativity and commutativity of direct products as weak equivalences
  • Binary coproducts and their basic properties
    • Distributivity of coproducts and direct products as a weak equivalence
    • Total space of a family over a coproduct
    • Pairwise sum of functions, coproduct associativity and commutativity
    • Coproduct with a "negative" type
    • Coproduct of two functions
    • The equality_cases construction and four applications to ii1 and ii2
    • Bool as coproduct
    • Pairwise coproducts as dependent sums of families over bool
    • Splitting of X into a coproduct defined by a function X -> Y ⨿ Z
    • Some properties of bool
    • Fibrations with only one non-empty fiber
  • Basics about fibration sequences.
    • Fibrations sequences and their first "left shifts"
    • The structures of a complex and of a fibration sequence on a composable pair of functions
    • Construction of the derived fibration sequence
    • Explicit description of the first map in the second derived sequence
    • Fibration sequences based on tpair P z and pr1 : total2 P -> Z ( the "pr1-case" )
    • Fibration sequences based on hfiberpr1 : hfiber g z -> Y and g : Y -> Z (the "g-case")
    • Fibration sequence of h-fibers defined by a composable pair of functions (the "hf-case")
  • Functions between total spaces of families
    • Function fpmap between the total spaces from a function between the bases
    • Homotopy fibers of fpmap
    • The fpmap from a weak equivalence is a weak equivalence
    • Total spaces of families over a contractible base
    • The function on the total spaces from functions on the bases and on the fibers
  • Homotopy fiber squares
    • Homotopy commutative squares
    • Short complexes and homotopy commutative squares
    • Homotopy fiber products
    • Homotopy fiber products and homotopy fibers
    • Homotopy fiber squares
    • Fiber sequences and homotopy fiber squares

Library UniMath.Foundations.PartB

• Univalent Foundations. Vladimir Voevodsky. Feb. 2010 - Sep. 2011.
  • Contents
  • Preamble
  • Basics about h-levels
    • h-levels of types
    • h-levels of functions
  • h -levels of pr1 , fiber inclusions, fibers, total spaces and bases of fibrations
    • h-levelf of pr1
    • h-level of the total space total2
  • Propositions, inclusions and sets
    • Basics about types of h-level 1 - "propositions"
    • Inclusions - functions of h-level 1
    • Basics about types of h-level 2 - "sets"
    • Decidable propositions isdecprop
    • Types with decidable equality
    • Isolated points
    • Decidable types are sets
    • Decidable equality on a sigma type
    • Construction of functions with specified values at a few isolated points
      • bool is a set
  • Splitting of X into a coproduct defined by a function X -> bool

Library UniMath.Foundations.PartC

• Univalent Foundations. Vladimir Voevodsky. Feb. 2010 - Sep. 2011. Port to coq
  • Contents
  • Preamble
    • More results on propositions
  • Isolated points and types with decidable equality.
    • Basic results on complements to a point
    • Decomposition of a type with an isolated point into two parts weqrecompl
    • Theorem saying that recompl commutes up to homotopy with maponcomplweq
    • Recomplement on functions
    • Equivalence between compl T t1 and compl T t2 for isolated t1 t2
    • Transposition of two isolated points
  • Semi-boolean hfiber of functions over isolated points
    • h-fibers of ii1 and ii2
    • ii1 and ii2 map isolated points to isolated points
    • h-fibers of coprodf of two functions
    • Theorem saying that coproduct of two functions of h-level n is of h-level n
    • Theorems about h-levels of coproducts and their component types
    • h-fibers of the sum of two functions sumofmaps f g
    • Theorem saying that the sum of two functions of h-level (S (S n)) is of hlevel (S (S n))
    • The sum of two functions of h-level n with non-intersecting images is of h-level n
    • Coproducts and complements
  • Decidable propositions and decidable inclusions
    • Decidable propositions isdecprop
    • Paths to and from an isolated point form a decidable proposition
    • Decidable inclusions
    • Decidable inclusions and isolated points
    • Decidable inclusions and coprojections

Library UniMath.Foundations.PartD

• Univalent Foundations. Vladimir Voevodsky. Feb. 2010 - Sep. 2011.
  • Contents
  • Preamble
  • Sections of "double fibration" (P : T -> UU) (PP : ∏ t : T, P t -> UU) and pairs of sections
    • General case
    • Functions to a dependent sum (to a total2 )
    • Functions to direct product
  • Homotopy fibers of the map ∏ x, P x -> ∏ x, Q x
    • General case
    • The weak equivalence between section spaces (dependent products) defined by a family of weak equivalences (P x) ≃ (Q x)
    • Composition of functions with a weak equivalence on the right
  • The map between section spaces (dependent products) defined by the map between the bases f : Y -> X
    • General case
    • Composition of functions with a weak equivalence on the left
  • Sections of families over an empty type and over coproducts
    • General case
    • Functions from the empty type
    • Functions from a coproduct
  • Sections of families over contractible types and over total2 (over dependent sums)
    • General case
    • Functions from unit and from contractible types
    • Functions from total2
    • Functions from direct product
  • Theorem saying that if each member of a family is of h-level n then the space of sections of the family is of h-level n.
    • General case
    • Functions to a contractible type
    • Functions to a proposition
    • Functions to an empty type (generalization of isapropneg )
  • Theorems saying that iscontr T , isweq f etc. are of h-level 1
  • Theorems saying that various pr1 maps are inclusions
  • Various weak equivalences between spaces of weak equivalences
    • Composition with a weak quivalence is a weak equivalence on weak equivalences
    • Invertion on weak equivalences as a weak equivalence
  • h-levels of spaces of weak equivalences
    • Weak equivalences to and from types of h-level (S n)
    • Weak equivalences to and from contractible types
    • Weak equivalences to and from propositions
    • Weak equivalences to and from sets
    • Weak equivalences to an empty type
    • Weak equivalences from an empty type
    • Weak equivalences to and from unit
  • Weak auto-equivalences of a type with an isolated point

Library UniMath.Foundations.Preamble

• Introduction. Vladimir Voevodsky . Feb. 2010 - Sep. 2011

Library UniMath.Foundations.Propositions

• Generalities on hProp. Vladimir Voevodsky . May - Sep. 2011 .
  • Contents
  • Preamble
  • To upstream files
  • The type hProp of types of h-level 1
  • The type tildehProp of pairs (P, p : P) where P : hProp
  • Intuitionistic logic on hProp
    • The hProp version of the "inhabited" construction.
    • ishinh and negation neg
    • ishinh and coprod
  • Images and surjectivity for functions between types
    • The two-out-of-three properties of surjections
    • A function between types which is an inclusion and a surjection is a weak equivalence
    • Intuitionistic logic on hProp.
    • Associativity and commutativity of hdisj and hconj up to logical equivalence
    • Proof of the only non-trivial axiom of intuitionistic logic for our constructions. For the full list of axioms see e.g. http://plato.stanford.edu/entries/logic-intuitionistic/
    • Negation and quantification.
    • Negation and conjunction ("and") and disjunction ("or").
    • Property of being decidable and hdisj ("or").
    • The double negation version of hinhabited (does not require RR1).
  • Univalence for hProp

Library UniMath.Foundations.Sets

• Generalities on hSet. Vladimir Voevodsky. Feb. - Sep. 2011
  • Contents
  • Preamble
  • The type of sets i.e. of types of h-level 2 in UU
    • hProp as a set
    • Booleans as a set
  • Types X which satisfy "weak" axiom of choice for all families P : X -> UU
  • The type of monic subtypes of a type (subsets of the set of connected components)
    • General definitions
    • Direct product of two subtypes
    • A subtype with paths between any two elements is an hProp.
  • Relations on types (or equivalently relations on the sets of connected components)
    • Relations and boolean relations
    • Standard properties of relations
    • Elementary implications between properties of relations
    • Standard properties of relations and logical equivalences
    • Preorderings, partial orderings, and associated types.
    • Eqivalence relations and associated types.
    • Direct product of two relations
    • Negation of a relation and its properties
    • Boolean representation of decidable equality
    • Boolean representation of decidable relations
    • Restriction of a relation to a subtype
    • Equivalence classes with respect to a given relation
    • Direct product of equivalence classes
  • Surjections to sets are epimorphisms
  • Epimorphisms are surjections to sets
  • Universal property enjoyed by surjections
  • Set quotients of types.
    • Setquotient defined in terms of equivalence classes
    • Universal property of seqtquot R for functions to sets satisfying compatibility condition iscomprelfun
    • Functoriality of setquot for functions mapping one relation to another
    • Universal property of setquot for predicates of one and several variables
    • The case when setquotfun is a surjection, inclusion or a weak equivalence
    • setquot with respect to the product of two relations
    • Universal property of setquot for functions of two variables
    • Functoriality of setquot for functions of two variables mapping one relation to another
    • Set quotients with respect to decidable equivalence relations have decidable equality
    • Relations on quotient sets
    • Subtypes of quotients and quotients of subtypes
    • The set of connected components of type.
  • Set quotients. Construction 2.
    • Functions compatible with a relation
    • The quotient set of a type by a relation.
    • Universal property of seqtquot2 R for functions to sets satisfying compatibility condition iscomprelfun
    • Weak equivalence from R x x' to paths (setquot2pr R x) (setquot2pr R x')
  • Consequences of univalence

Library UniMath.Foundations.Tests

Library UniMath.Foundations.UnivalenceAxiom

• • Proof of the functional extensionality for functions from univalence
  • Transport theorem.
    • Deduction of functional extensionality for dependent functions (sections) from functional extensionality of usual functions

Library UniMath.Foundations.UnivalenceAxiom2

Library UniMath.HomologicalAlgebra.CohomologyComplex

• Cohomology of complexes
  • Contents
• Cohomology functor
  • Introduction
  • Cohomology complex
  • Cohomology morphism
  • Cohomology functor
• Alternative definition of Cohomology complex
  • Introduction
• Definition of quasi-isomorphisms
  • Introduction
• Cohomology functor is an additive functor
  • Introduction
• CohomologyFunctor factors through naive homotopy category
  • Introduction
  • Homotopic maps are mapped to equal morphisms by the cohomology functor C(A) -> C(A)
  • Structure for the image of a morphism to make type cheking faster
  • Construction of the functor and commutativity
  • Additivity of CohomologyFunctorH
  • Quasi-isomorphisms in K(A)
• Complex of kernels and complex of cokernels
  • Construction of kernel and cokernel complexes
    • Complex of kernels
    • Complex of cokernels
  • Construction of h^i and isomorphisms with cohomology
    • Uniqueness and existence of h^i
    • Kernel and cohomology
    • Cokernel and cohomology

Library UniMath.HomologicalAlgebra.Complexes

• The category of complexes over an additive category
  • Contents
• Definition of complexes
  • Introduction
  • Basics of complexes
  • Direct sums
• Transport of morphisms indexed by integers
  • Construction of a complexes with one object
  • Construction of a complex with a given object in two adjacent positions
    • Construction of the complex ... --> 0 --> X -Id-> X --> 0 --> ...
    • Morphism from AcyclicComplexFromObject to a complex
    • Morphism from AcyclicComplexFromObject to a complex
• The category of complexes
  • Introduction
  • Construction of the category of complexes
  • Monic of complexes is indexwise monic
  • Epi of complexes is indexwise epi
  • An morphism in complexes is an isomorphism if it is so indexwise
• The category of complexes over CategoryWithAdditiveStructure is CategoryWithAdditiveStructure
  • Introduction
• Complexes over Abelian is Abelian
  • Introduction
  • Kernels in Complexes over Abelian
    • Construction of the kernel object
    • Construction of the KernelArrow
    • isEqualizer
    • Kernels
  • Cokernels in Complexes over Abelian
    • Cokernel complex
    • CokernelArrow
    • Cokernel
  • Monics are kernels
    • Kernel complex from Monic
  • Epis are Cokernels of kernels
    • EpisCokernelsData
  • Complexes over Abelian is Abelian
• Transport binary direct sums

Library UniMath.HomologicalAlgebra.KA

• K(A), the naive homotopy category of C(A)
  • Contents
• Homotopies of complexes and K(A), the naive homotopy category of A.
  • Introduction
  • Naive homotopy category

Library UniMath.HomologicalAlgebra.KAPreTriangulated

• K(A) is a pretriangulated category
• K(A) with a structure of a pretriangulated category
  • Introduction
  • Trivial triangle is distinguished
  • Rotation of distinguished triangles
  • Inverse rotation of distinguished triangles
  • Completion to distinguished triangle
  • Extension of squares
  • Closed under isomorphisms

Library UniMath.HomologicalAlgebra.KATriangulated

• K(A) is a triangulated category
• K(A) as a triangulated category

Library UniMath.HomologicalAlgebra.MappingCone

• Mapping cones in C(A)
  • Contents
• Mapping cone
  • Introduction
• Results on C(id)
  • Introduction
• Rotation
  • Introduction
• Inverse rotation
  • Introduction
• Extension of morphisms
  • Introduction
• Octahedral axiom for K(A)

Library UniMath.HomologicalAlgebra.MappingCylinder

• Mapping cylinder in C(A)
  • Introduction
• Mapping cylinder
  • Introduction
• Let f : X -> Y, then Y is isomorphic to Cyl(f) in K(A)
  • Introduction

Library UniMath.HomologicalAlgebra.TranslationFunctors

• Translation functors
• Translation funtor for C(A) and for K(A)
  • Introduction
  • Translation functor for C(A)
    • Translation functor preserves homotopies
    • Inverse of the translation functor functor
    • InvTranslation functor preserves homotopies
  • Translation functor is an isomorphism, with inverse the inverse translation.
    • Natural transformation for equivalence consisting of the translations
  • Translation functor for K(A)
    • Image for the translation functor
    • Construction of the functor
  • Inverse translation in K(A)
    • Construction of the functor
  • Translation equivalence for K(A)

Library UniMath.HomologicalAlgebra.Triangulated

• Triangulated categories
  • Contents
• Triangulated categories
  • Introduction
• Basic notions
  • Introduction
  • Triangles
  • Morphisms of triangles
    • Composition of morphisms is a morphism
  • is isomorphism
    • Composition of is isomorphism is isomorphism
    • Construction of an inverse and the fact that it is isomorphism
  • Isomorphisms of triangles
    • Composition of isomorphisms
    • Inverse of an isomorphism
    • Identity isomorphism
  • Trivial triangle, rotated triangle, and inv rotated triangle
    • X -Id-> X -> 0 -> X1
    • See introduction to this section for the diagram
  • Rotation and inverse rotation of a morphism
    • See the diagram in the introduction
  • Cone data
• Data for pretriangulated categories
  • PreTriangData
• Distinguished triangles and extentions
  • Inroduction
  • Distinguished triangles
  • Extensions
• PreTriangulated categories
  • • isPreTriang
    • Accessor functions
  • Pretriangulated category
• Triangulated categories
  • Octahedral data
  • Triangulated category
• Rotations and inverse rotations of morphisms, Extensions, and DTris
  • iso D InvRot (Rot D) and iso D Rot (InvRot D)
  • Extension of morphisms at 2 and 1
  • Rotations of DTris
• Composition is zero
  • Introduction
  • Introduction
  • Introduction
  • Change triangles in extension using isomorphisms
  • Change triangles in octa using isomorphisms

Library UniMath.Induction.FunctorAlgebras_legacy

• • Category of algebras of an endofunctor
  • This category is saturated if the base category is
  • Lambek's lemma: If (A,a) is an initial F-algebra then a is an iso
  • The natural numbers are intial for X ↦ 1 + X

Library UniMath.Induction.FunctorCoalgebras_legacy

Library UniMath.Induction.ImpredicativeInductiveSets

• • Impredicative Construction of Inductive Types that are Sets and Eliminate into Sets

Library UniMath.Induction.PolynomialAlgebras2Cells

• 2-cells of algebras over a polynomial functor.

Library UniMath.Induction.PolynomialFunctors

• • Polynomial functors

Library UniMath.Induction.M.Chains

• Limits of chains and cochains in the precategory of types

Library UniMath.Induction.M.ComputationalM

• • Refinement of M-types

Library UniMath.Induction.M.Core

• • M-types

Library UniMath.Induction.M.Limits

• Limits in the precategory of types

Library UniMath.Induction.M.Uniqueness

• • Uniqueness of M-types

Library UniMath.Induction.W.Core

Library UniMath.Induction.W.Fibered

• • Fibered algebras

Library UniMath.Induction.W.Naturals

• • Natural numbers

Library UniMath.Induction.W.Uniqueness

• • Uniqueness of W-types

Library UniMath.Induction.W.Wtypes

• Axiomatic definition of a W-type.
  • Axiomatic definition of a W-Type.
  • Constructor.
  • Accessors.
  • Derived rules.
    • First-order eta rule.
    • Second-order eta rule.

Library UniMath.Induction.W.WtypesAsW

• From axiomatic W-types to W-types as initial algebras.

Library UniMath.Ktheory.GrothendieckGroup

Library UniMath.ModelCategories.Examples

Library UniMath.ModelCategories.Helpers

Library UniMath.ModelCategories.Lifting

Library UniMath.ModelCategories.ModelCategory

Library UniMath.ModelCategories.MorphismClass

Library UniMath.ModelCategories.NWFS

Library UniMath.ModelCategories.NWFSisWFS

Library UniMath.ModelCategories.Retract

Library UniMath.ModelCategories.WFS

Library UniMath.ModelCategories.WeakEquivalences

Library UniMath.ModelCategories.Generated.FFMonoidalStructure

Library UniMath.ModelCategories.Generated.GenericFreeMonoid

Library UniMath.ModelCategories.Generated.GenericFreeMonoidSequence

Library UniMath.ModelCategories.Generated.LNWFSClosed

Library UniMath.ModelCategories.Generated.LNWFSCocomplete

Library UniMath.ModelCategories.Generated.LNWFSHelpers

Library UniMath.ModelCategories.Generated.LNWFSMonoidalStructure

Library UniMath.ModelCategories.Generated.LNWFSSmallnessReduction

Library UniMath.ModelCategories.Generated.LiftingWithClass

Library UniMath.ModelCategories.Generated.MonoidalHelpers

Library UniMath.ModelCategories.Generated.OneStepMonad

Library UniMath.ModelCategories.Generated.OneStepMonadSmall

Library UniMath.ModelCategories.Generated.SmallObjectArgument

Library UniMath.MoreFoundations.All

Library UniMath.MoreFoundations.AlternativeProofs

• • An alternative proof of total2_paths_equiv

Library UniMath.MoreFoundations.AxiomOfChoice

• Axiom of choice
  • Preliminaries
  • Characterize equivalence relations on bool
  • Statements of Axiom of Choice
  • Implications between forms of the Axiom of Choice
  • The Axiom of Choice implies a type receives a surjective map from a set
  • The Axiom of Choice implies the Law of the Excluded Middle

Library UniMath.MoreFoundations.Bool

• Booleans

Library UniMath.MoreFoundations.DecidablePropositions

• Miscellaneous lemmas
• The Law of Excluded Middle, and equivalent principles
• Complementary pairs
• Decidable Propositions

Library UniMath.MoreFoundations.DoubleNegation

Library UniMath.MoreFoundations.Equivalences

• Equivalences

Library UniMath.MoreFoundations.Interval

• A construction of the interval using propositional truncation
  • An easy proof of functional extensionality for sections using the interval, which is derived

Library UniMath.MoreFoundations.MoreEquivalences

• Equivalences

Library UniMath.MoreFoundations.Nat

• Recursion property
• Discernment family on ℕ
• Distance function on ℕ
• Miscellaneous arithmetic lemmas
• Bounded quantification
  • Some results on bounded quantification
  • Accessibility - the least element of an inhabited decidable subset of nat

Library UniMath.MoreFoundations.NegativePropositions

• • • Propositions equivalent to negations of propositions

Library UniMath.MoreFoundations.NoInjectivePairing

• Preliminaries
• Refutation of Injective Pairing
• Injective Pairing <-> Uniqueness of Identity Proofs

Library UniMath.MoreFoundations.Notations

• Notations
  • Variants on paths and coconus
  • Squashing

Library UniMath.MoreFoundations.NullHomotopies

• • Null homotopies, an aid for proving things about propositional truncation

Library UniMath.MoreFoundations.Orders

• • More results on types of ordering
• Preorders
• Strong orders
• Reverse orders

Library UniMath.MoreFoundations.PartA

• Generalisations of maponpaths
  • Pointed types
  • Paths
  • Pairs
  • Paths between pairs
  • Projections from pair types
  • Maps from pair types
  • Paths in coproducts
  • Sections and functions
  • Transport
    • Double transport
    • Transport a pair
  • h-levels and paths
  • Surjectivity

Library UniMath.MoreFoundations.PartD

Library UniMath.MoreFoundations.PathsOver

• • Paths over paths in families of types

Library UniMath.MoreFoundations.Propositions

• • Factoring maps through squash
  • Connected types

Library UniMath.MoreFoundations.QuotientSet

Library UniMath.MoreFoundations.Sets

• • More results on sets
  • Contents
  • Other universal properties for setquot
  • The trivial equivalence relation on the unit type
  • The equivalence relation of being in the same fiber
  • Subsets
  • Minimal equivalence relations
• Additional lemmas on binary relations

Library UniMath.MoreFoundations.StructureIdentity

• Structure identity
  • abstract the proof of Poset_rect for use in multiple situations

Library UniMath.MoreFoundations.Subtypes

Library UniMath.MoreFoundations.Tactics

Library UniMath.MoreFoundations.Test

• Tests
  • Bool.v

Library UniMath.MoreFoundations.Univalence

• Additional results about univalence

Library UniMath.MoreFoundations.WeakEquivalences

• Weak equivalences
  • Contents
  • Direct products

Library UniMath.NumberSystems.Integers

• Generalities on the type of integers and integer arithmetic. Vladimir Voevodsky . Aug. - Sep. 2011.
  • Preamble
  • The commutative ring hz of integres
    • General definitions
    • Properties of equlaity on hz
    • hz is a non-zero ring
    • Properties of addition and subtraction on hz
    • Properties of multiplication on hz
  • Definition and properties of "greater", "less", "greater or equal" and "less or equal" on hz .
    • Definitions and notations
    • Decidability
    • Properties of individual relations
    • Simple implications between comparisons
    • Comparison alternatives
    • Mixed transitivities
    • Addition and comparisons
    • Properties of hzgth in the terminology of algebra1.v (continued below)
    • Negation and comparisons
    • Multiplication and comparisons
    • hz as an integral domain
    • Comparisons and n -> n + 1
    • Two comparisons and n -> n + 1
    • Comparsion alternatives and n -> n + 1
    • Operations and comparisons on hz and natnattohz
    • Canonical rig homomorphism from nat to hz
    • Addition and subtraction on nat and hz
    • Absolute value on hz
    • Some common equalities on integers
    • hz is an archimedean ring
      • hz -> abgr, 1 ↦ x, n ↦ x + x + ... + x (n times), hz_abmonoid_abelian_group_morphism

Library UniMath.NumberSystems.NaturalNumbersAlgebra

• Facts about the natural numbers that depend on definitions from algebra
  • • Submonoid of non-zero elements in nat
    • nat as a commutative rig
    • Properties of comparisons in the terminology of algebra1.v
    • nat is an archimedean rig

Library UniMath.NumberSystems.NaturalNumbers_le_Inductive

• Natural numbers and their properties. Vladimir Voevodsky. Apr. - Sep. 2011
  • Contents
  • Preamble
  • Inductive types le with values in UU.
    • A generalization of le and its properties.
    • Inductive types le with values in UU are in hProp
    • Comparison between le with values in UU and natleh.

Library UniMath.NumberSystems.RationalNumbers

• Generalities on the type of rationals and rational arithmetic. Vladimir Voevodsky . Aug. - Sep. 2011.
  • Preamble
  • The commutative ring hq of integres
    • General definitions
    • Properties of equality on hq
    • Properties of addition and subtraction on hq
    • Properties of multiplication on hq
    • Multiplicative inverse and division on hq
  • Definition and properties of "greater", "less", "greater or equal" and "less or equal" on hq .
    • Definitions and notations
    • Decidability
    • Properties of individual relations
  • hq is archimedean
    • Simple implications between comparisons
    • Comparison alternatives
    • Mixed transitivities
    • Addition and comparisons
    • Properties of hqgth in the terminology of algebra1.v
    • Negation and comparisons
    • Multiplication and comparisons
    • Cancellation properties of multiplication on hq
    • Positive rationals
    • Canonical ring homomorphism from hz to hq
    • Integral part of a rational

Library UniMath.NumberSystems.Tests

Library UniMath.OrderTheory.DCPOs

Library UniMath.OrderTheory.Posets

Library UniMath.OrderTheory.Preorders

• 1. The preorder structure on a subtype
• 2. Down- and up-types
• 3. Downward closed subsets
• 4. The downward closure

Library UniMath.OrderTheory.DCPOs.AlternativeDefinitions.Dcpo

• Directed complete posets and least fixed points
  • Contents
  • Least upper bounds
  • Directed families
  • Directed complete posets (dcpos)
  • Morphisms of dcpos
  • The morphisms between two dcpos form a dcpo with the pointwise order.
  • Dcpos with bottom
  • The least fixed point

Library UniMath.OrderTheory.DCPOs.AlternativeDefinitions.FixedPointTheorems

• Fixed-point theorems on posets
  • Overview
  • Background material
    • Partial orders
    • HProp logic
    • Hsubtypes
  • Completeness properties
  • Upper bounds, completeness, etc in sub-posets
  • Function posets
  • Classes of maps
  • Fixpoints of endofunctions
  • The (Knaster–)Tarski fixpoint theorems
  • Bourbaki-Witt

Library UniMath.OrderTheory.DCPOs.Basis.Algebraic

Library UniMath.OrderTheory.DCPOs.Basis.Basis

Library UniMath.OrderTheory.DCPOs.Basis.CompactBasis

Library UniMath.OrderTheory.DCPOs.Basis.Continuous

Library UniMath.OrderTheory.DCPOs.Core.Basics

Library UniMath.OrderTheory.DCPOs.Core.CoordinateContinuity

Library UniMath.OrderTheory.DCPOs.Core.DirectedSets

Library UniMath.OrderTheory.DCPOs.Core.FubiniTheorem

Library UniMath.OrderTheory.DCPOs.Core.IntrinsicApartness

Library UniMath.OrderTheory.DCPOs.Core.ScottContinuous

Library UniMath.OrderTheory.DCPOs.Core.ScottTopology

• 7. Empty and top sets are Scott open
• 9. More examples of Scott open sets
  • 9.1. Intersection
  • 9.2. Type-indexed unions
  • 9.3. Exponentials
  • 9.4. Binary unions

Library UniMath.OrderTheory.DCPOs.Core.WayBelow

Library UniMath.OrderTheory.DCPOs.Elements.Maximal

• 1. Maximal elements
• 2. Hausdorff separated elements
• 3. Properties of Hausdorff separated elements
• 4. Hausdorff separatedness in continuous DCPOs
• 5. Strongly maximal elements
• 6. Strongly maximal elements are sharp
• 7. The intrinsic apartness relation on strongly maximal elements
• 8. In a continuous DCPO, strongly maximal elements are maximal
• 9. A simplified strong maximality condition in a continuous DCPO,
• 10. Apartness for strongly maximal elements is Hausdorff separatedness

Library UniMath.OrderTheory.DCPOs.Elements.Sharp

Library UniMath.OrderTheory.DCPOs.Examples.BinaryProducts

• 1. Upperbounds in the product
• 2. The DCPO
• 3. The first projection
• 4. The second projection
• 5. Pairing and (tensor) products of functions
• 6. Swap & associativity functions
• 7. Lemmas on upperbounds in the product
• 8. A basis for the product
• 9. Products of Scott-open sets
• 10. Strongly maximal elements in products

Library UniMath.OrderTheory.DCPOs.Examples.BinarySums

Library UniMath.OrderTheory.DCPOs.Examples.Discrete

Library UniMath.OrderTheory.DCPOs.Examples.Equalizers

Library UniMath.OrderTheory.DCPOs.Examples.Exponentials

Library UniMath.OrderTheory.DCPOs.Examples.Fixpoints

Library UniMath.OrderTheory.DCPOs.Examples.IdealCompletion

• 6. Hausdorff separatedness in the ideal completion

Library UniMath.OrderTheory.DCPOs.Examples.Products

Library UniMath.OrderTheory.DCPOs.Examples.Propositions

Library UniMath.OrderTheory.DCPOs.Examples.SubDCPO

Library UniMath.OrderTheory.DCPOs.Examples.Sums

Library UniMath.OrderTheory.DCPOs.Examples.Unit

Library UniMath.OrderTheory.DCPOs.FixpointTheorems.LeastFixpoint

Library UniMath.OrderTheory.DCPOs.FixpointTheorems.Pataraia

Library UniMath.OrderTheory.Lattice.Boolean

• Boolean algebras

Library UniMath.OrderTheory.Lattice.Bounded

• Bounded lattices

Library UniMath.OrderTheory.Lattice.Complement

• Complements

Library UniMath.OrderTheory.Lattice.CompleteHeyting

• 1. Complete Heyting algebra
• 2. Operations of complete Heyting algebras
• 3. Laws for complete Heyting algebras
• 4. Greatest lower bounds for complete Heyting algebras
• 5. Complete Heyting algebras from greatest upper bounds
• 6. Bases for complete Heyting algebras
• 7. Complete Boolean algebras

Library UniMath.OrderTheory.Lattice.DerivedLawsCompleteHeyting

Library UniMath.OrderTheory.Lattice.Distributive

• Distributive lattices

Library UniMath.OrderTheory.Lattice.Heyting

• Heyting algebras

Library UniMath.OrderTheory.Lattice.Lattice

• Lattice
  • Definition
  • Partial order in a lattice
  • Lattice with a strong order
  • Lattice with a total order
  • Lattice in an abmonoid
  • Truncated minus
  • lattice and weq
    • Definition
    • Value of Lle
    • Lattice with strong order
    • Lattice with a decidable order
  • lattice in abmonoid
    • lattice with a strong order in abmonoidfrac
    • lattice with a decidable order in abmonoidfrac

Library UniMath.OrderTheory.Lattice.Examples.Bool

• Lattice structure on boolset

Library UniMath.OrderTheory.Lattice.Examples.FromPartialOrder

• 1. Minimum and maximum operations in posets
• 2. Lattices from posets

Library UniMath.OrderTheory.Lattice.Examples.RegularElements

• 1. Regular elements
• 2. Examples of regular elements
  • 2.1. Top and bottom
• 2.2. The double negation
  • 2.3. Negation of regular elements
  • 2.4. Conjunction and disjunction
  • 2.5. Greatest lower bounds
• 3. The lattice of regular elements
• 4. The bounded lattice of regular elements
• 5. The complete lattice of regular elements
• 6. Least upper bounds of regular elements
• 7. Exponentials
• 8. The complete Boolean algebra of regular elements

Library UniMath.OrderTheory.Lattice.Examples.ScottOpen

• 1. Lattice operations
• 2. Top and bottom element
• 3. Suprema
• 4. Exponentials
• 5. The complete Heyting algebra of Scott open sets
• 6. A basis for this complete Heyting algebra
• 7. A basis for the Scott open sets in the rounded ideal completion

Library UniMath.OrderTheory.Lattice.Examples.Sieves

• 1. Sieves
• 2. Operations on sieve
• 3. The Heyting algebra of sieves
• 4. Coverages
• 5. Closed sieves
• 6. Operations on closed sieves
• 7. The complete Heyting algebra of closed sieves

Library UniMath.OrderTheory.Lattice.Examples.Subsets

• Lattice of subsets

Library UniMath.OrderTheory.Lattice.Examples.Trivial

Library UniMath.OrderTheory.OrderedSets.OrderedSets

• Ordered sets
• computably ordered sets

Library UniMath.OrderTheory.OrderedSets.WellOrderedSets

• Well Ordered Sets
  • Totally ordered subsets of a set
    • Adding a point on top of a totally ordered subset
  • Well ordered subsets of a set
  • The union of a chain of totally ordered subsets
  • The union of a chain of well ordered subsets
  • Choice functions
  • The guided well ordered subsets form a chain
  • The proof of the well ordering theorem of Zermelo
  • Well ordered sets

Library UniMath.OrderTheory.Posets.Basics

Library UniMath.OrderTheory.Posets.LiftPoset

Library UniMath.OrderTheory.Posets.MonotoneFunctions

Library UniMath.OrderTheory.Posets.PointedPosets

Library UniMath.OrderTheory.Posets.PosetSum

Library UniMath.OrderTheory.Posets.QuotientPoset

Library UniMath.OrderTheory.Posets.Subposets

Library UniMath.OrderTheory.Posets.Examples.StandardFiniteSet

• 1. The partially ordered set stn n

Library UniMath.OrderTheory.Prebilattice.Distributive

Library UniMath.OrderTheory.Prebilattice.Interlaced

Library UniMath.OrderTheory.Prebilattice.Prebilattice

Library UniMath.OrderTheory.Prebilattice.PrebilatticeDisplayedCat

Library UniMath.OrderTheory.Prebilattice.Product

Library UniMath.OrderTheory.Prebilattice.Examples.FOUR

Library UniMath.PAdics.fps

• • I. Summation in a commutative ring
• II. Reindexing along functions i : nat -> nat which are
• III. Formal Power Series
• IV. Apartness relation on formal power series

Library UniMath.PAdics.frac

• I. The field of fractions for an integrable domain with an apartness relation

Library UniMath.PAdics.lemmas

• Notation, terminology
• I. Lemmas on natural numbers
• II. Lemmas on rings
• III. Lemmas on hz
• IV. Generalities on apartness relations
• V. Apartness relations on rings
• VI. Lemmas on logic

Library UniMath.PAdics.padics

• I. Several basic lemmas
• II. The carrying operation and induced equivalence relation on
  • Some preparation for parts III/IV that does not depend on a prime number
  • Definition of p-adic integers
• III. The apartness relation on p-adic integers
• IV. The apartness domain of p-adic integers and the Heyting field of p-adic numbers

Library UniMath.PAdics.z_mod_p

• I. Divisibility and the division algorithm
• II. QUOTIENTS AND REMAINDERS
• III. THE EUCLIDEAN ALGORITHM
• IV. Bezout's lemma and the commutative ring Z/pZ
• V. Z/nZ

Library UniMath.Paradoxes.GirardsParadox

Library UniMath.RealNumbers.DecidableDedekindCuts

• A library about decidable Dedekind Cuts
  • Definition

Library UniMath.RealNumbers.DedekindCuts

• Usual constructive Dedekind cuts
  • Usual definitions
  • Equivalence between these two definitions
  • Equivalence of Dcuts with usual definitions

Library UniMath.RealNumbers.Fields

• Additional theorems about fields
  • Projections for fld
  • fld and the other structures

Library UniMath.RealNumbers.NonnegativeRationals

• Definition of non-negative rational numbers
  • Equality and order on non-negative rational numbers
  • hnnq is a half field
• Exportable definitions and theorems
  • Definitions
    • Correctness of definitions
  • Theorems about order
    • Decidability
    • Basic theorems about order
    • Order and 0
  • Theorems about algebra
    • Addition
    • Substraction
    • Multiplication
    • Multiplicative Inverse
    • Division
  • NQhalf
  • NQmax
  • NQmin
  • intpart
  • Opacify

Library UniMath.RealNumbers.NonnegativeReals

• Definition of Dedekind cuts for non-negative real numbers
  • Definition of Dedekind cuts
  • Dcuts is a effectively ordered set
  • Equivalence on Dcuts
  • Apartness on Dcuts
    • Various theorems about order
• Algebraic structures on Dcuts
  • From non negative rational numbers to Dedekind cuts
  • Addition in Dcuts
  • Multiplication in Dcuts
  • Multiplicative inverse in Dcuts
  • Algebraic properties
  • Structures
  • Additional useful definitions
    • Dcuts_minus
    • Dcuts_max
    • Dcuts_min
    • Dcuts_half
  • Locatedness
  • Limits of Cauchy sequences
  • Dedekind Completeness
• Definition of non-negative real numbers
  • Relations
  • Constants and Functions
  • Special functions
  • Theorems
  • Compatibility with NonnegativeRationals
  • NonnegativeRationals is dense in NonnegativeReals
  • Archimedean property
  • Completeness

Library UniMath.RealNumbers.Prelim

• Additional theorems and definitions
  • for RationalNumbers.v

Library UniMath.RealNumbers.Reals

• A library about decidable Real Numbers
  • Definition
    • commring
    • Constants and Operations
    • Order
    • Appartness
  • hr_abs
  • Archimedean
  • Completeness
• Interface for Reals
  • Operations and relations
  • NRNRtoR and RtoNRNR
  • Theorems about apartness and order
  • Algrebra
  • Rabs

Library UniMath.RealNumbers.Sets

• Additional theorems for Sets.v
• Partially-defined inverse functions
• Effective Orders
  • Constructive Total Effective Order
  • Complete Ordered Space

Library UniMath.Semantics.EnrichedEffectCalculus.ContinuationModel

Library UniMath.Semantics.EnrichedEffectCalculus.CopowerModel

Library UniMath.Semantics.EnrichedEffectCalculus.EECModel

Library UniMath.Semantics.LinearLogic.LafontCategory

Library UniMath.Semantics.LinearLogic.LiftingModel

Library UniMath.Semantics.LinearLogic.LinearCategory

Library UniMath.Semantics.LinearLogic.LinearCategoryEilenbergMooreAdjunction

Library UniMath.Semantics.LinearLogic.LinearNonLinear

Library UniMath.Semantics.LinearLogic.LinearToLinearNonLinear

Library UniMath.Semantics.LinearLogic.RelationalModel

• 1. The cofree comonoid on a set
• 2. Every comonoid in `REL` gives rise to a monoid in `SET`
• 3. The universal property of the cofree comonoid in `REL`
• 4. The relational model of linear logic

Library UniMath.SubstitutionSystems.ActionBasedStrengthOnHomsInBicat

Library UniMath.SubstitutionSystems.ActionScenarioForGenMendlerIteration_alt

Library UniMath.SubstitutionSystems.ApplicationsGenMendlerIteration_alt

Library UniMath.SubstitutionSystems.BinProductOfSignatures

• Definition of the data of the product of two signatures
• Proof of the laws of the product of two signatures

Library UniMath.SubstitutionSystems.BinSumOfSignatures

• Definition of the data of the sum of two signatures
• Proof of the laws of the sum of two signatures

Library UniMath.SubstitutionSystems.BindingSigToMonad

• Definition of binding signatures
• Translation from a binding signature to a monad
  • Binding signature to a signature with strength
  • Construction of initial algebra for a signature with strength
  • Construction of datatype specified by a binding signature
  • Signature with strength and initial algebra to a HSS
  • Function from binding signatures to monads
• Specialized versions of some of the above functions for HSET
  • Binding signature to signature with strength for HSET
  • Construction of initial algebra for a signature with strength for HSET
  • Binding signature to a monad for HSET

Library UniMath.SubstitutionSystems.BindingSigToMonad_actegorical

Library UniMath.SubstitutionSystems.CCS

Library UniMath.SubstitutionSystems.CCS_alt

Library UniMath.SubstitutionSystems.ConstructionOfGHSS

Library UniMath.SubstitutionSystems.EquivalenceLaxLineatorsHomogeneousCase

Library UniMath.SubstitutionSystems.EquivalenceSignaturesWithActegoryMorphisms

Library UniMath.SubstitutionSystems.Forests

Library UniMath.SubstitutionSystems.FromBindingSigsToMonads_Summary

Library UniMath.SubstitutionSystems.GenMendlerIteration

• Generalized Iteration in Mendler-style
• Specialized Mendler Iteration
• Fusion law for Generalized Iteration in Mendler-style

Library UniMath.SubstitutionSystems.GenMendlerIteration_alt

• Generalized Iteration in Mendler-style
• Specialized Mendler Iteration
• Fusion law for Generalized Iteration in Mendler-style

Library UniMath.SubstitutionSystems.GeneralizedSubstitutionSystems

Library UniMath.SubstitutionSystems.Lam

• Definition of a "model" of the flattening arity in pure lambda calculus
• Uniqueness of the bracket operation
• Specification of a morphism from lambda calculus with flattening to pure lambda calculus

Library UniMath.SubstitutionSystems.LamFromBindingSig

• The lambda calculus from a binding signature

Library UniMath.SubstitutionSystems.LamHSET

Library UniMath.SubstitutionSystems.LamSignature

Library UniMath.SubstitutionSystems.LiftingInitial

Library UniMath.SubstitutionSystems.LiftingInitial_alt

Library UniMath.SubstitutionSystems.MLTT79

Library UniMath.SubstitutionSystems.ModulesFromSignatures

• • Some variables and assumptions

Library UniMath.SubstitutionSystems.MonadicSubstitution_alt

Library UniMath.SubstitutionSystems.MonadsFromSubstitutionSystems

• • Some variables and assumptions
  • Derivation of the monad laws from a heterogeneous substitution system for signature with strength H
    • Proof of the first monad law
    • Proof of the second monad law
    • Proof of the third monad law via transitivity
  • A functor from hss to monads
    • The functor from hss to monads is faithful, i.e. forgets at most structure

Library UniMath.SubstitutionSystems.MonadsMultiSorted

Library UniMath.SubstitutionSystems.MonadsMultiSorted_alt

Library UniMath.SubstitutionSystems.MultiSorted

• Definition of multisorted binding signatures
• Construction of an endofunctor on HSET/sort,HSET/sort from a multisorted signature
• Construction of the strength for the endofunctor on HSET/sort,HSET/sort derived from a
• Proof that the functor obtained from a multisorted signature is omega-cocontinuous

Library UniMath.SubstitutionSystems.MultiSortedBindingSig

Library UniMath.SubstitutionSystems.MultiSortedEmbeddingIndCoindHSET

Library UniMath.SubstitutionSystems.MultiSortedMonadConstruction

• Definition of multisorted binding signatures
• Construction of a monad from a multisorted signature
  • Function from multisorted binding signatures to monads

Library UniMath.SubstitutionSystems.MultiSortedMonadConstruction_actegorical

• Construction of a monad from a multisorted signature

Library UniMath.SubstitutionSystems.MultiSortedMonadConstruction_alt

• Construction of a monad from a multisorted signature
  • Function from multisorted binding signatures to monads

Library UniMath.SubstitutionSystems.MultiSortedMonadConstruction_coind_actegorical

• Construction of a monad from a multisorted signature

Library UniMath.SubstitutionSystems.MultiSorted_actegorical

• Construction of the lineator for the endofunctor on C^sort,C^sort
  • • we now adapt the definitions to MultiSortedSigToFunctor'

Library UniMath.SubstitutionSystems.MultiSorted_alt

• Definition of multisorted binding signatures
• Construction of an endofunctor on C^sort,C^sort from a multisorted signature
• Construction of the strength for the endofunctor on C^sort,C^sort
• Proof that the functor obtained from a multisorted signature is omega-cocontinuous

Library UniMath.SubstitutionSystems.Notation

Library UniMath.SubstitutionSystems.PCF_alt

Library UniMath.SubstitutionSystems.STLC

• The simply typed lambda calculus from a multisorted binding signature

Library UniMath.SubstitutionSystems.STLC_actegorical

Library UniMath.SubstitutionSystems.STLC_actegorical_abstractcat

Library UniMath.SubstitutionSystems.STLC_alt

• The simply typed lambda calculus from a multisorted binding signature

Library UniMath.SubstitutionSystems.SigmaMonoids

Library UniMath.SubstitutionSystems.SignatureCategory

• The category of signatures with strength
• Binary products in the category of signatures
• Coproducts in the category of signatures

Library UniMath.SubstitutionSystems.SignatureExamples

Library UniMath.SubstitutionSystems.Signatures

• Definition of signatures
  • Source and target of the natural transformation θ
• Two alternative versions of the strength laws are defined and seen as equivalent
• Definition of encapsulations of strength (locally/globally, with/without laws

Library UniMath.SubstitutionSystems.SignaturesEquivRelativeStrength

Library UniMath.SubstitutionSystems.SortIndexing

Library UniMath.SubstitutionSystems.SubstitutionSystems

• • Some variables and assumptions
  • Morphisms of heterogeneous substitution systems
    • • Equality of morphisms of hss
  • The precategory of hss
    • Identity morphism of hss
    • Composition of morphisms of hss

Library UniMath.SubstitutionSystems.SubstitutionSystems_Summary

• Generalized Iteration in Mendler-style and fusion law
• Heterogeneous Substitution Systems
• Monads from hss
• Lifting initiality
• Sum of signatures
• Arities of signatures for lambda calculus
• Evaluation of explicit substitution as initial morphism

Library UniMath.SubstitutionSystems.SumOfSignatures

• Definition of the data of the sum of signatures
• Proof of the strength laws of the sum of two signatures

Library UniMath.SubstitutionSystems.UntypedForests

Library UniMath.SubstitutionSystems.ContinuitySignature.CommutingOfOmegaLimitsAndCoproducts

Library UniMath.SubstitutionSystems.ContinuitySignature.ContinuityOfMultiSortedSigToFunctor

• the following is a deviation from the main topic of this file

Library UniMath.SubstitutionSystems.ContinuitySignature.GeneralLemmas

Library UniMath.SubstitutionSystems.ContinuitySignature.InstantiateHSET

Library UniMath.SubstitutionSystems.ContinuitySignature.MultiSortedSignatureFunctorEquivalence

Library UniMath.SubstitutionSystems.SimplifiedHSS.BindingSigToMonad

• Definition of binding signatures
• Translation from a binding signature to a monad
  • Binding signature to a signature with strength
  • Construction of initial algebra for a signature with strength
  • Construction of datatype specified by a binding signature
  • Signature with strength and initial algebra to a HSS
  • Function from binding signatures to monads
• Specialized versions of some of the above functions for HSET
  • Binding signature to signature with strength for HSET
  • Construction of initial algebra for a signature with strength for HSET
  • Binding signature to a monad for HSET

Library UniMath.SubstitutionSystems.SimplifiedHSS.CCS

Library UniMath.SubstitutionSystems.SimplifiedHSS.CCS_alt

Library UniMath.SubstitutionSystems.SimplifiedHSS.FromBindingSigsToMonads_Summary

Library UniMath.SubstitutionSystems.SimplifiedHSS.Lam

• Definition of a "model" of the flattening arity in pure lambda calculus

Library UniMath.SubstitutionSystems.SimplifiedHSS.LamFromBindingSig

• The lambda calculus from a binding signature

Library UniMath.SubstitutionSystems.SimplifiedHSS.LamHSET

Library UniMath.SubstitutionSystems.SimplifiedHSS.LiftingInitial

Library UniMath.SubstitutionSystems.SimplifiedHSS.LiftingInitial_alt

Library UniMath.SubstitutionSystems.SimplifiedHSS.MLTT79

Library UniMath.SubstitutionSystems.SimplifiedHSS.ModulesFromSignatures

• • Some variables and assumptions

Library UniMath.SubstitutionSystems.SimplifiedHSS.MonadicSubstitution_alt

Library UniMath.SubstitutionSystems.SimplifiedHSS.MonadsFromSubstitutionSystems

• • Some variables and assumptions
  • Derivation of the monad laws from a heterogeneous substitution system for signature with strength H
    • Proof of the first monad law
    • Proof of the second monad law
    • Proof of the third monad law via transitivity
  • A functor from hss to monads
    • The functor from hss to monads is faithful, i.e. forgets at most structure

Library UniMath.SubstitutionSystems.SimplifiedHSS.MultiSortedMonadConstruction

• Definition of multisorted binding signatures
• Construction of a monad from a multisorted signature
  • Function from multisorted binding signatures to monads

Library UniMath.SubstitutionSystems.SimplifiedHSS.MultiSortedMonadConstruction_alt

• Construction of a monad from a multisorted signature
  • Function from multisorted binding signatures to monads

Library UniMath.SubstitutionSystems.SimplifiedHSS.PCF_alt

Library UniMath.SubstitutionSystems.SimplifiedHSS.STLC

• The simply typed lambda calculus from a multisorted binding signature

Library UniMath.SubstitutionSystems.SimplifiedHSS.STLC_alt

• The simply typed lambda calculus from a multisorted binding signature

Library UniMath.SubstitutionSystems.SimplifiedHSS.SubstitutionSystems

• • Some variables and assumptions
  • Morphisms of heterogeneous substitution systems
    • • Equality of morphisms of hss
  • The precategory of hss
    • Identity morphism of hss
    • Composition of morphisms of hss

Library UniMath.SubstitutionSystems.SimplifiedHSS.SubstitutionSystems_Summary

• Generalized Iteration in Mendler-style and fusion law
• Heterogeneous Substitution Systems
• Monads from hss
• Lifting initiality
• Sum of signatures
• Arities of signatures for lambda calculus
• Evaluation of explicit substitution as initial morphism

Library UniMath.SyntheticHomotopyTheory.AffineLine

• Construction of affine lines
  • Preliminaries
  • Recursion for ℤ
  • Bidirectional recursion for ℤ
  • Bidirectional recursion for ℤ-torsors
  • Guided null-homotopies from ℤ-torsors
  • From each torsor we get a guided homotopy
  • The construction of the affine line
  • The image of the mere point in an affine line

Library UniMath.SyntheticHomotopyTheory.Circle

• Construction of the circle
  • The total space of guided homotopies over BZ
  • Various paths in GH
  • The universal property of the circle
    • The recursion principle (non-dependent functions)
    • The induction principle (dependent functions)

Library UniMath.SyntheticHomotopyTheory.Circle2

Library UniMath.SyntheticHomotopyTheory.Coproduct

• Path spaces of coproducts

Library UniMath.SyntheticHomotopyTheory.Halfline

• The induction principle for the half line.
  • universal property for the half line

Library UniMath.SyntheticHomotopyTheory.Test

Library UniMath.Tactics.Abmonoids_Tactics

• I. Definitions.
• II. Tactics for rearranging words.
• TESTS

Library UniMath.Tactics.EnsureStructuredProofs

Library UniMath.Tactics.Groups_Tactics

Library UniMath.Tactics.Monoids_Tactics

• TESTS

Library UniMath.Tactics.Nat_Tactics

• Basic definitions and hints.
• Tactics for rearranging subterms of goals and hypotheses.
  • Tactics for performing ternary permutations of words written in + and *.
  • Tactics for grouping pairs of terms appearing in words written in + and *.
    • Helper tactics (which should not be considered as part of the public interface for these tactics).
    • The tactics.
• Tactics pertaining to inequalities.
  • Preprocessing of the ambient goal and hypotheses.
    • Helper tactics (which should not be considered as part of the public interface for these tactics).
  • Tactics for solving inequalities involving natural numbers.
    • Tactics for solving very simple inequalities using known lemmas.
    • General tactics for solving inequalities by depth-first search.
• Tactics for deriving contradictions.
• Several somewhat devious experimental tactics.
• Tactics for solving equations.
  • Helper tactics.
  • Some simple solver tactics which are concerned exclusively with equations involving only + or only *.
  • A simple solver tactic for mixed + * equations.
• Combined tactics for solving equations and inequalities of natural numbers.
• TESTS

Library UniMath.Tactics.Simplify

• 1. Some supporting types and definitions
• 2. The traversal tactic
• 3. The simplification tactic

Library UniMath.Tactics.Utilities

• 1. Ltac1 utilities
• 2. Ltac2 utilities

Library UniMath.Topology.CategoryTop

• Results about Topology
• Displayed category of topological spaces

Library UniMath.Topology.Filters

• Results about Filters
  • Definition of a Filter
    • Order on filters
    • Image of a filter
    • Limit: filter version
  • Some usefull filters
    • Filter on a domain
    • Filter on a subtype
    • Direct Product of filters
  • Other filters
    • Filter on nat
    • The upper filter
    • Intersection of filters
    • Filter generated by a set of subsets
    • Filter defined by a base

Library UniMath.Topology.Prelim

• Additional theorems
  • hProp
  • A new tactic
  • About nat
  • More about Sequence
  • More about sets

Library UniMath.Topology.Topology

• Results about Topology
  • Neighborhood
  • Base of Neighborhood
  • Some topologies
    • Topology from neighborhood
    • Generated Topology
    • Product of topologies
    • Topology on a subtype
  • Limits in a Topological Set
    • Limit of a filter
    • Limit of a function
    • Continuity
    • Continuity for 2 variable functions
    • Continuity of basic functions
  • Topology in algebraic structures