search

UniMath / SymmetryBook

This book will be an undergraduate textbook written in the univalent style, taking advantage of the presence of symmetry in the logic at an early stage.
Creative Commons Attribution Share Alike 4.0 International
378 stars 22 forks source link

fibers of first projection #111

Open DanGrayson opened 3 years ago

DanGrayson commented 3 years ago

This lemma is rather special, and gets used only to show that we can form an injection from a predicate. Perhaps we should just prove more generally the the fibers are the first projection are equivalent to the members of the family, for any family of types used to form a sum-type. Or do we already do that somewhere?

Screen Shot 2021-06-17 at 1 17 59 PM
UlrikBuchholtz commented 3 years ago

We have that later in Lemma 2.24.1 (lem:fst-fiber(a)=B(a)).