Library uuu
Library uu0
- Univalent Basics. Vladimir Voevodsky. Feb. 2010 - Sep. 2011
- Preambule
- 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 implications are proved below)
- Functions between fibers defined by a path on the base are weak equivalences
- unit and contractibility
- A homotopy equivalence is a weak equivalence
- Some basic weak equivalences
- The 2-out-of-3 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 ) ( pr21 : total2 P -> Z ) ( the "pr21-case" )
- Fibration sequences based on ( hfiberpr21 : 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
- Basics about h-levels
- h -levels of pr21 , fiber inclusions, fibers, total spaces and bases of fibrations
- Propositions, inclusions and sets
- 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.
- 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 pr21 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 hProp
- Generalities on hProp. Vladimir Voevodsky . May - Sep. 2011 .
- Preambule
- The type hProp of types of h-level 1
- Intuitionistic logic on hProp
- The hProp version of the "inhabited" construction.
- ishinh and coprod
- Intuitionistic logic on hProp .
- 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/
- The double negation version of hinhabited ( does not require RR1 ) .
- Univalence axiom for hProp
Library hSet
- Generalities on hSet . Vladimir Voevodsky. Feb. - Sep. 2011
- Preambule
- 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 -> UU0
- The type of monic sybtypes of a type (subsets of the set of connected components)
- Relations on types ( or equivalently relations on the sets of connected components)
- Images and surjectivity for functions between types (both depend only on the behavior of the corresponding function between the sets of connected components)
- 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 with 1 , 2 and 3 variables
- The case when the function between quotients defined by setquotfunt 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
- The set of connected components of type.
- Set quotients. Construction 2.
Library algebra1
- Standard algebraic structures. Vladimir Voevodsky. Aug. - Sep. 2011 .
Library hnat
- Natural numbers and their properties. Vladimir Voevodsky . Apr. - Sep. 2011
Library stnfsets
- Standard finite sets . Vladimir Voevodsky . Apr. - Sep. 2011 .
- Preambule
- 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 .
Library finitesets
- Finite sets. Vladimir Voevodsky . Apr. - Sep. 2011.
Library hz
This page has been generated by coqdoc