diff options
| author | Josh Chen | 2018-06-18 17:16:30 +0200 |
|---|---|---|
| committer | Josh Chen | 2018-06-18 17:16:30 +0200 |
| commit | 21077433667f6c2281aa522f170b93bb0c8c23ea (patch) | |
| tree | 75160b85debd56aa2151f2a0787e9973c31228a6 /HoTT_Base.thy | |
| parent | 912a4a4b909041cb280ae5cecd40867ce34b58de (diff) | |
Fixed wrong definition of snd_dep. Proved projection property of snd_dep. Added type formation rules expressing necessity of the conditions.
Diffstat (limited to '')
| -rw-r--r-- | HoTT_Base.thy | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 7794601..a0078fa 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -7,7 +7,6 @@ Basic setup and definitions of a homotopy type theory object logic without unive theory HoTT_Base imports Pure - begin section \<open>Setup\<close> @@ -34,7 +33,7 @@ consts is_of_type :: "[Term, Term] \<Rightarrow> prop" ("(1_ :/ _)" [0, 0] 1000) axiomatization where - inhabited_implies_type [intro]: "\<And>a A. a : A \<Longrightarrow> A : U" + inhabited_implies_type [intro, elim]: "\<And>a A. a : A \<Longrightarrow> A : U" section \<open>Type families\<close> |