Comments (6)
Yes, we discussed that and that's why you called it a principle and not an axiom.
from symmetrybook.
It might be better to move it to the section on equivalences, so we could take that function to be an inverse of the function in the exercise.
from symmetrybook.
The narrative I tried to follow is: if I introduce a type former, here X->Y, I explain what it "means" that to elements of the newly formed type are equal in terms of equality of the constituent types. This "means" is often modulo an equivalence, and cannot be made precise before the definition of equivalence is in place. Cf. "equivalent" in the last sentence of 5.3.
This narrative makes sense to me, and we discussed this a couple of times. Do you really want to change that? Or only in case of function extensionality? A good solution could be to add a short section in between 2.8 and 2.9, called "Identifying functions".
from symmetrybook.
What about this way of putting it?:
from symmetrybook.
Fine with me. But we could give a name to the function in Exc. 2.4.3 and come back to this when we have equivalences. I can make a proposal.
from symmetrybook.
Done 03739c1
The exercise had to become a definition since we cannot have an axiom depend on how somebody solves the exercise.
from symmetrybook.
Related Issues (20)
- Changing all xymatrix diagrams to tikzcd HOT 3
- image inclusion HOT 4
- Theorem 2.26.4 HOT 4
- Expand App. B.1 to discuss principles compatible with decidable equality and program extraction
- Introduce the subset notation HOT 4
- Footnote 66 explaining the first ! (bang) HOT 4
- Rings and abstract rings
- Injection/inclusion in Propositional Resizing 2.18.6, or rather just "map"? HOT 14
- Build problem HOT 1
- Building of book fails HOT 6
- Subscripts to \eqto HOT 2
- Commutativity of diagrams HOT 16
- Definition of transitive G-set HOT 7
- The concept of homotopy type HOT 2
- universal set bundle HOT 7
- Potential inconsistency in coproduct notation
- Higher deloopings of abelian groups
- "ad" is not defined HOT 1
- Can an object be considered the same if we change its type?
- Remark 4.2.21, universes HOT 3
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from symmetrybook.