diff options
| author | Josh Chen | 2018-09-19 11:55:45 +0200 |
|---|---|---|
| committer | Josh Chen | 2018-09-19 11:55:45 +0200 |
| commit | f602cb54b39b3c1bb4f755db09bdeeb2f31a9559 (patch) | |
| tree | 94a4b3016aebdc8855d6d12a2bd842649b0d3485 /HoTT_Base.thy | |
| parent | 59a1409b1d15860344e91a4512b60ab8d4368e44 (diff) | |
proof of associativity of path composition
Diffstat (limited to 'HoTT_Base.thy')
| -rw-r--r-- | HoTT_Base.thy | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 69cc1b1..0b460d9 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -25,9 +25,14 @@ axiomatization lt :: "[ord, ord] \<Rightarrow> prop" (infix "<" 999) and leq :: "[ord, ord] \<Rightarrow> prop" (infix "\<le>" 999) where - lt_Suc [intro]: "n < (Suc n)" and - lt_trans [intro]: "\<lbrakk>m1 < m2; m2 < m3\<rbrakk> \<Longrightarrow> m1 < m3" and - leq_min [intro]: "O \<le> n" + lt_Suc: "n < (Suc n)" and + lt_trans: "\<lbrakk>m1 < m2; m2 < m3\<rbrakk> \<Longrightarrow> m1 < m3" and + leq_min: "O \<le> n" + +declare + lt_Suc [intro!] + leq_min [intro!] + lt_trans [intro] section \<open>Judgment\<close> |