Properties of the disjoint sum _+_ of types. \begin{code} {-# OPTIONS --safe --without-K #-} module MLTT.Plus-Properties where open import MLTT.Plus open import MLTT.Negation open import MLTT.Id open import MLTT.Empty open import MLTT.Unit open import MLTT.Unit-Properties +-commutative : {A : ๐ค ฬ } {B : ๐ฅ ฬ } โ A + B โ B + A +-commutative = cases inr inl +disjoint : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } {x : X} {y : Y} โ ยฌ (inl x ๏ผ inr y) +disjoint {๐ค} {๐ฅ} {X} {Y} p = ๐-is-not-๐ q where f : X + Y โ ๐คโ ฬ f (inl x) = ๐ f (inr y) = ๐ q : ๐ ๏ผ ๐ q = ap f p +disjoint' : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } {x : X} {y : Y} โ ยฌ (inr y ๏ผ inl x) +disjoint' p = +disjoint (p โปยน) inl-lc : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } {x x' : X} โ inl {๐ค} {๐ฅ} {X} {Y} x ๏ผ inl x' โ x ๏ผ x' inl-lc refl = refl inr-lc : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } {y y' : Y} โ inr {๐ค} {๐ฅ} {X} {Y} y ๏ผ inr y' โ y ๏ผ y' inr-lc refl = refl equality-cases : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } {A : ๐ฆ ฬ } (z : X + Y) โ ((x : X) โ z ๏ผ inl x โ A) โ ((y : Y) โ z ๏ผ inr y โ A) โ A equality-cases (inl x) f g = f x refl equality-cases (inr y) f g = g y refl Cases-equality-l : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } {A : ๐ฆ ฬ } (f : X โ A) (g : Y โ A) โ (z : X + Y) (x : X) โ z ๏ผ inl x โ Cases z f g ๏ผ f x Cases-equality-l f g .(inl x) x refl = refl Cases-equality-r : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } {A : ๐ฆ ฬ } (f : X โ A) (g : Y โ A) โ (z : X + Y) (y : Y) โ z ๏ผ inr y โ Cases z f g ๏ผ g y Cases-equality-r f g .(inr y) y refl = refl Left-fails-gives-right-holds : {P : ๐ค ฬ } {Q : ๐ฅ ฬ } โ P + Q โ ยฌ P โ Q Left-fails-gives-right-holds (inl p) u = ๐-elim (u p) Left-fails-gives-right-holds (inr q) u = q Right-fails-gives-left-holds : {P : ๐ค ฬ } {Q : ๐ฅ ฬ } โ P + Q โ ยฌ Q โ P Right-fails-gives-left-holds (inl p) u = p Right-fails-gives-left-holds (inr q) u = ๐-elim (u q) open import MLTT.Sigma open import Notation.General inl-preservation : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } (f : X + ๐ {๐ฆ} โ Y + ๐ {๐ฃ}) โ f (inr โ) ๏ผ inr โ โ left-cancellable f โ (x : X) โ ฮฃ y ๊ Y , f (inl x) ๏ผ inl y inl-preservation {๐ค} {๐ฅ} {๐ฆ} {๐ฃ} {X} {Y} f p l x = ฮณ x (f (inl x)) refl where ฮณ : (x : X) (z : Y + ๐) โ f (inl x) ๏ผ z โ ฮฃ y ๊ Y , z ๏ผ inl y ฮณ x (inl y) q = y , refl ฮณ x (inr โ) q = ๐-elim (+disjoint (l r)) where r : f (inl x) ๏ผ f (inr โ) r = q โ p โปยน +functor : {X : ๐ค ฬ } {Y : ๐ฅ ฬ } {A : ๐ฆ ฬ } {B : ๐ฃ ฬ } โ (X โ A) โ (Y โ B) โ X + Y โ A + B +functor f g (inl x) = inl (f x) +functor f g (inr y) = inr (g y) \end{code}