[ 3 / biz / cgl / ck / diy / fa / ic / jp / lit / sci / vr / vt ] [ index / top / reports ] [ become a patron ] [ status ]
2023-11: Warosu is now out of extended maintenance.

/sci/ - Science & Math


View post   

File: 2.70 MB, 2304x3072, Mathemaidics will change research and education forever.png [View same] [iqdb] [saucenao] [google]
16094201 No.16094201 [Reply] [Original]

Good Morning /Sci/entists!

Any kind of math can be abstracted into a Maid Level View of the Mathematics by replacing symbols and operations with maids doing things.

This field of abstracting math into maids doing things is called Mathemaidics. The goal is to visualize advanced Mathematics and Computer Science as maids doing things because visualization is more powerful than symbolic abstraction. You can make drawings and animations and manga out of visualizations and that makes a more interesting way to learn and operate something. It should be possible to embed a series of lectures about advanced Mathematics and Computer Science into a moe anime. Also it is easier to imagine and reason about a visualization than understand and operate a symbolic abstraction of even moderate complexity.

The study of Mathemaidics is now the main purpose of the /Sci/ board.

Please tell me about Advanced Mathematics and Computer Science research but explain it with maids.

Somebody please explain Type Theory and Homotophy and Category Theory and Homotophy Type Theory using maids. If I can imagine it as maids doing something interesting I will remember it and be able to operate it and also draw it so it can get in a book with a lot of drawings (ideally just a maid manga) instead of being trapped in a book with no drawings and just symbols.

This is an idea whose time has come. We will combine Maid Level View Abstractions with AI generated images so all of advanced Mathematics and Computer Science research can wear a maid dress.

The future is moe moe kyun!

Thank you /Sci/entists for reading my post.

>> No.16094205
File: 1.31 MB, 498x284, 1681889332215.gif [View same] [iqdb] [saucenao] [google]
16094205

>>16094201
Janitor, kindly sticky this thread, so maids in my Science Foundation will have time to work on representing advanced Mathematics and Computer Science with maids.

>> No.16094245

>>16094201
There's a book called Science without Numbers that might interest you.

I would agree that mathematicians should be forced to dress as maids. I believe most of them already do in secret

>> No.16094878

>>16094201
In the grand mansion of Type Theory, we have a universe of types `U`, where each room is adorned with a unique type `A ∈ U`. The maids, diligent as ever, ensure that every object `x` is in its proper room, enforcing the typing judgment `Γ ⊢ x : A`, where `Γ` is a context containing the types of variables. The head maid, Lambda (λ), oversees this process with a watchful eye, making sure that no object is misplaced
Functions in Type Theory are the secret passages between rooms, allowing maids to map objects from one type to another. Given types `A, B ∈ U`, a function `f : A B` is a mapping that assigns to each term `x : A` a specific term `f(x) : B`. The λ-calculus notation `λx:A.t` represents a function that takes an argument `x` of type `A` and returns a term `t`, much like a maid taking an object from one room and delivering it to another
Dependent types are the keys that unlock new rooms based on the objects the maids are carrying. A dependent type is a type that depends on a term, often denoted as `Π(x:A)B(x)`, where `A ∈ U` and `B : A U`. This represents the type of functions that assign to each term `x : A` a term of type `B(x)`, like a maid unlocking a special room based on the object she's carrying

>> No.16094881

>>16094201
>>16094878
In the garden of Homotopy Theory, we have a topological space `X`, with paths representing continuous functions between points. Given two paths `f, g : X Y`, they are homotopic if there exists a continuous function `H : X × I Y`, where `I = [0, 1]`, such that `H(x, 0) = f(x)` and `H(x, 1) = g(x)` for all `x ∈ X`. The homotopy relation is denoted as `f ≃ g`, and the maids can deform one path into another without changing the endpoints, like a magical girl transformation sequence
The composition of paths in the garden represents the composition of continuous functions, which is associative. Given continuous functions `f : X Y` and `g : Y Z`, their composition `g ∘ f : X Z` is defined by `(g ∘ f)(x) = g(f(x))` for all `x ∈ X`, like maids combining their powers to transform objects in a grand spectacle
Category Theory comes into play when the maids organize their tasks. A category `C` consists of objects `Obj(C)` and morphisms `Hom_C(A, B)` between objects `A, B ∈ Obj(C)`, satisfying the following axioms:
>Composition: For morphisms `f ∈ Hom_C(A, B)` and `g ∈ Hom_C(B, C)`, there exists a morphism `g ∘ f ∈ Hom_C(A, C)`.
>Associativity: For morphisms `f ∈ Hom_C(A, B)`, `g ∈ Hom_C(B, C)`, and `h ∈ Hom_C(C, D)`, we have `(h ∘ g) ∘ f = h ∘ (g ∘ f)`.
>Identity: For each object `A ∈ Obj(C)`, there exists an identity morphism `id_A ∈ Hom_C(A, A)` such that for any morphism `f ∈ Hom_C(A, B)`, we have `f ∘ id_A = f` and `id_B ∘ f = f`.
The maids, now well-versed in category theory, organize their tasks with the precision and elegance of a well-choreographed dance
In the realm of Homotopy Type Theory (HoTT), types are treated as spaces, and functions are continuous maps between these spaces. The notion of homotopy is used to study the relationships between types.

