Library uu0

• Univalent Basics.

Library uu0a

• Univalent Basics.
  • Preambule
  • Imports
  • Universe structure
  • 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
    • Iteration of an endomorphism
    • Basic constructions related to the adjoint evaluation
    • Pairwise direct products
    • Negation and double negation
    • Logical equivalence
  • Operations on paths
    • Composition of paths and inverse paths
    • Direct product of paths
    • The function maponpaths between paths types defined by a
    • maponpaths for the identity functions and compositions of
  • Fibrations and paths
  • First homotopy notions
    • Homotopy between functions
    • Contractibility, homotopy fibers etc.
  • Weak equivalences
    • Basics
    • Weak equivalences between contractible types (other
    • Functions between fibers defined by a path on the base are
    • unit and contractibility
    • A homotopy equivalence is a weak equivalence
    • Some basic weak equivalences
    • The 2-out-of-3 property of weak equivalences.
    • The 2-out-of-6 (two-out-of-six) property of weak equivalences.
    • Associativity of total2
    • Associativity and commutativity of dirprod
    • Coproducts and direct products
    • Total space of a family over a coproduct
    • Weak equivalences and pairwise direct products
    • Basics on pairwise coproducts (disjoint unions)
    • Fibrations with only one non-empty fiber.
    • Pairwise coproducts as dependent sums of families over bool
    • Splitting of X into a coproduct defined by a function X -> coprod Y Z
    • Some properties of bool
  • Basics about fibration sequences.
    • Fibrations sequences and their first "left shifts".
    • Fibration sequences based on ( tpair P z : P z -> total2 P ) ( pr1 : total2 P -> Z ) ( the "pr1-case" )
    • Fibration sequences based on ( hfiberpr1 : hfiber g z -> Y ) ( g : Y -> Z ) (the "g-case")
    • Fibration sequence of h-fibers defined by a composable pair of functions (the "hf-case")
  • Fiber-wise weak equivalences.
  • Homotopy fibers of the function fpmap: total2 X (P f) -> total2 Y P.
    • Total spaces of families over a contractible base
  • The maps between total spaces of families given by a map between the bases of the families and maps between the corresponding members of the families
  • 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 uu0b

• Univalent Basics. Vladimir Voevodsky. Feb. 2010 - Sep. 2011. Port to coq trunk (8.4-8.5) in
  • Preambule
  • 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"
    • Two pairs are equal if their first components are and the type of the second
    • Inclusions - functions of h-level 1
    • Basics about types of h-level 2 - "sets"

Library uu0c

• Univalent Basics. Vladimir Voevodsky. Feb. 2010 - Sep. 2011. Port to coq trunk (8.4-8.5) in
  • Preambule
    • Functional extensionality for functions to the empty type
    • More results on propositions
  • Isolated points and types with decidable equality.
    • Basic results on complements to a point
    • Basic results on types with an isolated point.
    • Weak equivalence weqrecompl from the coproduct of the complement to an isolated point with unit and the original type
    • Theorem saying that recompl commutes up to homotopy with maponcomplweq
    • Recomplement on functions
    • Standard weak equivalence between compl T t1 and compl T t2 for isolated t1 t2
    • Transposition of two isolated points
    • Types with decidable equality
    • bool is a deceq type and a set
    • Splitting of X into a coproduct defined by a function X -> bool
  • Semi-boolean hfiber of functions over isolated points
    • h-fibers of ii1 and ii2
    • ii1 and ii2 map isolated points to isoloated 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 ) )
    • Theorem saying that 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
    • Decibadle inclusions and isolated points
    • Decidable inclusions and coprojections
  • Results using full form of the functional extentionality axioms.
    • Axioms and their basic corollaries

Library uu0d

