blob: db18454d3872edd6d187b0e37ce492da7ce5b90c (
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
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
|
(*
Title: Prod.thy
Author: Joshua Chen
Date: 2018
Dependent product type
*)
theory Prod
imports HoTT_Base HoTT_Methods
begin
section ‹Basic definitions›
axiomatization
Prod :: "[t, tf] ⇒ t" and
lambda :: "(t ⇒ t) ⇒ t" (binder "❙λ" 30) and
appl :: "[t, t] ⇒ t" ("(1_`/_)" [60, 61] 60) ― ‹Application binds tighter than abstraction.›
syntax
"_prod" :: "[idt, t, t] ⇒ t" ("(3∏_:_./ _)" 30)
"_prod_ascii" :: "[idt, t, t] ⇒ t" ("(3II _:_./ _)" 30)
text ‹The translations below bind the variable @{term x} in the expressions @{term B} and @{term b}.›
translations
"∏x:A. B" ⇌ "CONST Prod A (λx. B)"
"II x:A. B" ⇀ "CONST Prod A (λx. B)"
text ‹Non-dependent functions are a special case.›
abbreviation Fun :: "[t, t] ⇒ t" (infixr "→" 40)
where "A → B ≡ ∏_: A. B"
axiomatization where
― ‹Type rules›
Prod_form: "⟦A: U i; B: A ⟶ U i⟧ ⟹ ∏x:A. B x: U i" and
Prod_intro: "⟦⋀x. x: A ⟹ b x: B x; A: U i⟧ ⟹ ❙λx. b x: ∏x:A. B x" and
Prod_elim: "⟦f: ∏x:A. B x; a: A⟧ ⟹ f`a: B a" and
Prod_comp: "⟦⋀x. x: A ⟹ b x: B x; a: A⟧ ⟹ (❙λx. b x)`a ≡ b a" and
Prod_uniq: "f: ∏x:A. B x ⟹ ❙λx. f`x ≡ f" and
― ‹Congruence rules›
Prod_form_eq: "⟦A: U i; B: A ⟶ U i; C: A ⟶ U i; ⋀x. x: A ⟹ B x ≡ C x⟧ ⟹ ∏x:A. B x ≡ ∏x:A. C x" and
Prod_intro_eq: "⟦⋀x. x: A ⟹ b x ≡ c x; A: U i⟧ ⟹ ❙λx. b x ≡ ❙λx. c x"
text ‹
The Pure rules for ‹≡› only let us judge strict syntactic equality of object lambda expressions.
The actual definitional equality rule is @{thm Prod_intro_eq}.
Note that this is a separate rule from function extensionality.
Note that the bold lambda symbol ‹❙λ› used for dependent functions clashes with the proof term syntax (cf. §2.5.2 of the Isabelle/Isar Implementation).
›
lemmas Prod_routine [intro] = Prod_form Prod_intro Prod_elim
lemmas Prod_comps [comp] = Prod_comp Prod_uniq
section ‹Additional definitions›
definition compose :: "[t, t] ⇒ t" (infixr "o" 110) where "g o f ≡ ❙λx. g`(f`x)"
syntax "_compose" :: "[t, t] ⇒ t" (infixr "∘" 110)
translations "g ∘ f" ⇌ "g o f"
declare compose_def [comp]
lemma compose_assoc:
assumes "A: U i" and "f: A → B" "g: B → C" "h: ∏x:C. D x"
shows "(h ∘ g) ∘ f ≡ h ∘ (g ∘ f)"
by (derive lems: assms Prod_intro_eq)
lemma compose_comp:
assumes "A: U i" and "⋀x. x: A ⟹ b x: B" and "⋀x. x: B ⟹ c x: C x"
shows "(❙λx. c x) ∘ (❙λx. b x) ≡ ❙λx. c (b x)"
by (derive lems: assms Prod_intro_eq)
abbreviation id :: t where "id ≡ ❙λx. x" ― ‹Polymorphic identity function›
end
|
