Library UniMath.Foundations.Init

Library UniMath.Foundations.Preamble

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

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.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.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.UnivalenceAxiom2

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.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.Tests

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.All

Library UniMath.MoreFoundations.Bool

• Booleans

Library UniMath.MoreFoundations.Test

• Tests
  • Bool.v

Library UniMath.MoreFoundations.WeakEquivalences

• Weak equivalences
  • Contents
  • Direct products

Library UniMath.MoreFoundations.Tactics

Library UniMath.MoreFoundations.PartA

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

Library UniMath.MoreFoundations.PathsOver

• • Paths over paths in families of types

Library UniMath.MoreFoundations.Nat

• Natural numbers

Library UniMath.MoreFoundations.Notations

• Notations
  • Variants on paths and coconus
  • Squashing

Library UniMath.MoreFoundations.AlternativeProofs

• • An alternative proof of total2_paths_equiv

Library UniMath.MoreFoundations.Subposets

Library UniMath.MoreFoundations.DoubleNegation

Library UniMath.MoreFoundations.DecidablePropositions

• • Decidability via complementary pairs

Library UniMath.MoreFoundations.Propositions

• • Factoring maps through squash
  • Connected types

Library UniMath.MoreFoundations.NullHomotopies

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

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.NegativePropositions

• • • Propositions equivalent to negations of propositions

Library UniMath.MoreFoundations.Sets

• • More results on sets
  • Contents
  • Other universal properties for setquot
  • The equivalence relation of being in the same fiber
  • Subsets
  • Minimal equivalence relations

Library UniMath.MoreFoundations.Equivalences

• Equivalences

Library UniMath.MoreFoundations.MoreEquivalences

• Equivalences

Library UniMath.MoreFoundations.QuotientSet

Library UniMath.MoreFoundations.Subtypes

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.StructureIdentity

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

Library UniMath.MoreFoundations.Univalence

• Additional results about univalence

Library UniMath.MoreFoundations.NoInjectivePairing

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

Library UniMath.MoreFoundations.PartD

Library UniMath.MoreFoundations.All

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 .
  • Some results on bounded quantification
  • Accessibility - the least element of an inhabited decidable subset of nat

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.Lists

• Lists
• Lists over an arbitrary type

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 weq ( stn n ) X
    • The property of X to have n elements
  • General finite sets.
    • Finite structure on a type X defined as a pair ( n , w ) where n : nat and w : weq ( stn n ) X
    • The property of being finite

Library UniMath.Combinatorics.Graph

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

Library UniMath.Combinatorics.GraphPaths

Library UniMath.Combinatorics.Equivalence_Relations

Library UniMath.Combinatorics.OrderedSets

• Ordered sets
• computably ordered sets

Library UniMath.Combinatorics.WellFoundedRelations

Library UniMath.Combinatorics.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.Combinatorics.ZFstructures

Library UniMath.Combinatorics.FiniteSequences

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

Library UniMath.Combinatorics.BoundedSearch

Library UniMath.Combinatorics.MetricTree

• Metric trees
  • Definitions

Library UniMath.Combinatorics.Tests

• • Test computations.

Library UniMath.Combinatorics.DecSet

• Decidable sets.

Library UniMath.Combinatorics.Maybe

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

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.All

Library UniMath.Algebra.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.Algebra.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.Algebra.BinaryOperations

• Algebra 1. Part A. Generalities. Vladimir Voevodsky. Aug. 2011 -.
  • Contents
  • Preamble
  • Sets with one and two binary operations
    • Unary operations
    • Binary operations
      • General definitions
      • Transfer of binary operations relative to weak equivalences
      • Standard conditions on one binary operation on a set
      • Standard conditions on a pair of binary operations on a set
      • Transfer properties of binary operations relative to weak equivalences
    • Sets with one binary operation
      • General definitions
      • Functions compatible with a binary operation (homomorphisms) and their properties
      • (X = Y) ≃ (binopiso X Y)
      • hfiber and binop
      • Transport of properties of a binary operation
      • Subobjects
      • Relations compatible with a binary operation and quotient objects
      • Relations inversely compatible with a binary operation
      • Homomorphisms and relations
      • Quotient relations
      • Direct products
    • Sets with two binary operations
      • General definitions
      • Functions compatible with a pair of binary operation (homomorphisms) and their properties
      • X = Y ≃ (X ≃ Y)
      • Transport of properties of a pair of binary operations
      • Subobjects
      • Quotient objects
      • Direct products

Library UniMath.Algebra.Monoids

