Skip to content

Commit 10ea5fe

Browse files
author
Madeleine Sydney Ślaga
committed
Revert false positives
1 parent 860e516 commit 10ea5fe

File tree

2 files changed

+40
-40
lines changed

2 files changed

+40
-40
lines changed

‎Cubical/CW/Instances/Pushout.agda‎

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -253,19 +253,19 @@ module CWPushout (ℓ : Level) (Bʷ Cʷ Dʷ : CWskel ℓ)
253253
id→modifySₙ→id X n (inr x) = refl
254254
id→modifySₙ→id X n (push (a , x) i) j =
255255
hcomp (λ k →
256-
λ{ (i = i0) → inl (strictifyFamα X (suc n) (a , ret x (j ∨ k)))
256+
λ{ (i = i0) → inl (strictifyFamα X (suc n) (a , leftInv x (j ∨ k)))
257257
; (i = i1) → inr a
258258
; (j = i0) → modifySₙ→id X n
259259
(doubleCompPath-filler
260260
(λ i → inl (e (str X) n .fst
261-
(α (str X) (suc n) (a , ret x (~ i)))))
261+
(α (str X) (suc n) (a , leftInv x (~ i)))))
262262
(push (a , fun x)) refl k i)
263263
; (j = i1) → push (a , x) i})
264-
(push (a , ret x j) i)
264+
(push (a , leftInv x j) i)
265265
where
266266
fun = invEq (EquivSphereSusp n)
267267
inv = (EquivSphereSusp n) .fst
268-
ret = secEq (EquivSphereSusp n)
268+
leftInv = secEq (EquivSphereSusp n)
269269

270270
modifySₙ→id→modifySₙ : (X : CWskel ℓ) (n : ℕ)
271271
(x : modifySₙ (str X) (suc (suc n))) → id→modifySₙ X n (modifySₙ→id X n x) ≡ x
@@ -275,22 +275,22 @@ module CWPushout (ℓ : Level) (Bʷ Cʷ Dʷ : CWskel ℓ)
275275
hcomp (λ k →
276276
λ{ (i = i0) → inl (e (str X) n .fst (α (str X) (suc n)
277277
(a , compPath→Square
278-
{p = ret (inv x)} {refl}
279-
{λ i → inv (sec x i)} {refl}
278+
{p = leftInv (inv x)} {refl}
279+
{λ i → inv (rightInv x i)} {refl}
280280
(cong (λ X → X ∙ refl)
281281
(commPathIsEq (EquivSphereSusp n .snd) x)) k j)))
282282
; (i = i1) → inr a
283283
; (j = i0) → doubleCompPath-filler
284284
(λ i → inl (e (str X) n .fst (α (str X) (suc n)
285-
(a , ret (inv x) (~ i)))))
285+
(a , leftInv (inv x) (~ i)))))
286286
(push (a , fun (inv x))) refl k i
287287
; (j = i1) → push (a , x) i})
288-
(push (a , sec x j) i)
288+
(push (a , rightInv x j) i)
289289
where
290290
fun = invEq (EquivSphereSusp n)
291291
inv = (EquivSphereSusp n) .fst
292-
ret = secEq (EquivSphereSusp n)
293-
sec = retEq (EquivSphereSusp n)
292+
leftInv = secEq (EquivSphereSusp n)
293+
rightInv = retEq (EquivSphereSusp n)
294294

295295
modifiedPushout : (n : ℕ) → Type ℓ
296296
modifiedPushout n = Pushout {A = B .fst (suc n)} {B = modifySₙ C (suc (suc n))}

‎Cubical/Foundations/Equiv/Dependent.agda‎

Lines changed: 30 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -91,8 +91,8 @@ record IsoOver {ℓ ℓ'} {A : Type ℓ}{B : Type ℓ'}
9191
field
9292
fun : mapOver (isom .fun) P Q
9393
inv : mapOver (isom .inv) Q P
94-
sec : sectionOver (isom .sec) fun inv
95-
ret : retractOver (isom .ret ) fun inv
94+
rightInv : sectionOver (isom .sec) fun inv
95+
leftInv : retractOver (isom .ret) fun inv
9696

