From c835e655a05c73f7dd2dc46c652be3d43e91a4b7 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Sun, 25 Nov 2018 10:35:23 +0100 Subject: 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. --- Structures.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'Structures.agda') 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 -- cgit v1.2.3