Post #2424423

@jeanas@mathstodon.xyz Also, in type theory, the formalization of "the type A is inhabited" is precisely "A" :-) (Or the truncation "∥ A ∥".) More seriously, in constructive mathematics, "X ≬ Y" is used to express that X and Y have an element in common.