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
|