• Algebra I. Part B. Monoids, abelian monoids. Vladimir Voevodsky. Aug. 2011 - .
  • Contents
  • Preamble
  • Standard Algebraic Structures
    • Monoids
      • Basic definitions
      • Construction of the trivial monoid consisting of one element given by unit.
      • Functions between monoids compatible with structure (homomorphisms) and their properties
      • (X = Y) ≃ (monoidiso X Y)
      • Subobjects
      • Kernels
      • Quotient objects
      • Cosets
      • Direct products
    • Abelian (commutative) monoids
      • Basic definitions
      • Construction of the trivial abmonoid consisting of one element given by unit.
      • Abelian monoid structure on homsets
      • (X = Y) ≃ (monoidiso X Y)
      • Subobjects
      • Quotient objects
      • Direct products
      • Monoid of fractions of an abelian monoid
      • Canonical homomorphism to the monoid of fractions
      • Abelian monoid of fractions in the case when elements of the localziation submonoid are cancelable
      • Relations on the abelian monoid of fractions
      • Relations and the canonical homomorphism to abmonoidfrac

Library UniMath.Algebra.Groups

• Algebra I. Part C. Groups, abelian groups. Vladimir Voevodsky. Aug. 2011 - .
  • Contents
  • Groups
    • Basic definitions
    • Construction of the trivial abmonoid consisting of one element given by unit.
    • (X = Y) ≃ (monoidiso X Y)
    • Computation lemmas for groups
    • Relations on groups
    • Subobjects
    • Quotient objects
    • Cosets
    • Direct products
  • Abelian groups
    • Basic definitions
    • Construction of the trivial abgr consisting of one element given by unit.
    • Abelian group structure on morphism between abelian groups
    • (X = Y) ≃ (monoidiso X Y)
    • Subobjects
• Kernels
  • Kernel as abelian group
  • The inclusion Kernel f --> X is a morphism of abelian groups
  • Image of f is a subgroup
    • Quotient objects
    • Direct products
    • Abelian group of fractions of an abelian unitary monoid
    • Abelian group of fractions and abelian monoid of fractions
    • Canonical homomorphism to the abelian group of fractions
    • Abelian group of fractions in the case when all elements are cancelable
    • Relations on the abelian group of fractions
    • Relations and the canonical homomorphism to abgrdiff

Library UniMath.Algebra.GroupAction

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

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
      • Realations 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
      • Realations and the canonical homomorphism to the ring of fractions

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.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.DivisionRig

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

Library UniMath.Algebra.Apartness

• Definition of appartness relation
  • Additionals theorems about relations
  • Apartness
  • Tight apartness
  • Operations and apartness

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.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.Lattice

• Lattice
  • Strong Order
  • Definition
  • Partial order in a lattice
  • Lattice with a strong order
  • Lattice with a total order
  • Lattice in an abmonoid
  • Truncated minus

Library UniMath.Algebra.IteratedBinaryOperations

Library UniMath.Algebra.Free_Monoids_and_Groups

• • Contents

Library UniMath.Algebra.Tests

Library UniMath.Algebra.Modules.Core

• • Contents
  • The ring of endomorphisms of an abelian group
  • Modules: the definition of the small type of R-modules over a ring R
    • R-module morphisms
      • Linearity
      • modulefun
      • Isomorphisms (moduleiso)

Library UniMath.Algebra.Modules.Submodule

• • Contents

Library UniMath.Algebra.Modules.Multimodules

• • Contents
  • Definitions
    • • Propositions
    • Multimodule morphisms
      • Multilinearity
      • Multimodule morphisms

Library UniMath.Algebra.Modules.Examples

• • Contents
  • Morphisms
  • (Multi)modules
    • Bimodules

Library UniMath.Algebra.Modules.Quotient

• Taking a quotient of a submodule of a module over a fixed ring
• Preliminaries: notion of an equivalence relation on a module that is closed under the module
• Preliminaries: construction of an appropriate equivalence relation from a submodule
• Construction of quotient module, as well as its universal property
• Universal property in terms of submodules

Library UniMath.Algebra.Modules

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.Universal.HVectors

• Heterogeneous vectors.
  • Basic definitions.
  • Level-1 heterogeneous vectors.
    • Miscellanea of operations on level-1 hvecs.
    • Map for level-1 hvecs.
  • Level-2 heterogeneous vectors.

Library UniMath.Algebra.Universal.SortedTypes

• Sorted types.

Library UniMath.Algebra.Universal.Signatures

• Signatures for universal algebra.

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.

Library UniMath.Algebra.Universal.Examples.Nat

• Example on natural numbers

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.Monoid

• Example on monoids.

Library UniMath.Algebra.Universal.Examples.Group

• Example on groups.

Library UniMath.Algebra.Universal.Examples.ListDataType

• Example of lists

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.
• Curried version of build_term

Library UniMath.Algebra.Universal.TermAlgebras

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

Library UniMath.Algebra.Universal.Examples.Tests

• Several tests for univeral algebra operations.

