blob: d174ddece2bcf8981827cbd806a48cf1a3dd0afd (
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
|
(* Title: HoTT/ex/Methods.thy
Author: Josh Chen
Date: Jul 2018
HoTT method usage examples
*)
theory Methods
imports "../HoTT"
begin
lemma
assumes "A : U" "B: A → U" "⋀x. x : A ⟹ C x: B x → U"
shows "∑x:A. ∏y:B x. ∑z:C x y. ∏w:A. x =⇩A w : U"
by (simple lems: assms)
lemma
assumes "f : ∑x:A. ∏y: B x. ∑z: C x y. D x y z"
shows
"A : U" and
"B: A → U" and
"⋀x. x : A ⟹ C x: B x → U" and
"⋀x y. ⟦x : A; y : B x⟧ ⟹ D x y: C x y → U"
proof -
show "A : U" by (wellformed jdgmt: assms)
show "B: A → U" by (wellformed jdgmt: assms)
show "⋀x. x : A ⟹ C x: B x → U" by (wellformed jdgmt: assms)
show "⋀x y. ⟦x : A; y : B x⟧ ⟹ D x y: C x y → U" by (wellformed jdgmt: assms)
qed
text "Typechecking:"
― ‹Correctly determines the type of the pair›
schematic_goal "⟦a : A; b : B⟧ ⟹ (a, b) : ?A" by simple
― ‹Finds element›
schematic_goal "⟦a : A; b : B⟧ ⟹ ?x : A × B" by simple
end
|
