# Ω : Set -> Set

Various axiomatizations of type theories variously deal with sum types. For one, you can define the type _+_ : (Type, Type) -> Type where
injr: {A: Type, B: Type} -> A -> (A + B)
injr: {A: Type, B: Type} -> B -> (A + B)
axiomatically. Or you can define the enumerations and say that sums are dependent pairs:
A + B = (head: {'left, 'right}) * (value: {'left => A | 'right => B}).

One other elegant option is axiomatic introduction of the Maybe type with constructors
nil
val a
and its eliminator (default | value => result). It's a very nice solution because you can define lots of useful types a'la carte:

Nat = Maybe Rec[Nat]
List (A: Type) = Maybe (A, Rec [List A])
BTree A = Maybe(A, Rec [BTree A], Rec [BTree A])

Fin (n: Nat) = (() | prevN => Maybe (Fin prevN))
Vec (A: Type) (l: Nat) = (() | prevL => (A, (Vec A prevL)))

Note how short and natural primitive recursion looks in this setting:
add (a: Nat) (b: Nat) = (a || prevB => add (val a) prevB)
mul (a: Nat) (b: Nat) = (nil || prevB => add a (mul (val a) prevB))
• #### (no subject)

Встретил фотографию толпы футбольных фанатов, и она меня скорее напугала, у меня уж точно нет желания быть там среди них. Но внезапно я понял, что…

• #### Прогресс

Десять дней назад, вторая ступень SpaceX'овского корабля Starship своим ходом слетала своим ходом на десять километров вверх, и усмепшно приземлилась…

• #### О водосбережении

Как известно, питьевая вода во многих странах дефицитный ресурс. И даже в дождливой Германии летом иногда случаются засухи, в результате которых она…

• Post a new comment

#### Error

default userpic