/sci/ - Science & Math

>>7136732
wat, Herbrand 80 years ago? :D

>equalities are paths
I tried for some time to understand the semantics for equality a presented in
http://ncatlab.org/nlab/show/univalence+axiom

Am I on the right track with this?:
You have the diagonal map "<span class="math">\Delta_A:A\to (A \times A) :: a \mapsto (a,a)[/spoiler]".
The image of <span class="math">\Delta_A[/spoiler] represents the equality relation.
Now if <span class="math">p:A^I[/spoiler] is a path in <span class="math">A[/spoiler] and if <span class="math">ends(p):=(p_0,p_1)[/spoiler] maps it to its endpoints, then any map <span class="math">aloop:A\to A^I[/spoiler] which maps <span class="math">A[/spoiler] to some loop provides a factorization of <span class="math">\delta=ends\circ aloop[/spoiler].
Now, roughly, if <span class="math">end[/spoiler] is invertible, we can replace the substitute relation with the path object.
(What's not mentioned above, I guess, is that all of this must be done for types <span class="math">a:A\vdash Q(a): Type [/spoiler]. Only then, i.e. if there is more structure going on, can the above "inversion" be nontrivial.)

Also, more generally, can you connect the dots for me how the dependent product function - defined as adjoint to the base change in the -slice- categories gives rise to the normal dependent product, which clearly is defined a a map of objects, not just bundle/display maps.

>>6910230
>>6910237
I've written a longer answer in another thread some time ago, and I'm just gonna copy paste it. Maybe it helps:

(1/3)
>take one grain of wheat, add it to another grain of wheat and how many grains do you have? 2.
>take one grain of wheat, add 2 grains to that, add 3 grains etc… and you end up with -1/12 grains of wheat.
>sorry, but if that makes sense to you, you're an idiot.

What you say here isn't an argument against 1+2+3+...=-1/12.
Let me elaborate:
(the first part is gonna be basic)
Yes, most here will agree that 1+1=2. That's “obviously self-evident”. People have know how to add grains of wheat and written down the rules for addition accordingly.

So what is 1+3 (one grain of wheat plus three more grains) or 4+8, or 2+3? In your head, you reduce the expressions to 4, 12 and 5, respectively. How does your head do it? You can imagine to make a list of all results: Store "1+3 is 4" and "4+8 is 12" and so on. But you couldn’t even store all those results in your head
(side note: never mind that the number of such equations is actually uncountable! P(N)=R)

You can make computation of numbers general possible and also much more efficient by setting up the computational rules!:
Store only specific representations of numbers, e.g. "5 is (((1+1)+1)+1)+1", and then the rule
"a+(b+1) is (a+b)+1"
That's arithmetic as in
http://en.wikipedia.org/wiki/Peano_axioms#Arithmetic
and it let's you -compute- the value of 1+3:
1+3
is 1+((1+1)+1) by the stored information 3 is (1+1)+1, and now this
is (1+(1+1))+1 by the computational rule, and this is
is ((1+1)+1)+1 by the computational rule again used inside the brackets, and this
is 4 by the stored information 4 is ((1+1)+1)+1
That’s all a computer can do, btw.

In the reals, consider
(a-b)^2+(a-c)^2

Without loss of generality, write can set b=a+x and c=a+y and the term reduces to x^2+y^2. This shows that x=y=0, i.e. a=b=c is only way of this being zero.