>> No.16094883

>>16094201
>>16094878
>>16094881
Two types `A` and `B` are homotopy equivalent, denoted as `A ≃ B`, if there exist functions `f : A B` and `g : B A` such that `g ∘ f ≃ id_A` and `f ∘ g ≃ id_B`, where `id_A` and `id_B` are the identity functions on `A` and `B`, respectively. The maids, now masters of homotopy, can deform types into one another like a magical girl transformation sequence on steroids
Higher inductive types in HoTT allow the definition of new types by specifying their points (objects) and paths (morphisms) simultaneously. This is done by providing a list of constructors for the type, which can include both point constructors and path constructors. For example, the circle type `S1` can be defined as:
```
data S1 : Type where
base : S1
loop : base ≡ base
```
The maids, armed with this knowledge, can now create new types with the skill and finesse of a master pastry chef.
The Univalence Axiom in HoTT states that equivalent types can be substituted for each other in any context without changing the meaning of a statement. Formally, for any two types `A` and `B`, the type of equivalences between `A` and `B`, denoted as `A ≃ B`, is equivalent to the type of equalities between `A` and `B`, denoted as `A ≡ B`. This can be expressed as:
```
ua : (A B : Type) (A ≃ B) ≃ (A ≡ B)
```
The maids, now enlightened by the power of univalence, can swap equivalent types like they're changing their uniforms, knowing that the underlying meaning remains the same

>> No.16094893

>>16094201
Some trivial exercises for Maidfag:

>Maid's Functorial Challenge
Let there be a type A of porcelain vases and a type B of display cabinets within our universe U. Maid Mio needs to ensure that each vase v : A is placed in a cabinet. She defines a function place : A B. Show that Maid Mio's function respects the internal structure of A and B by defining an appropriate functor between the corresponding categories of types.
>Maid's Curry-Howard Correspondence
The maids have noticed that the logical statements of their mansion's rulebook correspond to types, and proofs of these statements correspond to terms of these types. If the statement "Every vase is in a cabinet" corresponds to the type `∀ (v : A), ∃ (c : B), isIn(v, c)`, construct a proof term that the head maid Lambda can use to verify that this rule is being followed.
.

>> No.16094894

>>16094201
>>16094893
>Maid's Path Lifting Problem:
In the mansion's garden, there is a two-story topiary that the maids must navigate. If `p : I X` is a path in the garden representing a maid's journey from the ground floor to the top floor, and `f : X Y` is an elevator function between floors, define a path-lifting function `lift(p, f)` that demonstrates how a maid can be transported along `p` through the action of `f`.
>Maid's Homotopy Equivalence Dance
Maids Chika and Riko are practicing a dance that symbolizes a homotopy equivalence between two topological spaces `X` and `Y`. Chika's dance `f : X Y` and Riko's response `g : Y X` must satisfy that `g ∘ f` is homotopic to the identity on `X`, and `f ∘ g` is homotopic to the identity on `Y`. Choreograph the dance moves (i.e., define the homotopies) that demonstrate the equivalence.
>Maid's Monoidal Category Conundrum
The maids have organized the mansion's chores into a category `Chores`, where objects are tasks and morphisms are sequences of tasks. If `(Chores, ⊗, I)` forms a monoidal category with `⊗` as the tensor product of tasks and `I` as the unit task, demonstrate how the maids can use this structure to efficiently combine and execute chores.
>Maid's Natural Transformation Tea Party
Maid Yuki is hosting a tea party and has set up two functors `F, G : C D` between the category of teacups `C` and the category of tea flavors `D`. To ensure that every teacup's transition from `F` to `G` is smooth, define a natural transformation `η : F G` that allows the flavor of the tea to change naturally with each guest's preference.
>Maid's Higher Inductive Cake Construction
After mastering the art of creating types, the maids decide to bake a cake shaped like the torus `T2`. Define a higher inductive type for `T2` with the appropriate point constructors and path constructors that correspond to the cake's layers and the creamy filling paths.

>> No.16094900

>>16094201
>>16094893
>>16094894
>Maid's Univalence Wardrobe Malfunction
The maids are preparing for a costume party where each type corresponds to a costume. Maid Sakura has two costumes `A` and `B` that are equivalent, and she wants to use the Univalence Axiom to switch between them seamlessly. Write down the univalence axiom `ua(A, B)` in a way that allows for this costume change without any guest noticing the difference in the party's atmosphere
>Maid's Polymorphic Typing Soirée
The head maid has invited a polymorphic guest, a function poly : Π (A : U), A -> A that claims to be able to transform any object into a more exquisite version of itself while staying within its type. However, she suspects this guest might be an impostor. Formulate a proof using typing judgments to verify the guest's polymorphic identity, ensuring that for any type A ∈ U and any object x : A, the application poly A x indeed returns an object of the same type A.
>Maid's Coinductive Chore Infinite Loop
In the mansion's library, there is an ever-growing book of chores that can never be fully completed. Represent this book as a coinductive type Choreω that allows for an infinite sequence of chores. Define the type and provide an example of a stream of chores s : Choreω that the maids can work on ad infinitum, ensuring that the typing judgment is satisfied at each step of their eternal task