Library UniMath.Algebra.Universal.VTerms

• • Variables and terms with variables

Library UniMath.Algebra.Universal.FreeAlgebras

• Free algebras.

Library UniMath.Algebra.Universal.Equations

• Equations over a signature and equational theories

Library UniMath.Algebra.Universal.EqAlgebras

• Varieties.

Library UniMath.Algebra.Universal

• Universal algebra: signatures, algebras and terms

Library UniMath.Algebra.All

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.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_monoidfun

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.NumberSystems.All

Library UniMath.SyntheticHomotopyTheory.Halfline

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

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.Test

Library UniMath.SyntheticHomotopyTheory.All

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.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.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.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.All

Library UniMath.CategoryTheory.Core.Categories

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

Library UniMath.CategoryTheory.Core.TwoCategories

• 2-categories
  • Laws
  • Bicategories
  • Laws for id to 2 mor

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.Univalence

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

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.Setcategories

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

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.NaturalTransformations

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

Library UniMath.CategoryTheory.Core.Prelude

• Prelude for category theory

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.categories.HSET.Core

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

Library UniMath.CategoryTheory.opp_precat

• The opposite precategory of a precategory
• The opposite functor

Library UniMath.CategoryTheory.Groupoids

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

Library UniMath.CategoryTheory.PrecategoryBinProduct

• Binary product of (pre)categories
  • Contents :

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.whiskering

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

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.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.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.SplitMonicsAndEpis

• Split monics, split epis
  • Contents
  • Split monomorphisms

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
• 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.Monads.RelativeMonads

• Definition of relative monads

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.Equivalences.Core

• • Equivalence of categories
  • Contents:
• Sloppy equivalence of (pre)categories
• Equivalence of (pre)categories
• Adjointification of a sloppy equivalence
  • One triangle equality is enough
  • Adjointification
• 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.CompositesAndInverses

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

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.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.Univalence

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

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.CategoriesWithBinOps

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

Library UniMath.CategoryTheory.PrecategoriesWithAbgrops

• • Precategories with homsets abelian groups (abgrops).

Library UniMath.CategoryTheory.limits.cones

Library UniMath.CategoryTheory.limits.equalizers

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

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.limits

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

Library UniMath.CategoryTheory.limits.graphs.eqdiag

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.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.products

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

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.terminal

• Construction of terminal object in a functor category

Library UniMath.CategoryTheory.limits.zero

• • Transport of ZeroArrow

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.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.pullbacks

• Criteria for existence of pullbacks.
• A square isomorphic to a pullback is a pullback (case 1)
• 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

Library UniMath.CategoryTheory.limits.graphs.initial

• • Maps between initial as special colimit and direct definition

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.limits.graphs.pullbacks

• • Maps between pullbacks as special limits and

Library UniMath.CategoryTheory.limits.coequalizers

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.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.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.limits.pushouts

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.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.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.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.cokernels

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

Library UniMath.CategoryTheory.limits.cats.limits

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.FinOrdProducts

Library UniMath.CategoryTheory.limits.FinOrdCoproducts

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.SubobjectClassifier

• Subobject classifiers
  • Contents
  • Definition
  • Accessors

Library UniMath.CategoryTheory.NNO

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.EpiFacts

Library UniMath.CategoryTheory.exponentials

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

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.SimplicialSets

• Homotopy theory of simplicial sets.

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.Monads.Monads

• Definition of monads
• Monad precategory
• 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.KleisliCategory

Library UniMath.CategoryTheory.Monads.LModules

• Definition of module
• Monad precategory

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.FunctorCoalgebras

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.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.rezk_completion

• Construction of the Rezk completion via Yoneda
• Universal property of the Rezk completion

Library UniMath.CategoryTheory.UnitorsAndAssociatorsForEndofunctors

Library UniMath.CategoryTheory.CategoricalRecursionSchemes

Library UniMath.CategoryTheory.PointedFunctors

Library UniMath.CategoryTheory.HorizontalComposition

• • currying functorial composition

Library UniMath.CategoryTheory.CATAsInstanceOfBicat

Library UniMath.CategoryTheory.PointedFunctorsComposition

Library UniMath.CategoryTheory.CommaCategories

• The general comma categories
  • Projection functors

Library UniMath.CategoryTheory.IsoCommaCategory

Library UniMath.CategoryTheory.ArrowCategory

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

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.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.coslicecat

• Coslice categories
  • Contents:
• Definition of coslice categories

Library UniMath.CategoryTheory.limits.pullbacks_slice_products_equiv

• 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.covyoneda

• Covariant Yoneda functor
  • On objects
  • On morphisms
  • Functorial properties of the yoneda assignments

Library UniMath.CategoryTheory.catiso

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

Library UniMath.CategoryTheory.CategoryEquality

