You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Peiyuan Zhu (Jan 04 2022 at 23:59):How to understand dependent type? What does ":" mean? Can I call it "is of" and "is"? What's its operational priority compared to forcing? I think the leftist ":" gets evaluated first and then "|-" and then the rightest ":", so like B(t) is a type that depends on t which is of type A. Does this correspond to a line of code in agda? I'm still trying to setup agda on my computer, what kind of IDE do people usually use? image.png
How to understand dependent sum and dependent products? The text says dependent sum corresponds to conjunction and total space, while dependent product corresponds to implication and section, and they "appear in gauge field theory often in the guise of principal bundles", how? image.png
Peiyuan Zhu (Jan 05 2022 at 01:23):What are the levels about? From the previous paragraph the levels seem to be related to one another by questions that reduces more complicated structures to simpler ones. It's said 'what homotopy type theory
does is take observations such as these not merely as an analogy, but as the first steps of a
series of levels.' which seems to be talking about the very fundamental of how intuitionistic mathematics work. image.png
Mike Shulman (Jan 05 2022 at 01:51):I find it very confusing to have a single topic called "beginner questions" in which lots of very different questions and their answers get mixed together. Wouldn't it make more sense to open a separate topic for each question?
Peiyuan Zhu (Jan 05 2022 at 02:30):Yea I guess maybe I can open a new topic for dependent types?
Morgan Rogers (he/him) (Jan 05 2022 at 11:20):I've moved this discussion to such a topic on your behalf :)
Mike Shulman (Jan 05 2022 at 17:40):You have a lot of questions; I'll try to answer some of them.
Mike Shulman (Jan 05 2022 at 17:40):should be parsed as .
Mike Shulman (Jan 05 2022 at 17:40):More generally, should be parsed as .
Mike Shulman (Jan 05 2022 at 17:41):The standard interface to Agda is the Emacs mode.
Mike Shulman (Jan 05 2022 at 17:42):The colon in type theory is like the set-membership sign , but differs in that it is a judgment rather than a proposition. That means that the type an element belongs to is an intrinsic property of it, and (with certain exceptions) is unique, whereas in set theory one can consider elements separately from sets and ask which set or sets an element might belong to.
Mike Shulman (Jan 05 2022 at 17:42):What text are you reading? What others have you looked at? There are plenty of good introductions to dependent type theory out there that would answer many of your other questions.
Peiyuan Zhu (Jan 05 2022 at 22:55):I'm currently reading modal HoTT by David Corfield, I think philosophy is a good context that I can grasp, but when he talked about algebraic geometry I had no idea how logic and geometry are related to one another, and how to write this in program
Peiyuan Zhu (Jan 05 2022 at 22:58):My primary interest in to understand imprecise probabilities with modal HoTT https://www.researchgate.net/publication/328494616_Visions_of_a_generalized_probability_theory
Peiyuan Zhu (Jan 05 2022 at 23:04):Mike Shulman said:
The colon in type theory is like the set-membership sign , but differs in that it is a judgment rather than a proposition. That means that the type an element belongs to is an intrinsic property of it, and (with certain exceptions) is unique, whereas in set theory one can consider elements separately from sets and ask which set or sets an element might belong to.
So for imprecise probability, a judgement is exactly an assertion that the truth is in some subset of a set, except the judgement is probabilistic. The Dempster-Shafer rule combines the judgements into one assuming probabilistic independence. The combined outcome is accessed upper-and-lower intervals by taking a set of interest that intersects or contains these sets. There's also this fibre bundle structure in the projection algorithm that I believe is highly similar to what I read in Modal HoTT.
John Baez (Jan 05 2022 at 23:10):when he talked about algebraic geometry I had no idea how logic and geometry are related to one another, and how to write this in program
This connection is what topos theory is all about.
John Baez (Jan 05 2022 at 23:15):Mac Lane and Moerdijk's book Sheaves in Geometry and Logic is the obvious book on that.
Peiyuan Zhu (Jan 05 2022 at 23:22):John Baez said:
Mac Lane and Moerdijk's book Sheaves in Geometry and Logic is the obvious book on that.
What kind of geometry background is assumed for a book like this? I only know bit of Riemanian geometry and Euclidean geometry, which can be very different I think. Also what kind of logic background? I only know standard math curriculum such as Boolean logic, set theory, truth table, and quantifier. I guess I shouldn't assume somehow Euclidean geometry has some deep connection with Boolean logic.
John Baez (Jan 05 2022 at 23:29):Looking at the book, it seems you'll only need to know some basic stuff about manifolds.
Zhen Lin Low (Jan 05 2022 at 23:30):I don't think you even really need to know manifolds, just topological spaces.
John Baez (Jan 05 2022 at 23:31):Well, in Section II.3, "Sheaves and manifolds", the book gives examples of sheaves on manifolds. One could skip that section but it's a bit sad to study sheaves without many interesting examples. Luckily, since Peiyuan says he knows some Riemannian geometry he presumably knows a bit about manifolds.
John Baez (Jan 05 2022 at 23:35):Looking a bit harder at this book, I see it doesn't spend a lot of time explaining how topos theory is connected to algebraic geometry, but it also doesn't assume prior knowledge of algebraic geometry. There's a brief introduction in section III.3, "The Zariski site".
Zhen Lin Low (Jan 05 2022 at 23:37):I think that's about as much as you could hope to cover without prerequisite knowledge about schemes...
John Baez (Jan 05 2022 at 23:39):Yeah. And I don't think Peiyuan actually wants to learn algebraic geometry, which is sort of a serious job in itself.
Zhen Lin Low (Jan 05 2022 at 23:42):It's been close to 10 years since I read the book, but what I am sure about is that it is far more important to have a solid grounding in category theory – limits, colimits, functors, concrete categories of common algebraic structures – than detailed knowledge of general topology or manifolds or logic.
Peiyuan Zhu (Jan 05 2022 at 23:45):I see. I guess when I read it the question that I should ask about is whether imprecise probability can be written in this language like this but also whether there shall be some new mathematical device to be invented to talk about it
Peiyuan Zhu (Jan 05 2022 at 23:45):Just this murder trial example of imprecise probability make it a lot like what topos theory is about image.png
John Baez (Jan 05 2022 at 23:59):It would be more efficient to talk to someone who knows topos theory, how topos theory has been used in fuzzy logic, etc.
John Baez (Jan 06 2022 at 00:00):However, finding the right people and convincing them to talk can be a bit hard sometimes.
Peiyuan Zhu (Jan 06 2022 at 00:01):Interesting. Are you saying someone must have done this already?
John Baez (Jan 06 2022 at 00:04):No, I'm just saying that there exist people who could figure this out 100 times faster than you, so talking to them - repeatedly, not just once - could greatly accelerate your project.
Peiyuan Zhu (Jan 06 2022 at 00:04):I see, thanks!
John Baez (Jan 06 2022 at 00:04):(This is true of many people's projects - I'm not trying to be mean to you!)
John Baez (Jan 06 2022 at 00:07):Is this paper at all helpful?
https://www.sipta.org/isipta19/contributions/crane19.pdf
John Baez (Jan 06 2022 at 00:07):I'm not claiming it is... it's just what showed up when I did a one-minute search.
Peiyuan Zhu (Jan 06 2022 at 00:10):Yeah that sounds like it, I guess I didn't expect a paper with such title would be relevant (also might have filtered out a lot of formal reasoning paper because I'm not familiar with the syntax, but it doesn't mean I don't need to get familiar with it)
Peiyuan Zhu (Jan 06 2022 at 00:11):Thanks a lot
Peiyuan Zhu (Jan 06 2022 at 00:11):It really speeds up 5e10 times faster
Fawzi Hreiki (Jan 06 2022 at 00:15):Topos theory relates to geometry insofar as it gives a language in which to talk about local behaviour and glueing
Fawzi Hreiki (Jan 06 2022 at 00:16):Which is of course prevalent all throughout topology and geometry.
Fawzi Hreiki (Jan 06 2022 at 00:19):A good starting point is the definition of a smooth manifold as a certain kind of locally ringed space.
Peiyuan Zhu (Jan 06 2022 at 00:23):Hmm... this sounds like what you mean image.png
Fawzi Hreiki (Jan 06 2022 at 00:24):Yes it seems to be. The reason this approach is important is that it generalises very quickly to many different kinds of ‘glued spaces’ such as complex-analytic spaces, schemes, etc
Fawzi Hreiki (Jan 06 2022 at 00:26):The correct framework for such ‘function structured spaces’ is the theory of ringed toposes.
Peiyuan Zhu (Jan 06 2022 at 08:53):John Baez said:
Yeah. And I don't think Peiyuan actually wants to learn algebraic geometry, which is sort of a serious job in itself.
When I'm reading HoTT, I found it hard to understand the 'homotopy' part. How come topology, paths, groupoid, fiber section one of a sudden become relevant? (there hasn't been a definition of manifold appearing yet) Are we saying a program is really different algebraic structures? I think to understand this better I'll have to seriously study algebraic geometry, although it can be of lower priority for now before I pick up/formalized the basics. For example, I would ask where is topology when I'm proving a fibonacci sequence, and what are the paths are they just flow of inference or intuitions, and why use groupoid instead of group, what's the use of fiber section here... I think these cannot be explained easily without algebraic geometry? I found this discussion really helpful, so I can really pinpoint what I don't know. I think another good starting point for me is to write Boole's Investigation into Laws of thoughts in the language of algebraic geometry.
Zhen Lin Low (Jan 06 2022 at 08:57):It is an analogy (that can be made precise). You don't have to think too hard about it now. Algebraic geometry is not relevant.
Peiyuan Zhu (Jan 06 2022 at 08:58):I think it can be relevant some day no? What if thermodynamics can be written in the language of algebraic geometry? That would make all the difference.
Zhen Lin Low (Jan 06 2022 at 09:00):Let me add some words. Algebraic geometry is not relevant to the interpretation of HoTT in ∞-groupoids.
Peiyuan Zhu (Jan 06 2022 at 09:03):I think it may still be important to really understand it no? By understanding it kinda means that all things considered.
Peiyuan Zhu (Jan 06 2022 at 09:03):For example, I cannot see why group is not enough
Zhen Lin Low (Jan 06 2022 at 09:04):Algebraic geometry does not (alone) hold the answer to that. Algebraic topology would be a better place to look.
Peiyuan Zhu (Jan 06 2022 at 09:07):Zhen Lin Low said:
It is an analogy (that can be made precise). You don't have to think too hard about it now. Algebraic geometry is not relevant.
I was hoping analogy will end-up being something fundamental, but maybe this is not true, at least at this point in time
Peiyuan Zhu (Jan 06 2022 at 09:08):Zhen Lin Low said:
Algebraic geometry does not (alone) hold the answer to that. Algebraic topology would be a better place to look.
Can you elaborate on the difference? Are they trying to answer fundamentally different questions, if so what are the questions that they're trying to answer that are different
Zhen Lin Low (Jan 06 2022 at 09:11):Algebraic geometry and algebraic topology are different subjects, and fundamentally about different things (varieties vs topological spaces). In modern research they use some of the same tools so you will see the same language being used, but the roots are different.
Fawzi Hreiki (Jan 06 2022 at 12:36):A simple explanation is that algebraic topology studies spaces by associating to them algebraic invariants, while algebraic geometry builds spaces from algebraic equations and structures.
Peiyuan Zhu (Jan 06 2022 at 19:45):Ahh I think Galois theory might have much more to do with this question than the theories that I just looked at
Peiyuan Zhu (Jan 06 2022 at 19:46):https://link.springer.com/chapter/10.1007/978-1-4020-1898-5_1
John Baez (Jan 07 2022 at 00:43):Peiyuan wrote:
When I'm reading HoTT, I found it hard to understand the 'homotopy' part. How come topology, paths, groupoid, fiber, section one of a sudden become relevant? (there hasn't been a definition of manifold appearing yet) Are we saying a program is really different algebraic structures? I think to understand this better I'll have to seriously study algebraic geometry [...]
That's a strange last sentence, because all the concept you just mentioned are about topology: topology, paths, groupoid, fiber, section. To understand homotopy type theory you need to understand how topology is connected to logic. Algebraic geometry is not so relevant here!
John Baez (Jan 07 2022 at 00:46):(there hasn't been a definition of manifold appearing yet)
To be more specific, to understand HoTT you need to understand how a specific aspect of topology is connected to logic: homotopy theory. Homotopy theory is not primarily about manifolds, so you shouldn't care about manifolds too much when learning HoTT.
I imagine the HoTT book talks quite a lot about homotopy theory and logic, and how they're connected.
Peiyuan Zhu (Jan 07 2022 at 02:00):John Baez said:
Peiyuan wrote:
When I'm reading HoTT, I found it hard to understand the 'homotopy' part. How come topology, paths, groupoid, fiber, section one of a sudden become relevant? (there hasn't been a definition of manifold appearing yet) Are we saying a program is really different algebraic structures? I think to understand this better I'll have to seriously study algebraic geometry [...]
That's a strange last sentence, because all the concept you just mentioned are about topology: topology, paths, groupoid, fiber, section. To understand homotopy type theory you need to understand how topology is connected to logic. Algebraic geometry is not so relevant here!
Is there something like 'how algebra is connected to logic'? I didn't find anything like this but the book I found in the previous post in Galois theory seems to included all important people, or is this assumed to be known by everyone, because logic IS algebra?
Zhen Lin Low (Jan 07 2022 at 02:47):I wouldn't say that. Algebra is a tool used to study logic. Logic is sometimes used to study algebra.
Zhen Lin Low (Jan 07 2022 at 02:53):I notice you are asking a lot of "how is X connected to Y" questions. Here's some unsolicited advice: you should first spend some time learning the basics of either X or Y, or better yet, both. Because if you don't, honest answers are likely to fly over your head and not be very convincing.
John Baez (Jan 07 2022 at 03:45):Is there something like 'how algebra is connected to logic'?
Yes, there are several subjects that study this. You can probably name any two big subjects like algebra, geometry, logic, topology, analysis and find a bunch of work connecting them. E.g. algebraic geometry, geometric algebra, etc. etc. etc.
Peiyuan Zhu (Jan 07 2022 at 03:56):Hmm… I see, I’m just trying to find out which one is the most important to give a solid understanding of semiotics… because by looking at that book it seems that some people might just say they’re ‘obviously’ consisting of one lines of thought in history, just in the way how they’re written makes me think that there’s a very deep reason that they’re put together
Peiyuan Zhu (Jan 07 2022 at 03:56):7CFAE4B1-5636-4FC4-B0E4-5ECD5B889D7D.png
John Baez (Jan 07 2022 at 03:59):What book is this from? This page is just a long list of related ideas. I think it's better to focus on something concrete. For example, most of the ideas on this list are connected to 'adjoint functors' - one of the most important concepts in category theory. If you want to do anything with category theory you need to understand adjoint functors. So you might try to learn about those.
Peiyuan Zhu (Jan 07 2022 at 04:15):It’s from a book with topic: Adjunctions and Galois Connections: Origins, History and Development https://link.springer.com/chapter/10.1007/978-1-4020-1898-5_1
The reason that I encountered this chapter is while reading Laws of Thoughts on probabilities by George Boole, there are sets of probabilistic algebraic equations that comes from everyday language that needs to be approximated by intervals, so I was thinking whether there is such a numerical method that is well-known in mathematics that give these interval estimates to large sets of algebraic equations or whether anyone has studied the algebraic structures of these type of equations.
The theory of imprecise probabilities talks a lot about lattices but the algebraic side is not discussed very often (not even was pointed out in any papers I read, mostly dived directly into a setting of a power set and probabilistic mappings into the power set). Galois connection seems to be the basis of any numerical algorithms (I even saw a paper on second law of thermodynamics being a special Galois connection), or at least in my superficial knowledge has something to do with solving algebraic equations. So somehow this paper is wrapping everything together. But I also don’t know how complex a math topic like this is and whether it will be helpful for my understanding. Not sure if my approach is the best to do this.
While the HoTT book (along with the book John sent yesterday) seems has a lot to say about algebraic geometry (or topology?), I wonder if that ‘algebraic’ really has anything to do with the systems of probabilistic equations that I’m trying to understand. There’s also this book Geometry of Uncertainty that talks about geometry but I’m still trying to see if it has anything to do with the ‘geometry’ or ‘topology’ in HoTT.
But what seems certain is that imprecise probabilities such as possibility theory must be something to do with toposes, I’m just trying to dig that out.
Peiyuan Zhu (Jan 07 2022 at 04:30):It’s astonishing that these fields have a lot of shared structures, but I haven’t yet found a unifying theory, which I think is where category theory can be helpful
Peiyuan Zhu (Jan 07 2022 at 04:30):Or even just a unifying story
John Baez (Jan 07 2022 at 17:56):While the HoTT book (along with the book John sent yesterday) seems has a lot to say about algebraic geometry (or topology?)
I haven't read the HoTT book carefully, but my impression is that it says almost nothing about algebraic geometry.
John Baez (Jan 07 2022 at 17:57):In case it's not clear yet, algebraic topology and algebraic geometry are quite different subjects.
John Baez (Jan 07 2022 at 17:58):But what seems certain is that imprecise probabilities such as possibility theory must be something to do with toposes, I’m just trying to dig that out.
Have you seen Michael Barr's paper on toposes in fuzzy set theory? If I had to invent a way to use topos theory for "imprecise probabilities", I might start there. (Of course I already know some basic topos theory. If you don't, you should start by learning that.)
Peiyuan Zhu (Jan 07 2022 at 23:38):John Baez said:
While the HoTT book (along with the book John sent yesterday) seems has a lot to say about algebraic geometry (or topology?)
I haven't read the HoTT book carefully, but my impression is that it says almost nothing about algebraic geometry.
As mentioned previously by @Zhen Lin Low it has more to do with algebraic topology. Why is this analogy important? Why do people like this idea for programming languages? Do people expect some day this language to be used for programming quantum computers?
Zhen Lin Low (Jan 07 2022 at 23:45):The analogy is important if you want to do HoTT, because we – the collective body of all mathematicians – know a lot more about algebraic topology than HoTT right now. The situation may change in the future. But it is not by any means necessary: conceivably, a genius could appear who could discover great things in HoTT directly without relying on the crutch of foreknowledge of algebraic topology.
Zhen Lin Low (Jan 07 2022 at 23:47):I would not say people like this idea for programming languages. You may get that impression if all you read is the writing of HoTT or computer verification advocates, but I guarantee if you go talk to actual software engineers most will not even have heard of dependent types.
Zhen Lin Low (Jan 07 2022 at 23:50):As for quantum computers, I don't think type theory as usually conceived is suitable. Linear type theory is probably more appropriate.
Peiyuan Zhu (Jan 07 2022 at 23:57):How about Modal type? It just came to me because I heard of the 'possible world interpretation' of quantum mechanics, which I think has some correspondence with the philosophical 'possible world', which was referenced many times in Modal HoTT
Zhen Lin Low (Jan 07 2022 at 23:59):I think those turn out to be quite different if you look into the underlying mathematics.
Mike Shulman (Jan 08 2022 at 02:03):Zhen Lin Low said:
conceivably, a genius could appear who could discover great things in HoTT directly without relying on the crutch of foreknowledge of algebraic topology.
In fact, there are already students who learned HoTT without much prior exposure to classical algebraic topology, and who've discovered new things about it that us oldsters didn't notice.
Mike Shulman (Jan 08 2022 at 02:04):Zhen Lin Low said:
I would not say people like this idea for programming languages. You may get that impression if all you read is the writing of HoTT or computer verification advocates, but I guarantee if you go talk to actual software engineers most will not even have heard of dependent types.
In other words, some people like this idea, while others haven't learned to like it yet. (-:O
John Baez (Jan 08 2022 at 04:15):In my mind homotopy type theory is mainly important as part of the ongoing homotopification of mathematics. As Yuri Manin said:
Instead of sets, clouds of discrete elements, we
envisage some sorts of vague spaces, which can be
very severely deformed, mapped one to another,
and all the while the specific space is not important,
but only the space up to deformation. If we
really want to return to discrete objects, we see
continuous components, the pieces whose form or
even dimension does not matter. Earlier, all these
spaces were thought of as Cantor sets with topology,
their maps were Cantor maps, some of them
were homotopies that should have been factored
out, and so on.
I am pretty strongly convinced that there is an
ongoing reversal in the collective consciousness of
mathematicians: the right hemispherical and
homotopical picture of the world becomes the basic
intuition, and if you want to get a discrete set, then
you pass to the set of connected components of a
space defined only up to homotopy.
That is, the Cantor points become continuous
components, or attractors, and so on—almost from
the start. Cantor’s problems of the infinite recede
to the background: from the very start, our images
are so infinite that if you want to make something
finite out of them, you must divide them by another
infinity.
John Baez (Jan 08 2022 at 04:18):Thus, in homotopy type theory the basic entities are not sets but homotopy types.
Peiyuan Zhu (Jan 08 2022 at 05:02):Seems like Modal Homotopy Type is used in geometry:
[1] https://arxiv.org/pdf/1806.05966.pdf
[2] http://nlab-pages.s3.us-east-2.amazonaws.com/nlab/show/geometric+homotopy+type+theory
Also algebra
http://nlab-pages.s3.us-east-2.amazonaws.com/nlab/show/Galois+theory#GaloisInTopos
Peiyuan Zhu (Jan 08 2022 at 05:09):So it's not just topology
John Baez (Jan 08 2022 at 05:10):Yes, but now you're talking about the use of modalities to capture "cohesion".
John Baez (Jan 08 2022 at 05:11):I'll admit I'm getting a bit tired of talking about things in such a vague, sketchy manner. It's like flying over the country at an altitude of 100,000 feet, where even the biggest mountains look tiny, and all the smaller details are lost.
Peiyuan Zhu (Jan 08 2022 at 05:13):I think I already have enough to start, Thanks! I also have found the word 'sheaf' being mentioned in the book that I'm reading so I'll have a very concrete example to work on.
Peiyuan Zhu (Jan 08 2022 at 05:20):To me it's been good to first sort unknown subjects by complexity & relevancy, before digging in. I think this is the most resource-efficient way than dig in and then realize there's something fundamental missing, so all the knowledge semantics needs to be reconstructed somehow to fit the most relevant narrative, or that spending so much time pursuing something and then realize it is trivial in another discipline, which can be frustrating and inefficient. My charts have been university mathematics, so I've been operating in this 'possible world' of mathematics with cardinality 2^n where n in the number of subjects of advanced mathematics, which is huge.
Jon Sterling (Jan 08 2022 at 12:50):It really is better to just dive in, and learn the Grand Narratives once you have some context for them.
David Egolf (Jan 09 2022 at 01:21):Peiyuan Zhu said:
To me it's been good to first sort unknown subjects by complexity & relevancy, before digging in. I think this is the most resource-efficient way...
For what it's worth, I feel that focusing on something in detail (even near-randomly chosen!) can sometimes substantially accelerate the process of characterizing unknown subjects. Sometimes authors assume prerequisites that they don't list anywhere, and you'll only realize that you needed to know something after you've already learned it. For example, I really underestimated the value of knowing some basic topology, and I was only able to recognize this once I learned some!
Peiyuan Zhu (Jan 09 2022 at 03:30):Thanks for the great advices. So I started writing a proof of category theory, and I began with the category of relations, thinking that it's going to be useful later on. Is it possible to do this proof in HoTT, since there're existential quantifiers? image.png If this is possible I'll try to find a way to do it, but just wanted to make sure it's something possible.
Matteo Capucci (he/him) (Jan 09 2022 at 09:00):Good start, just catching a small misnomer in ther: what you call commutativity is actually associativity
Peiyuan Zhu (Jan 09 2022 at 16:48):Ah good catch my math really got rusty :)
Peiyuan Zhu (Jan 09 2022 at 16:48):A stack exchange post: does type theory have a concept of relation: https://math.stackexchange.com/questions/1265598/does-type-theory-have-a-concept-of-relation
Reid Barton (Jan 09 2022 at 17:21):Questions like this are tricky to answer because "type theory" doesn't refer to a single specific thing. ("Set theory" isn't necessarily a single specific thing either, but most people would assume you mean ZFC.)
In a type theory which is intended to be used as a language for ordinary mathematics, the answer is yes because a relation is a notion of ordinary mathematics.
Reid Barton (Jan 09 2022 at 17:21):Typically you would have a universe of propositions Prop and define a relation between A and B to be something of type A -> B -> Prop.
Peiyuan Zhu (Jan 11 2022 at 03:14):Reid Barton said:
Questions like this are tricky to answer because "type theory" doesn't refer to a single specific thing. ("Set theory" isn't necessarily a single specific thing either, but most people would assume you mean ZFC.)
In a type theory which is intended to be used as a language for ordinary mathematics, the answer is yes because a relation is a notion of ordinary mathematics.
Would I get a different answer if I restrict myself to HoTT?
Peiyuan Zhu (Jan 11 2022 at 03:16):What's the difference between "|-" versus "-|" and "|=" and "|->"in type theory? I head the third means forcing and the fourth means transportation, but not sure about the first two. Are they referring to adjointness?
James Wood (Jan 14 2022 at 11:28):Even restricting to HoTT, you'll have to worry about propositional resizing and (im)predicativity. The most basic answer (i.e, Book HoTT with none of the optional axioms) is that relations become large, and you have to keep track of their size (universe level). But I think it still basically works to have relations be binary maps into a universe of h-propositions.
James Wood (Jan 14 2022 at 11:39):Peiyuan Zhu said:
What's the difference between "|-" versus "-|" and "|=" and "|->"in type theory? I head the third means forcing and the fourth means transportation, but not sure about the first two. Are they referring to adjointness?
is part of the judgement syntax of type theory, roughly saying “in the given context, this judgement holds”. It gives a way to divide the context from the judgement in question. is used in category theory as to say that functors and are [[adjoint functor]] s. has domain-specific meaning, usually in logic. Often it's a semantic counterpart to the syntactic , in one way or another. is usually part of the judgemental syntax of a theory, stating that, when we are constructing something function-like, we want it to map the thing on the left to the thing on the right (judgementally). It might also have some other (propositional) meanings, but I think they usually have a “maps to” reading.
Peiyuan Zhu (Feb 03 2022 at 21:13):How can I understand this page about 'groupoid', 'base change', and 'modality'? image.png
Peiyuan Zhu (Feb 03 2022 at 21:21):By 'climbing the hierarchy', does it mean the -groupoid/category hierarchy? image.png So it's suggesting this adjoint base-change morphism works analogously on groups as they are on propositions and sets. In this case are they now called "geometric morphisms"?
Peiyuan Zhu (Feb 03 2022 at 21:26):If I have two posets with a common refinement, what will be the "base change morphism" in this case? So there will be a map between the posets modulo the individual parts of each of the two posets? Moving upwards the hierarchy, is there a simple example in group? Maybe two groups with a common subgroup?