scientific article; zbMATH DE number 2247252

zbMath1092.03038MaRDI QIDQ5718564

Thomas Streicher

Publication date: 16 January 2006

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

universerealizability topossheaf toposextension of higher-order intuitionistic arithmetic

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Topoi (18B25) Second- and higher-order arithmetic and fragments (03F35) Intuitionistic mathematics (03F55)

Related Items (10)

The intrinsic topology of Martin-Löf universes ⋮ Simplicial sets inside cubical sets ⋮ What should a generic object be? ⋮ Computer theorem proving in mathematics ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Models of Type Theory Based on Moore Paths ⋮ Higher order functions and Brouwer’s thesis

This page was built for publication: