aboutsummaryrefslogtreecommitdiff
path: root/Unit.thy
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