diff options
| author | Josh Chen | 2018-08-12 13:04:16 +0200 |
|---|---|---|
| committer | Josh Chen | 2018-08-12 13:04:16 +0200 |
| commit | 7a89ec1e72f61179767c6488177c6d12e69388c5 (patch) | |
| tree | a305bd9d92d6a51dec49b4c741dc77323ff3ab0c /HoTT_Base.thy | |
| parent | 25225e0c637a43319fef6889dabc222df05bfd3c (diff) | |
Commit before testing polymorphic equality eliminator
Diffstat (limited to '')
| -rw-r--r-- | HoTT_Base.thy | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 614419e..e94ca5c 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -56,6 +56,7 @@ and U_cumulative: "\<And>A i j. \<lbrakk>A: U(i); i <- j\<rbrakk> \<Longrightarrow> A: U(j)" \<comment> \<open>WARNING: \<open>rule Universe_cumulative\<close> can result in an infinite rewrite loop!\<close> + section \<open>Type families\<close> text " |