diff options
Diffstat (limited to 'EqualProps.thy')
| -rw-r--r-- | EqualProps.thy | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/EqualProps.thy b/EqualProps.thy index f00020f..0107e8e 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -275,7 +275,22 @@ sorry section \<open>Transport\<close> +definition transport :: "Term \<Rightarrow> Term" where + "transport p \<equiv> ind\<^sub>= (\<lambda>x. (\<^bold>\<lambda>x. x)) p" +lemma transport_type: + assumes + "A: U i" "P: A \<longrightarrow> U i" + "x: A" "y: A" + "p: x =\<^sub>A y" + shows "transport p: P x \<rightarrow> P y" +unfolding transport_def +by (rule Equal_elim[where ?p=p and ?x=x and ?y=y]) (routine lems: assms) + +lemma transport_comp: + assumes "A: U i" and "x: A" + shows "transport (refl x) \<equiv> id" +unfolding transport_def by (derive lems: assms) end |