blob: 7c221f0d642b0199a9c8ddd1ed198649e76e5780 (
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
31
32
|
(*
Title: Unit.thy
Author: Joshua Chen
Date: 2018
Unit type
*)
theory Unit
imports HoTT_Base
begin
axiomatization
Unit :: t ("\<one>") and
pt :: t ("\<star>") and
indUnit :: "[t, t] \<Rightarrow> t" ("(1ind\<^sub>\<one>)")
where
Unit_form: "\<one>: U O" and
Unit_intro: "\<star>: \<one>" and
Unit_elim: "\<lbrakk>a: \<one>; c: C \<star>; C: \<one> \<longrightarrow> U i\<rbrakk> \<Longrightarrow> ind\<^sub>\<one> c a: C a" and
Unit_comp: "\<lbrakk>c: C \<star>; C: \<one> \<longrightarrow> U i\<rbrakk> \<Longrightarrow> ind\<^sub>\<one> c \<star> \<equiv> c"
lemmas Unit_form [form]
lemmas Unit_routine [intro] = Unit_form Unit_intro Unit_elim
lemmas Unit_comp [comp]
end
|