• • Equality of precategories

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

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.category_binops

• • Equivalence between isomorphisms and binopisos

Library UniMath.CategoryTheory.AbelianToAdditive

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

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.ExactCategories.ExactCategories

• Exact categories
  • Contents

Library UniMath.CategoryTheory.ExactCategories.Tests

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.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.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.UnderCategories

• Morphism of tips induces a functor

Library UniMath.CategoryTheory.Subobjects

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

Library UniMath.CategoryTheory.Quotobjects

• Quotobjects
• Definition of quotient objects

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.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.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.LatticeObject

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

Library UniMath.CategoryTheory.Elements

Library UniMath.CategoryTheory.Monads.KTriples

• Kleisli Triples

Library UniMath.CategoryTheory.Monads.Kleisli

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

Library UniMath.CategoryTheory.Monads.KTriplesEquiv

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.MonadAlgebras

Library UniMath.CategoryTheory.Adjunctions.Restriction

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

Library UniMath.CategoryTheory.Adjunctions.Examples

• Examples of adjunctions
• Swapping of arguments in functor categories

Library UniMath.CategoryTheory.Subcategory.Reflective

• Reflective subcategories
  • Contents

Library UniMath.CategoryTheory.categories.setwith2binops

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

Library UniMath.CategoryTheory.categories.monoids

• Category of monoids
  • Contents
  • Precategory of monoids
  • Category of monoids
  • (monoidiso X Y) ≃ (iso X Y)
  • Category of monoids
  • Forgetful functor to HSET
  • Free functor from HSET
  • Free/forgetful adjunction

Library UniMath.CategoryTheory.categories.abmonoids

• Category of abmonoids
  • Contents
• Precategory of abmonoids
• Category of abmonoids
  • (monoidsiso X Y) ≃ (iso X Y)
  • Category of abmonoids

Library UniMath.CategoryTheory.categories.grs

• Category of grs
  • Contents
• Precategory of grs
• Category of grs
  • (monoidiso X Y) ≃ (iso X Y)
  • Category of grs

Library UniMath.CategoryTheory.categories.abgrs

• Category of abelian groups
  • Contents
• Precategory of abelian groups
  • precategory_data
  • is_precategory
  • precategory and category
• Category of abelian groups
  • (monoidiso X Y) ≃ (iso X Y)
  • Category of abelian groups
• Zero object and Zero arrow
  • Zero in abelian category
  • Computations on zero object
• Preadditive structure on the category of abelian groups
  • Binary operations on homsets
  • categoryWithAbgrops structure on the category of abelian groups
  • PreAdditive structure on the category of abelian groups
• Additive structure on the category of abelian groups
  • Direct sums
• Kernels and Cokernels
  • • Composition Kernel f --> X --> Y is the zero arrow
    • KernelIn morphism
    • Kernels
  • Cokernels
    • Subgroup gives an equivalence relation.
    • Construction of the quotient abelian group Y/(Im f)
    • The canonical morphism Y --> Y/(Im f)
    • CokernelOut
    • Cokernels
• Monics are injective and epis are surjective
  • Epis
  • Monics
• Monics are kernels of their cokernels and epis are cokernels of their kernels
  • Monics are kernels of their cokernels
  • Epis are cokernels of their kernels
• Category of abelian groups is an abelian category
• Corollaries to additive categories
  • Isomorphism criteria
    • (_ · ZeroArrow) = ZeroArrow = (ZeroArrow · _)
    • f isomorphism ⇒ (f · _) isomorphism
    • f isomorphism ⇒ (_ · f) isomorphism
    • Pre- and postcomposition with f is an isomorphism ⇒ f isomorphism
  • A criteria for isKernel which uses only the elements in the abelian group.

Library UniMath.CategoryTheory.categories.rigs

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

Library UniMath.CategoryTheory.categories.commrigs

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

Library UniMath.CategoryTheory.categories.rings

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

Library UniMath.CategoryTheory.categories.commrings

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

Library UniMath.CategoryTheory.categories.intdoms

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

Library UniMath.CategoryTheory.categories.flds

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

Library UniMath.CategoryTheory.categories.modules

• Contents:
• The category of (left) R-modules (mod_category)
• Abelian structure
  • Zero object and zero arrow
  • Zero in abelian category
  • Preadditive structure
  • Additive structure

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.Cats

• The (pre)category of (pre)categories
  • Contents:
  • Definitions
    • The precategory of 𝒰-small precategories (for fixed 𝒰) (precat_precat)
    • The precategory of 𝒰-small categories (cat_precat)
    • The precategory of 𝒰-small univalent categories (univalent_cat_precat)
    • The category of 𝒰-small set categories (setcat_cat)
      • The precategory of 𝒰-small categories with objects of hlevel n and homtypes
      • Setcategories, the case where n = m = 2.

