About: Homotopy type theory

An Entity of Type: Thing, from Named Graph: http://dbpedia.org, within Data Space: dbpedia.org

Variant of type theory incorporating the univalence axiom of Voevodsky

Property	Value
dbo:description	théorie des types comprenant l'axiome d'univalence de Voïevodski (fr) variant of type theory incorporating the univalence axiom of Voevodsky (en)
dbo:thumbnail	wiki-commons:Special:FilePath/Hott_book_cover.png?width=300
dbo:wikiPageExternalLink	http://hottheory.files.wordpress.com/2012/08/hott2.pdf https://github.com/HoTT/HoTT https://github.com/UniMath/UniMath https://github.com/UniMath/UniMath/tree/master/UniMath/Foundations https://github.com/UniMath/UniMath/tree/master/UniMath/Ktheory https://github.com/UniMath/UniMath/tree/master/UniMath/PAdics https://github.com/benediktahrens/rezk_completion http://www.andrew.cmu.edu/user/awodey/htt.html http://www.andrew.cmu.edu/user/awodey/preprints/TTH.pdf http://www.andrew.cmu.edu/user/awodey/preprints/homotopy.pdf http://www.andrew.cmu.edu/user/awodey/students/warren.pdf http://ncatlab.org/homotopytypetheory/show/HomePage http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations.html http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/Hlambda_short_current.pdf http://www.mathematik.tu-darmstadt.de/~streicher/venedig.ps.gz http://video.ias.edu/univalent/awodey http://homotopytypetheory.org/%7CHomotopy https://web.archive.org/web/20170707022332/https:/hott.github.io/book/nightly/hott-a4-1075-g3c53219.pdf https://books.google.com/books%3Fid=LkDUKMv3yp0C https://books.google.com/books%3Fid=pLnKggT_In4C&pg=PA83
dbo:wikiPageWikiLink	dbr:Institute_for_Advanced_Study dbr:Path_space_(algebraic_topology) dbr:Category_theory dbr:Model_(mathematical_logic) dbr:Model_category dbr:Lambda_calculus dbr:Intuitionistic_type_theory dbr:Per_Martin-Löf dbr:Peter_Aczel dbr:André_Joyal dbr:Kan_fibration dbc:Formal_methods dbr:First-order_logic dbr:Topology dbr:Steve_Awodey dbr:Proof_assistant dbr:Fibration dbr:Path_(topology) dbc:Homotopy_theory dbr:Fork_(software_development) dbr:Homotopy dbr:Category_of_sets dbr:ArXiv dbc:Articles_containing_video_clips dbr:GitHub dbr:Groupoid dbr:Homotopy_hypothesis dbr:Coq dbr:Dependent_type dbr:Formal_proof dbr:Coherence_condition dbr:Computer_science dbc:Type_theory dbr:Carnegie_Mellon_University dbr:Uppsala_University dbr:Thierry_Coquand dbr:Mathematical_logic dbr:Simplicial_set dbr:Giovanni_Felder dbr:Dimension dbr:David_Corfield dbr:Homotopy_theory dbr:Robert_Harper_(computer_scientist) dbr:Creative_Commons_license dbc:Foundations_of_mathematics dbr:Calculus_of_constructions dbr:Vladimir_Voevodsky dbr:Curry–Howard_correspondence dbr:Higher_category_theory dbr:Homotopical_algebra dbr:ACM_Computing_Reviews dbr:Univalent_foundations dbr:Mathematical_Research_Institute_of_Oberwolfach dbr:Thomas_Streicher dbr:Foundation_of_mathematics dbr:Michael_Shulman_(mathematician) dbr:Mathematical_folklore dbr:Thorsten_Altenkirch dbr:Identity_type dbr:ETH_Zürich dbr:Internal_language dbr:Kan_complex dbr:Computer_programming_language dbr:Propositional_equality dbr:Propositions_as_types_principle dbr:File:Hott_book_cover.png dbr:File:The_making_of_HoTT_book.webm
dbp:id	homotopy+type+theory (en)
dbp:title	Homotopy type theory (en)
dbp:wikiPageUsesTemplate	dbt:Foundations-footer dbt:Nlab dbt:Commons_category dbt:Cite_book dbt:Reflist dbt:Notelist dbt:Clear dbt:Cite_journal dbt:Arxiv dbt:R dbt:Citation dbt:Use_dmy_dates dbt:Refend dbt:Div_col dbt:Div_col_end dbt:Refbegin dbt:Cite_thesis dbt:Rp dbt:Efn dbt:Short_description
dct:subject	dbc:Formal_methods dbc:Homotopy_theory dbc:Articles_containing_video_clips dbc:Type_theory dbc:Foundations_of_mathematics
rdfs:label	Homotopy type theory (en) Teoría de tipos homotópica (es) Homotopietypentheorie (de) Théorie des types homotopiques (fr) Гомотопическая теория типов (ru) 同伦类型论 (zh)
owl:sameAs	freebase:Homotopy type theory yago-res:Homotopy type theory wikidata:Homotopy type theory dbpedia-de:Homotopy type theory dbpedia-fr:Homotopy type theory dbpedia-zh:Homotopy type theory dbpedia-es:Homotopy type theory dbpedia-ru:Homotopy type theory dbpedia-vi:Homotopy type theory dbpedia-global:Homotopy type theory
prov:wasDerivedFrom	wikipedia-en:Homotopy_type_theory?oldid=1294289114&ns=0
foaf:depiction	wiki-commons:Special:FilePath/Hott_book_cover.png
foaf:isPrimaryTopicOf	wikipedia-en:Homotopy_type_theory
is dbo:academicDiscipline of	dbr:Steve_Awodey dbr:Thorsten_Altenkirch
is dbo:notableIdea of	dbr:David_Corfield
is dbo:wikiPageRedirects of	dbr:HoTT dbr:HoTT_Book dbr:HoTT_book dbr:Homotopic_type_theory dbr:Homotopical_type_theory dbr:Homotopy_Type_Theory dbr:Fibrations-as-Types dbr:Fibrations-as-Types_interpretation dbr:Fibrations-as-types dbr:Fibrations-as-types_interpretation dbr:Mere_proposition dbr:Higher_inductive_type dbr:Univalence_axiom
is dbo:wikiPageWikiLink of	dbr:Institute_for_Advanced_Study dbr:Currying dbr:Inductive_type dbr:Intuitionistic_type_theory dbr:Set_theory dbr:Steve_Awodey dbr:Type_theory dbr:Surreal_number dbr:Homotopy dbr:Equivalence_of_categories dbr:Groupoid dbr:Isomorphism dbr:Vertical_bar dbr:Equality_(mathematics) dbr:David_Corfield dbr:NLab dbr:Homotopy_theory dbr:Hott dbr:Calculus_of_constructions dbr:∞-groupoid dbr:Vladimir_Voevodsky dbr:Curry–Howard_correspondence dbr:Lambda_cube dbr:Ruth_Lyttle_Satter_Prize_in_Mathematics dbr:Blakers–Massey_theorem dbr:Constructive_set_theory dbr:Univalent_foundations dbr:Polynomial_functor_(type_theory) dbr:Equivalent_definitions_of_mathematical_structures dbr:Thomas_Streicher dbr:Michael_Shulman_(mathematician) dbr:Thorsten_Altenkirch dbr:Identity_type dbr:HoTT dbr:HoTT_Book dbr:HoTT_book dbr:Homotopic_type_theory dbr:Homotopical_type_theory dbr:Homotopy_Type_Theory dbr:Fibrations-as-Types dbr:Fibrations-as-Types_interpretation dbr:Fibrations-as-types dbr:Fibrations-as-types_interpretation dbr:Mere_proposition dbr:Higher_inductive_type dbr:Univalence_axiom
is dbp:discipline of	dbr:Michael_Shulman_(mathematician)
is dbp:fields of	dbr:Steve_Awodey dbr:Thorsten_Altenkirch
is foaf:primaryTopic of	wikipedia-en:Homotopy_type_theory