------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of pointwise equality for containers
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.Container.Relation.Binary.Pointwise.Properties where
open import Axiom.Extensionality.Propositional using (Extensionality)
open import Data.Container.Core using (Container; ⟦_⟧)
open import Data.Container.Relation.Binary.Pointwise
using (Pointwise; _,_)
open import Data.Product.Base using (_,_; Σ-syntax; -,_)
open import Level using (_⊔_)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Definitions
using (Reflexive; Symmetric; Transitive)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.PropositionalEquality.Core as ≡
using (_≡_; subst; cong)
module _ {s p x r} {X : Set x} (C : Container s p) (R : Rel X r) where
refl : Reflexive R → Reflexive (Pointwise C R)
refl R-refl = ≡.refl , λ p → R-refl
sym : Symmetric R → Symmetric (Pointwise C R)
sym R-sym (≡.refl , f) = ≡.refl , λ p → R-sym (f p)
trans : Transitive R → Transitive (Pointwise C R)
trans R-trans (≡.refl , f) (≡.refl , g) = ≡.refl , λ p → R-trans (f p) (g p)
private
-- Note that, if propositional equality were extensional, then
-- Eq _≡_ and _≡_ would coincide.
Eq⇒≡ : ∀ {s p x} {C : Container s p} {X : Set x} {xs ys : ⟦ C ⟧ X} →
Extensionality p x → Pointwise C _≡_ xs ys → xs ≡ ys
Eq⇒≡ ext (≡.refl , f≈f′) = cong -,_ (ext f≈f′)
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4