diff options
Diffstat (limited to 'Structures.agda')
| -rw-r--r-- | Structures.agda | 4 |
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 |