blob: 8f5cc8c0dc0991f61a0c584d785335b745b19c3d (
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
|
