Setoid type theory -- a syntactic translation

DOI10.1007/978-3-030-33636-3_7zbMath1434.03034OpenAlexW2972845810MaRDI QIDQ2176677

Thorsten Altenkirch, Simon Boulier, Nicolas Tabareau, Ambrus Kaposi

Publication date: 5 May 2020

Full work available at URL: https://doi.org/10.1007/978-3-030-33636-3_7

zbMATH Keywords

univalencetype theoryfunction extensionalityproof irrelevance

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Relative consistency and interpretations (03F25) Type theory (03B38)

Related Items (3)

The compatibility of the minimalist foundation with homotopy type theory ⋮ Constructing a universe for the setoid model ⋮ Unnamed Item

This page was built for publication: Setoid type theory -- a syntactic translation