blob: ee110451bbf9996d727d3ce048c1fd017e1ff39e (
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
|
(*
Title: Empty.thy
Author: Joshua Chen
Date: 2018
Empty type
*)
theory Empty
imports HoTT_Base
begin
axiomatization
Empty :: t ("\<zero>") and
indEmpty :: "t \<Rightarrow> t" ("(1ind\<^sub>\<zero>)")
where
Empty_form: "\<zero>: U O" and
Empty_elim: "\<lbrakk>a: \<zero>; C: \<zero> \<longrightarrow> U i\<rbrakk> \<Longrightarrow> ind\<^sub>\<zero> a: C a"
lemmas Empty_form [form]
lemmas Empty_routine [intro] = Empty_form Empty_elim
end
|
