Categories.Category.Instance.SimplicialSet.Properties: new function h…

…ierarchy

src/Categories/Category/Instance/SimplicialSet/Properties.agda

@@ -93,7 +93,7 @@ boundary-map {n = n} f b = record
       }
     }
   ; F₁ = λ f → record
-    { _⟨$⟩_ = λ (lift b) → lift (boundary-map f b)
+    { to = λ (lift b) → lift (boundary-map f b)
     ; cong = λ (lift eq) → lift (Δ-eq (Δ-pointwise eq))
     }
   ; identity = λ (lift eq) → lift (Δ-eq (Δ-pointwise eq))
@@ -135,7 +135,7 @@ record Horn (m n-1 : ℕ) (k : Fin (ℕ.suc n-1)) : Set where
       }
     }
   ; F₁ = λ f → record
-    { _⟨$⟩_ = λ (lift h) → lift record
+    { to = λ (lift h) → lift record
       { horn = boundary-map f (horn h)
       ; is-horn = is-horn h
       }
@@ -164,14 +164,14 @@ module _ where
   ∂Δ-inj : ∀ {n} → ∂Δ[ n ] ⇒ Δ[ n ]
   ∂Δ-inj {ℕ.zero} = ntHelper record
     { η = λ X → record
-      { _⟨$⟩_ = ⊥-elim
+      { to = ⊥-elim
       ; cong = λ { {()} }
       }
     ; commute = λ { _ {()} _ }
     }
   ∂Δ-inj {ℕ.suc n} = ntHelper record
     { η = λ X → record
-      { _⟨$⟩_ = λ (lift b) → lift (hom b)
+      { to = λ (lift b) → lift (hom b)
       ; cong = λ (lift eq) → lift (Δ-eq (Δ-pointwise eq))
       }
     ; commute = λ f (lift eq) → lift (Δ-eq (Δ-pointwise eq))
@@ -183,7 +183,7 @@ module _ where
   Λ-inj : ∀ {n} → (k : Fin n) → Λ[ n , k ] ⇒ Δ[ n ]
   Λ-inj {n = ℕ.suc n} k = ntHelper record
     { η = λ X → record
-      { _⟨$⟩_ = λ (lift h) → lift (hom h)
+      { to = λ (lift h) → lift (hom h)
       ; cong = λ (lift eq) → lift (Δ-eq (Δ-pointwise eq))
       }
     ; commute = λ f (lift eq) → lift (Δ-eq (Δ-pointwise eq))