blob: 6760f27c642bef3369213a75d9e065597edabd7a (
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
33
|
(* Title: HoTT/Unit.thy
Author: Josh Chen
Unit type
*)
theory Unit
imports HoTT_Base
begin
section \<open>Constants and type rules\<close>
axiomatization
Unit :: Term ("\<one>") and
pt :: Term ("\<star>") and
indUnit :: "[Term, Term] \<Rightarrow> Term" ("(1ind\<^sub>\<one>)")
where
Unit_form: "\<one>: U O"
and
Unit_intro: "\<star>: \<one>"
and
Unit_elim: "\<lbrakk>C: \<one> \<longrightarrow> U i; c: C \<star>; a: \<one>\<rbrakk> \<Longrightarrow> ind\<^sub>\<one> c a: C a"
and
Unit_comp: "\<lbrakk>C: \<one> \<longrightarrow> U i; c: C \<star>\<rbrakk> \<Longrightarrow> ind\<^sub>\<one> c \<star> \<equiv> c"
text "Rule attribute declarations:"
lemmas Unit_comp [comp]
lemmas Unit_routine [intro] = Unit_form Unit_intro Unit_elim
end
|
