reorganize equality imports

Since we are working with multiple setoids now, it makes more sense to
qualify their members. Follow the "as P" pattern from the standard
library. Also stop importing those symbols from Relation.Binary.Core as
later agda-stdlib versions will move them away. Rather than EqSetoid or
PropEq, use P.setoid consistently.

1 files changed, 2 insertions, 2 deletions

diff --git a/Structures.agda b/Structures.agda
index 10abd42..1a8fd64 100644
--- a/Structures.agda
+++ b/Structures.agda
@@ -9,7 +9,7 @@ import Data.Vec.Properties as VP
 open import Function using (_∘_ ; flip ; id)
 open import Function.Equality using (_⟶_ ; _⇨_ ; _⟨$⟩_)
 open import Relation.Binary using (_Preserves_⟶_)
-open import Relation.Binary.PropositionalEquality as P using (_≗_ ; _≡_ ; refl ; module ≡-Reasoning)
+open import Relation.Binary.PropositionalEquality as P using (_≗_ ; _≡_ ; module ≡-Reasoning)
 
 open import Generic using (sequenceV)
 
@@ -26,7 +26,7 @@ record IsFunctor (F : Set → Set) (f : {α β : Set} → (α →  β) → F α
       { _⟨$⟩_ = f (_⟨$⟩_ g)
       ; cong = P.cong (f (_⟨$⟩_ g))
       }
-    ; cong = λ {g} {h} g≗h {x} x≡y → P.subst (λ z → f (_⟨$⟩_ g) x ≡ f (_⟨$⟩_ h) z) x≡y (cong (λ _ → g≗h refl) x)
+    ; cong = λ {g} {h} g≗h {x} x≡y → P.subst (λ z → f (_⟨$⟩_ g) x ≡ f (_⟨$⟩_ h) z) x≡y (cong (λ _ → g≗h P.refl) x)
     }
 
 record Functor (f : Set → Set) : Set₁ where