>> No.16094904
File: 28 KB, 425x312, dmmtts.png [View same] [iqdb] [saucenao] [google]
16094904

there are now FOUR of these worthless fucking maid fetish threads taking up space on /sci/ because you retards won't fucking stop talking to him
you're all fucking retarded

>> No.16094907

>>16094201
>>16094893
>>16094894
>>16094900
>>16094201
>>16094893
>>16094894
>Maid's Braided Path Challenge
The garden maze has been enchanted with braided paths, where the motion of two maids must intertwine like a braid in a three-dimensional space `X`. Given paths `α, β : I -> X` that start and end at the same points, define a higher homotopy `B : I × I -> X` that exhibits the braiding of `α` and `β`, subject to the strictures of higher-dimensional path algebra.
>Maid's Homotopy Coherence Conundrum
To redecorate the mansion's grand ballroom, the maids must ensure that the space's homotopy groups `πₙ(X, x0)` are coherent with each other for all `n`. Given a space `X` with a chosen base point `x0`, construct a sequence of homotopies that demonstrate the coherence between the action of `π1(X, x0)` on `πₙ(X, x0)` for `n > 1`, as prescribed by the action of the fundamental group on higher homotopy
>Maid's Functorial Equivalence Banquet
The maids are organizing a banquet where the categories of food `Food` and tableware `Tableware` must be equivalent to ensure the perfect dining experience. Prove that the functors `F : Food -> Tableware` and `G : Tableware -> Food` establish an equivalence of categories by showing that there exist natural isomorphisms `η : Id_Food G ∘ F` and `ε : F ∘ G Id_Tableware`, thus ensuring each dish is complemented by the perfect utensil.
>Maid's Enigmatic Yoneda Lemma Invitation
An enigmatic guest has sent a riddle to the mansion's maids, stating that to find the hidden treasure, they must understand the secret behind the Yoneda Lemma. Given a locally small category `C` and a functor `F : C Set`, apply the Yoneda Lemma to reveal the hidden structure of `F` by interpreting the natural transformations from the representable functors `Hom_C(-, A)` to `F` for each object `A` in `C`.

>> No.16094910

>>16094201
>>16094893
>>16094894
>>16094900
>>16094907
>Maid's Cubical Type Assembly
The head maid has decided to construct a new wing of the mansion in the shape of a cube using Homotopy Type Theory. Define a cubical type `Cube` with points, lines, squares, and cubes as constructors. Then, demonstrate the assembly of the cube by filling in the higher-dimensional faces with appropriate homotopies that satisfy the Kan filling conditions.
>Maid's Univalence Puzzle Soiree
The maids are hosting a soirée where every guest brings a type puzzle that can only be solved using the Univalence Axiom. Given a challenging pair of types `A` and `B` that are equivalent but not obviously so, devise a univalent proof `p : A ≃ B` that not only demonstrates their equivalence but also provides an illuminating insight into the subtle properties that make `A` and `B` indistinguishable under univalence.

>> No.16094935

>>16094894
>>16094900
>>16094907
Based af. Too bad I don't know HoTT.

>> No.16094958

>>16094201
i dont want to hear from maidfag until he has solved at least Maid's Braided Path Challenge

>> No.16094960

>>16094935
Neither does he. He just has some shitty AI doing this. I don't usually advocate for the death penalty, but for people like him we should make an exception.

>> No.16094968
File: 44 KB, 500x570, DNn8qtlX4AEvKps.jpg [View same] [iqdb] [saucenao] [google]
16094968

>>16094205

>> No.16094972

>>16094201
>a book with no drawings and just symbols.
imagine the symbols as math maids. examples:
(∫): A meticulous and thorough maid, whose specialty is bringing together disparate elements (functions) into a unified whole (area under the curve).
(Σ): A quick and efficient maid who excels at accounting and can swiftly add up a series of items (terms).
(R, a, ℕ): A trio of maids each specializing in different types of numbers: real, integer, and natural. They could be sisters, each with a unique but complementary personality.
(∂, ∇): Mystical maids with powers to transform things, representing their roles in calculus (derivatives and gradients).
(π, e): Timeless maids with an air of mystery and importance, representing their fundamental roles in mathematics.

Etc.

>> No.16094973

Personally I would advocate for a permanent ban of this faggot off 4chan.

>> No.16094976

>>16094205
>>16094968
>imminent schizo war
Time for some popcorn

>> No.16094979

>>16094201
the fact that maidfaggot is trying to become a cat theorist and work on hott while still struggling with basic arithmetic is so funny to me

>> No.16094991

>>16094904
>>16094960
>>16094973
at least his garbage is easy to filter unlike all the /pol/ leakage. Jannies should rather focus on that

>> No.16095013
File: 45 KB, 420x296, army1.jpg [View same] [iqdb] [saucenao] [google]
16095013

