chore: adotalypse

Author: plt-amy

src/1Lab/Counterexamples/Isovalence.lagda.md

@@ -93,7 +93,7 @@ that four copies of the identity path are identical to a single copy:
 ```agda
     at-id : P A id-iso
     at-id = ap (iso id (λ x → refl)) $ funext λ x →
-      refl ∙ refl ∙ refl ∙ refl ≡⟨ (∙-idl _ ·· ∙-idl _ ·· ∙-idl _) ⟩
+      refl ∙ refl ∙ refl ∙ refl ≡⟨ (∙-idl _ ∙∙ ∙-idl _ ∙∙ ∙-idl _) ⟩
       refl                      ∎
 ```
 

src/1Lab/Equiv.lagda.md

@@ -774,7 +774,7 @@ module Iso {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} ((f , f-iso) : Iso A B) whe
   open is-iso f-iso renaming (inverse to inverse-iso)
 
   injective : ∀ {x y} → f x ≡ f y → x ≡ y
-  injective p = sym (linv _) ·· ap inv p ·· linv _
+  injective p = sym (linv _) ∙∙ ap inv p ∙∙ linv _
 
   inverse : Iso B A
   inverse = inv , inverse-iso
@@ -891,8 +891,8 @@ precomposition with $p\inv$.
   ∙-pre-equiv p .fst q = p ∙ q
   ∙-pre-equiv p .snd = is-iso→is-equiv λ where
     .inv q  → sym p ∙ q
-    .rinv q → ∙-assoc p _ _       ·· ap (_∙ q) (∙-invr p) ·· ∙-idl q
-    .linv q → ∙-assoc (sym p) _ _ ·· ap (_∙ q) (∙-invl p) ·· ∙-idl q
+    .rinv q → ∙-assoc p _ _       ∙∙ ap (_∙ q) (∙-invr p) ∙∙ ∙-idl q
+    .linv q → ∙-assoc (sym p) _ _ ∙∙ ap (_∙ q) (∙-invl p) ∙∙ ∙-idl q
 ```
 
 Similarly, *post*composition with $p$ is inverted on both sides by
@@ -903,8 +903,8 @@ postcomposition with $p\inv$, so it too is an equivalence.
   ∙-post-equiv p .fst q = q ∙ p
   ∙-post-equiv p .snd = is-iso→is-equiv λ where
     .inv q  → q ∙ sym p
-    .rinv q → sym (∙-assoc q _ _) ·· ap (q ∙_) (∙-invl p) ·· ∙-idr q
-    .linv q → sym (∙-assoc q _ _) ·· ap (q ∙_) (∙-invr p) ·· ∙-idr q
+    .rinv q → sym (∙-assoc q _ _) ∙∙ ap (q ∙_) (∙-invl p) ∙∙ ∙-idr q
+    .linv q → sym (∙-assoc q _ _) ∙∙ ap (q ∙_) (∙-invr p) ∙∙ ∙-idr q
 ```
 
 ### The Lift type

src/1Lab/HIT/Truncation.lagda.md

@@ -282,7 +282,7 @@ proposition.
 is-constant→image-is-prop bset f fconst (a , x) (b , y) =
   Σ-prop-path (λ _ → squash)
     (∥-∥-elim₂ (λ _ _ → bset _ _)
-      (λ { (f*a , p) (f*b , q) → sym p ·· fconst f*a f*b ·· q }) x y)
+      (λ { (f*a , p) (f*b , q) → sym p ∙∙ fconst f*a f*b ∙∙ q }) x y)
 ```
 
 Using the image factorisation, we can project from a propositional

src/1Lab/Path.lagda.md

@@ -1464,10 +1464,10 @@ face for the [square] at the start of this section.
 [square]: 1Lab.Path.html#composition
 
 ```agda
-_··_··_ : ∀ {ℓ} {A : Type ℓ} {w x y z : A}
+_∙∙_∙∙_ : ∀ {ℓ} {A : Type ℓ} {w x y z : A}
         → w ≡ x → x ≡ y → y ≡ z
         → w ≡ z
