diff options
author | Josh Chen | 2019-02-17 18:34:38 +0100 |
---|---|---|
committer | Josh Chen | 2019-02-17 18:34:38 +0100 |
commit | 68aa069172933b875d70a5ef71e9db0ae685a92d (patch) | |
tree | bd1da2111e12bab878641661d91f95f66f8132cc /HoTT_Base.thy | |
parent | 76b57317d7568f4dcd673b1b8085601c6c723355 (diff) |
Method "quantify" converts product inhabitation into Pure universal statements. Also misc. cleanups.
Diffstat (limited to 'HoTT_Base.thy')
-rw-r--r-- | HoTT_Base.thy | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 9dcf6d0..1dcf61c 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -2,11 +2,11 @@ Isabelle/HoTT: Basic logical definitions and notation Feb 2019 -This file completes the basic logical and functional setup of the HoTT logic. -Among other things, it: +This file completes the basic logical and functional setup of the HoTT logic. It defines: -* Defines the universe hierarchy and its governing rules. -* Defines named theorems for later use by proof methods. +* The universe hierarchy and its governing rules. +* Some notational abbreviations. +* Named theorems for later use by proof methods. ********) @@ -50,13 +50,16 @@ Instead use @{method elim}, or instantiate the rules suitably. \<close> -section \<open>Type families\<close> +section \<open>Notation\<close> abbreviation (input) constraint :: "[t \<Rightarrow> t, t, t] \<Rightarrow> prop" ("(1_:/ _ \<leadsto> _)") where "f: A \<leadsto> B \<equiv> (\<And>x. x: A \<Longrightarrow> f x: B)" text \<open>We use the notation @{prop "B: A \<leadsto> U i"} to abbreviate type families.\<close> +abbreviation (input) K_combinator :: "'a \<Rightarrow> 'b \<Rightarrow> 'a" ("^_" [1000]) +where "^A \<equiv> \<lambda>_. A" + section \<open>Named theorems\<close> |