Library UniMath.CategoryTheory.categories.preorder_categories

Library UniMath.CategoryTheory.categories.Type.Colimits

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

Library UniMath.CategoryTheory.categories.Type.Limits

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

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.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
    • 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.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.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.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.SliceFamEquiv

Library UniMath.CategoryTheory.categories.HSET.All

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.SetValuedFunctors

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.wosets

• 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.Graph

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

Library UniMath.CategoryTheory.GrothendieckTopos

• Grothendick toposes
  • Contents
• Definiton of Grothendieck topology
  • Grothendieck topology
  • Sheaves
• Definition of Grothendieck topos

Library UniMath.CategoryTheory.Presheaf

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

Library UniMath.CategoryTheory.ElementsOp

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.YonedaBinproducts

Library UniMath.CategoryTheory.ExponentiationLeftAdjoint

Library UniMath.CategoryTheory.categories.CartesianCubicalSets

Library UniMath.CategoryTheory.Chains.Chains

• Chains
  • Definition of (ω-)(co)continuous functors

Library UniMath.CategoryTheory.Chains.Cochains

• Cochains

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.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.All

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.Trees

• Binary trees
  • Flattening of a tree into a list

Library UniMath.CategoryTheory.Inductives.LambdaCalculus

Library UniMath.CategoryTheory.Inductives.PropositionalLogic

• • Contents

Library UniMath.CategoryTheory.DisplayedCats.Auxiliary

• Direct products of precategories should instead be imported from CategoryTheory.PrecategoryBinProduct.
• The unit precategory should be imported from CategoryTheory.categories.StandardCategories.
• Direct products of types.
• Direct products of precategories
• Miscellaneous lemmas

Library UniMath.CategoryTheory.DisplayedCats.Core

• Displayed categories
  • Definition
  • Utility lemmas
  • Isomorphisms (and lemmas)
  • More utility lemmas
  • Saturation: displayed univalent categories
• Total categories
  • Definition and forgetful functor
  • Isomorphisms and saturation
• Functors
  • Reindexing
  • Functors into displayed categories
  • Functors over functors between bases
  • Composite and identity functors.
  • Action of functors on isos.
  • Properties of functors
  • Total functors of displayed functors
  • A functor of displayed categories from reindexing
  • Natural Transformations

Library UniMath.CategoryTheory.DisplayedCats.Constructions

• Full subcategories
• Displayed category from structure on objects and compatibility on morphisms
• Products of displayed (pre)categories
  • Characterization of the isomorphisms of the direct product of displayed categories
• Sigmas of displayed (pre)categories
  • Transport and isomorphism lemmas
  • Univalence
• Displayed functor category
• 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.Equivalences

• General definition of displayed adjunctions and equivalences
• Main definitions
  • Adjunctions
  • Equivalences (adjoint and quasi)
  • Lemmas on the triangle identities
• Constructions on and of equivalences
  • 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.Equivalences_bis

• General definition of displayed adjunctions and equivalences
• Main definitions
  • Adjunctions
  • Equivalences (adjoint and quasi)
  • Lemmas on the triangle identities
• Constructions on and of equivalences
  • Full + faithful + ess split => equivalence
    • Utility lemmas from fullness+faithfulness
    • Converse functor
  • Inverses and composition of adjunctions/equivalences
  • Induced adjunctions/equivalences of fiber cats

Library UniMath.CategoryTheory.DisplayedCats.Codomain

• The slice displayed category
  • The displayed codomain

Library UniMath.CategoryTheory.DisplayedCats.Projection

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.Limits

Library UniMath.CategoryTheory.DisplayedCats.Examples

• Examples
• Displayed category of groups
  • The displayed arrow category
  • Objects with N-action
  • Elements of sets
• Any category is a displayed category over unit

Library UniMath.CategoryTheory.DisplayedCats.Examples.UnitalBinop

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.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.ComprehensionC

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

Library UniMath.CategoryTheory.DisplayedCats.Examples.Reindexing

Library UniMath.CategoryTheory.Monoidal.MonoidalCategories

Library UniMath.CategoryTheory.Monoidal.EndofunctorsMonoidal

Library UniMath.CategoryTheory.Monoidal.PointedFunctorsMonoidal

Library UniMath.CategoryTheory.Monoidal.MonoidalFunctors

Library UniMath.CategoryTheory.Monoidal.DisplayedMonoidal

Library UniMath.CategoryTheory.Monoidal.CategoriesOfMonoids

Library UniMath.CategoryTheory.Monoidal.Actions

Library UniMath.CategoryTheory.Monoidal.ConstructionOfActions

Library UniMath.CategoryTheory.Monoidal.ActionBasedStrongFunctorsMonoidal

Library UniMath.CategoryTheory.Monoidal.MonoidalFromBicategory

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

