aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJosh Chen2020-05-31 01:13:34 +0200
committerJosh Chen2020-05-31 01:13:34 +0200
commit4faad4fcb1359aa7835c89a3af759afa2917ffd4 (patch)
treebf1f00d34ee01118884324507ed3f4b04ac44017
parent126312747d3005f8fd0611613b26db532a77f3c5 (diff)
transport method
-rw-r--r--hott/Identity.thy2
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"