Skip to content

Commit 353efa7

Browse files
rw111rw111
committed
possible white space violations checked with sed
1 parent 8a98596 commit 353efa7

File tree

1 file changed

+48
-48
lines changed

1 file changed

+48
-48
lines changed

‎Cubical/HITs/SetQuotients/Properties.agda‎

Lines changed: 48 additions & 48 deletions
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@ open import Cubical.Relation.Binary.Base
2727
open import Cubical.HITs.TypeQuotients as TypeQuot using (_/ₜ_ ; [_] ; eq/)
2828
open import Cubical.HITs.PropositionalTruncation as PropTrunc
2929
using (∥_∥₁ ; ∣_∣₁ ; squash₁) renaming (rec to propRec)
30-
open import Cubical.HITs.PropositionalTruncation.Monad
30+
open import Cubical.HITs.PropositionalTruncation.Monad
3131
open import Cubical.HITs.SetTruncation as SetTrunc
3232
using (∥_∥₂ ; ∣_∣₂ ; squash₂ ; isSetSetTrunc)
3333

@@ -352,12 +352,12 @@ descendMapPath f g isSetM path i x =
352352
g x ∎ })
353353
([]surjective x)
354354
i
355-
355+
356356
-- An Isomorphism/R: An Isomorphism but up to equivalence R instead of equality _≡_:
357357
module _ {A : Type ℓ} {B : Type ℓ'} {R : A → A → Type ℓ} (ER : isEquivRel R) where
358-
358+
359359
retract/R : (f : A → B) → (g : B → A) → Type ℓ
360-
retract/R f g = ∀ a → R (g (f a)) a
360+
retract/R f g = ∀ a → R (g (f a)) a
361361

362362
record Iso/R (A : Type ℓ) (B : Type ℓ') {R : A → A → Type ℓ} (ER : isEquivRel R) : Type (ℓ-max ℓ ℓ') where
363363
--no-eta-equality
@@ -374,10 +374,10 @@ R* : {A : Type ℓ} {B : Type ℓ'} {R : A → A → Type ℓ}{ER : isEquivRel R
374374
R* {ℓ}{ℓ'}{A}{B}{R}{ER} {iso/r} b b' = R (iso/r .inv/R b) (iso/r .inv/R b')
375375

376376
section/R : {A : Type ℓ} {B : Type ℓ'} {R : A → A → Type ℓ}{ER : isEquivRel R} {iso/r : Iso/R A B {R} ER} → Type (ℓ-max ℓ ℓ')
377-
section/R {iso/r = iso/r} = ∀ b → R* {iso/r = iso/r} (iso/r .fun/R (iso/r .inv/R b)) b
377+
section/R {iso/r = iso/r} = ∀ b → R* {iso/r = iso/r} (iso/r .fun/R (iso/r .inv/R b)) b
378378

379379
retract/R→section/R : {A : Type ℓ} {B : Type ℓ'} {R : A → A → Type ℓ}{ER : isEquivRel R} {iso/r : Iso/R A B {R} ER} →
380-
section/R {iso/r = iso/r}
380+
section/R {iso/r = iso/r}
381381
retract/R→section/R {R = R} {equivRel reflexive symmetric transitive} {iso/r = iso/r} b = iso/r .leftInv/R (iso/r .inv/R b)
382382

383383
-- Iso/R is a RelIso
@@ -393,7 +393,7 @@ iso/R-A≡B {ℓ} {A}{B}{R} ER@{equivRel reflexive symmetric transitive} AB .lef
393393
help : transport (sym AB) (transport AB a) ≡ a
394394
help = transport⁻Transport AB a
395395
step1 : ∀ x y → x ≡ y → R x y
396-
step1 x y xy = subst (R x) xy (reflexive x)
396+
step1 x y xy = subst (R x) xy (reflexive x)
397397

398398
ER≡ : (A : Type ℓ) → isEquivRel ((_≡_) {ℓ = ℓ} {A})
399399
ER≡ {ℓ} A = equivRel (λ a i → a) (λ a b x i → x (~ i)) λ a b c x y i → (x ∙ y) i
@@ -403,8 +403,8 @@ R→R* : {A : Type ℓ} {B : Type ℓ'} {R : A → A → Type ℓ}{ER : isEquivR
403403
R→R* {ℓ}{ℓ'}{A}{B}{R} {ER} {iso/r} raa' =
404404
ER .isEquivRel.transitive (iso/r .inv/R (iso/r .fun/R _)) _ (iso/r .inv/R (iso/r .fun/R _))
405405
(ER .isEquivRel.transitive (iso/r .inv/R (iso/r .fun/R _)) _ _ (iso/r .leftInv/R _) raa')
406-
(ER .isEquivRel.symmetric (iso/r .inv/R (iso/r .fun/R _)) _ (iso/r .leftInv/R _))
407-
406+
(ER .isEquivRel.symmetric (iso/r .inv/R (iso/r .fun/R _)) _ (iso/r .leftInv/R _))
407+
408408
R*→R : {A : Type ℓ} {B : Type ℓ'} {R : A → A → Type ℓ}{ER : isEquivRel R} → {iso/r : Iso/R A B {R} ER}{b b' : B} →
409409
R* {iso/r = iso/r} b b' → R (iso/r .inv/R b) (iso/r .inv/R b')
410410
R*→R z = z
@@ -413,7 +413,7 @@ R*→R z = z
413413
-- relation on A to _≡_ and assuming that inv/R has an inverse inv/R⁻¹,
414414
-- ie by assuming it is 1-to-1:
415415
iso/R→≡→Iso : {A : Type ℓ} {B : Type ℓ'} →
416-
(iso/r : Iso/R {ℓ}{ℓ'} A B {R = (_≡_) {ℓ}{A}} (ER≡ A)) → (inv/R⁻¹ : A → B) → (∀ b → inv/R⁻¹ (iso/r .inv/R b) ≡ b) → Iso A B
416+
(iso/r : Iso/R {ℓ}{ℓ'} A B {R = (_≡_) {ℓ}{A}} (ER≡ A)) → (inv/R⁻¹ : A → B) → (∀ b → inv/R⁻¹ (iso/r .inv/R b) ≡ b) → Iso A B
417417
iso/R→≡→Iso {ℓ}{ℓ'}{A}{B} iso/r@(iso/R fun/R₁ inv/R₁ leftInv/R₁) inv/R⁻¹ invertible = iso fun/R₁ inv/R₁ section' leftInv/R₁
418418
where
419419
sectionR : section/R {ℓ}{ℓ'}{A}{B}{_≡_}{ER≡ A}{iso/r}
@@ -427,54 +427,54 @@ iso/R→≡→Iso {ℓ}{ℓ'}{A}{B} iso/r@(iso/R fun/R₁ inv/R₁ leftInv/R₁)
427427
step4 : ∀ b → inv/R⁻¹ (inv/R₁ (fun/R₁ (inv/R₁ b))) ≡ fun/R₁ (inv/R₁ b)
428428
step4 b = invertible (fun/R₁ (inv/R₁ b))
429429
section' : ∀ b → fun/R₁ (inv/R₁ b) ≡ b
430-
section' b = (sym (step4 b) ∙ step2 b) ∙ step3 b
430+
section' b = (sym (step4 b) ∙ step2 b) ∙ step3 b
431431

432432
-- R* is an equivalence relation:
433433
isEquivRelR* : (A : Type ℓ) (B : Type ℓ') {R : A → A → Type ℓ} {ER : isEquivRel R} → (iso/r : Iso/R A B ER) → isEquivRel (R* {iso/r = iso/r})
434434
isEquivRelR* A B {R} {ER} iso/r = equivRel
435435
(λ a → ER .isEquivRel.reflexive (iso/r .inv/R a))
436436
(λ a b → ER .isEquivRel.symmetric (iso/r .inv/R a) (iso/r .inv/R b))
437-
(λ a b c → ER .isEquivRel.transitive (iso/r .inv/R a) (iso/r .inv/R b) (iso/r .inv/R c))
438-
437+
(λ a b c → ER .isEquivRel.transitive (iso/r .inv/R a) (iso/r .inv/R b) (iso/r .inv/R c))
438+
439439
-- There is an induced isomorphism/R with respect to R*:
440440
iso/R→Iso/R* : {A : Type ℓ} {B : Type ℓ} {R : A → A → Type ℓ}{ER : isEquivRel R} →
441441
(iso/r : Iso/R A B {R} ER) →
442442
Iso/R B A {R = R* {iso/r = iso/r}} (isEquivRelR* A B iso/r)
443-
iso/R→Iso/R* iso/r = iso/R (iso/r .inv/R) (iso/r .fun/R) (λ a → iso/r .leftInv/R (iso/r .inv/R a))
443+
iso/R→Iso/R* iso/r = iso/R (iso/r .inv/R) (iso/r .fun/R) (λ a → iso/r .leftInv/R (iso/r .inv/R a))
444444

445445
-- The propositionality of R implies the propositionality of R*:
446446
isPropR→IsPropR* : {A : Type ℓ} {B : Type ℓ'} {R : A → A → Type ℓ}{ER : isEquivRel R} → (iso/r : Iso/R {ℓ} A B {R} ER)
447-
→ (∀ a a' → isProp (R a a')) → (∀ b b' → isProp ((R* {iso/r = iso/r}) b b'))
448-
isPropR→IsPropR* iso/r ispRxy x y = ispRxy (iso/r .inv/R x) (iso/r .inv/R y)
447+
→ (∀ a a' → isProp (R a a')) → (∀ b b' → isProp ((R* {iso/r = iso/r}) b b'))
448+
isPropR→IsPropR* iso/r ispRxy x y = ispRxy (iso/r .inv/R x) (iso/r .inv/R y)
449449

450-
-- An example of duality:
450+
-- An example of duality:
451451
isPropR→IsPropR** : {A : Type ℓ} {B : Type ℓ} {R : A → A → Type ℓ}{ER : isEquivRel R} → (iso/r : Iso/R {ℓ} A B {R} ER)
452-
→ (∀ x y → isProp (R x y)) → (∀ x y → isProp (R* {R = R* {iso/r = iso/r}} {iso/r = iso/R→Iso/R* iso/r} x y))
452+
→ (∀ x y → isProp (R x y)) → (∀ x y → isProp (R* {R = R* {iso/r = iso/r}} {iso/r = iso/R→Iso/R* iso/r} x y))
453453
isPropR→IsPropR** {ℓ} {A} {B} {R} {equivRel reflexive symmetric transitive} iso/r x y ispRxy = λ x' y'
454454
→ x (iso/r .inv/R (iso/r .fun/R y)) (iso/r .inv/R (iso/r .fun/R ispRxy)) x' y'
455455

456456
R**→R : {ℓ : Level} {A : Type ℓ} {B : Type ℓ} {R : A → A → Type ℓ}{ER : isEquivRel R}{iso/r : Iso/R {ℓ} A B {R} ER}
457-
→ ∀ x y → (R* {R = R* {iso/r = iso/r}} {iso/r = iso/R→Iso/R* iso/r} x y → R x y)
457+
→ ∀ x y → (R* {R = R* {iso/r = iso/r}} {iso/r = iso/R→Iso/R* iso/r} x y → R x y)
458458
R**→R {ℓ} {A} {B} {R} {equivRel reflexive symmetric transitive} {iso/R f g leftInv/R₁} x y =
459459
λ z → transitive x (g (f y)) y
460460
(transitive x (g (f x)) (g (f y))
461461
(symmetric (g (f x)) x (leftInv/R₁ x)) z) (leftInv/R₁ y)
462-
462+
463463
R→R** : {ℓ : Level} {A : Type ℓ} {B : Type ℓ} {R : A → A → Type ℓ}{ER : isEquivRel R}{iso/r : Iso/R {ℓ} A B {R} ER}
464-
→ ∀ x y → (R x y → R* {R = R* {iso/r = iso/r}} {iso/r = iso/R→Iso/R* iso/r} x y)
464+
→ ∀ x y → (R x y → R* {R = R* {iso/r = iso/r}} {iso/r = iso/R→Iso/R* iso/r} x y)
465465
R→R** {ℓ} {A} {B} {R} {equivRel reflexive symmetric transitive} {iso/R f g leftInv/R₁} x y =
466466
λ z → transitive (g (f x)) y (g (f y))
467467
(transitive (g (f x)) x y (leftInv/R₁ x) z)
468468
(symmetric (g (f y)) y (leftInv/R₁ y))
469-
469+
470470
R*-IsProp-Def1 : {ℓ : Level} {A : Type ℓ} {B : Type ℓ} {R : A → A → Type ℓ}{ER : isEquivRel R}{iso/r : Iso/R {ℓ} A B {R} ER}
471471
{isp : ∀ x y → isProp (R x y)} → ∀ x y → (R* {R = R* {iso/r = iso/r}} {iso/r = iso/R→Iso/R* iso/r} x y) ≡ (R x y)
472472
R*-IsProp-Def1 {ℓ} {A} {B} {R} {equivRel reflexive symmetric transitive} {iso/r@(iso/R f g leftInv/R₁)} {isp} x y =
473473
isoToPath (iso (R**→R {iso/r = iso/r} x y) (R→R** {iso/r = iso/r} x y)
474474
(λ rxy → isp x y (R**→R {iso/r = iso/r} x y (R→R** {iso/r = iso/r} x y rxy)) rxy)
475475
λ rgf → isp (g (f x)) (g (f y)) (R→R** {iso/r = iso/r} x y (R**→R {iso/r = iso/r} x y rgf)) rgf)
476476

477-
-- An isProp duality proof:
477+
-- An isProp duality proof:
478478
R**≡R : {ℓ : Level} {A : Type ℓ} {B : Type ℓ} {R : A → A → Type ℓ}{ER : isEquivRel R}{iso/r : Iso/R {ℓ} A B {R} ER}
479479
{isp : ∀ x y → isProp (R x y)} → (R* {R = R* {iso/r = iso/r}} {iso/r = iso/R→Iso/R* iso/r}) ≡ R
480480
R**≡R {ℓ} {A} {B} {R} ER@{equivRel reflexive symmetric transitive} {iso/r@(iso/R f g leftInv/R₁)} {isp} i x y = help x y i
@@ -483,28 +483,28 @@ R**≡R {ℓ} {A} {B} {R} ER@{equivRel reflexive symmetric transitive} {iso/r@(i
483483
isp' = isp x y
484484
help : (x' y' : A) → R* {R = R* {iso/r = iso/r}} {ER = isEquivRelR* A B {ER = ER}
485485
(iso/R f g leftInv/R₁)} {iso/r = iso/R g f λ a → leftInv/R₁ (g a)} x' y' ≡ R x' y'
486-
help = R*-IsProp-Def1 {iso/r = iso/r}{isp}
486+
help = R*-IsProp-Def1 {iso/r = iso/r}{isp}
487487

488488
-- A few more R* identity lemmas:
489489
R*≡Rinv : {A : Type ℓ} {B : Type ℓ} {R : A → A → Type ℓ}{ER : isEquivRel R}{iso/r : Iso/R A B {R} ER} →
490-
∀ b b' → R* {ℓ}{ℓ}{A}{B}{R}{ER}{iso/r} b b' ≡ R (iso/r .inv/R b) (iso/r .inv/R b')
491-
R*≡Rinv b b' = refl
490+
∀ b b' → R* {ℓ}{ℓ}{A}{B}{R}{ER}{iso/r} b b' ≡ R (iso/r .inv/R b) (iso/r .inv/R b')
491+
R*≡Rinv b b' = refl
492492

493493
R*≡λttHlp : {A : Type ℓ} {B : Type ℓ} {R : A → A → Type ℓ}{ER : isEquivRel R}{AB : A ≡ B} →
494-
∀ b b' → R* {iso/r = iso/R-A≡B {ℓ}{A}{B}{R}{ER} AB} b b' ≡ (R (transport (sym AB) b) (transport (sym AB) b'))
494+
∀ b b' → R* {iso/r = iso/R-A≡B {ℓ}{A}{B}{R}{ER} AB} b b' ≡ (R (transport (sym AB) b) (transport (sym AB) b'))
495495
R*≡λttHlp {ℓ}{A}{B}{R}{ER} {AB} b b' = isoToPath (iso (λ z → z) (λ z → z) (λ b₁ i → b₁) λ a i → a)
496496
where
497497
iso/r = iso/R-A≡B {ℓ}{A}{B}{R}{ER} AB
498498
defR* : R* {iso/r = iso/r} b b' ≡ R (iso/r .inv/R b) (iso/r .inv/R b')
499499
defR* = refl
500500

501501
R*≡λR : {A : Type ℓ} {B : Type ℓ} {R : A → A → Type ℓ}{ER : isEquivRel R}{iso/r : Iso/R A B {R} ER} →
502-
R* {iso/r = iso/r} ≡ (λ b b' → R (iso/r .inv/R b) (iso/r .inv/R b'))
502+
R* {iso/r = iso/r} ≡ (λ b b' → R (iso/r .inv/R b) (iso/r .inv/R b'))
503503
R*≡λR {ℓ}{A}{B}{R}{ER}{iso/r} = λ i b b' → R*≡Rinv {ℓ}{A}{B}{R}{ER}{iso/r} b b' i
504504

505505
R*≡λtt : {A : Type ℓ} {B : Type ℓ} {R : A → A → Type ℓ}{ER : isEquivRel R}{AB : A ≡ B} →
506-
R* {iso/r = iso/R-A≡B {ℓ}{A}{B}{R}{ER} AB} ≡ (λ b b' → R (transport (sym AB) b) (transport (sym AB) b'))
507-
R*≡λtt {ℓ}{A}{B}{R}{ER}{AB} = λ i b b' → R*≡λttHlp {ℓ}{A}{B}{R}{ER}{AB} b b' i
506+
R* {iso/r = iso/R-A≡B {ℓ}{A}{B}{R}{ER} AB} ≡ (λ b b' → R (transport (sym AB) b) (transport (sym AB) b'))
507+
R*≡λtt {ℓ}{A}{B}{R}{ER}{AB} = λ i b b' → R*≡λttHlp {ℓ}{A}{B}{R}{ER}{AB} b b' i
508508

509509
-- Definitions, functions and lemmas concerning A/R as a set quotient:
510510
A/R→B/R* : {ℓ : Level} {A : Type ℓ} {B : Type ℓ} {R : A → A → Type ℓ}{ER : isEquivRel R}{iso/r : Iso/R {ℓ} A B {R} ER} →
@@ -522,23 +522,23 @@ B/R*→A/R {ℓ} {A}{B}{R}{ER}{iso/r} (squash/ b b' p q i j) =
522522
squash/ (B/R*→A/R {iso/r = iso/r} b) (B/R*→A/R {iso/r = iso/r} b')
523523
(cong (λ u → B/R*→A/R {iso/r = iso/r} u) p) (cong (λ u → B/R*→A/R {iso/r = iso/r} u) q) i j
524524

525-
raa'→[a]≡[a'] : {ℓ : Level} {A : Type ℓ} {R : A → A → Type ℓ} {a a' : A} → R a a' → (_≡_) {ℓ} {A / R} (_/_.[ a ]) (_/_.[ a' ])
526-
raa'→[a]≡[a'] {ℓ} {A} {R} {a} {a'} raa' = _/_.eq/ a a' raa'
525+
raa'→[a]≡[a'] : {ℓ : Level} {A : Type ℓ} {R : A → A → Type ℓ} {a a' : A} → R a a' → (_≡_) {ℓ} {A / R} (_/_.[ a ]) (_/_.[ a' ])
526+
raa'→[a]≡[a'] {ℓ} {A} {R} {a} {a'} raa' = _/_.eq/ a a' raa'
527527

528-
∥f∥₁-map : {A : Type ℓ} {B : Type ℓ'} → (f : A → B) → ∥ A ∥₁ → ∥ B ∥₁
528+
∥f∥₁-map : {A : Type ℓ} {B : Type ℓ'} → (f : A → B) → ∥ A ∥₁ → ∥ B ∥₁
529529
∥f∥₁-map {ℓ} {ℓ'} {A} {B} f A' = A' >>= λ a → return (f a)
530530

531531
extrapolate[] : {ℓ : Level} {A : Type ℓ} {R : A → A → Type ℓ} →
532-
(f : (A / R) → (A / R)) → (∀ (a : A) → f [ a ] ≡ [ a ]) → ∀ (aᵣ : A / R) → ∥ f aᵣ ≡ aᵣ ∥₁
532+
(f : (A / R) → (A / R)) → (∀ (a : A) → f [ a ] ≡ [ a ]) → ∀ (aᵣ : A / R) → ∥ f aᵣ ≡ aᵣ ∥₁
533533
extrapolate[] {ℓ} {A} {R} f fa aᵣ = ∥f∥₁-map (λ z → z .snd) goal
534534
where
535535
a[] : ∀ (aᵣ : A / R) → ∥ A ∥₁
536536
a[] aᵣ = ∥f∥₁-map fst ([]surjective aᵣ)
537-
a[]* : ∥ Σ A (λ a → [ a ] ≡ aᵣ) ∥₁
537+
a[]* : ∥ Σ A (λ a → [ a ] ≡ aᵣ) ∥₁
538538
a[]* = []surjective aᵣ
539539
step1 : Σ A (λ a → [ a ] ≡ aᵣ) → Σ A (λ a → f [ a ] ≡ aᵣ)
540540
step1 (fst₁ , snd₁) = fst₁ , ((fa fst₁) ∙ snd₁)
541-
step2 : Σ A (λ a → [ a ] ≡ aᵣ) → Σ A (λ a → f aᵣ ≡ f [ a ])
541+
step2 : Σ A (λ a → [ a ] ≡ aᵣ) → Σ A (λ a → f aᵣ ≡ f [ a ])
542542
step2 (fst₁ , snd₁) = fst₁ , (sym (cong f snd₁))
543543
stepf : Σ A (λ a → [ a ] ≡ aᵣ) → Σ A (λ a → f aᵣ ≡ aᵣ)
544544
stepf (fst₁ , snd₁) = fst₁ , (snd (step2 (fst₁ , snd₁))) ∙ (snd (step1 (fst₁ , snd₁)))
@@ -551,7 +551,7 @@ isoA/R-B/R'Hlp3 {ℓ} {A} {R} f fid aᵣ = propRec (squash/ (f aᵣ) aᵣ) (λ u
551551

552552
isoA/R-B/R'Hlp1 : {ℓ : Level} {A : Type ℓ} {B : Type ℓ} {R : A → A → Type ℓ}{ER : isEquivRel R}
553553
→ (iso/r : Iso/R {ℓ} A B {R} ER) → (aᵣ : A / R)
554-
→ (B/R*→A/R {iso/r = iso/r} (A/R→B/R* {iso/r = iso/r} aᵣ)) ≡ aᵣ
554+
→ (B/R*→A/R {iso/r = iso/r} (A/R→B/R* {iso/r = iso/r} aᵣ)) ≡ aᵣ
555555
isoA/R-B/R'Hlp1 {ℓ} {A} {B} {R} ER@{equivRel rf sm trns} iso/r@(iso/R f g rgfa≡a) aᵣ =
556556
step2 (λ x → B/R*→A/R {iso/r = iso/r} (A/R→B/R* {iso/r = iso/r} x)) (λ a → step1 a) aᵣ
557557
where
@@ -560,23 +560,23 @@ isoA/R-B/R'Hlp1 {ℓ} {A} {B} {R} ER@{equivRel rf sm trns} iso/r@(iso/R f g rgfa
560560
step1 : ∀ (a : A) → [ g (f a) ] ≡ [ a ]
561561
step1 a = raa'→[a]≡[a'] (help1 a)
562562
step2 : (f' : (A / R) → (A / R)) → (∀ (a : A) → f' [ a ] ≡ [ a ]) → ∀ (aᵣ : A / R) → f' aᵣ ≡ aᵣ
563-
step2 f' x aᵣ i = isoA/R-B/R'Hlp3 f' x aᵣ i
563+
step2 f' x aᵣ i = isoA/R-B/R'Hlp3 f' x aᵣ i
564564

565565
isoA/R-B/R'Hlp2 : {ℓ : Level} {A : Type ℓ} {B : Type ℓ} {R : A → A → Type ℓ}{ER : isEquivRel R}
566566
→ (iso/r : Iso/R {ℓ} A B {R} ER) → (bᵣ : B / R* {iso/r = iso/r})
567-
→ (A/R→B/R* {iso/r = iso/r} (B/R*→A/R {iso/r = iso/r} bᵣ)) ≡ bᵣ
567+
→ (A/R→B/R* {iso/r = iso/r} (B/R*→A/R {iso/r = iso/r} bᵣ)) ≡ bᵣ
568568
isoA/R-B/R'Hlp2 {ℓ} {A} {B} {R} ER@{equivRel rf sm trns} iso/r@(iso/R f g rgfa≡a) bᵣ =
569569
step2 (λ x → A/R→B/R* {iso/r = iso/r} (B/R*→A/R {iso/r = iso/r} x)) (λ b → step1 b) bᵣ
570570
where
571571
help1 : ∀ (a : A) → R (g (f a)) a
572572
help1 a = rgfa≡a a
573573
help2 : ∀ (b : B) → (R* {iso/r = iso/r} (f (g b))) b
574574
help2 = λ b → rgfa≡a (g b)
575-
step1 : ∀ (b : B) → (_≡_) {A = B / R* {iso/r = iso/r}} [ f (g b) ] [ b ]
575+
step1 : ∀ (b : B) → (_≡_) {A = B / R* {iso/r = iso/r}} [ f (g b) ] [ b ]
576576
step1 b = raa'→[a]≡[a'] (help2 b)
577577
step2 : (g' : (B / R* {iso/r = iso/r}) → (B / R* {iso/r = iso/r})) → (∀ (b : B) → g' [ b ] ≡ [ b ]) →
578578
∀ (bᵣ : B / R* {iso/r = iso/r}) → g' bᵣ ≡ bᵣ
579-
step2 g' x bᵣ i = isoA/R-B/R'Hlp3 g' x bᵣ i
579+
step2 g' x bᵣ i = isoA/R-B/R'Hlp3 g' x bᵣ i
580580

581581
-- An important set quotient isomorphism:
582582
isoA/R-B/R' : {ℓ : Level} {A : Type ℓ} {B : Type ℓ} {R : A → A → Type ℓ}{ER : isEquivRel R}{iso/r : Iso/R {ℓ} A B {R} ER} →
@@ -626,32 +626,32 @@ quotientEqualityLemma2 : {A B : Type ℓ}{R : A → A → Type ℓ}{ER : isEquiv
626626
quotientEqualityLemma2 {ℓ}{A}{B}{R}{ER} AB = quotientEqualityLemma {iso/r = iso/R-A≡B {ℓ}{A}{B}{R}{ER} AB}
627627
where
628628
lemma : (A / R) ≡ (B / R* {iso/r = iso/R-A≡B {ℓ}{A}{B}{R}{ER} AB})
629-
lemma = quotientEqualityLemma {iso/r = iso/R-A≡B {ℓ}{A}{B}{R}{ER} AB}
629+
lemma = quotientEqualityLemma {iso/r = iso/R-A≡B {ℓ}{A}{B}{R}{ER} AB}
630630

631631
quotientEqualityLemma3 : {A : Type ℓ} {B : Type ℓ} {R : A → A → Type ℓ}{R' : B → B → Type ℓ}
632632
{ER : isEquivRel R} →
633-
(iso/r : Iso/R {ℓ} A B {R} ER) →
633+
(iso/r : Iso/R {ℓ} A B {R} ER) →
634634
(R'→R* : ∀ b b' → (R' b b' → R* {iso/r = iso/r} b b')) →
635635
(R*→R' : ∀ b b' → (R* {iso/r = iso/r} b b' → R' b b')) →
636636
A / R ≡ B / R'
637-
quotientEqualityLemma3 {ℓ} {A}{B}{R}{R'}{ER} iso/r R'→R* R*→R' = step1 ∙ A/R≡A/R' R*→R' R'→R*
637+
quotientEqualityLemma3 {ℓ} {A}{B}{R}{R'}{ER} iso/r R'→R* R*→R' = step1 ∙ A/R≡A/R' R*→R' R'→R*
638638
where
639639
step1 : (A / R) ≡ (B / R* {iso/r = iso/r})
640640
step1 = quotientEqualityLemma {ℓ}{A}{B}{R}{ER}{iso/r}
641-
641+
642642
quotientEqualityLemma4 : {A : Type ℓ} {B : Type ℓ} {R : A → A → Type ℓ}{R' : B → B → Type ℓ}
643643
{ER : isEquivRel R} →
644-
(iso/r : Iso/R {ℓ} A B {R} ER) →
644+
(iso/r : Iso/R {ℓ} A B {R} ER) →
645645
(R'→Rinv : ∀ b b' → (R' b b' → R (iso/r .inv/R b) (iso/r .inv/R b'))) →
646646
(Rinv→R' : ∀ b b' → (R (iso/r .inv/R b) (iso/r .inv/R b') → R' b b')) →
647647
A / R ≡ B / R'
648648
quotientEqualityLemma4 {ℓ} {A}{B}{R}{R'}{ER} iso/r R'→R R→R' =
649649
step1 ∙ A/R≡A/R' (λ b b' z → R→R' b b' z) (λ b b' x → R'→R b b' x)
650650
where
651651
help : ∀ b b' → R* {ℓ}{ℓ}{A}{B}{R}{ER}{iso/r} b b' ≡ R (iso/r .inv/R b) (iso/r .inv/R b')
652-
help b b' = refl
652+
help b b' = refl
653653
step1 : (A / R) ≡ (B / R* {iso/r = iso/r})
654654
step1 = quotientEqualityLemma {ℓ}{A}{B}{R}{ER}{iso/r}
655655

656-
656+
657657

0 commit comments

Comments
 (0)