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 ‹Constants and type rules›
axiomatization
Unit :: Term ("𝟭") and
pt :: Term ("⋆") and
indUnit :: "[Term, Term] ⇒ Term" ("(1ind⇩𝟭)")
where
Unit_form: "𝟭: U O"
and
Unit_intro: "⋆: 𝟭"
and
Unit_elim: "⟦C: 𝟭 ⟶ U i; c: C ⋆; a: 𝟭⟧ ⟹ ind⇩𝟭 c a: C a"
and
Unit_comp: "⟦C: 𝟭 ⟶ U i; c: C ⋆⟧ ⟹ ind⇩𝟭 c ⋆ ≡ c"
text "Rule attribute declarations:"
lemmas Unit_comp [comp]
lemmas Unit_routine [intro] = Unit_form Unit_intro Unit_elim
end
|