Library UniMath.CategoryTheory.Monoidal.ActionOfEndomorphismsInBicat

Library UniMath.CategoryTheory.Monoidal.ActionBasedStrength

Library UniMath.CategoryTheory.Monoidal.ActionBasedStrongFunctorCategory

Library UniMath.CategoryTheory.Monoidal.ActionsFormBicategory

Library UniMath.CategoryTheory.Monoidal.ActionBasedStrengthOnHomsInBicat

Library UniMath.CategoryTheory.Monoidal.BraidedMonoidalCategories

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

Library UniMath.CategoryTheory.SkewMonoidal.SkewMonoidalCategories

Library UniMath.CategoryTheory.SkewMonoidal.CategoriesOfMonoids

Library UniMath.CategoryTheory.Enriched.Enriched

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

Library UniMath.CategoryTheory.RepresentableFunctors.Precategories

• • • make a precategory

Library UniMath.CategoryTheory.RepresentableFunctors.Bifunctor

Library UniMath.CategoryTheory.RepresentableFunctors.Representation

Library UniMath.CategoryTheory.RepresentableFunctors.RawMatrix

• • raw matrices

Library UniMath.CategoryTheory.RepresentableFunctors.DirectSum

• • • direct sums

Library UniMath.CategoryTheory.RepresentableFunctors.Test

Library UniMath.CategoryTheory.All

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
  • Discrete bicat
  • Associators and unitors are isos.
  • Functor structure on associators and unitors.
  • Precomposition functor
  • Postcomposition functor
  • Notations.

Library UniMath.Bicategories.Core.Invertible_2cells

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

Library UniMath.Bicategories.Core.Adjunctions

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

Library UniMath.Bicategories.Core.Examples.OpMorBicat

Library UniMath.Bicategories.Core.Examples.OpCellBicat

• • op2 bicategory.

Library UniMath.Bicategories.Core.Unitors

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

Library UniMath.Bicategories.Core.BicategoryLaws

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.TransportLaws

Library UniMath.Bicategories.Core.EquivToAdjequiv

Library UniMath.Bicategories.Core.AdjointUnique

Library UniMath.Bicategories.Core.UnivalenceOp

• Univalence for opposite bicategories

Library UniMath.Bicategories.Core.Examples.OneTypes

Library UniMath.Bicategories.Core.Examples.PointedOneTypesBicat

Library UniMath.Bicategories.Core.Examples.TwoType

Library UniMath.Bicategories.Core.Examples.BicatOfUnivCats

• Bicategory of 1-categories

Library UniMath.Bicategories.Core.Examples.BicatOfCats

• Bicategory of 1-categories

Library UniMath.Bicategories.Core.Strictness

• Strict bicategories

Library UniMath.Bicategories.Core.Examples.StrictCats

• Bicategory of strict categories

Library UniMath.Bicategories.Core.Examples.Initial

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

Library UniMath.Bicategories.Core.Examples.Final

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

Library UniMath.Bicategories.Core.Examples.BicategoryFromMonoidal

Library UniMath.Bicategories.Core.FullyFaithful

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.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.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.DispUnivalence

• Internal adjunction in displayed bicategories

Library UniMath.Bicategories.DisplayedBicats.Fibration

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

Library UniMath.Bicategories.DisplayedBicats.FiberCategory

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

Library UniMath.Bicategories.DisplayedBicats.FiberBicategory.FiberBicategory1

• Bicategories

Library UniMath.Bicategories.DisplayedBicats.FiberBicategory.FiberBicategory2

• Bicategories

Library UniMath.Bicategories.DisplayedBicats.FiberBicategory

Library UniMath.Bicategories.DisplayedBicats.Examples.Sigma

• Bicategories

Library UniMath.Bicategories.DisplayedBicats.Examples.DispBicatOfDispCats

• Bicategories

Library UniMath.Bicategories.DisplayedBicats.Examples.Sub1Cell

Library UniMath.Bicategories.DisplayedBicats.Examples.DisplayedCatToBicat

Library UniMath.Bicategories.DisplayedBicats.Examples.Prod

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

Library UniMath.Bicategories.DisplayedBicats.Examples.DispDepProd

Library UniMath.Bicategories.DisplayedBicats.Examples.FullSub

• Bicategories

Library UniMath.Bicategories.DisplayedBicats.Examples.Trivial

• • Trivial display.

Library UniMath.Bicategories.Core.Examples.Groupoids

Library UniMath.Bicategories.PseudoFunctors.Display.Base

Library UniMath.Bicategories.PseudoFunctors.Display.Map1Cells

Library UniMath.Bicategories.PseudoFunctors.Display.Map2Cells

Library UniMath.Bicategories.PseudoFunctors.Display.Identitor

