I really like TodePond's video "Screens in Screens in Screens". I've been wanting to do the same kinda thing with mathematical formulas instead of shapes, a kind of "formulas in formulas in formulas", but I'm an awful programmer so I'll describe some math you can do to that effect. Apologies in advance for the shoddy explanation though. Here's a thing you can do with "screens". You can name screens. Start with some screens A B C. Then if C is inside A, and A and B are the same color, then there is a copy of C inside B. What do you call this copy? "The copy of B from A to C"? It will be convenient if we give it a symbolic name. Call it (A->B)C. Or if you are really hardcore you can call it just t(A,B,C) where t is a ternary operator describing the result of copying C from A to B. You may think to only consider (A->B)C when C is inside A, but the math becomes tractable if you consider all screens at once. Then we can stipulate some axioms: 1. (A->A)B = B 2. (A->B)A=B 3. (B->C)(A->B)=(A->C) 3. (A->(X->Y)A)=(X->Y) The first axiom means if you are copying a screen from one screen to itself, you aren't changing anything. The second axiom is "obvious" except for considering (A->B)A in the first place. The third axiom means if you copy a screen from A to B and then from B to C that is the same as if you were to copy it from A to C directly. It is also shorthand for (B->C)((A->B)D) = (A->C)D for all screens D. The fourth axiom takes a bit more explaining. Basically we want this equation to be true whenever A is in X, and both sides are being used to copy something from A. But our theory at this point doesn't have a predicate for "A is contained in X" so we say it holds in all cases. With these axioms you can show the operators (A->B) form an algebraic structure called a group: You can multiply them by performing one copy after the other (C->D)(A->B). This operation is associative (I mean, it must be), and has an identity element and inverses. The identity being (A->A) and the inverse of (A->B) being (B->A). Another perspective is to view screens as points in an affine space (i.e. vector space without a specified origin). Then (A->B)C can be thought of as (B-A)+C, and each of the axioms above can be interpreted as vector equations. This isn't a good model though because it ends up saying some screens are the same when they should be different. You can still take the above axioms and show that screens form a generalization of affine spaces called torsors. I'll share more if anybody is interested. It really needs a much longer write up, but I thought somebody might know if its already been done before.

hey interesting! I'm not sure I completely understand, but it's nice to see how different people might model this sort of thing. i know @Elliot has been working on a screens-like thing recently, and he modelled it completely differently from me. I'd love to write up a blog post explaining how I model it. it would be nice to see what people think of it

If you do write up that post that would be awesome!

Cool! I really like screens too. I also like this mathematical modeling of screens! I like the idea to model screens as a group. I have been trying out some models related to the following model: screens as a category: the objects are screens and the arrows mean "contains".

I think axiom 2 is hard to picture because in the expression (A->B)C you normally think of C as lying inside A. But in the case of (A->B)A, where C is A, C is no longer strictly inside A, since it coincides with A. Maybe a better way to think of it is to let C vary in size and shape inside A, and let it "tend to A", making the size shape and position approach that of A. Then in the limit as C approaches A in size shape and position, the copy (A->B)C approaches B in size shape and position. Then if copying is a continuous function we are justified in inferring (A->B)A=B. Sorry for the math-speak.

Ah I see! It is maybe quite different than how I've been thinking about things! Can you share how you came up with these axioms? It's starting to make sense but I'm wondering what your intuition was when you were making them.

Oh, that question is so open ended, I love it but I'm really stumped on how to answer it! There is a lot of context I haven't shared, but much of it would be only marginally useful. Maybe I can say this though. A key component of the system I am trying to build are one way live copies. These copies would not only reflect the contents of their source but also the 'behavior' at their source. For instance in the image below the arrows indicate that we are copying from X to Y, from A to C, and from C to B. Then from the point of view of X, we are effectively copying from A to B, so this should be reflected in their copies in Y. One way to ensure this is to also formally copy C from X to Y, even though C isn't inside X, and ensure we copy from (X->Y)A to (X->Y)C, and from (X->Y)C to (X->Y)B. This was my motivation for considering all copies (A->B)C even if C isn't in A. This example also illustrates how my model really only answers how to name the different copies, and not how it is carried out in practice. I don't know if that is all useful to you, but I'm curious, in your implementation of screens is everything two way copies (plus transforms), or are there one way copies too? Is this the difference taking the category as is or making it into a groupoid first makes?

