This paper presents generic derivations of induction for
impredicatively typed lambda-encoded datatypes, in the Cedille
type theory. Cedille is a pure type theory extending the
Curry-style Calculus of Constructions with implicit products,
primitive heterogeneous equality, and dependent intersections.
All data erase to pure lambda terms, and there is no built-in
notion of datatype. The derivations are generic in the sense
that we derive induction for any datatype which arises as the
least fixed point of a signature functor. We consider
Church-style and Mendler-style lambda-encodings. Moreover, the
isomorphism of these encodings is proved. Also, we formalize
Lambek's lemma as a consequence of expected laws of cancellation,
reflection, and fusion.

Tue 9 Jan

Displayed time zone: Tijuana, Baja California change

13:30 - 15:30
Type Theory, Set Theory, and Formalized MathematicsCPP at Museum A
Chair(s): Thorsten Altenkirch University of Nottingham
13:30
30m
Talk
Finite Sets in Homotopy Type Theory
CPP
Dan Frumin Radboud University, Herman Geuvers Radboud University Nijmegen, Netherlands, Léon Gondelman LRI, Université Paris-Sud, Niels van der Weide Radboud University Nijmegen, Netherlands
DOI
14:00
30m
Talk
Generic Derivation of Induction for Impredicative Encodings in Cedille
CPP
Denis Firsov University of Iowa, USA, Aaron Stump University of Iowa, USA
DOI
14:30
30m
Talk
Large Model Constructions for Second-Order ZF in Dependent Type Theory
CPP
Dominik Kirst Saarland University, Gert Smolka Saarland University
DOI
15:00
30m
Talk
A Constructive Formalisation of Semi-algebraic Sets and Functions
CPP