-(p ·· q ·· r) i = hcomp (∂ i) sys module ··-sys where
+(p ∙∙ q ∙∙ r) i = hcomp (∂ i) sys module ∙∙-sys where
   sys : ∀ j → Partial (∂ i ∨ ~ j) _
   sys j (i = i0) = p (~ j)
   sys j (i = i1) = r j
@@ -1476,21 +1476,21 @@ _··_··_ : ∀ {ℓ} {A : Type ℓ} {w x y z : A}
 
 <!--
 ```agda
-{-# DISPLAY hcomp _ (··-sys.sys {ℓ} {A} {w} {x} {y} {z} p q r i) = _··_··_ {ℓ} {A} {w} {x} {y} {z} p q r i #-}
+{-# DISPLAY hcomp _ (∙∙-sys.sys {ℓ} {A} {w} {x} {y} {z} p q r i) = _∙∙_∙∙_ {ℓ} {A} {w} {x} {y} {z} p q r i #-}
 ```
 -->
 
 Since it will be useful later, we also give an explicit name for the
 *filler* of the double composition square. Since `Square`{.Agda}
 expresses an equation between paths, we can read the type of
-`··-filler`{.Agda} as saying that $p\inv \cdot (p \dcomp q \dcomp r) = q
+`∙∙-filler`{.Agda} as saying that $p\inv \cdot (p \dcomp q \dcomp r) = q
 \cdot r$.
 
 ```agda
-··-filler : ∀ {ℓ} {A : Type ℓ} {w x y z : A}
+∙∙-filler : ∀ {ℓ} {A : Type ℓ} {w x y z : A}
           → (p : w ≡ x) (q : x ≡ y) (r : y ≡ z)
-          → Square (sym p) q (p ·· q ·· r) r
-··-filler p q r i j = hfill (∂ j) i λ where
+          → Square (sym p) q (p ∙∙ q ∙∙ r) r
+∙∙-filler p q r i j = hfill (∂ j) i λ where
   k (j = i0) → p (~ k)
   k (j = i1) → r k
   k (k = i0) → q j
@@ -1525,12 +1525,12 @@ for the single composition, whose type we read as saying that $\refl
 ```agda
 _∙_
   : ∀ {ℓ} {A : Type ℓ} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
-p ∙ q = refl ·· p ·· q
+p ∙ q = refl ∙∙ p ∙∙ q
 
 ∙-filler
   : ∀ {ℓ} {A : Type ℓ} {x y z : A}
   → (p : x ≡ y) (q : y ≡ z) → Square refl p (p ∙ q) q
-∙-filler {x = x} {y} {z} p q = ··-filler refl p q
+∙-filler {x = x} {y} {z} p q = ∙∙-filler refl p q
 
 infixr 30 _∙_
 ```
@@ -1692,7 +1692,7 @@ answer, fortunately, is no: we can show that any triple of paths has a
 *square* whose boundary includes the two *lines* we're comparing.
 
 ```agda
-··-unique
+∙∙-unique
   : ∀ {ℓ} {A : Type ℓ} {w x y z : A}
   → (p : w ≡ x) (q : x ≡ y) (r : y ≡ z)
   → (α β : Σ[ s ∈ (w ≡ z) ] Square (sym p) q s r)
@@ -1706,7 +1706,7 @@ Note that the proof of this involves filling a cube in a context that
 *already* has an interval variable in scope - a hypercube!
 
 ```agda
-··-unique {w = w} {x} {y} {z} p q r (α , α-fill) (β , β-fill) =
+∙∙-unique {w = w} {x} {y} {z} p q r (α , α-fill) (β , β-fill) =
   λ i → (λ j → square i j) , (λ j k → cube i j k)
   where
     cube : (i j : I) → p (~ j) ≡ r j
@@ -1783,17 +1783,17 @@ edges going up rather than down. This is to match the direction of the
 3D diagram above. The colours are also matching.
 
 Readers who are already familiar with the notion of h-level will have
-noticed that the proof `··-unique`{.Agda} expresses that the type of
-double composites `p ·· q ·· r` is a _proposition_, not that it is
-contractible. However, since it is inhabited (by `_··_··_`{.Agda} and
+noticed that the proof `∙∙-unique`{.Agda} expresses that the type of
+double composites `p ∙∙ q ∙∙ r` is a _proposition_, not that it is
+contractible. However, since it is inhabited (by `_∙∙_∙∙_`{.Agda} and
 its filler), it is contractible:
 
 ```agda