• Univalent Basics. Vladimir Voevodsky. Feb. 2010 - Sep. 2011. Port to coq trunk (8.4-8.5) in
  • Preambule
    • Deduction of functional extnsionality for dependent functions (sections) from functional extensionality of usual functions
  • Sections of "double fibration" (P: T -> UU)(PP: forall 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 forall x:X, P x -> forall x:X, Q x
    • General case
    • The weak equivalence between section spaces (dependent products) defined by a family of weak equivalences weq ( 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 uuu

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

Library hProp

• Generalities on hProp. Vladimir Voevodsky . May - Sep. 2011 .
  • 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 axiom for hProp

Library algebra1a

• Algebra 1 . Part A . Generalities. Vladimir Voevodsky. Aug. 2011 - .
  • Preamble
  • Sets with one and two binary operations
    • Binary operations
      • General definitions
      • Standard conditions on one binary operation on a set
      • Standard conditions on a pair of binary operations on a set
    • Sets with one binary operation
      • General definitions
      • Functions compatible with a binary operation ( homomorphisms ) and their properties
      • 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
      • Transport of properties of a pair binary operations
      • Subobjects
      • Quotient objects
      • Direct products

Library algebra1b

• Algebra I. Part B. Monoids, abelian monoids groups, abelian groups. Vladimir Voevodsky. Aug. 2011 - .
  • Preamble
  • Standard Algebraic Structures
    • Monoids
      • Basic definitions
      • Functions betweens monoids compatible with structure ( homomorphisms ) and their properties
      • Subobjects
      • Quotient objects
      • Direct products
    • Abelian ( commutative ) monoids
      • Basic definitions
      • 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
    • Groups
      • Basic definitions
      • Computation lemmas for groups
      • Relations on groups
      • Subobjects
      • Quotient objects
      • Direct products
    • Abelian groups
      • Basic definitions
      • Subobjects
      • 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 abgrfrac

Library algebra1c

• Algebra I. Part C. 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)
      • Relations similar to "greater" or "greater or equal" on rigs
      • Subobjects
      • Quotient objects
      • Direct products
    • Commutative rigs
      • General definitions
      • Relations similar to "greater" on commutative rigs
      • Subobjects
      • Quotient objects
      • Direct products
    • Rings
      • General definitions
      • Homomorphisms of rings
      • 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
      • 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
      • Computational lemmas for commutative rings
      • Subobjects
      • Quotient objects
      • Direct products
      • Commutative rigs to commuttaive 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 algebra1d

• Algebra I. Part D. Integral domains and fileds. Vladimir Voevodsky. Aug. 2011 - .
  • Preamble
  • Standard Algebraic Structures (cont.) Integral domains and Fileds.
    • Integral domains
      • General definitions
      • 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
      • 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 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
  • Test computations.

Library hSet

• Generalities on hSet . Vladimir Voevodsky. Feb. - Sep. 2011
  • Preamble
  • The type of sets i.e. of types of h-level 2 in UU
  • 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)
    • Genneral definitions
    • Direct product of two subtypes
    • A a subtype of with a paths between any every two elements is an h-prop.
  • 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 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
  • 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 the function between quotients defined by 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' )

Library hnat

• Natural numbers and their properties. Vladimir Voevodsky . Apr. - Sep. 2011
  • Preamble
  • Equality 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
    • Comparsion alternatives and S
  • Some properties of plus on nat
    • The structure of the additive ablelian monoid on nat
    • Addition and comparisons
    • Comparisons and n -> n + 1
    • Two comparisons and n -> n + 1
    • Comparsion alternatives and n -> n + 1
    • Cancellation properties of plus on nat
    • Some properties of minus on nat
  • Some properties of mult on nat
    • Basic algebraic properties of mult on nat
    • nat as a commutative rig
    • Cancellation properties of mult on nat
    • Multiplication and comparisons
    • Properties of comparisons in the terminology of algebra1.v
    • Submonoid of non-zero elements in nat
    • 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 to one element i .
  • 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 hq

• 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 equlaity on hq
    • Properties of addition and subtraction on hq
    • Proparties 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
    • 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 hz

• 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

Library sSet

• Homotopy theory of simplicial sets.

Library stnfsets

• Standard finite sets . Vladimir Voevodsky . Apr. - Sep. 2011 .
  • Preamble
  • Standard finite sets stn .
  • "Boundary" maps dni : stn n -> stn ( S n ) and their properties .
  • Weak equivalences between standard finite sets and constructions on these sets
    • The weak equivalence from stn n to the compl of a point j in stn ( S n ) defined by dni n j
    • Weak equivalence from coprod ( stn n ) unit to stn ( S n ) defined by dni n 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 weq ( 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
  • Accesibility - the least element of an inhabited decidable subset of nat

Library funextfun

• Univalence axiom and functional extensionality. Vladimir Voevodsky. Feb. 2010 - Sep. 2011
  • • Preamble.
    • Imports.
  • Univalence axiom.
  • Transport theorem.
  • Proof of the functional extensionality for functions