let maybe: Type -> Type = \lambda t. Sum { Just t | Nothing };

let the: \Pi t: Type. (t -> t) = \lambda _. \lambda a. a;

let unwrap_type (t : Type): (maybe t) -> Type = split
  { Just _ => t
  | Nothing => 1
  };

let unwrap_bad: \Pi t: Type. \Pi mt: maybe t. (unwrap_type t) mt = \lambda t.
  (the (\Pi mt: maybe t. ((unwrap_type t) mt))) split
    { Just a => a
    | Nothing => 0
    };

-- A cubicaltt-like replacement:

let unwrap (t : Type): \Pi mt: maybe t. (unwrap_type t) mt = split
  -- I'm so sorry for the dumb parser, function application is accidentally
  -- right-associative.
  { Just a => a
  | Nothing => 0
  };