Thank you for this detailed explanation @Robin! I've never come across torsors before but framed rectangles and affine transforms make a lot of sense so I'm really interested.

@Elliot Your intuition on torsors about being able to form differences is exactly correct. It holds for all torsors (e.g. of framed rectangles) and not just free torsors. You are also right, when I write (X->Y)A->B I mean ((X->Y)A)->B. The key property of free torsors (technically its 'universal property') is totally abstract. I don't have a great way of explaining it. Its very similar to other 'free' objects such as free monoids if you ever come across those.

Does this mean that the free torsor on two elements A and B is given by the following procedure? 1. Construct the free monoid on two elements A and B (aside: this is easy in programming, this is just strings of As and Bs) 2. Construct the free group on two elements A and B by adding A^{-1} and B^{-1} to the monoid from last step and modifying concatenation (written as juxtaposition) so that the inverses actually satisfy AA^{-1}=id. 3. Construct the free torsor on two elements A and B by taking all elements X of the free group (from last step) of the form X=YZ^{-1}W and keeping concatenation the same (modified to be a group operation in the last step).

Note to self: I need to catch up with this thread!

@Elliot I almost entirely agree with your description of the free torsor, but I would make one small change to step 3. You write "Construct the free torsor on two elements A and B by taking all elements X of the free group of the form X=YZ^{-1}W" but I don't think Y,Z, and W can be arbitrary elements of the free group. I think they have to be only those elements you get by starting with A and B and applying that operation repeatedly to get larger and larger subsets of the free group. Explicitly, let S be a subgroup of the free group on {A,B} and let H(S)={YZ^{-1}W | Y,Z,W \in S}. I'm thinking "H" for "Heap operation". Let T_0={A,B} and define T_n inductively by T_n = T_{n-1} U H(T_{n-1}). Then the free torsor on {A,B} is the union of all the T_n for n=0,1,2, etc. (I think this accurately describes the idea from the last paragraph, but the idea is the more important thing at any rate.) So for example, T_0 = {A,B} so these are both elements of the free torsor. Then we find T_1 = {A,B} U { YZ^{-1}W | Y,Z,W are in {A,B} }. The second set in this union equals {A,B, AB^{-1}A, BA^{-1}B}. Thus T_1={A,B,AB^{-1}A, BA^{-1}B} so each of these are elements of the free torsor. You can keep on doing this but I don't think you are ever able to construct A^{-1} from this procedure. Consequently the free torsor is a strict subset of the free group. What does it look like then? I'll quote from a previous post In general, for the free torsor on X "I expect both the structure group and the torsor itself embed in the free group on X, with the structure group being the subgroup of the free group generated by all elements xy^{-1} with x and y in X, and the torsor itself consisting of all products tx with t in the structure group and x in X. And (A->B)C is represented as AB^{-1}C." Thus a typical element of the free torsor looks like (ab^{-1})(cd^{-1})...(xy^{-1})z with each of the elements a...z belonging to X. In terms of how this is justified the very rough idea is that you can quantify how many heap operations it takes to produce a particular element starting with (the set the torsor is free on, namely) X. Then you can do induction on how many heap operations it takes to form each element in a particular expression.

Thank you for fixing my construction! I see how you have to iteratively construct each "layer" of the torsor; very roughly: you start by writing down the differences, then the differences of differences, then differences of differences of differences and so on forever. Then you can refer to any element of the torsor in a finite sequence of steps by saying what "layer" it is in.

@Elliot Yes, I'm going about it very algebraically. I have all sorts of images in my head of what different things mean, but I can't hold it all in my head at once. I hope once I have the math worked out I can translate it back into pictures 🙂.