From 4faad4fcb1359aa7835c89a3af759afa2917ffd4 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sun, 31 May 2020 01:13:34 +0200
Subject: transport method

---
 hott/Identity.thy | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'hott')

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"
-- 
cgit v1.2.3