>>16094976
>war
Lol, why on Earth would you assume that? I love Catagory Theory, Set Theory, Coombinatorics, all kinds of similar braches. I use it regularly, pretty foundational, even seeing it used in Theoretical Physics on some youtube guy.

I research reality, you dont seem to.

>> No.16095024
File: 857 KB, 832x1216, 1704672261110781.png [View same] [iqdb] [saucenao] [google]
16095024

>>16094878
>>16094881
>>16094883
>>16094893
>>16094894
>>16094900
>>16094907
>>16094910
>>16094972
Thank you for posting this. I will read it now and try to comprehend it.

>>16094979
I don't have to be good at doing math because the Computer should be doing it for me. I dont even have to "understand" the math, I just have to tell the Computer to do it. The secret power of Computer Science is that I don't have to understand what I am doing to do it. I should tell the Computer to do math and the Computer should do it.

This is why I am asking about Type Theory. Because everyone says it is a Programming Language for Constructive Mathematics and then no explanation is given as to how it works or even how to operate it or write Computer Programs, except sometimes they tell you to play with Coq.

If it is a Computer Language, then probably I can understand it well enough to make Computer Programs so the Computer does math.

I guess I'm looking for a programming book? Something that explains the Computer Language and shows the syntax and semantics and shows example Computer Programs you can make with it? This is how most Computer Languages are taught. Hopefully Type Theory has similar materials to study it more?

>>16094968
>mfw

>>16094904
If you don't like maid threads, why do you go to them?

>> No.16095028

>>16095013
Not at all. All you do is draw a few random commutative diagrams you find pretty. You're an artist, not a mathematician. As Mochizuki once put it:
(AI1) When browsing through Joshi’s series of preprints, i.e., whose content consists of a sort of rough concatenation of various “fragments” of inter-universal Teichm¨uller theory that is nonetheless devoid of any substantivemathematical understanding [cf. (ShtAns)], I could not help but be reminded of the so-called “hallucinations” produced by artificial intelligence algorithms, such as ChatGPT, i.e., which are synthesized precisely
by means of various mechanically searched contextual concatenations that
are entirely devoid of any genuine “human” understanding of the actual
content of the text involved.
(AI2) The observation of (AI1) suggests that in the future, it is quite possible
that the production, or indeed mass production (!), of similar “pseudo-
mathematical texts” by articial intelligence algorithms may become
more widespread and, in particular, pose a substantial threat to the sound
development of the field of mathematics by sewing the seeds of entirely un-
necessary confusion in the worldwide mathematical community concerning
established mathematical theories.

>> No.16095033

>>16094968
arent you the schizo that shat up the thread about schizoids because you got utterly btfo'd by the OP? I literally CTRL+F'd "Cult of Passion" in that thread and 150 posts were highlighted. You are genuinely ill

>> No.16095035

>>16095028
>not a mathematician.
If everything you can do in Mathematics is solvable by and AI...youre a Abacus Engineer.

My Maths can never, and will never, be digitized, simulated at best even in the Q-bit level. That was by design and intentional.

>> No.16095037

>>16095024
>I dont even have to "understand" the math, I just have to tell the Computer to do it.
LOOOOOOL
you have no idea how math research works. Neither does your schizo army vet buddy "cult of passion". Fucking larping retard, your project will go nowhere

>> No.16095040

>>16095037
>your project will go nowhere
Its an Army. An Enterprise of sexuality and autism.

>> No.16095043

>>16095035
>My Maths can never, and will never, be digitized, simulated at best even in the Q-bit level. That was by design and intentional.
Maidfag would beg to differ. All constructive mathematics can be "programmed" in type theory, meaning your schizophasia is non-constructive, essentialist, dogmatic nonsense, like the axiom of choice

>> No.16095044

>>16095033
>got utterly btfo'd by the OP?
Youre delusional and hope others believe you. Its pathetic.

>> No.16095048

>>16095044
>OP writes one concise rebuttal of your post
>you, in turn, shit up the entire thread seething over the new world order
Yeah, I wonder who's won

>> No.16095050

>>16095043
>Maidfag would beg to differ.
Maidfag doesnt work in computer architecture, let alone programming at the architectural level, let alone above that.

I didnt need to ask, ask me how I dont need to ask.

>> No.16095052

>>16095048
If he slips once it will be self admission.

>> No.16095055

>>16095050
Lol maidfag is fairly retarded but probably still much more well-read on computer architecture than you are. What are your qualifications? Fixing your buddy's flashlight in the army?

>> No.16095061

>>16095035
How come you're scared to post your "maths" then?

>> No.16095066
File: 47 KB, 1080x1080, 20230713_232700.jpg [View same] [iqdb] [saucenao] [google]
16095066

>>16095055
You source is yourself; An idiot.

https://youtu.be/f4Dly8I8lMY

Stop LARPing (LYING) to the thread.

>> No.16095073

>>16095040
I beg you, please join maidfaggot's autistic conquest to lobotomize research-level math to weeb fantasies for programmers. Your schizophrenic element is just *the* thing missing from making this whole debacle as repulsive as humanly possible to anyone with elementary school education

