blob: a42f7ff17eee4037be54f1bc527fdf02be269027 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
|
(* Title: HoTT/Empty.thy
Author: Josh Chen
Empty type
*)
theory Empty
imports HoTT_Base
begin
section \<open>Constants and type rules\<close>
section \<open>Empty type\<close>
axiomatization
Empty :: Term ("\<zero>") and
indEmpty :: "Term \<Rightarrow> Term" ("(1ind\<^sub>\<zero>)")
where
Empty_form: "\<zero>: U O"
and
Empty_elim: "\<lbrakk>C: \<zero> \<longrightarrow> U i; z: \<zero>\<rbrakk> \<Longrightarrow> ind\<^sub>\<zero> z: C z"
text "Rule attribute declarations:"
lemmas Empty_routine [intro] = Empty_form Empty_elim
end
|
