topos.py

#!/usr/bin/env python3
# The Category of M-sets
#   M. Mehdi Ebrahimi and M. Mahmoudi
#   Department of Mathematics
#   Shahid Beheshti University
#   Tehran 19839, Iran

class FinSet(set):
    def __init__(self, s = ()):
        set.__init__(self, s)

    @classmethod
    def _wrap_methods(cls, names):
        def wrap_method_closure(name):
            def inner(self, *args):
                result = getattr(super(cls, self), name)(*args)
                if isinstance(result, set) and not hasattr(result, 'foo'):
                    result = cls(result, foo=self.foo)
                return result
            inner.fn_name = name
            setattr(cls, name, inner)
        for name in names:
            wrap_method_closure(name)


class SetFn:
    def __init__(self, dom, f, codom):
        assert isinstance(dom, set); assert isinstance(codom, set)
        self.dom = dom; self.codom = codom; self.f = f;

        for d in self.dom: 
            if self.f(d) not in self.codom:
                raise AssertionError("fn(%s) = %s not in codomain(%s)" % (d, self.f(d), self.codom))

    def image(self): return { self.f(x) for x in self.dom }
    def graph(self): return { (x, self.f(x)) for x in self.dom }
    def is_monic(self): return len(self.image()) == len(self.dom)
    def is_epic(self): return len(self.image()) == len(self.codom)

    def __eq__(self, other):
        assert isinstance(other, SetFn)
        if self.dom != other.dom: return False
        if self.codom != other.codom: return False
        if self.image() != other.image(): return False
        return True

    def __call__(self, x): return self.f(x)

    def __repr__(self):
        return "[%s -> %s : %s]" % (self.dom, self.codom, self.graph())

    # compute self.other
    # f @ g : f(g(x))
    def __matmul__(self, other):
        for y in other.codom:
            if y not in self.dom:
                raise AssertionError("unable to compose on (%s)" % (y, ))

        return SetFn(other.dom, lambda x: self(other(x)), self.codom)
        

# topos of sets
class SetTopos:
    @classmethod
    def initial(cls): return { "*" }

    @classmethod
    def initial2classifier(cls):
        return SetFn(cls.initial(), lambda _: 1, cls.classifier())

    @classmethod
    def set2initial(cls, b):
        assert isinstance (b, set)
        return SetFn(b, lambda _: "*", cls.initial())

    @classmethod
    def classifier(cls):
        return {0, 1}

    @classmethod
    def mk_classifier(cls, f):
        return SetFn(f.codom, lambda b: 1 if b in f.image() else 0, SetTopos.classifier())

# a -f-> b
# |      | cls(f)
# v      v
# 1 ---> O
def does_diagram_commute(f):
    assert isinstance(f, SetFn)
    return (SetTopos.initial2classifier() @ SetTopos.set2initial(f.dom)) == (SetTopos.mk_classifier(f) @ f)

def test_set_monic():
    f = SetFn({1, 2, 3}, lambda x: x + 1, {2, 3, 4, 5})
    g = SetTopos.mk_classifier(f)
    print("testing monic:")
    print("f: %s" % f)
    print("g: %s" % g)
    print("g @ f: %s" % (g @ f, ))
    print("commutes?: %s" % (does_diagram_commute(f)))

def test_set_epic():
    f = SetFn({1, 2, 3}, lambda x: 42, {42, 43, 44})
    g = SetTopos.mk_classifier(f)
    print("testing epic:")
    print("f: %s" % f)
    print("g: %s" % g)
    print("g @ f: %s" % (g @ f, ))
    print("commutes?: %s" % (does_diagram_commute(f)))

def test_set():
    test_set_monic()
    test_set_epic()


class Monoid:
    pass

# monoid of (Z/nZ, +)
class PlusModN(Monoid):
    def __init__(i, n):
        assert isinstance(i, int)
        assert isinstance(n, int)
        self.i = i % n; self.n  = n;

    def __repr__(self): return "%s%%%s" % (self.i, self.n)

    def __add__(self, other):
        assert self.n == other.n
        return PlusModN((self.i + other.i) % n, self.n)
    
    @classmethod
    def enumerate(cls, n):
        return { PlusModN(i, n) for i in range(n) }

class MonoidFn(SetFn):
    def __init__(self, dom, f, codom):
        SetFn.__init__(self, dom, f, codom)
        assert isinstance(dom, Monoid)
        assert isinstance(codom, Monoid)

class MonoidTopos:
    pass


if __name__ == "__main__":
    test_set()