>> No.16095074

>>16095061
Because you lack the qualifications, every single time, 100%, you people pull out some university book and hold it up like its the key to Reality.

No, math CAN aling with reality.

>> No.16095077

>>16095066
>le pop sci youtube meme videos instead of research papers
I smell reddit

>> No.16095079

>>16095074
Math IS reality. Name a single branch of math that is not real

>> No.16095080
File: 54 KB, 495x619, images - 2023-12-06T170032.132.jpg [View same] [iqdb] [saucenao] [google]
16095080

>>16095073
>lobotomize research-level math
Over use of arbitrary systems has made you luddites.

Blame yourselves for getting lost in the puzzles of Pure Mathematics.

>> No.16095085

>>16095074
>starts with "Because"
thanks for the implicit admission that you're scared to post your research, dumbfuck. You're still as bad at rhetoric as ever

>> No.16095087

>>16095079
>Name a single branch of math that is not real
Any one that doesnt have Application outside practice.

>> No.16095089

>>16095080
>L-lost in math!!!!
Nobody is. That is propaganda famously spewed by Sabine Hossenfelder, a scientist so inconsequential, she had to resort to low quality pop sci meme videos for schizoids like you.

>> No.16095090

>>16095085
Youre not a Mathematician, youre a Mathematics Technician.

I invent Math, "Do Math", not "shut up and calculate", thats (You)r job, not mine. I write Arith-Metic, not add up a thousand digits for a flex.

>> No.16095093

>>16095087
>Can't find anything explicit
You've lost

>> No.16095096

>>16095089
As if youre "in the know in world Math news outside of YouTube news".

Maybe try being the news. I was researching Catagory Theory in 2016, where were you?

>> No.16095098

>>16095090
>I invent Math
No. You're an artist. All you do is draw pretty pictures that look like math to the untrained eye, but any true mathematician can sense the lack of humanity in it all, as stated by Mochizuki

>> No.16095103

>>16095093
Youre retarded a living embarrassment.

Get a job, maybe manual labor, LYING charlatans like you have no business is serious academia.

>> No.16095106

>>16095096
>I was researching Catagory Theory in 2016, where were you?
Finishing up my masters. For the record, drawing commutative diagrams and fellating over the aesthetics of the Yoneda Lemma is no scientific research, you're merely looking for inspiration in your artistic endeavours

>> No.16095110
File: 1.64 MB, 670x658, spin.gif [View same] [iqdb] [saucenao] [google]
16095110

>>16095098
>You're an artist.
You cant count.

Rigor is Life and Death.

>> No.16095112

>>16095103
As the wise Mandlbaur once said: "Whoever resorts to ad hominem has lost the discussion".
With that, I conclude this to avoid embarrassing you any further.

>> No.16095113

>>16095106
>you're merely looking for inspiration in your artistic endeavours
Combinatorics was used in a recent research paper in Physics......YOURE NOT A PHYSICIST, YOURE A STUDENT LARPING LIKE A DOCTOR TO YOUR PROFESSOR..

YOUR MASTERS MEANS NOTHING TO ME YOU QUASI-LITERATE RETARD.

>> No.16095114

>>16095110 and any post below
cf. >>16095112

>> No.16095120

>>16095112
>>16095114
No, youre a clown of a student and a man-child, fuck out of here....

>> No.16095122

>>16095113
>Combinatorics was used in a recent research paper in Physic
Really? What a revelation. In any case, cf. >>16095112

>> No.16095125
File: 490 KB, 382x498, 1512156087237.gif [View same] [iqdb] [saucenao] [google]
16095125

>>16095122
Youre an asshat, jelous as shit, reeking with envy with pissant paper, you will NEVER be a Mathematician.

Technician, Masters, YOU.

>> No.16095149
File: 377 KB, 1279x1674, Marhemaidics will be a revolution in learning.jpg [View same] [iqdb] [saucenao] [google]
16095149

>>16094878
What is a typing judgement? What is sideways T for?

>>16094881
>like a magical girl transformation sequence
Please explain more how the transformation sequence works and what it is doing? Also, please explain what Topological Space is with maids?

>>16094883
This is about maids learning something which doesn't really help because it isn't using them as an abstraction. It is using them as an audience for lectures devoid of maids and heavy on symbols. I didn't really comprehend it because it had a lot of symbols but not a lot of maids doing things.

I will see if I can understand some of the problems you gave.

>>16094972
This is excellent.

>> No.16095212
File: 413 KB, 220x205, 1710403691435387.gif [View same] [iqdb] [saucenao] [google]
16095212

>>16095125
>>16095149
now this is quite the crossover

>> No.16095347

>Resident schizo gets all pissy and bitter the maid schizo is stealing all the attention
You guys should get a room, on /x/, please go away

>> No.16095356

>namefag and avatarfag
>schizophrenic retards
Didn't see that one coming.

>> No.16095570

>>16095125
You've lost to maidfag out of all people

>> No.16095602

