Library uu0
Library uu0a
- Univalent Basics.
- Preambule
- Imports
- Universe structure
- Some standard constructions not using identity types (paths)
- Operations on paths
- Fibrations and paths
- First homotopy notions
- 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.
- 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
Library uu0b
- Univalent Basics. Vladimir Voevodsky. Feb. 2010 - Sep. 2011. Port to coq trunk (8.4-8.5) in
Library uu0c
- Univalent Basics. Vladimir Voevodsky. Feb. 2010 - Sep. 2011. Port to coq trunk (8.4-8.5) in
- Preambule
- 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
- Results using full form of the functional extentionality axioms.
Library uu0d
- Univalent Basics. Vladimir Voevodsky. Feb. 2010 - Sep. 2011. Port to coq trunk (8.4-8.5) in
- Preambule
- Sections of "double fibration" (P: T -> UU)(PP: forall t:T, P t -> UU) and pairs of sections
- Homotopy fibers of the map forall x:X, P x -> forall x:X, Q x
- The map between section spaces (dependent products) defined by the map between the bases f: Y -> X
- Sections of families over an empty type and over coproducts
- Sections of families over contractible types and over total2 (over dependent sums)
- 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.
- 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
- h-levels of spaces of weak equivalences
- Weak auto-equivalences of a type with an isolated point
Library uuu
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
- 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
- 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
Library algebra1b
- Algebra I. Part B. Monoids, abelian monoids groups, abelian groups. Vladimir Voevodsky. Aug. 2011 - .
- Preamble
- Standard Algebraic Structures
- Monoids
- 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
- 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
- Commutative rigs
- 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 - .
Library finitesets
- Finite sets. Vladimir Voevodsky . Apr. - Sep. 2011.
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)
- 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
- 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.
Library hnat
- Natural numbers and their properties. Vladimir Voevodsky . Apr. - Sep. 2011
- Preamble
- Equality on nat
- 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
- 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 .
Library hq
- Generalities on the type of rationals and rational arithmetic. Vladimir Voevodsky . Aug. - Sep. 2011.
- Preamble
- The commutative ring hq of integres
- 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
- 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
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
This page has been generated by coqdoc