-··-contract : ∀ {ℓ} {A : Type ℓ} {w x y z : A}
+∙∙-contract : ∀ {ℓ} {A : Type ℓ} {w x y z : A}
             → (p : w ≡ x) (q : x ≡ y) (r : y ≡ z)
             → (β : Σ[ s ∈ (w ≡ z) ] Square (sym p) q s r)
-            → (p ·· q ·· r , ··-filler p q r) ≡ β
-··-contract p q r β = ··-unique p q r _ β
+            → (p ∙∙ q ∙∙ r , ∙∙-filler p q r) ≡ β
+∙∙-contract p q r β = ∙∙-unique p q r _ β
 ```
 
 <!--
@@ -1804,13 +1804,13 @@ its filler), it is contractible:
   → Square refl p r q
   → r ≡ p ∙ q
 ∙-unique {p = p} {q} r square i =
-  ··-unique refl p q (_ , square) (_ , (∙-filler p q)) i .fst
+  ∙∙-unique refl p q (_ , square) (_ , (∙-filler p q)) i .fst
 
-··-unique' : ∀ {ℓ} {A : Type ℓ} {w x y z : A}
+∙∙-unique' : ∀ {ℓ} {A : Type ℓ} {w x y z : A}
            → {p : w ≡ x} {q : x ≡ y} {r : y ≡ z} {s : w ≡ z}
            → (β : Square (sym p) q s r)
-           → s ≡ p ·· q ·· r
-··-unique' β i = ··-contract _ _ _ (_ , β) (~ i) .fst
+           → s ≡ p ∙∙ q ∙∙ r
+∙∙-unique' β i = ∙∙-contract _ _ _ (_ , β) (~ i) .fst
 ```
 -->
 
@@ -1850,7 +1850,7 @@ ap-square f α i j = f (α i j)
 
 Despite the nightmare type (to allow `f` to be a dependent function),
 the definition is just as straightforward as that of `ap`{.Agda}. Using
-this with `··filler`{.Agda}, we get a square with boundary
+this with `∙∙filler`{.Agda}, we get a square with boundary
 
 ~~~{.quiver}
 \[\begin{tikzcd}[ampersand replacement=\&]
@@ -1864,19 +1864,19 @@ this with `··filler`{.Agda}, we get a square with boundary
 \end{tikzcd}\]
 ~~~
 
-but note that our lemma `··-unique'`{.Agda} says precisely that, for
+but note that our lemma `∙∙-unique'`{.Agda} says precisely that, for
 every square with this boundary, we can get a square connecting the red
 path $\ap{f}{(p \dcomp q \dcomp r)}$ and the composition $\ap{f}{p} \dcomp
 \ap{f}{q} \dcomp \ap{f}{r}$.
 
 ```agda
-ap-·· : (f : A → B) {x y z w : A} (p : x ≡ y) (q : y ≡ z) (r : z ≡ w)
-      → ap f (p ·· q ·· r) ≡ ap f p ·· ap f q ·· ap f r
-ap-·· f p q r = ··-unique' (ap-square f (··-filler p q r))
+ap-∙∙ : (f : A → B) {x y z w : A} (p : x ≡ y) (q : y ≡ z) (r : z ≡ w)
+      → ap f (p ∙∙ q ∙∙ r) ≡ ap f p ∙∙ ap f q ∙∙ ap f r
+ap-∙∙ f p q r = ∙∙-unique' (ap-square f (∙∙-filler p q r))
 
 ap-∙ : (f : A → B) {x y z : A} (p : x ≡ y) (q : y ≡ z)
       → ap f (p ∙ q) ≡ ap f p ∙ ap f q
-ap-∙ f p q = ap-·· f refl p q
+ap-∙ f p q = ap-∙∙ f refl p q
 ```
 
 ## Dependent paths, continued
@@ -2079,7 +2079,7 @@ with weird names are defined:
   → (q : x ≡ y)
   → (r : y ≡ z)
   → w ≡ z