Library UniMath.Bicategories.PseudoFunctors.Display.Compositor

Library UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat

Library UniMath.Bicategories.PseudoFunctors.Display.StrictIdentitor

Library UniMath.Bicategories.PseudoFunctors.Display.StrictCompositor

Library UniMath.Bicategories.PseudoFunctors.Display.StrictPseudoFunctorBicat

Library UniMath.Bicategories.PseudoFunctors.PseudoFunctor

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

Library UniMath.Bicategories.PseudoFunctors.StrictPseudoFunctor

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

Library UniMath.Bicategories.PseudoFunctors.Examples.Identity

Library UniMath.Bicategories.PseudoFunctors.Examples.Composition

Library UniMath.Bicategories.PseudoFunctors.Examples.Constant

Library UniMath.Bicategories.PseudoFunctors.Examples.ApFunctor

Library UniMath.Bicategories.PseudoFunctors.Examples.OpFunctor

Library UniMath.Bicategories.PseudoFunctors.Examples.PseudofunctorFromMonoidal

• • • Going into the opposite direction

Library UniMath.Bicategories.Transformations.PseudoTransformation

Library UniMath.Bicategories.Transformations.Examples.Whiskering

Library UniMath.Bicategories.Transformations.Examples.Unitality

Library UniMath.Bicategories.Transformations.Examples.Associativity

Library UniMath.Bicategories.Transformations.Examples.ApTransformation

Library UniMath.Bicategories.Modifications.Modification

• Modifications between pseudo transformations

Library UniMath.Bicategories.Modifications.Examples.ApModification

Library UniMath.Bicategories.Modifications.Examples.Unitality

Library UniMath.Bicategories.Modifications.Examples.Associativity

Library UniMath.Bicategories.PseudoFunctors.Representable

• Representable pseudofunctor, pseudotransformation, and modifications

Library UniMath.Bicategories.PseudoFunctors.Yoneda

• Yoneda embedding

Library UniMath.Bicategories.PseudoFunctors.Biequivalence

• Biequivalence

Library UniMath.Bicategories.PseudoFunctors.Examples.StrictToPseudo

Library UniMath.Bicategories.PseudoFunctors.Examples.Projection

Library UniMath.Bicategories.DisplayedBicats.Examples.PointedOneTypes

Library UniMath.Bicategories.DisplayedBicats.Examples.DisplayedInserter

Library UniMath.Bicategories.DisplayedBicats.Examples.Displayed2Inserter

Library UniMath.Bicategories.DisplayedBicats.Examples.Algebras

Library UniMath.Bicategories.DisplayedBicats.Examples.Add2Cell

Library UniMath.Bicategories.DisplayedBicats.Examples.ContravariantFunctor

• Bicategories

Library UniMath.Bicategories.DisplayedBicats.Examples.Cofunctormap

• Bicategories

Library UniMath.Bicategories.DisplayedBicats.Examples.CwF

• Bicategories

Library UniMath.Bicategories.DisplayedBicats.Examples.Domain

Library UniMath.Bicategories.DisplayedBicats.Examples.Codomain

Library UniMath.Bicategories.DisplayedBicats.DispPseudofunctor

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

Library UniMath.Bicategories.Transformations.Examples.AlgebraMap

Library UniMath.Bicategories.DisplayedBicats.Examples.Monads

Library UniMath.Bicategories.DisplayedBicats.Examples.KleisliTriple

Library UniMath.Bicategories.DisplayedBicats.DispTransformation

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

Library UniMath.Bicategories.DisplayedBicats.DispModification

• • Definition of displayed modifications
    • Data
    • Data

Library UniMath.Bicategories.DisplayedBicats.DispBiequivalence

• • Data
  • Total biequivalence.

Library UniMath.Bicategories.Core.Examples.Image

Library UniMath.Bicategories.PseudoFunctors.Examples.CorestrictImage

Library UniMath.Bicategories.Core.YonedaLemma

• Yoneda Lemma

Library UniMath.Bicategories.Colimits.Initial

• Biinitial object in a bicategory
  • Biinitial object is unique.

Library UniMath.Bicategories.Colimits.Final

• Bifinal object in a bicategory
  • Bifinal object is unique.

Library UniMath.Bicategories.Colimits.Products

Library UniMath.Bicategories.Colimits.Pullback

Library UniMath.Bicategories.PseudoFunctors.Biadjunction

Library UniMath.Bicategories.PseudoFunctors.Examples.CurryingInBicatOfCats

Library UniMath.Bicategories.PseudoFunctors.PseudoFunctorLimits

Library UniMath.Bicategories.DisplayedBicats.DispBiadjunction

• • Triangles
  • Data
  • Total biadjunction.

Library UniMath.Bicategories.PseudoFunctors.Examples.PathGroupoid

