Library TypeTheory.Auxiliary.Auxiliary
- Some tactics
- Some argument settings
- Path-algebra: general lemmas about transport, equivalences, etc.
- Algebra in (pre)categories
- Unorganised lemmas
Library TypeTheory.Auxiliary.UnicodeNotations
Library TypeTheory.Auxiliary.CategoryTheoryImports
Library TypeTheory.ALV1.CwF_def
- Preliminaries
- Definition of a CwF
- Useful facts about representations
- Equivalence with relative universe structures on Yoneda
- Transport along a weak equivalence
Library TypeTheory.ALV1.RepMaps
- Definition of a representable map of presheaves
- Map from cwfs to representable maps of presheaves
- Equivalence from cwfs to rep. maps of presheaves for C univalent
- Equivalence between representable maps of presheaves and weak relative universes
- Equivalence between rep. maps of presheaves on C and on its Rezk completion
- Commutativity of a map from cwfs to rep. maps with transport along Rezk
Library TypeTheory.ALV1.CwF_SplitTypeCat_Equivalence
- Every compatible term structure is equal to the canoncial one
- Every compatible q-morphism structure is equal to the canonical one
- Equivalence between term structures and q-morphism structures
- Equivalence between types of pairs of object extension, term and q-morphism structures
Library TypeTheory.ALV1.CwF_SplitTypeCat_Maps
- Compatibility between term-structures and q-morphism structures
- Term-structures from q-morphism structures
- Defining a (compatible) q-morphism structure, given a term structure
Library TypeTheory.ALV1.CwF_SplitTypeCat_Cats_Standalone
Library TypeTheory.ALV1.RelativeUniverses
- Relative universe structures
- Uniqueness of relative universe structures under some assumptions
- Transfer of a relative universe
Library TypeTheory.ALV1.RelUnivYonedaCompletion
Library TypeTheory.ALV1.CwF_SplitTypeCat_Defs
- Object-extension structures
- Families structures
- q-morphism structures, split type-categories
- CwF’s, split type-categories
Library TypeTheory.ALV1.CwF_Defs_Equiv
- Definition of an intermediate structure
- Equivalence between cwf'_structure and intermediate cwf1_structure
- Equivalence between cwf_structure and intermediate
- Main result: equivalence between cwf_structure C and cwf'_structure C
Library TypeTheory.ALV1.Transport_along_Equivs
- Transfer of relative universes to Yoneda along weak equivalence
- Transfer of a relative universe
- Transfer of a relative weak universe
Library TypeTheory.ALV1.TypeCat
- Type pre-categories
- A "preview" of the definition
- Types, reindexing and context extension
- Pullback of dependent projections
- Type-saturation
- Splitness
- Lemmas about type-(pre)categories
Library TypeTheory.ALV1.TypeCat_Reassoc
Library TypeTheory.Displayed_Cats.Auxiliary
- Direct products of types.
- Direct products of precategories
- Groupoids
- Discrete categories on hSets.
- Miscellaneous lemmas
Library TypeTheory.Displayed_Cats.Constructions
- Full subcategories
- Displayed category from structure on objects and compatibility on morphisms
- Products of displayed (pre)categories
- Sigmas of displayed (pre)categories
- Displayed functor category
- Fiber categories
Library TypeTheory.Displayed_Cats.Core
Library TypeTheory.Displayed_Cats.Equivalences
- General definition of displayed adjunctions and equivalences
- Main definitions
- Constructions on and of equivalences
Library TypeTheory.Displayed_Cats.Equivalences_bis
- General definition of displayed adjunctions and equivalences
- Main definitions
- Constructions on and of equivalences
Library TypeTheory.Displayed_Cats.Codomain
Library TypeTheory.Displayed_Cats.Examples
- Examples
- Displayed category of groups
- Displayed category of topological spaces
- Any category is a displayed category over unit
Library TypeTheory.Displayed_Cats.Fibrations
- Isofibrations
- Fibrations
Library TypeTheory.Displayed_Cats.SIP
Library TypeTheory.Displayed_Cats.DisplayedCatFromCwDM
Library TypeTheory.Displayed_Cats.ComprehensionC
Library TypeTheory.Displayed_Cats.Limits
Library TypeTheory.ALV2.CwF_SplitTypeCat_Cats
- category of object-extension structures
- category of term structures
- category of q-morphism-structures
Library TypeTheory.ALV2.CwF_SplitTypeCat_Equiv_Cats
Library TypeTheory.ALV2.CwF_SplitTypeCat_Equiv_Comparison
Library TypeTheory.ALV2.CwF_SplitTypeCat_Univalent_Cats
Library TypeTheory.OtherDefs.CwF_1
- A "preview" of the definition
- Type and terms of a CwF
- Reindexing of types A[γ] and terms a⟦γ⟧ along a morphism γ : Γ' --> Γ
- Reindexing laws
- Comprehension structure
- Definition of precategory with families
- Various access functions to the components
- Lemmas about CwFs, in particular that reindexing forms pullback
Library TypeTheory.OtherDefs.CwF_Dybjer
Library TypeTheory.OtherDefs.CwF_Pitts_completion
Library TypeTheory.OtherDefs.CwF_Pitts_to_DM
Library TypeTheory.OtherDefs.CwF_Pitts_to_TypeCat_to_DM
Library TypeTheory.OtherDefs.CwF_Pitts_to_TypeCat
Library TypeTheory.OtherDefs.CwF_Pitts
- A "preview" of the definition
- Type and terms of a CwF
- Reindexing of types A{{γ] and terms a⟦γ⟧ along a morphism γ : Γ' --> Γ
- Reindexing laws
- Comprehension structure
- Definition of precategory with families
- Various access functions to the components
- Lemmas about CwFs, in particular that reindexing forms pullback
Library TypeTheory.OtherDefs.DM_to_TypeCat_to_DM
Library TypeTheory.OtherDefs.DM_to_TypeCat
Library TypeTheory.OtherDefs.DM
Library TypeTheory.OtherDefs.TypeCat_to_CwF_Pitts
Library TypeTheory.OtherDefs.TypeCat_to_DM
Library TypeTheory.Categories.category_FAM
Library TypeTheory.Categories.category_of_elements
Library TypeTheory.Categories.ess_alg_categories
- Definition of a graph as two types with source and target maps
- Definition of a graph with composition
- A category in essentially algebraic style is a graph with composition
Library TypeTheory.Categories.ess_and_gen_alg_cats
- Categories in essentially algebraic and generalized algebraic style
- From generalized algebraic precategories to essentially algebraic ones.
- From ess. alg. categories to gen. alg. ones
Library TypeTheory.Articles.ALV_2017
This page has been generated by coqdoc