9797
record isIsoOver {ℓ ℓ'} {A : Type ℓ}{B : Type ℓ'}
9898
(isom : Iso A B)(P : A → Type ℓ'')(Q : B → Type ℓ''')
@@ -102,8 +102,8 @@ record isIsoOver {ℓ ℓ'} {A : Type ℓ}{B : Type ℓ'}
102102
constructor isisoover
103103
field
104104
inv : mapOver (isom .inv) Q P
105-
sec : sectionOver (isom .sec) fun inv
106-
ret : retractOver (isom .ret ) fun inv
105+
rightInv : sectionOver (isom .sec) fun inv
106+
leftInv : retractOver (isom .ret) fun inv
107107

108108
open IsoOver
109109
open isIsoOver
@@ -116,22 +116,22 @@ isIsoOver→IsoOver :
116116
→ IsoOver isom P Q
117117
isIsoOver→IsoOver {fun = fun} isom .fun = fun
118118
isIsoOver→IsoOver {fun = fun} isom .inv = isom .inv
119-
isIsoOver→IsoOver {fun = fun} isom .sec = isom .sec
120-
isIsoOver→IsoOver {fun = fun} isom .ret = isom .ret
119+
isIsoOver→IsoOver {fun = fun} isom .rightInv = isom .rightInv
120+
isIsoOver→IsoOver {fun = fun} isom .leftInv = isom .leftInv
121121

122122
IsoOver→isIsoOver :
123123
{isom : Iso A B}
124124
→ (isom' : IsoOver isom P Q)
125125
→ isIsoOver isom P Q (isom' .fun)
126126
IsoOver→isIsoOver isom .inv = isom .inv
127-
IsoOver→isIsoOver isom .sec = isom .sec
128-
IsoOver→isIsoOver isom .ret = isom .ret
127+
IsoOver→isIsoOver isom .rightInv = isom .rightInv
128+
IsoOver→isIsoOver isom .leftInv = isom .leftInv
129129

130130
invIsoOver : {isom : Iso A B} → IsoOver isom P Q → IsoOver (invIso isom) Q P
131131
invIsoOver {isom = isom} isom' .fun = isom' .inv
132132
invIsoOver {isom = isom} isom' .inv = isom' .fun
133-
invIsoOver {isom = isom} isom' .sec = isom' .ret
134-
invIsoOver {isom = isom} isom' .ret = isom' .sec
133+
invIsoOver {isom = isom} isom' .rightInv = isom' .leftInv
134+
invIsoOver {isom = isom} isom' .leftInv = isom' .rightInv
135135

136136
compIsoOver :
137137
{ℓA ℓB ℓC ℓP ℓQ ℓR : Level}
@@ -145,20 +145,20 @@ compIsoOver {A = A} {B} {C} {P} {Q} {R} {isom₁} {isom₂} isoover₁ isoover
145145
w : IsoOver _ _ _
146146
w .fun _ = isoover₂ .fun _ ∘ isoover₁ .fun _
147147
w .inv _ = isoover₁ .inv _ ∘ isoover₂ .inv _
148-
w .sec b q i =
148+
w .rightInv b q i =
149149
comp
150150
(λ j → R (compPath-filler (cong (isom₂ .fun) (isom₁ .sec _)) (isom₂ .sec b) j i))
151151
(λ j → λ
152152
{ (i = i0) → w .fun _ (w .inv _ q)
153-
; (i = i1) → isoover₂ .sec _ q j })
154-
(isoover₂ .fun _ (isoover₁ .sec _ (isoover₂ .inv _ q) i))
155-
w .ret a p i =
153+
; (i = i1) → isoover₂ .rightInv _ q j })
154+
(isoover₂ .fun _ (isoover₁ .rightInv _ (isoover₂ .inv _ q) i))
155+
w .leftInv a p i =
156156
comp
157157
(λ j → P (compPath-filler (cong (isom₁ .inv) (isom₂ .ret _)) (isom₁ .ret a) j i))
158158
(λ j → λ
159159
{ (i = i0) → w .inv _ (w .fun _ p)
160-
; (i = i1) → isoover₁ .ret _ p j })
161-
(isoover₁ .inv _ (isoover₂ .ret _ (isoover₁ .fun _ p) i))
160+
; (i = i1) → isoover₁ .leftInv _ p j })
161+
(isoover₁ .inv _ (isoover₂ .leftInv _ (isoover₁ .fun _ p) i))
162162

163163

164164
-- Special cases
@@ -171,8 +171,8 @@ fiberIso→IsoOver :
171171
→ IsoOver idIso P Q
172172
fiberIso→IsoOver isom .fun a = isom a .fun
173173
fiberIso→IsoOver isom .inv b = isom b .inv
174-
fiberIso→IsoOver isom .sec b = isom b .sec
175-
fiberIso→IsoOver isom .ret a = isom a .ret
174+
fiberIso→IsoOver isom .rightInv b = isom b .sec
175+
fiberIso→IsoOver isom .leftInv a = isom a .ret
176176

177177
-- Only half-adjoint equivalence can be lifted.
178178
-- This is another clue that HAE is more natural than isomorphism.
@@ -193,14 +193,14 @@ pullbackIsoOver {A = A} {B} {P} f hae = w
193193
w : IsoOver _ _ _
194194
w .fun a = idfun _
195195
w .inv b = subst P (sym (isom .sec b))
196-
w .sec b p i = subst-filler P (sym (isom .sec b)) p (~ i)
197-
w .ret a p i =
196+
w .rightInv b p i = subst-filler P (sym (isom .sec b)) p (~ i)
197+
w .leftInv a p i =
198198
comp
199199
(λ j → P (hae .com a (~ j) i))
200200
(λ j → λ
201201
{ (i = i0) → w .inv _ (w .fun _ p)
202202
; (i = i1) → p })
203-
(w .sec _ p i)
203+
(w .rightInv _ p i)
204204

205205

206206
-- Lifting isomorphism of bases to isomorphism of families
@@ -230,8 +230,8 @@ equivOver→IsoOver {P = P} {Q = Q} e f equiv = w
230230
w : IsoOver (equivToIso e) P Q
231231
w .fun = isom .fun
232232
w .inv = isom .inv
233-
w .sec = isom .sec
234-
w .ret = isom .ret
233+
w .rightInv = isom .rightInv
234+
w .leftInv = isom .leftInv
235235

236236

237237
-- Turn isomorphism over HAE into relative equivalence,
@@ -251,11 +251,11 @@ isoToEquivOver {A = A} {P} {Q = Q} f hae isom' a = isoToEquiv (fibiso a) .snd
251251
fibiso : (a : A) → Iso (P a) (Q (f a))
252252
fibiso a .fun = isom' .fun a
253253
fibiso a .inv x = transport (λ i → P (isom .ret a i)) (isom' .inv (f a) x)
254-
fibiso a .ret x = fromPathP (isom' .ret _ _)
254+
fibiso a .ret x = fromPathP (isom' .leftInv _ _)
255255
fibiso a .sec x =
256256
sym (substCommSlice _ _ (isom' .fun) _ _)
257257
∙ cong (λ p → subst Q p (isom' .fun _ (isom' .inv _ x))) (hae .com a)
258-
∙ fromPathP (isom' .sec _ _)
258+
∙ fromPathP (isom' .rightInv _ _)
259259

260260

261261
-- Half-adjoint equivalence over half-adjoint equivalence
@@ -285,8 +285,8 @@ isHAEquivOver→isIsoOver :
285285
→ IsoOver (isHAEquiv→Iso (hae .snd)) P Q
286286
isHAEquivOver→isIsoOver hae' .fun = hae' .fst
287287
isHAEquivOver→isIsoOver hae' .inv = hae' .snd .inv
288-
isHAEquivOver→isIsoOver hae' .ret = hae' .snd .linv
289-
isHAEquivOver→isIsoOver hae' .sec = hae' .snd .rinv
288+
isHAEquivOver→isIsoOver hae' .leftInv = hae' .snd .linv
289+
isHAEquivOver→isIsoOver hae' .rightInv = hae' .snd .rinv
290290

291291

292292
-- A dependent version of `isoToHAEquiv`
@@ -304,8 +304,8 @@ IsoOver→HAEquivOver {A = A} {P = P} {Q = Q} {isom = isom} isom' = w
304304

305305
f' = isom' .fun
306306
g' = isom' .inv
307-
ε' = isom' .sec
308-
η' = isom' .ret
307+
ε' = isom' .rightInv
308+
η' = isom' .leftInv
309309

310310
sq : _ → I → I → _
311311
sq b i j =
@@ -350,7 +350,7 @@ IsoOver→HAEquivOver {A = A} {P = P} {Q = Q} {isom = isom} isom' = w
350350

351351
w : isHAEquivOver _ _ _ _
352352
w .inv = isom' .inv
353-
w .linv = isom' .ret
353+
w .linv = isom' .leftInv
354354
w .rinv b x i =
355355
comp (λ j → Q (sq b i j))
356356
(λ j → λ

0 commit comments

Comments
 (0)