-≡⟨⟩≡⟨⟩-syntax w x p q r = p ·· q ·· r
+≡⟨⟩≡⟨⟩-syntax w x p q r = p ∙∙ q ∙∙ r
 
 infixr 2 ≡⟨⟩-syntax
 syntax ≡⟨⟩-syntax x q p = x ≡⟨ p ⟩ q
@@ -2233,7 +2233,7 @@ double-composite
   : ∀ {ℓ} {A : Type ℓ}
   → {x y z w : A}
   → (p : x ≡ y) (q : y ≡ z) (r : z ≡ w)
-  → p ·· q ·· r ≡ p ∙ q ∙ r
+  → p ∙∙ q ∙∙ r ≡ p ∙ q ∙ r
 double-composite p q r i j =
   hcomp (i ∨ ∂ j) λ where
     k (i = i1) → ∙-filler' p (q ∙ r) k j
@@ -2265,7 +2265,7 @@ to adjust the path by a bunch of transports:
 
 ```agda
   where
-    lemma : _ ≡ (sym left ·· p ·· right)
+    lemma : _ ≡ (sym left ∙∙ p ∙∙ right)
     lemma i j = hcomp (~ i ∨ ∂ j) λ where
       k (k = i0) → transp (λ j → A) i (p j)
       k (i = i0) → hfill (∂ j) k λ where
@@ -2339,10 +2339,10 @@ infixl 32 _▷_
 Square≡double-composite-path : ∀ {ℓ} {A : Type ℓ}
           → {w x y z : A}
           → {p : x ≡ w} {q : x ≡ y} {s : w ≡ z} {r : y ≡ z}
-          → Square p q s r ≡ (sym p ·· q ·· r ≡ s)
+          → Square p q s r ≡ (sym p ∙∙ q ∙∙ r ≡ s)
 Square≡double-composite-path {p = p} {q} {s} {r} k =
   PathP (λ i → p (i ∨ k) ≡ r (i ∨ k))
-    (··-filler (sym p) q r k) s
+    (∙∙-filler (sym p) q r k) s
 
 J' : ∀ {ℓ₁ ℓ₂} {A : Type ℓ₁}
      (P : (x y : A) → x ≡ y → Type ℓ₂)

src/1Lab/Path/Groupoid.lagda.md

@@ -258,14 +258,14 @@ more than a handful of intermediate steps:
 
   ∙-cancel'-l : {x y z : A} (p : x ≡ y) (q r : y ≡ z)
               → p ∙ q ≡ p ∙ r → q ≡ r
-  ∙-cancel'-l p q r sq = sym (∙-cancell p q) ·· ap (sym p ∙_) sq ·· ∙-cancell p r
+  ∙-cancel'-l p q r sq = sym (∙-cancell p q) ∙∙ ap (sym p ∙_) sq ∙∙ ∙-cancell p r
 
   ∙-cancel'-r : {x y z : A} (p : y ≡ z) (q r : x ≡ y)
               → q ∙ p ≡ r ∙ p → q ≡ r
   ∙-cancel'-r p q r sq =
        sym (∙-cancelr q (sym p))
-    ·· ap (_∙ sym p) sq
-    ·· ∙-cancelr r (sym p)
+    ∙∙ ap (_∙ sym p) sq
+    ∙∙ ∙-cancelr r (sym p)
 ```
 
 While [[connections]] give us degenerate squares where two adjacent faces are

src/1Lab/Path/Reasoning.lagda.md

@@ -92,7 +92,7 @@ module _ (pq≡s : p ∙ q ≡ s) where
   ∙-pulll : p ∙ q ∙ r ≡ s ∙ r
   ∙-pulll {r = r} = ∙-assoc p q r ∙ ap (_∙ r) pq≡s
 
-  double-left : p ·· q ·· r ≡ s ∙ r
+  double-left : p ∙∙ q ∙∙ r ≡ s ∙ r
   double-left {r = r} = double-composite p q r ∙ ∙-pulll
 
   ∙-pullr : (r ∙ p) ∙ q ≡ r ∙ s