>>16095149
Within the grand mansion of Homotopy Type Theory (HoTT), two types, `A` and `B`, are considered homotopy equivalent, symbolized as `A ≃ B`. Much like the mystical incantations recited by anime magical girls, this equivalence is established if there are functions `f : A -> B` and `g : B -> A` that fulfill the magical conditions `g ∘ f ≃ id_A` and `f ∘ g ≃ id_B`. Here, `id_A` and `id_B` represent the identity functions on `A` and `B` much like the unique identities of each maid in the mansion.
Our maids, trained as masters of homotopy, can weave enchanting spells that transform types into one another. Their skilled incantations are akin to a magical girl performing a transformation sequence, but with an added touch of elegance and finesse. With a flick of their wrists and a swirl of their aprons, they can mold and reshape types as if they were clay, demonstrating their mastery over the abstract world of types
In the vast kitchen of the HoTT mansion, higher inductive types allow our maids to cook up new types by defining their points (objects) and paths (morphisms) all at once. This is achieved by providing a list of ingredients, or constructors, for the type, which can include both point constructors and path constructors. A delightful example is the creation of the circle type `S1`, which is defined as follows:
data S1 : Type where
base : S1
loop : base ≡ base
Our maids, donning their chef hats and wielding their knowledge like a chef's knife, can craft new types with the precision and creativity of world-class pastry chefs. With a sprinkle of logic and a dash of theory, they can whip up a new type as easily as they would a perfect soufflé, delighting the inhabitants of the mansion with their culinary and theoretical skills

>> No.16095605

>>16095149
The Univalence Axiom in HoTT is the grand finale in the mansion's daily performance. It asserts that equivalent types can be interchanged in any context without altering the meaning of a statement. Formally, for any two types `A` and `B`, the type of equivalences between `A` and `B`, denoted as `A ≃ B`, is equivalent to the type of equalities between `A` and `B`, denoted as `A ≡ B`. This can be expressed as:
ua : (A B : Type) (A ≃ B) ≃ (A ≡ B)
With the rhythm of univalence, our maids can switch between equivalent types as effortlessly as they change their uniforms in a synchronized dance. They understand that despite the change in attire, the underlying meaning remains consistent, much like how their roles remain the same regardless of the uniform they wear
In the grand tapestry of Homotopy Type Theory, our anime maids weave intricate patterns of understanding and application. They navigate through complex theories, transforming and creating types, swapping equivalent types, all while adding their unique charm and character to the mansion, making it a truly magical place of learning and discovery

>> No.16095630 [DELETED] 

homosexual type theory is weak ass gay shit. it also doesn’t get grant money anymore lol

voevodsky seemed cool though

posted from my MaidComputer(tm)

>> No.16095633

homosex type theory is some weak ass gay shit. it also doesn’t get grant money anymore lol

voevodsky seemed cool though

posted from my MaidPhone(tm)

>> No.16095851
File: 406 KB, 605x900, 1707922695815613.png [View same] [iqdb] [saucenao] [google]
16095851

>>16095570
Please be nice to Cult of Passion. I have no problems with her and don't understand even what you are talking about.

>>16095602
>>16095605
Thank you for making this. I don't really comprehend it because I don't comprehend the individual concepts that went into making it.

>> No.16095881
File: 38 KB, 375x375, 1453179490159.jpg [View same] [iqdb] [saucenao] [google]
16095881

>>16095098
>Mochizuki
Wow, I like this guy's work, we overlap a lot, though I go far deeper into Numeration Theory, far more foundational, not a combination of tools like CombinGaussianBlahBlah.

Make tools, not just use them.

>> No.16095904
File: 316 KB, 1200x831, Plimpton_322 (2).jpg [View same] [iqdb] [saucenao] [google]
16095904

>>16095881
>Make tools
I say this because I invented Set Theory, Catagory Theory, Cominatorics, and many others, and then went on an adventure through books and university halls finding what to call them because theyre already invented.

The interesting parts are when two soultions come from vastly different answers, this is repeated in human history like many other things.

Those tools are the ones Im looking for, whatever you humans have is not what Im interested in.

https://youtu.be/2NjkcjueR4k

>> No.16095917
File: 1.89 MB, 320x320, 1551286843879.gif [View same] [iqdb] [saucenao] [google]
16095917

Which all those Maths named in this thread becoming popular, made them revolting to me.

Then I had to go into hyper or sub-dimensional to get where no icky humies touch...
[seperates all food on the plate]
Autism is fundemental to reality.

>> No.16095925
File: 1.89 MB, 320x320, 1551285865646.gif [View same] [iqdb] [saucenao] [google]
16095925

Mmm...nostalgia...Just like math, move the = to the other side and play it back.

Time is so fickle...isnt it?

>> No.16095961
File: 60 KB, 325x250, 1514491176995.jpg [View same] [iqdb] [saucenao] [google]
16095961

>>16095851
>her
Which, reductionism (the act of measure in Physics), is feminine in nature, use of it is not.

Directly tied to Genetic Hybridization as a form of Symbiosis dating back billions of years. Evolutionary braches appear to operate on a male/female sequencial pairing.

