Author: Jasper Stein
Title: Subsets in formalised linear algebra
Abstract: 
This talk is based on my LinAlg contribution, where I formalised
preliminary linear algebra based on the setoid formalism. In mathematics, if
$B\subset A$, then $a\in B$ and $a\in A$ simultaneously. In Coq, however, the
setoid B needs a different carrier type, essentially Sigma a:A. P(a) for some
predicate P. So typing both {\tt a:A} and {\tt a:B} is not possible, since
terms have unique types up to conversion. One certainly wants pi_1 as a
coercion B>->A, but this is not enough when one formalises linear algebra.
Additional type casting functions are needed when one works with subsets, and
with subsets of subsets. In my talk I will introduce a few of them, and
explain their necessity.