Library UniMath.Bicategories.DisplayedBicats.DispToFiberEquivalence

• Displayed biequivalences give rise to equivalences on the fiber.

Library UniMath.Bicategories.DisplayedBicats.DispBuilders

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.PointedGroupoid

Library UniMath.Bicategories.WkCatEnrichment.prebicategory

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

Library UniMath.Bicategories.WkCatEnrichment.Notations

Library UniMath.Bicategories.WkCatEnrichment.whiskering

Library UniMath.Bicategories.WkCatEnrichment.Cat

Library UniMath.Bicategories.WkCatEnrichment.internal_equivalence

Library UniMath.Bicategories.WkCatEnrichment.bicategory

Library UniMath.Bicategories.WkCatEnrichment.hcomp_bicat

Library UniMath.Bicategories.PseudoFunctors.Examples.Strictify

Library UniMath.Bicategories.Discreteness

Library UniMath.Bicategories.BicategoryOfBicat

• Bicategories

Library UniMath.Bicategories.BicatOfBicategory

• Bicategories

Library UniMath.Bicategories.DisplayedBicats.CleavingOfBicat

Library UniMath.Bicategories.DisplayedBicats.ExamplesOfCleavings.TrivialCleaving

Library UniMath.Bicategories.DisplayedBicats.ExamplesOfCleavings.DomainCleaving

Library UniMath.Bicategories.DisplayedBicats.ExamplesOfCleavings.CodomainCleaving

Library UniMath.Bicategories.DisplayedBicats.ExamplesOfCleavings.FibrationCleaving

Library UniMath.Bicategories.All

Library UniMath.Ktheory.GrothendieckGroup

Library UniMath.Ktheory.All

Library UniMath.Topology.Prelim

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

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.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

Library UniMath.Topology.CategoryTop

• Results about Topology
• Displayed category of topological spaces

Library UniMath.Topology.All

Library UniMath.RealNumbers.Prelim

• Additionals theorems and definitions
  • for RationalNumbers.v

Library UniMath.RealNumbers.Fields

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

Library UniMath.RealNumbers.Sets

• Additionnals theorems for Sets.v
  • Additional definitions
  • Properties of po
  • Strong Order
  • Reverse orderse
  • Effectively Ordered
  • Constructive Total Effective Order
  • Complete Ordered Space

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 usefull 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.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.DedekindCuts

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

Library UniMath.RealNumbers.DecidableDedekindCuts

• A library about decidable Dedekind Cuts
  • Definition

Library UniMath.RealNumbers.All

Library UniMath.Tactics.Utilities

Library UniMath.Tactics.Monoids_Tactics

• TESTS

Library UniMath.Tactics.Abmonoids_Tactics

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

Library UniMath.Tactics.Groups_Tactics

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.All

Library UniMath.SubstitutionSystems.Notation

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.BinSumOfSignatures

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

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.BinProductOfSignatures

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

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.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.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.LiftingInitial

Library UniMath.SubstitutionSystems.LiftingInitial_alt

Library UniMath.SubstitutionSystems.ModulesFromSignatures

• • Some variables and assumptions

Library UniMath.SubstitutionSystems.LamSignature

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.SignatureExamples

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.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.LamHSET

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.LamFromBindingSig

• The lambda calculus from a binding signature

Library UniMath.SubstitutionSystems.MLTT79

Library UniMath.SubstitutionSystems.FromBindingSigsToMonads_Summary

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
• Construction of a monad from a multisorted signature
  • Function from multisorted binding signatures to monads

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
• Construction of a monad from a multisorted signature
  • Function from multisorted binding signatures to monads

Library UniMath.SubstitutionSystems.MonadicSubstitution_alt

Library UniMath.SubstitutionSystems.STLC

• The simply typed lambda calculus from a multisorted binding signature

Library UniMath.SubstitutionSystems.STLC_alt

• The simply typed lambda calculus from a multisorted binding signature

Library UniMath.SubstitutionSystems.CCS

Library UniMath.SubstitutionSystems.CCS_alt

Library UniMath.SubstitutionSystems.PCF_alt

Library UniMath.SubstitutionSystems.All

Library UniMath.Folds.UnicodeNotations

Library UniMath.Folds.aux_lemmas

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.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.All

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.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.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.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.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.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.All

Library UniMath.AlgebraicGeometry.Topology

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.All

Library UniMath.Paradoxes.GirardsParadox

Library UniMath.Paradoxes.All

Library UniMath.Induction.PolynomialFunctors

• • Polynomial functors

Library UniMath.Induction.ImpredicativeInductiveSets

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

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.M.Chains

• Limits of chains and cochains in the precategory of types

Library UniMath.Induction.M.ComputationalM

• • Refinement of M-types

Library UniMath.Induction.All

Library UniMath.All