aboutsummaryrefslogtreecommitdiff
path: root/Empty.thy
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 ‹Constants and type rules›

section ‹Empty type›

axiomatization
  Empty :: Term  ("𝟬") and
  indEmpty :: "Term ⇒ Term"  ("(1ind⇩𝟬)")
where
  Empty_form: "𝟬: U(O)"
and
  Empty_elim: "⟦C: 𝟬 ⟶ U(i); z: 𝟬⟧ ⟹ ind⇩𝟬(z): C(z)"


text "Rule attribute declarations:"

lemmas Empty_routine [intro] = Empty_form Empty_elim


end