@@ -122,28 +122,28 @@ module _ (s≡pq : s ≡ p ∙ q) where
 
 module _ (pq≡rs : p ∙ q ≡ r ∙ s) where
   ∙-extendl : p ∙ (q ∙ t) ≡ r ∙ (s ∙ t)
-  ∙-extendl {t = t} = ∙-assoc _ _ _ ·· ap (_∙ t) pq≡rs ·· sym (∙-assoc _ _ _)
+  ∙-extendl {t = t} = ∙-assoc _ _ _ ∙∙ ap (_∙ t) pq≡rs ∙∙ sym (∙-assoc _ _ _)
 
   ∙-extendr : (t ∙ p) ∙ q ≡ (t ∙ r) ∙ s
-  ∙-extendr {t = t} = sym (∙-assoc _ _ _) ·· ap (t ∙_) pq≡rs ·· ∙-assoc _ _ _
+  ∙-extendr {t = t} = sym (∙-assoc _ _ _) ∙∙ ap (t ∙_) pq≡rs ∙∙ ∙-assoc _ _ _
 
-··-stack : (sym p' ·· (sym p ·· q ·· r) ·· r') ≡ (sym (p ∙ p') ·· q ·· (r ∙ r'))
-··-stack = ··-unique' (··-filler _ _ _ ∙₂ ··-filler _ _ _)
+∙∙-stack : (sym p' ∙∙ (sym p ∙∙ q ∙∙ r) ∙∙ r') ≡ (sym (p ∙ p') ∙∙ q ∙∙ (r ∙ r'))
+∙∙-stack = ∙∙-unique' (∙∙-filler _ _ _ ∙₂ ∙∙-filler _ _ _)
 
