diff --git a/master/Relation.Binary.HeterogeneousEquality.Quotients.Examples.html b/master/Relation.Binary.HeterogeneousEquality.Quotients.Examples.html
index 6459cc80e6..d1beba6242 100644
--- a/master/Relation.Binary.HeterogeneousEquality.Quotients.Examples.html
+++ b/master/Relation.Binary.HeterogeneousEquality.Quotients.Examples.html
@@ -34,10 +34,10 @@
≡-to-≅ $ +-cancelˡ-≡ y₂ _ _ $ ≅-to-≡ $ begin
y₂ + (x₁ + y₃) ≡⟨ ≡.sym (+-assoc y₂ x₁ y₃) ⟩
y₂ + x₁ + y₃ ≡⟨ ≡.cong (_+ y₃) (+-comm y₂ x₁) ⟩
- x₁ + y₂ + y₃ ≅⟨ cong (_+ y₃) p ⟩
+ x₁ + y₂ + y₃ ≅⟨ cong (_+ y₃) p ⟩
x₂ + y₁ + y₃ ≡⟨ ≡.cong (_+ y₃) (+-comm x₂ y₁) ⟩
y₁ + x₂ + y₃ ≡⟨ +-assoc y₁ x₂ y₃ ⟩
- y₁ + (x₂ + y₃) ≅⟨ cong (y₁ +_) q ⟩
+ y₁ + (x₂ + y₃) ≅⟨ cong (y₁ +_) q ⟩
y₁ + (x₃ + y₂) ≡⟨ +-comm y₁ (x₃ + y₂) ⟩
x₃ + y₂ + y₁ ≡⟨ ≡.cong (_+ y₁) (+-comm x₃ y₂) ⟩
y₂ + x₃ + y₁ ≡⟨ +-assoc y₂ x₃ y₁ ⟩
@@ -70,14 +70,14 @@
(a₁ + c₁) + (b₂ + d₂) ≡⟨ ≡.cong (_+ (b₂ + d₂)) (+-comm a₁ c₁) ⟩
(c₁ + a₁) + (b₂ + d₂) ≡⟨ +-assoc c₁ a₁ (b₂ + d₂) ⟩
c₁ + (a₁ + (b₂ + d₂)) ≡⟨ ≡.cong (c₁ +_) (≡.sym (+-assoc a₁ b₂ d₂)) ⟩
- c₁ + (a₁ + b₂ + d₂) ≅⟨ cong (λ n → c₁ + (n + d₂)) ab∼cd₁ ⟩
+ c₁ + (a₁ + b₂ + d₂) ≅⟨ cong (λ n → c₁ + (n + d₂)) ab∼cd₁ ⟩
c₁ + (a₂ + b₁ + d₂) ≡⟨ ≡.cong (c₁ +_) (+-assoc a₂ b₁ d₂) ⟩
c₁ + (a₂ + (b₁ + d₂)) ≡⟨ ≡.cong (λ n → c₁ + (a₂ + n)) (+-comm b₁ d₂) ⟩
c₁ + (a₂ + (d₂ + b₁)) ≡⟨ ≡.sym (+-assoc c₁ a₂ (d₂ + b₁)) ⟩
(c₁ + a₂) + (d₂ + b₁) ≡⟨ ≡.cong (_+ (d₂ + b₁)) (+-comm c₁ a₂) ⟩
(a₂ + c₁) + (d₂ + b₁) ≡⟨ +-assoc a₂ c₁ (d₂ + b₁) ⟩
a₂ + (c₁ + (d₂ + b₁)) ≡⟨ ≡.cong (a₂ +_) (≡.sym (+-assoc c₁ d₂ b₁)) ⟩
- a₂ + (c₁ + d₂ + b₁) ≅⟨ cong (λ n → a₂ + (n + b₁)) ab∼cd₂ ⟩
+ a₂ + (c₁ + d₂ + b₁) ≅⟨ cong (λ n → a₂ + (n + b₁)) ab∼cd₂ ⟩
a₂ + (c₂ + d₁ + b₁) ≡⟨ ≡.cong (a₂ +_) (+-assoc c₂ d₁ b₁) ⟩
a₂ + (c₂ + (d₁ + b₁)) ≡⟨ ≡.cong (λ n → a₂ + (c₂ + n)) (+-comm d₁ b₁) ⟩
a₂ + (c₂ + (b₁ + d₁)) ≡⟨ ≡.sym (+-assoc a₂ c₂ (b₁ + d₁)) ⟩
@@ -114,8 +114,8 @@
eq : ∀ a → abs a +ℤ zeroℤ ≅ abs a
eq a = begin
abs a +ℤ zeroℤ ≡⟨⟩
- abs a +ℤ abs zero² ≅⟨ +ℤ-on-abs≅abs-+₂ a zero² ⟩
- abs (a +² zero²) ≅⟨ compat-abs (+²-identityʳ a) ⟩
+ abs a +ℤ abs zero² ≅⟨ +ℤ-on-abs≅abs-+₂ a zero² ⟩
+ abs (a +² zero²) ≅⟨ compat-abs (+²-identityʳ a) ⟩
abs a ∎
+²-identityˡ : (i : ℕ²) → (zero² +² i) ∼ i
@@ -127,8 +127,8 @@
eq : ∀ a → zeroℤ +ℤ abs a ≅ abs a
eq a = begin
zeroℤ +ℤ abs a ≡⟨⟩
- abs zero² +ℤ abs a ≅⟨ +ℤ-on-abs≅abs-+₂ zero² a ⟩
- abs (zero² +² a) ≅⟨ compat-abs (+²-identityˡ a) ⟩
+ abs zero² +ℤ abs a ≅⟨ +ℤ-on-abs≅abs-+₂ zero² a ⟩
+ abs (zero² +² a) ≅⟨ compat-abs (+²-identityˡ a) ⟩
abs a ∎
+²-assoc : (i j k : ℕ²) → ((i +² j) +² k) ∼ (i +² (j +² k))
@@ -142,11 +142,11 @@
eq : ∀ i j k → (abs i +ℤ abs j) +ℤ abs k ≅ abs i +ℤ (abs j +ℤ abs k)
eq i j k = begin
- (abs i +ℤ abs j) +ℤ abs k ≅⟨ cong (_+ℤ abs k) (+ℤ-on-abs≅abs-+₂ i j) ⟩
- (abs (i +² j) +ℤ abs k) ≅⟨ +ℤ-on-abs≅abs-+₂ (i +² j) k ⟩
- abs ((i +² j) +² k) ≅⟨ compat-abs (+²-assoc i j k) ⟩
- abs (i +² (j +² k)) ≅⟨ sym (+ℤ-on-abs≅abs-+₂ i (j +² k)) ⟩
- (abs i +ℤ abs (j +² k)) ≅⟨ cong (abs i +ℤ_) (sym (+ℤ-on-abs≅abs-+₂ j k)) ⟩
+ (abs i +ℤ abs j) +ℤ abs k ≅⟨ cong (_+ℤ abs k) (+ℤ-on-abs≅abs-+₂ i j) ⟩
+ (abs (i +² j) +ℤ abs k) ≅⟨ +ℤ-on-abs≅abs-+₂ (i +² j) k ⟩
+ abs ((i +² j) +² k) ≅⟨ compat-abs (+²-assoc i j k) ⟩
+ abs (i +² (j +² k)) ≅⟨ sym (+ℤ-on-abs≅abs-+₂ i (j +² k)) ⟩
+ (abs i +ℤ abs (j +² k)) ≅⟨ cong (abs i +ℤ_) (sym (+ℤ-on-abs≅abs-+₂ j k)) ⟩
abs i +ℤ (abs j +ℤ abs k) ∎
compat₃ : ∀ {a a′ b b′ c c′} → a ∼ a′ → b ∼ b′ → c ∼ c′ → eq a b c ≅ eq a′ b′ c′
diff --git a/master/Relation.Binary.HeterogeneousEquality.Quotients.html b/master/Relation.Binary.HeterogeneousEquality.Quotients.html
index b0053edbcc..c1b81e1dfc 100644
--- a/master/Relation.Binary.HeterogeneousEquality.Quotients.html
+++ b/master/Relation.Binary.HeterogeneousEquality.Quotients.html
@@ -46,8 +46,8 @@
liftf≅g : ∀ a → lift B f p (abs a) ≅ g (abs a)
liftf≅g x = begin
- lift _ f p (abs x) ≅⟨ lift-conv f p x ⟩
- f x ≅⟨ sym (ext x) ⟩
+ lift _ f p (abs x) ≅⟨ lift-conv f p x ⟩
+ f x ≅⟨ sym (ext x) ⟩
g (abs x) ∎
liftf≅g-ext : ∀ {a a′} → a ≈ a′ → liftf≅g a ≅ liftf≅g a′
@@ -57,8 +57,8 @@
lift-ext : {g : ∀ a → B′ (abs a)} {p′ : compat B′ g} → (∀ x → f x ≅ g x) →
∀ x → lift B f p x ≅ lift B′ g p′ x
lift-ext {g} {p′} h = lift-unique $ λ a → begin
- lift B′ g p′ (abs a) ≅⟨ lift-conv g p′ a ⟩
- g a ≅⟨ sym (h a) ⟩
+ lift B′ g p′ (abs a) ≅⟨ lift-conv g p′ a ⟩
+ g a ≅⟨ sym (h a) ⟩
f a ∎
lift-conv-abs : ∀ a → lift (const Q) abs compat-abs a ≅ a
@@ -71,9 +71,9 @@
abs-epimorphism : {B : Q → Set c} {f g : ∀ q → B q} →
(∀ x → f (abs x) ≅ g (abs x)) → ∀ q → f q ≅ g q
abs-epimorphism {B} {f} {g} p q = begin
- f q ≅⟨ sym (lift-fold f q) ⟩
- lift B (f ∘ abs) (cong f ∘ compat-abs) q ≅⟨ lift-ext p q ⟩
- lift B (g ∘ abs) (cong g ∘ compat-abs) q ≅⟨ lift-fold g q ⟩
+ f q ≅⟨ sym (lift-fold f q) ⟩
+ lift B (f ∘ abs) (cong f ∘ compat-abs) q ≅⟨ lift-ext p q ⟩
+ lift B (g ∘ abs) (cong g ∘ compat-abs) q ≅⟨ lift-fold g q ⟩
g q ∎
@@ -108,11 +108,11 @@
lift₂-conv : (p : compat₂) → ∀ a a′ → lift₂ p (Qu₁.abs a) (Qu₂.abs a′) ≅ f a a′
lift₂-conv p a a′ = begin
lift₂ p (Qu₁.abs a) (Qu₂.abs a′)
- ≅⟨ cong (_$ (Qu₂.abs a′)) (Qu₁.lift-conv (Lift₂.g p) (ext ∘ Lift₂.g-ext p) a) ⟩
+ ≅⟨ cong (_$ (Qu₂.abs a′)) (Qu₁.lift-conv (Lift₂.g p) (ext ∘ Lift₂.g-ext p) a) ⟩
Lift₂.g p a (Qu₂.abs a′)
≡⟨⟩
Qu₂.lift (B (Qu₁.abs a)) (f a) (p S₁.refl) (Qu₂.abs a′)
- ≅⟨ Qu₂.lift-conv (f a) (p S₁.refl) a′ ⟩
+ ≅⟨ Qu₂.lift-conv (f a) (p S₁.refl) a′ ⟩
f a a′
∎
diff --git a/master/Relation.Binary.HeterogeneousEquality.html b/master/Relation.Binary.HeterogeneousEquality.html
index 0dce2cf2fa..8ce21fafc8 100644
--- a/master/Relation.Binary.HeterogeneousEquality.html
+++ b/master/Relation.Binary.HeterogeneousEquality.html
@@ -235,63 +235,63 @@
infix 4 _IsRelatedTo_
- data _IsRelatedTo_ {A : Set ℓ} {B : Set ℓ} (x : A) (y : B) : Set ℓ where
+ data _IsRelatedTo_ {A : Set a} {B : Set b} (x : A) (y : B) : Set a where
relTo : (x≅y : x ≅ y) → x IsRelatedTo y
start : ∀ {x : A} {y : B} → x IsRelatedTo y → x ≅ y
start (relTo x≅y) = x≅y
- ≡-go : ∀ {A : Set a} → Trans {A = A} {C = A} _≡_ _IsRelatedTo_ _IsRelatedTo_
- ≡-go x≡y (relTo y≅z) = relTo (trans (reflexive x≡y) y≅z)
+ ≡-go : ∀ {A : Set a} {B : Set b} → Trans {A = A} {C = B} _≡_ _IsRelatedTo_ _IsRelatedTo_
+ ≡-go x≡y (relTo y≅z) = relTo (trans (reflexive x≡y) y≅z)
-
- module _ {A : Set ℓ} {B : Set ℓ} where
- open begin-syntax (_IsRelatedTo_ {A = A} {B}) start public
+
+ module _ {A : Set a} {B : Set b} where
+ open begin-syntax (_IsRelatedTo_ {A = A} {B}) start public
+ open ≡-syntax (_IsRelatedTo_ {A = A} {B}) ≡-go public
-
- module _ {A : Set ℓ} where
- open ≡-syntax (_IsRelatedTo_ {A = A}) ≡-go public
- open end-syntax (_IsRelatedTo_ {A = A}) (relTo refl) public
+
+ module _ {A : Set a} where
+ open end-syntax (_IsRelatedTo_ {A = A}) (relTo refl) public
-
-
-
- infixr 2 _≅⟨_⟩_ _≅⟨_⟨_
+
+
+
+ infixr 2 _≅⟨_⟩_ _≅⟨_⟨_
- _≅⟨_⟩_ : ∀ (x : A) {y : B} {z : C} →
- x ≅ y → y IsRelatedTo z → x IsRelatedTo z
- _ ≅⟨ x≅y ⟩ relTo y≅z = relTo (trans x≅y y≅z)
+ _≅⟨_⟩_ : ∀ (x : A) {y : B} {z : C} →
+ x ≅ y → y IsRelatedTo z → x IsRelatedTo z
+ _ ≅⟨ x≅y ⟩ relTo y≅z = relTo (trans x≅y y≅z)
- _≅⟨_⟨_ : ∀ (x : A) {y : B} {z : C} →
- y ≅ x → y IsRelatedTo z → x IsRelatedTo z
- _ ≅⟨ y≅x ⟨ relTo y≅z = relTo (trans (sym y≅x) y≅z)
+ _≅⟨_⟨_ : ∀ (x : A) {y : B} {z : C} →
+ y ≅ x → y IsRelatedTo z → x IsRelatedTo z
+ _ ≅⟨ y≅x ⟨ relTo y≅z = relTo (trans (sym y≅x) y≅z)
-
- infixr 2 _≅˘⟨_⟩_
- _≅˘⟨_⟩_ = _≅⟨_⟨_
- {-# WARNING_ON_USAGE _≅˘⟨_⟩_
- "Warning: _≅˘⟨_⟩_ was deprecated in v2.0.
+
+ infixr 2 _≅˘⟨_⟩_
+ _≅˘⟨_⟩_ = _≅⟨_⟨_
+ {-# WARNING_ON_USAGE _≅˘⟨_⟩_
+ "Warning: _≅˘⟨_⟩_ was deprecated in v2.0.
Please use _≅⟨_⟨_ instead."
- #-}
+ #-}
-
-
+
+
-
-
+
+
-record Reveal_·_is_ {A : Set a} {B : A → Set b}
- (f : (x : A) → B x) (x : A) (y : B x) :
- Set (a ⊔ b) where
- constructor [_]
- field eq : f x ≅ y
+record Reveal_·_is_ {A : Set a} {B : A → Set b}
+ (f : (x : A) → B x) (x : A) (y : B x) :
+ Set (a ⊔ b) where
+ constructor [_]
+ field eq : f x ≅ y
-inspect : ∀ {A : Set a} {B : A → Set b}
- (f : (x : A) → B x) (x : A) → Reveal f · x is f x
-inspect f x = [ refl ]
+inspect : ∀ {A : Set a} {B : A → Set b}
+ (f : (x : A) → B x) (x : A) → Reveal f · x is f x
+inspect f x = [ refl ]
-
+
-
-
+
+