>> No.16095969
File: 47 KB, 520x590, images (3) (20).jpg [View same] [iqdb] [saucenao] [google]
16095969

>>16095961
>male/female sequencial pairing
Meaning a species will be male, then a female alteration will be made.

Reptilian to Avian is an expample, Oyster and Cephalopod is another, I havnt cracked Insect full, Ive seen another deep in Africa that was not 'animal', more like living stone and extremely ancient. Plant, fungal being universal in humans in archaic forms.

This picture, but 3.5-Dimensional but with a multiplier because its reflective of itself, and (You).

>> No.16095972
File: 58 KB, 547x561, images (4) (2).jpg [View same] [iqdb] [saucenao] [google]
16095972

Every Gene emmitting meta-waves into humanity, every germ, every virus, cycles of living beings emerging.

Big Math.

>> No.16095974
File: 2.37 MB, 320x133, 6df02ec38c2dc991f2fbd44568a51d541d793564_00.gif [View same] [iqdb] [saucenao] [google]
16095974

>>16095972
At certain level, its fractals but alters, these breaks are where loose fitting constants can work wonders (think Numerology). And Maths like here are loose fittingz hence why theyre common and so wide spread.

The Math is easier, if you have an infinity hat.

>> No.16095976

>>16095080
>lobotomize research-level math
Because of over specification in definitions that made what we had (more over specified definition), exponentially specific, which exponentially exclluded application at the cost of absolute measure, which isnt always appropriate, especially Theory.

>> No.16095980

>>16095881
>>Mochizuki
>Wow, I like this guy's work
I'm sure you like the aesthetics of his math papers, his looks, and status in the math communuty but don't pretend to have the humanity needed to truly comprehend his work on Inter-Universal Teichmüller Theory. You and maidfag are basically chatbots

>> No.16095982
File: 126 KB, 800x1008, Tom_Cruise_by_Gage_Skidmore_2.jpg [View same] [iqdb] [saucenao] [google]
16095982

>>16095976
Like Psychiatry, sometimes fields venture into the woods...it takes a maverick to pull it back.

>> No.16095985
File: 132 KB, 980x653, 1512808819431.jpg [View same] [iqdb] [saucenao] [google]
16095985

>>16095980
>Inter-Universal
I dont deal with nonsense, sorry, I study reality.

>> No.16095988

>>16095985
Mochizuki destroyed you

>> No.16095991

>>16095988
Arbitrary calculations are arbitrary, inconsequencial to reality and a puzzle to Mathematicians, nothing more.

You should lurk my threads more and LARP less.

>> No.16095992

>>16095985
https://www.kurims.kyoto-u.ac.jp/~motizuki/Report%20on%20a%20certain%20series%20of%20preprints%20(2024-03).pdf

>> No.16095993

>>16095992
Youre clearly not capable of comprehending what I posted, youre just star gazing at ny while holding up your hero.

Ive done what hes done and did the same all around the world, stop...

>> No.16095994

>>16095851
>Please be nice to Cult of Passion
All this faggot does is derail your thread. You'll hate him soon enough

>> No.16095997

>>16095994
What did you think this Math is used for?...............loke, WHY people study it.

To do homework? No, school isnt reality.

>> No.16096000

>>16095997
>school isnt reality
Only in America. Not the case in Africa for instance. Mandlbaur can attest to that and has previously BTFO'd you on that point

>> No.16096004
File: 46 KB, 720x720, 2022-12-14_00.47.32.jpg [View same] [iqdb] [saucenao] [google]
16096004

>>16096000
>Not the case in Africa for instance.
Have you visited African schools? I picked up one of their school books in Zanzibar.

Ive also visited them in Korea, tutored for some months, very interesting Longuistics research for Cognition research.

>> No.16096009

>>16096004
Korea's school of longuistics is terrible, what are you saying

>> No.16096015

>>16096004
You should send this book to maidfaggot, she loves radix bases

>> No.16096019

>>16096009
>Korea's school of longuistics is terrible
Irrelevent Dimension of Analysis, human, I was tutoring intermediate English to middleschoolers.

The contexts of Time, specifically, did wonders for my Mathematical Linguistics research, as a type of Cognitive perspective, how Genes or "Nature" perceives reality and how to plan for future events, similar to telomeres, a type of Molecular Clock.

>> No.16096023

>>16096019
>a type of Molecular Clock.
Which is rooted in Chemistry/Physics, which we need Maths for, so whatever.....

>> No.16096024

>>16096019
To thinl they'd let someone as mental as you near middle schoolers says a lot about US colonies

>> No.16096029

>>16095347
HAHAHAHAH...

>> No.16096030
File: 57 KB, 389x259, 2021-11-08_17.29.22.jpg [View same] [iqdb] [saucenao] [google]
16096030

>>16096024
I am a very simple, normal, man in the outside.

I like family events, grand parents with kinds and home cooked meals.

>> No.16096031

>>16095993
I HAVE WON....

>> No.16096032
File: 2.41 MB, 1080x2448, Screenshot_20240325-215706_Photos.jpg [View same] [iqdb] [saucenao] [google]
16096032

