cross-posted from: https://lemmy.blahaj.zone/post/25349985
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.
Hopefully, this thing fits here.
