diff options
| author | Josh Chen | 2020-05-31 01:13:34 +0200 |
|---|---|---|
| committer | Josh Chen | 2020-05-31 01:13:34 +0200 |
| commit | 4faad4fcb1359aa7835c89a3af759afa2917ffd4 (patch) | |
| tree | bf1f00d34ee01118884324507ed3f4b04ac44017 | |
| parent | 126312747d3005f8fd0611613b26db532a77f3c5 (diff) | |
transport method
| -rw-r--r-- | hott/Identity.thy | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/hott/Identity.thy b/hott/Identity.thy index 571617a..b82c9c2 100644 --- a/hott/Identity.thy +++ b/hott/Identity.thy @@ -304,6 +304,8 @@ Lemma use_transport: shows "trans P p\<inverse> u: P y" by typechk +method transport uses eq = (rule use_transport[OF eq]) + Lemma (derive) transport_left_inv: assumes "A: U i" |