The Eternal Doorman

6:03 In Mathlib they try to formalise theories at the highest level of abstraction they can to avoid having to prove the same theorems many times for specific instantiations.  So for example, they use a general multi-dimensional integration theory of box-additive measures in  Mathlib.Analysis.BoxIntegral.Basic : In this file we define the integral of a function over a box in ℝⁿ. The same definition works for Riemann, Henstock-Kurzweil, and McShane integrals. As usual, we represent ℝⁿ as the type of functions ι → ℝ for some finite type ι. A rectangular box (l, u] in ℝⁿ is defined to be the set {x : ι → ℝ | ∀ i, l i < x i ∧ x i ≤ u i}, see BoxIntegral.Box . Let vol be a box-additive function on boxes in ℝⁿ with codomain E →L[ℝ] F. Given a function f : ℝⁿ → E, a box I and a tagged partition π of this box, the integral sum of f over π with respect to the volume vol is the sum of vol J (f (π.tag J)) over all boxes of π. Here π.tag J is the point (tag) in ℝⁿ associated with the ...

See  https://dannypineros.com/  This is going to be something amazing!  Subscribe to  Dust  and  Daniel Piñeros . 

See  Wiesław Kubiś - Generic Mathematical Structures .  55:12 Wouldn't it be great if you could cook up a comonad that gives a tower of categories that sum to differential calculus on a real vector space? See below .  Subscribe to  Topos Institute .  What is a comonad on a category? It's just a monad on the opposite category:  ... "Set theory is linear coalgebra on vector spaces":  Subscribe to  Sheafification of G .  But they have to make everything much more complicated: We discuss differentiable smoothness structures on 𝑹⁴ from three different categorical perspectives. The first one relies on considering open atlases on 𝑹⁴ with certain (not all) of its local charts residing in a smooth topos. Thus exotic smooth functions on 𝑹⁴ are finelly approached without any use of Casson handles and handle decompositions. The second approach takes into account entire space of all smoothness structures on 𝑹⁴ . Forcing extensions naturally order the...

See the video description : A mathematical object can be called “generic” if it appears, up to isomorphism, with probability one as the result of a natural stochastic process. Instead of [using] probability, one may [give] its topological counterpart, using the Baire category theorem . Yet another option is using a natural infinite game for two players, declaring an object U ”generic” if one of the players has a suitable winning strategy leading to the isomorphic copy of U.... ... The story of generic mathematical structures goes back to Cantor, who was the first to identify the set of rational numbers as the generic countable linearly ordered set. About half a century later, Fraïssé developed an abstract theory of universal homogeneous structures (nowadays called ”Fraïssé limits”) which until recent years was viewed as a part of model theory. As it happens, Fraïssé limits are particular cases of generic mathematical objects which can be found in several branches of mathematics, starti...

Subscribe to Elle Cordoba . 

13:13 How do you define volume in an infinite dimensional phase space on a finite whiteboard ?  1:05:39 I enjoyed listening to this discussion. Thanks to everyone who took part.  I was thinking about causal sets as modeling those second countable collections of empirically verifiable statements. That may not be how Sorkin sees it though! See  Geometry from order: causal sets .  Subscribe to  Assumptions of Physics .  See also this discussion with Urs Schreiber on Gauge fields and configuration spaces at 44:33 . The earlier discussion he referred to on differential geometry and compact spaces is at 17:05 . He's saying that you do not want to restrict physics to describing only compact spaces. But you do want to restrict observations to compact spaces. At 26:03 you can get a coherent notion of field configuration spaces in a topos. 35:10 Lawvere started out in physics, but then he asked "What is a vector space, really?" and within a decade wrote a paper...

It does configuration by WebUSB to download the firmware onto the modules, but I'm sure that's all encrypted too. See  Ian Clarke Answering Questions About Freenet  and  Wi-Wi 900 MHz Radio-synced Oscillators  so that you can use a distributed computation to authenticate messages. See  Ian Clarke on Freenet .  Subscribe to  Taylor and Amy Show .  Tomaz has made a 10Gb/s router and fiber optic cable is pretty cheap: from 10 cents per meter. So you are all set to help each other with offsite backups now: see How to Create a Successful Open Source Project FUTO - Immich Demonstration and Technical Talk FUTO FUBS Subscribe to  Tomaž Zaman .

Duality is not just good, it's the good!   Codensity monads  though,... See William Lawvere's remarks on the semi-lattice construction of Set in  About Logic Interview with Urs Schreiber .  52:21 In case you're like me and don't remember what an ultrafilter  on a set is: Filters are dual to ideals .  Subscribe to  Topos Institute .  Daniela Petrisan - Operations on languages and Codensity monads Talk given at  Simons Institute in November 2016: Given some operation on languages, a natural question to ask is what is the corresponding operation at the level of recognisers. For example, the concatenation of two languages recognized by monoids M and N, respectively, is recognized by the Schutzenberger product of M and N....  See  The Schützenberger product for syntactic spaces  by Mai Gehrke, Daniela Petrisan and Luca Reggio.  See also  https://www.irif.fr/~petrisan/  and  The Vietoris monad and weak distrib...

Using LLVM IR:  https://github.com/SheafificationOfG/QueenJewels . He did another one about groupoid models but it has lots of annoying video clips which make it a bit hard to follow, but it's still interesting.  Here's the one on equality, which you might want to watch first:  But you might want to watch this one first: See  About Logic Interview with Urs Schreiber  and  Vladimir Voevodsky - What if Current Foundations of Mathematics are Inconsistent .  Subscribe to  Sheafification of G .