------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties related to All
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.Maybe.Relation.Unary.All.Properties where
open import Data.Maybe.Base using (Maybe; just; nothing; map; _<∣>_)
open import Data.Maybe.Relation.Unary.All as All
using (All; nothing; just)
open import Data.Maybe.Relation.Binary.Connected
using (Connected; just-nothing; nothing-just; nothing; just)
open import Data.Product.Base using (_×_; _,_)
open import Function.Base using (_∘_)
open import Level using (Level)
open import Relation.Unary using (Pred; _⊆_)
open import Relation.Binary.Core using (Rel)
private
variable
a b p q ℓ : Level
A : Set a
B : Set b
P : Pred A p
Q : Pred B q
------------------------------------------------------------------------
-- Relationship with other combinators
------------------------------------------------------------------------
All⇒Connectedˡ : ∀ {R : Rel A ℓ} {x y} →
All (R x) y → Connected R (just x) y
All⇒Connectedˡ (just x) = just x
All⇒Connectedˡ nothing = just-nothing
All⇒Connectedʳ : ∀ {R : Rel A ℓ} {x y} →
All (λ v → R v y) x → Connected R x (just y)
All⇒Connectedʳ (just x) = just x
All⇒Connectedʳ nothing = nothing-just
------------------------------------------------------------------------
-- Introduction (⁺) and elimination (⁻) rules for maybe operations
------------------------------------------------------------------------
-- map
map⁺ : ∀ {f : A → B} {mx} → All (P ∘ f) mx → All P (map f mx)
map⁺ (just p) = just p
map⁺ nothing = nothing
map⁻ : ∀ {f : A → B} {mx} → All P (map f mx) → All (P ∘ f) mx
map⁻ {mx = just x} (just px) = just px
map⁻ {mx = nothing} nothing = nothing
-- A variant of All.map.
gmap : ∀ {f : A → B} → P ⊆ Q ∘ f → All P ⊆ All Q ∘ map f
gmap g = map⁺ ∘ All.map g
------------------------------------------------------------------------
-- _<∣>_
<∣>⁺ : ∀ {mx my} → All P mx → All P my → All P (mx <∣> my)
<∣>⁺ (just px) pmy = just px
<∣>⁺ nothing pmy = pmy
<∣>⁻ : ∀ mx {my} → All P (mx <∣> my) → All P mx
<∣>⁻ (just x) pmxy = pmxy
<∣>⁻ nothing pmxy = nothing
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