-··-chain : (sym p ·· q ·· r) ∙ (sym r ·· q' ·· s) ≡ sym p ·· (q ∙ q') ·· s
-··-chain {p = p} {q = q} {r = r} {q' = q'} {s = s} = sym (∙-unique _ square) where
-  square : Square refl (sym p ·· q ·· r) (sym p ·· (q ∙ q') ·· s) (sym r ·· q' ·· s)
+∙∙-chain : (sym p ∙∙ q ∙∙ r) ∙ (sym r ∙∙ q' ∙∙ s) ≡ sym p ∙∙ (q ∙ q') ∙∙ s
+∙∙-chain {p = p} {q = q} {r = r} {q' = q'} {s = s} = sym (∙-unique _ square) where
+  square : Square refl (sym p ∙∙ q ∙∙ r) (sym p ∙∙ (q ∙ q') ∙∙ s) (sym r ∙∙ q' ∙∙ s)
   square i j = hcomp (~ j ∨ (j ∧ (i ∨ ~ i))) λ where
     k (k = i0) → ∙-filler q q' i j
     k (j = i0) → p k
     k (j = i1) (i = i0) → r k
     k (j = i1) (i = i1) → s k
 
-··-∙-assoc : p ·· q ·· (r ∙ s) ≡ (p ·· q ·· r) ∙ s
-··-∙-assoc {p = p} {q = q} {r = r} {s = s} = sym (··-unique' square) where
-  square : Square (sym p) q ((p ·· q ·· r) ∙ s) (r ∙ s)
+∙∙-∙-assoc : p ∙∙ q ∙∙ (r ∙ s) ≡ (p ∙∙ q ∙∙ r) ∙ s
+∙∙-∙-assoc {p = p} {q = q} {r = r} {s = s} = sym (∙∙-unique' square) where
+  square : Square (sym p) q ((p ∙∙ q ∙∙ r) ∙ s) (r ∙ s)
   square i j = hcomp (~ i ∨ ~ j ∨ (i ∧ j)) λ where
-    k (k = i0) → ··-filler p q r i j
+    k (k = i0) → ∙∙-filler p q r i j
     k (i = i0) → q j
     k (j = i0) → p (~ i)
     k (i = i1) (j = i1) → s k

src/1Lab/Underlying.agda

@@ -75,11 +75,11 @@ from-is-true prf = subst ⌞_⌟ (sym prf) (hlevel 0 .centre)
 -- categories.
 record Funlike {ℓ ℓ' ℓ''} (A : Type ℓ) (arg : Type ℓ') (out : arg → Type ℓ'') : Type (ℓ ⊔ ℓ' ⊔ ℓ'') where
   field
-    _#_ : A → (x : arg) → out x
-  infixl 999 _#_
+    _·_ : A → (x : arg) → out x
+  infixl 999 _·_
 
-open Funlike ⦃ ... ⦄ using (_#_) public
-{-# DISPLAY Funlike._#_ _ f x = f # x #-}
+open Funlike ⦃ ... ⦄ using (_·_) public
+{-# DISPLAY Funlike._·_ _ f x = f · x #-}
 
 -- Sections of the _#_ operator tend to be badly-behaved since they
 -- introduce an argument x : ⌞ ?0 ⌟ whose Underlying instance meta
@@ -89,36 +89,36 @@ apply
   : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : A → Type ℓ'} {F : Type ℓ''}
   → ⦃ _ : Funlike F A B ⦄
   → F → (x : A) → B x
-apply = _#_
+apply = _·_
 
 -- Shortcut for ap (apply ...)
-ap#
+ap·
   : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : A → Type ℓ'} {F : Type ℓ''}
   → ⦃ _ : Funlike F A B ⦄
-  → (f : F) {x y : A} (p : x ≡ y) → PathP (λ i → B (p i)) (f # x) (f # y)
-ap# f = ap (apply f)
+  → (f : F) {x y : A} (p : x ≡ y) → PathP (λ i → B (p i)) (f · x) (f · y)
+ap· f = ap (apply f)
 
 -- Generalised happly.
-_#ₚ_
+_·ₚ_
   : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : A → Type ℓ'} {F : Type ℓ''}
   → ⦃ _ : Funlike F A B ⦄
-  → {f g : F} → f ≡ g → (x : A) → f # x ≡ g # x
-f #ₚ x = ap₂ _#_ f refl
+  → {f g : F} → f ≡ g → (x : A) → f · x ≡ g · x
+f ·ₚ x = ap₂ _·_ f refl
 
 instance
   Funlike-Π : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} → Funlike ((x : A) → B x) A B
-  Funlike-Π = record { _#_ = id }
+  Funlike-Π = record { _·_ = id }
 
   Funlike-Homotopy
     : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} {f g : ∀ x → B x}
     → Funlike (f ≡ g) A (λ x → f x ≡ g x)
-  Funlike-Homotopy = record { _#_ = happly }
+  Funlike-Homotopy = record { _·_ = happly }
 
   Funlike-Σ
     : ∀ {ℓ ℓ' ℓx ℓp} {A : Type ℓ} {B : A → Type ℓ'} {X : Type ℓx} {P : X → Type ℓp}
     → ⦃ Funlike X A B ⦄
     → Funlike (Σ X P) A B
-  Funlike-Σ = record { _#_ = λ (f , _) → f #_ }
+  Funlike-Σ = record { _·_ = λ (f , _) → f ·_ }
   {-# OVERLAPPABLE Funlike-Σ #-}
 
 -- Generalised "sections" (e.g. of a presheaf) notation.
@@ -127,7 +127,7 @@ _ʻ_
   → ⦃ _ : Funlike F A B ⦄
   → F → (x : A) → ⦃ _ : Underlying (B x) ⦄
   → Type _
-F ʻ x = ⌞ F # x ⌟
+F ʻ x = ⌞ F · x ⌟
 
 infix 999 _ʻ_
 

src/1Lab/Univalence/SIP.lagda.md

@@ -465,8 +465,8 @@ sym-transport-str :
   → equiv→inverse (α e .snd) t ≡ subst S (sym (ua e)) t
 sym-transport-str {S = S} α τ e t =
      sym (transport⁻transport (ap S (ua e)) (ae.from t))
-  ·· sym (ap (subst S (sym (ua e))) (τ e (ae.from t)))
-  ·· ap (subst S (sym (ua e))) (ae.ε t)
+  ∙∙ sym (ap (subst S (sym (ua e))) (τ e (ae.from t)))
+  ∙∙ ap (subst S (sym (ua e))) (ae.ε t)
   where module ae = Equiv (α e)
 ```
 -->