TypeTheory

The mathematical study of type theories, in univalent foundations

This project is maintained by UniMath

Library TypeTheory.Auxiliary.Auxiliary

Library TypeTheory.Auxiliary.UnicodeNotations

Library TypeTheory.Auxiliary.CategoryTheoryImports

Library TypeTheory.ALV1.CwF_def

Library TypeTheory.ALV1.RepMaps

Library TypeTheory.ALV1.CwF_SplitTypeCat_Equivalence

Library TypeTheory.ALV1.CwF_SplitTypeCat_Maps

Library TypeTheory.ALV1.CwF_SplitTypeCat_Cats_Standalone

Library TypeTheory.ALV1.RelativeUniverses

Library TypeTheory.ALV1.RelUnivYonedaCompletion

Library TypeTheory.ALV1.CwF_SplitTypeCat_Defs

Library TypeTheory.ALV1.CwF_Defs_Equiv

Library TypeTheory.ALV1.Transport_along_Equivs

Library TypeTheory.ALV1.TypeCat

Library TypeTheory.ALV1.TypeCat_Reassoc

Library TypeTheory.Displayed_Cats.Auxiliary

Library TypeTheory.Displayed_Cats.Constructions

Library TypeTheory.Displayed_Cats.Core

Library TypeTheory.Displayed_Cats.Equivalences

Library TypeTheory.Displayed_Cats.Equivalences_bis

Library TypeTheory.Displayed_Cats.Codomain

Library TypeTheory.Displayed_Cats.Examples

Library TypeTheory.Displayed_Cats.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

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

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

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

Library TypeTheory.Categories.ess_and_gen_alg_cats

Library TypeTheory.Articles.ALV_2017


This page has been generated by coqdoc