IoI is transport #641

Merged
merged 2 commits into from Oct 14, 2014

Conversation

Projects
None yet
3 participants
@mikeshulman
Contributor

mikeshulman commented Mar 2, 2014

Did we really not ever mention explicitly that these are the same?

@mikeshulman

This comment has been minimized.

Show comment Hide comment
@mikeshulman

mikeshulman Apr 16, 2014

Contributor

bump

Contributor

mikeshulman commented Apr 16, 2014

bump

preliminaries.tex
@@ -1655,7 +1655,7 @@ \subsection{Path induction}
\[ \indid{A}(C,c,x,x,\refl{x}) \defeq c(x). \]
The function $ \indid{A}$ is traditionally called $J$.
\indexsee{J@$J$}{induction principle for identity type}%
-We leave it as an easy exercise to show that indiscernability of identicals follows from path induction.
+It as an easy exercise to show that indiscernability of identicals follows from path induction; we will do this in \autoref{lem:transport}, where we will also give a new name and notation for indiscernability of identicals.

This comment has been minimized.

Show comment Hide comment
@EgbertRijke

EgbertRijke Oct 14, 2014

Contributor

There's a typo: "It as" should read "It is"

@EgbertRijke

EgbertRijke Oct 14, 2014

Contributor

There's a typo: "It as" should read "It is"

This comment has been minimized.

Show comment Hide comment
@EgbertRijke

EgbertRijke Oct 14, 2014

Contributor

Since we prove IoI as a lemma, why don't we skip the "exercise" and rephrase this sentence as: "We will show in \autoref{lem:transport} that indiscernability of identicals is an instance of path induction. There we will also give a new name and notation for indiscernability of identicals."

This way we also tell why it is easy, because it is a special case.

@EgbertRijke

EgbertRijke Oct 14, 2014

Contributor

Since we prove IoI as a lemma, why don't we skip the "exercise" and rephrase this sentence as: "We will show in \autoref{lem:transport} that indiscernability of identicals is an instance of path induction. There we will also give a new name and notation for indiscernability of identicals."

This way we also tell why it is easy, because it is a special case.

@mikeshulman

This comment has been minimized.

Show comment Hide comment
@mikeshulman

mikeshulman Oct 14, 2014

Contributor

@EgbertRijke, thanks for the suggestions; fixed (and also rebased against master, since so much time has passed since this was submitted, e.g. autoref -> cref happened).

Contributor

mikeshulman commented Oct 14, 2014

@EgbertRijke, thanks for the suggestions; fixed (and also rebased against master, since so much time has passed since this was submitted, e.g. autoref -> cref happened).

andrejbauer added a commit that referenced this pull request Oct 14, 2014

@andrejbauer andrejbauer merged commit 354bc0a into HoTT:master Oct 14, 2014

1 check passed

continuous-integration/travis-ci The Travis CI build passed
Details

@mikeshulman mikeshulman deleted the mikeshulman:ioi-is-transport branch Oct 14, 2014

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment