Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Clarify extra condition on transp #4914

Merged
merged 1 commit into from Oct 7, 2020
Merged

Clarify extra condition on transp #4914

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
19 changes: 10 additions & 9 deletions doc/user-manual/language/cubical.lagda.rst
View file
Open in desktop
Expand Up @@ -241,30 +241,31 @@ While path types are great for reasoning about equality they don't let
us transport along paths between types or even compose paths, which in
particular means that we cannot yet prove the induction principle for
paths. In order to remedy this we also have a built-in (generalized)
transport operation and homogeneous composition operations. The
transport operation `transp` and homogeneous composition operations `hcomp`. The
transport operation is generalized in the sense that it lets us
specify where it is the identity function.

.. code-block:: agda

transp : ∀ {ℓ} (A : I → Set ℓ) (r : I) (a : A i0) → A i1

There is an additional side condition to be satisfied for ``transp A r
a`` to type-check, which is that ``A`` has to be *constant* on
``r``. This means that ``A`` should be a constant function whenever
the constraint ``r = i1`` is satisfied. For example:
There is an additional side condition to be satisfied for a usage of ``transp`` to type-check.
In a call ``transp A r a``, where ``A`` and ``r`` can both depend on any other interval variables currently in scope,
Agda will try to convert ``A`` to a constant function in those cases where
the constraint ``r = i1`` is satisfied. This must succeed for the call to ``transp`` to type-check,
as it is necessary for the computation rule of ``transp`` to make sense:
When``r`` is ``i1``, ``transp A r`` will compute as the identity function, requiring ``A i0`` to be convertible to ``A i1``.

For example:

* If ``r`` is ``i0`` then ``A`` can be anything, since this side
condition is vacuously true.

* If ``r`` is ``i1`` then ``A`` must be a constant function.

* If ``r`` is some in-scope variable ``i`` then ``A`` only needs to be
* If ``r`` is some in-scope variable ``i`` on which ``A`` depends as well, then ``A`` only needs to be
a constant function when substituting ``i1`` for ``i``.
Copy link
Contributor

@Saizan Saizan Sep 10, 2020 •
edited

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

the condition is still relevant even if A does not mention i, e.g. suppose we are in a context with variables, A : I -> Set, i : I, and x : A i0 then transp A i x will not typecheck. Or did you mean something else by this edit?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@Saizan I thought that this case is covered in the previous bullet points, but I'm probably wrong then. How about "on which A may depend as well"?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The previous bullet points do not cover the case where "r" is a variable in scope like "i".

Also, was the use of "convertible" rather than "equal" intentional? I'm not sure if "convertibility" is defined in the documentation anywhere.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ok, but would my new formulation be good?

Also, was the use of "convertible" rather than "equal" intentional? I'm not sure if "convertibility" is defined in the documentation anywhere.

Thanks for asking. Yes, "convertible" is presumably more precise because "equal" can mean so many things (starting with definitially vs. propositionally), and the whole point here is to make it more precise. But to be honest I don't know what "convertible" means or where it is defined. @mortberg do you have a hint?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe "definitionally/judgmentally equal" is better than "convertible". I don't know what is used elsewhere in the documentation for this equality

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Your new formulation would be good. Whether "A" depends or not on "i" is not strictly relevant to the condition, but I guess for transp A i to typecheck either A is always a constant function or it will mention i.

I imagine other readers would also not know about convertibility, I would rather use definitionally equal which is more descriptive at least.


When ``r`` is equal to ``i1`` the ``transp`` function will compute as
the identity function.

.. code-block:: agda

transp A i1 a = a
Expand Down