14:22 < naturalog> hmm i just figured out a very interesting result
14:23 < naturalog> Rudin defines measurable funcs using funcs from a topological space to a measurable space
14:23 < naturalog> each one of those spaces have only 3 axioms, very close to each other but different
14:23 < naturalog> but i see now that such funcs behave like proofs
14:24 < naturalog> like in topological space, is the theorem space: you can AND and OR any sets you want
14:24 < naturalog> and the measurable space is closed under union (ie proof of A&B will contain proof for A
                   and proof for B)
14:24 < naturalog> and complementary: if you can prove A is true then you can prove ~A is false
14:24 < naturalog> (in decidable systems)
14:26 < naturalog> hott is looking at proofs like funcs between two topological spaces
14:26 < naturalog> so one can give a measure-theoretic interpretation
14:26 < naturalog> which agrees with probability theory which is also founded upon measure theory