Coproducts
Table of Contents
1 Co-products
module Lib.Data.Coprod where
This file defines the coproduct of two types A and B, usually denoted A + B, and proves basic facts on this new type.
1.1 Inductive definition
data Coprod (A B : U) : U = inl (x : A) | inr (y : B)
1.2 Induction principle
ind-Coprod (A B : U) (P : Coprod A B → U) (f : (x : A) → P (inl x)) (g : (y : B) → P (inr y)) : (z : Coprod A B) → (P z) = split inl x → f x inr y → g y
1.3 Basic facts
If A, A', B, B' are types, then there is a map h : A + B → A' + B'.
Coprod/map (A B A' B' : U) (f : A → A') (g : B → B') : (z : Coprod A B) → (Coprod A' B') = ind-Coprod A B (λ_. Coprod A' B') (λx. inl (f x)) (λy. inr (g y))