aboutsummaryrefslogtreecommitdiff
path: root/Univalence.thy
blob: b7f4400890ac6a3f0d0a88206b7734868e57d8a1 (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
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
(*  Title:  HoTT/Univalence.thy
    Author: Josh Chen

Definitions of homotopy, equivalence and the univalence axiom.
*)

theory Univalence
  imports
    HoTT_Methods
    EqualProps
    ProdProps
    Sum
begin


section \<open>Homotopy and equivalence\<close>

text "We define polymorphic constants implementing the definitions of homotopy and equivalence."

axiomatization homotopic :: "[Term, Term] \<Rightarrow> Term"  (infix "~" 100) where
  homotopic_def: "\<lbrakk>
    f: \<Prod>x:A. B x;
    g: \<Prod>x:A. B x
  \<rbrakk> \<Longrightarrow> f ~ g \<equiv> \<Prod>x:A. (f`x) =[B x] (g`x)"

axiomatization isequiv :: "Term \<Rightarrow> Term" where
  isequiv_def: "f: A \<rightarrow> B \<Longrightarrow> isequiv f \<equiv> (\<Sum>g: B \<rightarrow> A. g \<circ> f ~ id) \<times> (\<Sum>g: B \<rightarrow> A. f \<circ> g ~ id)"

definition equivalence :: "[Term, Term] \<Rightarrow> Term"  (infix "\<simeq>" 100)
  where "A \<simeq> B \<equiv> \<Sum>f: A \<rightarrow> B. isequiv f"


text "The identity function is an equivalence:"

lemma isequiv_id:
  assumes "A: U i" and "id: A \<rightarrow> A"
  shows "<<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>: isequiv id"
proof (derive lems: assms isequiv_def homotopic_def)
  fix g assume asm: "g: A \<rightarrow> A"
  show "id \<circ> g: A \<rightarrow> A"
    unfolding compose_def by (routine lems: asm assms)

  show "\<Prod>x:A. ((id \<circ> g)`x) =\<^sub>A (id`x): U i"
    unfolding compose_def by (routine lems: asm assms)
  next
  
  show "<\<^bold>\<lambda>x. x, \<^bold>\<lambda>x. refl x>: \<Sum>g:A \<rightarrow> A. (g \<circ> id) ~ id"
    unfolding compose_def by (derive lems: assms homotopic_def)

  show "<\<^bold>\<lambda>x. x, lambda refl>: \<Sum>g:A \<rightarrow> A. (id \<circ> g) ~ id"
    unfolding compose_def by (derive lems: assms homotopic_def)
qed (rule assms)


text "We use the following lemma in a few proofs:"

lemma isequiv_type:
  assumes "A: U i" and "B: U i" and "f: A \<rightarrow> B"
  shows "isequiv f: U i"
  by (derive lems: assms isequiv_def homotopic_def compose_def)


text "The equivalence relation \<open>\<simeq>\<close> is symmetric:"

lemma equiv_sym:
  assumes "A: U i" and "id: A \<rightarrow> A"
  shows "<id, <<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>>: A \<simeq> A"
unfolding equivalence_def proof
  show "<<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>: isequiv id" using assms by (rule isequiv_id)
  
  fix f assume "f: A \<rightarrow> A"
  with assms(1) assms(1) show "isequiv f: U i" by (rule isequiv_type)
qed (rule assms)


section \<open>idtoeqv and the univalence axiom\<close>

definition idtoeqv :: Term
  where "idtoeqv \<equiv> \<^bold>\<lambda>p. <transport p, ind\<^sub>= (\<lambda>A. <<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>) p>"


text "We prove that equal types are equivalent. The proof is long and uses universes."

theorem
  assumes "A: U i" and "B: U i"
  shows "idtoeqv: (A =[U i] B) \<rightarrow> A \<simeq> B"
unfolding idtoeqv_def equivalence_def
proof
  fix p assume "p: A =[U i] B"
  show "<transport p, ind\<^sub>= (\<lambda>A. <<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>) p>: \<Sum>f: A \<rightarrow> B. isequiv f"
  proof
    { fix f assume "f: A \<rightarrow> B"
    with assms show "isequiv f: U i" by (rule isequiv_type)
    }
    
    show "transport p: A \<rightarrow> B"
    proof (rule transport_type[where ?P="\<lambda>x. x" and ?A="U i" and ?i="S i"])
      show "\<And>x. x: U i \<Longrightarrow> x: U S i" by (elim U_cumulative) standard
      show "U i: U S i" by (rule U_hierarchy) standard
    qed fact+
    
    show "ind\<^sub>= (\<lambda>A. <<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>) p: isequiv (transport p)"
    proof (rule Equal_elim[where ?C="\<lambda>_ _ p. isequiv (transport p)"])
      fix A assume asm: "A: U i"
      show "<<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>: isequiv (transport (refl A))"
      proof (derive lems: isequiv_def)
        show "transport (refl A): A \<rightarrow> A"
          unfolding transport_def
          by (compute lems: Equal_comp[where ?A="U i" and ?C="\<lambda>_ _ _. A \<rightarrow> A"]) (derive lems: asm)
        
        show "<<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>:
                (\<Sum>g:A \<rightarrow> A. g \<circ> (transport (refl A)) ~ id) \<times>
                (\<Sum>g:A \<rightarrow> A. (transport (refl A)) \<circ> g ~ id)"
        proof (subst (1 2) transport_comp)
          show "U i: U S i" by (rule U_hierarchy) standard
          show "U i: U S i" by (rule U_hierarchy) standard
          
          show "<<id, \<^bold>\<lambda>x. refl x>, <id, \<^bold>\<lambda>x. refl x>>:
                  (\<Sum>g:A \<rightarrow> A. g \<circ> id ~ id) \<times> (\<Sum>g:A \<rightarrow> A. id \<circ> g ~ id)"
          proof
            show "\<Sum>g:A \<rightarrow> A. id \<circ> g ~ id: U i"
            proof (derive lems: asm homotopic_def)
              fix g assume asm': "g: A \<rightarrow> A"
              show *: "id \<circ> g: A \<rightarrow> A" by (derive lems: asm asm' compose_def)
              show "\<Prod>x:A. ((id \<circ> g)`x) =\<^sub>A (id`x): U i" by (derive lems: asm *)
            qed (routine lems: asm)

            show "<id, \<^bold>\<lambda>x. refl x>: \<Sum>g:A \<rightarrow> A. id \<circ> g ~ id"
            proof
              fix g assume asm': "g: A \<rightarrow> A"
              show "id \<circ> g ~ id: U i"
              proof (derive lems: homotopic_def)
                show *: "id \<circ> g: A \<rightarrow> A" by (derive lems: asm asm' compose_def)
                show "\<Prod>x:A. ((id \<circ> g)`x) =\<^sub>A (id`x): U i" by (derive lems: asm *)
              qed (routine lems: asm)
              next
              show "\<^bold>\<lambda>x. refl x: id \<circ> id ~ id"
              proof compute
                show "\<^bold>\<lambda>x. refl x: id ~ id" by (subst homotopic_def) (derive lems: asm)
              qed (rule asm)
            qed (routine lems: asm)

            show "<id, \<^bold>\<lambda>x. refl x>: \<Sum>g:A \<rightarrow> A. g \<circ> id ~ id"
            proof
              fix g assume asm': "g: A \<rightarrow> A"
              show "g \<circ> id ~ id: U i" by (derive lems: asm asm' homotopic_def compose_def)
              next
              show "\<^bold>\<lambda>x. refl x: id \<circ> id ~ id"
              proof compute
                show "\<^bold>\<lambda>x. refl x: id ~ id" by (subst homotopic_def) (derive lems: asm)
              qed (rule asm)
            qed (routine lems: asm)
          qed
        qed fact+
      qed
      next
      
      fix A' B' p' assume asm:  "A': U i" "B': U i" "p': A' =[U i] B'"
      show "isequiv (transport p'): U i"
      proof (rule isequiv_type)
        show "transport p': A' \<rightarrow> B'" by (derive lems: asm transport_def)
      qed fact+
    qed fact+
  qed
  next

  show "A =[U i] B: U (S i)" by (derive lems: assms | rule U_hierarchy)+
qed


text "The univalence axiom."

axiomatization univalence :: Term where
  UA: "univalence: isequiv idtoeqv"


end