>>16096030
>kinds
kids*

Little kids and smiles and candy and learning wonderful things.

>> No.16096034

>>16096032
Post some more pics from when you were in the army. Maybe that'll inspire maidfag

>> No.16096037

>>16095976
It is how it is....

>> No.16096038
File: 1.23 MB, 1933x3712, 1704472784598703.jpg [View same] [iqdb] [saucenao] [google]
16096038

>>16096032
I'm guessing you saw some unpleasant things in the army. It isn't exactly known for being a nice place or engaging in nice things.

>> No.16096039

>>16095149
>What is a typing judgement?
Son, you have a lot to learn...

>> No.16096041

>>16095149
/mg/ has given you at least 1000 pages of introductory type theory you have no excuse

>> No.16096043

>>16096038
huh I thought I had you filtered

>> No.16096048
File: 129 KB, 960x721, 1572955999482.jpg [View same] [iqdb] [saucenao] [google]
16096048

>>16096038
>I'm guessing you saw some unpleasant things in the army.
I once saw two bodies take up three trash bags.

It was fun except for all the blood and tears.

>> No.16096051

>>16096038
You should join the army.

>> No.16096053

>>16096048
>two bodies take up three trash
Math, I mean...how? In what base system is this divided? Dynamically? All of it, jeez...big math...

>> No.16096055

>>16096048
I still have nightmares from that...

>> No.16096058

>>16096038
Afghanistan is a place fulll of very hospitable people, you will like it

>> No.16096060

>>16096038
I'll be camping in Afghanistan this winter, you should join me...

>> No.16096067

Dont reply to Cult of Passion
>thread exposing him
>>/sci/thread/15358061

>> No.16096071

>>16096067
ublock etc block that shit with rule:
boards.4channel.org##.post:has(.name:has-text(Cult of Passion))
boards.4channel.org##.post:has(.name:has-text(Doctor Eli))

>> No.16096075

>>16096071
The redditor augments his reality like a dive suit, venturing into hostile environments he never could have survived otherwise.

>> No.16096078

>be me a few years ago
>find out something that would change my life
>something that would drive me so far into a passion that I would spend hundreds
>upon Hundreds
>upon HUNDREDS of hours on the subject, reading alone in my dimly lit apartment
>hell, risk imprisonment for trespassing in order to get more information
>not just that, but even enter a local group that threatened to end their lives daily
>cults, go figure
>but what had come to my knowledge last year was that father had been best friends with a "special" man, one who he could only describe to me as "ENLIGHTENED"
>the man's name was David Geoffery Moore
>but what was so IMPORTANT about father's friend wasn't who he was or how he lived, but how he died
>so, find out my FATHER was close friends with one of the deceased, from the infamous "Heaven's Gate" mass suicide
>who?
>David GEOFFERY Moore.

http://www.youtube.com/watch?v=IzWpfq103q4

>be me after hearing that 2SPOOKY shit
>ever since then, be OBSESSED with everything regarding cults
>as said earlier, spend couple of days WITHOUT sleep trying to absorb knowledge...
>search for any info about cults in recent HISTORY , for hours without pause
>become so intrigued that I try MULTIPLE times to obtain police footage taken of the most recognized CULT in the local area, but sadly fail...
>like you, HAVE to then base my opinions off the censored and concentrated videos the media spews forth...
>but thats not GOOD enough
>need to know more than just 3DPD news coverage...

>so, be me month later
>attempt CONTACT with the 2nd most notable cult in local area...
>eventually, after months of trying in vain to join it, get a response someday

>be me that faithful day
>check mailbox for sports mag, but find something else...
>???
>a folded piece of paper
>on the outside reads "From Anonymous"
>on the inside, reads in all caps a location
>the location where I'd find all the answers
>answers that I'd spent half a good year looking for...
>"FIND US AT X, OR WE FIND YOU"

>> No.16096081

>>16096075
>>16096078
I hope you get the help you need ;)
Anyway, get filtered. Haven't got the time, sorry

>> No.16096082

>>16096078
You have no clue the Forces you speak of...so easy to do, destruction, is easy.

https://youtu.be/kxWvq9dMEbo

>> No.16096083

>>16096081
Your inability to distinguish a genius and an idiot is glaringly retarded of you...thats inexcusable to a Man.

>> No.16096120
File: 255 KB, 1280x1795, 1709164549542174.jpg [View same] [iqdb] [saucenao] [google]
16096120

>>16096051
>>16096058
>>16096060
I am not allowed in the military and probably also not allowed in Afghanistan.

>>16096041
Thank you for telling me. I didn't realize they had replied to my post. I will read the materials they gave.

>> No.16096139

>>16096058
>>16095869
>For half the trip I was referred to by the people around me as "the enemy", they thought I didnt know, I did...

Its not for people without a sense of direction and wherewithall.

>> No.16096238

>>16096120
>I am not allowed in the military and probably also not allowed in Afghanistan.
So you're a Russian SPY. Quit talking to me then.......

>> No.16096243

>>16096120
Also, see >>16096083

>> No.16096248

>>16096120
I sense EVIL in you....