{- Run-time Maybe Type:
Copyright (c) Groupoid Infinity, 2014-2018. -}
module maybe where
import proto
import proto_path
data maybe (A: U) = nothing | just (a: A)
fromMaybe (A: U) (n: A): maybe A->A = split { nothing -> n; just a -> a}
maybeMap (A B: U) (f: A->B): maybe A->maybe B = split { nothing -> nothing; just x -> just (f x) }
maybeRec (A P: U) (n: P) (j: A->P): maybe A->P = split { nothing -> n; just a -> j a}
maybeInd (A: U) (P: maybe A -> U) (n: P nothing) (j: (a: A) -> P (just a)):
(a: maybe A) -> P a = split { nothing -> n ; just x -> j x }
maybeId (A: U): maybe A->maybe A = maybeMap A A (idfun A)
maybeRefl (A: U) (a: maybe A): Path (maybe A) a a = refl (maybe A) a
maybeIsElim (A: U): (a: maybe A) -> Path (maybe A) a (maybeRec A (maybe A) nothing (\(a:A) -> just a) a)
= split { nothing -> maybeRefl A nothing ; just x -> maybeRefl A (just x) }
-- usage
-- maybeElim nat nat zero (\ (x: nat) -> x) (just zero)
-- law of maybeElim
-- maybe_ nothing just a == a