Dependent pairs in Python

Is possible to encode dependent pairs (or sigma types) in python using TypeGuard , abtract classes and subtyping. Dependent pair is a pair of a value and a predicate about that value, in Coq is denoted like this (x : { n : T, P n }) , where T is a type and P is a predicate. Using abstract classes, subtyping and type guards is possible to achieve dependent pairs, here is an example: from abc import ABCMeta , abstractmethod from typing import * class Nat ( int , metaclass = ABCMeta ): @ abstractmethod def __i