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
Times are displayed in time zone: Tijuana, Baja California change

13:30 - 15:30: Type Theory, Set Theory, and Formalized MathematicsCPP at Museum A
Chair(s): Thorsten AltenkirchUniversity of Nottingham
13:30 - 14:00
Finite Sets in Homotopy Type Theory
Dan FruminRadboud University, Herman GeuversRadboud University Nijmegen, Netherlands, Léon GondelmanLRI, Université Paris-Sud, Niels van der WeideRadboud University Nijmegen, Netherlands
14:00 - 14:30
Generic Derivation of Induction for Impredicative Encodings in Cedille
Denis FirsovUniversity of Iowa, USA, Aaron StumpUniversity of Iowa, USA
14:30 - 15:00
Large Model Constructions for Second-Order ZF in Dependent Type Theory
Dominik KirstSaarland University, Gert SmolkaSaarland University
15:00 - 15:30
A Constructive Formalisation of Semi-algebraic Sets and Functions