In some type theories, \mathsf{Maybe} : \prod_{\left(a : \mathsf{Level}\right)} \left(\mathsf{Set}\ a \rightarrow \mathsf{Set}\ a\right) is a type function for creating optional values, i.e., "objects which may or may not contain a value". More formally, a term of type \mathsf{Maybe}\ A is either \mathsf{nothing} or \mathsf{just}\ x, where x is some term of type A.

This idea is lent well to being agender; after all, not everyone has a gender.