Categoricity results for second-order ZF in dependent type theory
type: Item
instance of: scholarly article
title: Categoricity results for second-order ZF in dependent type theory
zbMATH Open document ID: 1468.03012
DOI: 10.1007/978-3-319-66107-0_20
author: Dominik Kirst
author: Gert Smolka
publication date: 2018-01-04T00:00:00Z
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 03B38
Mathematics Subject Classification ID: 03C35
Mathematics Subject Classification ID: 03C62
Mathematics Subject Classification ID: 03E70
Mathematics Subject Classification ID: 68V20
zbMATH DE Number: 6821859
describes a project that uses: Coq
MaRDI profile type: Publication
full work available at URL: 978-3-319-66107-0 20
OpenAlex ID: W2748981990
cites work: Die Widerspruchsfreiheit der allgemeinen Mengenlehre
cites work: Q3075242
cites work: Sur le théorème de Zorn
cites work: EVERY COUNTABLE MODEL OF SET THEORY EMBEDS INTO ITS OWN CONSTRUCTIBLE UNIVERSE
cites work: Q4256417
cites work: Two notes on the foundations of set-theory
cites work: Set theory. An introduction to independence proofs
cites work: Set theory for verification. I: From foundations to functions
cites work: Q4081251
cites work: Transfinite Constructions in Classical Type Theory
cites work: Hereditarily Finite Sets in Constructive Type Theory
cites work: Q4340909
cites work: Q3265769
cites work: A Declarative Language for the Coq Proof Assistant
cites work: Models of Second-Order Zermelo Set Theory
cites work: Second Order Logic or Set Theory?
cites work: Q4364399
cites work: Q5563362
description: scientific article; zbMATH DE number 6821859