------------------------------------------------------------------------
-- The Agda standard library
--
-- A universe of proposition functors, along with some properties
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Relation.Nullary.Universe where
open import Data.Sum.Base as Sum hiding (map)
open import Data.Sum.Relation.Binary.Pointwise using (_⊎ₛ_; inj₁; inj₂)
open import Data.Product.Base as Product hiding (map)
open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
open import Data.Empty using (⊥)
open import Effect.Applicative using (RawApplicative)
open import Effect.Monad using (RawMonad)
open import Function.Base using (_∘_; id)
open import Function.Indexed.Relation.Binary.Equality using (≡-setoid)
open import Level using (Level; _⊔_; suc; Lift; lift; lower)
open import Relation.Nullary.Negation
using (¬_; contradiction; ¬¬-Monad; ¬¬-map; negated-stable)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Bundles using (Setoid)
import Relation.Binary.Construct.Always as Always using (setoid)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
import Relation.Binary.PropositionalEquality.Properties as PropEq
using (setoid)
import Relation.Binary.Indexed.Heterogeneous.Construct.Trivial
as Trivial using (indexedSetoid)
infix 5 ¬¬_
infixr 4 _⇒_
infixr 3 _∧_
infixr 2 _∨_
infix 1 ⟨_⟩_≈_
-- The universe.
data PropF p : Set (suc p) where
Id : PropF p
K : (P : Set p) → PropF p
_∨_ : (F₁ F₂ : PropF p) → PropF p
_∧_ : (F₁ F₂ : PropF p) → PropF p
_⇒_ : (P₁ : Set p) (F₂ : PropF p) → PropF p
¬¬_ : (F : PropF p) → PropF p
-- Equalities for universe inhabitants.
mutual
setoid : ∀ {p} → PropF p → Set p → Setoid p p
setoid Id P = PropEq.setoid P
setoid (K P) _ = PropEq.setoid P
setoid (F₁ ∨ F₂) P = (setoid F₁ P) ⊎ₛ (setoid F₂ P)
setoid (F₁ ∧ F₂) P = (setoid F₁ P) ×ₛ (setoid F₂ P)
setoid (P₁ ⇒ F₂) P = ≡-setoid P₁
(Trivial.indexedSetoid (setoid F₂ P))
setoid (¬¬ F) P = Always.setoid (¬ ¬ ⟦ F ⟧ P) _
⟦_⟧ : ∀ {p} → PropF p → (Set p → Set p)
⟦ F ⟧ P = Setoid.Carrier (setoid F P)
⟨_⟩_≈_ : ∀ {p} (F : PropF p) {P : Set p} → Rel (⟦ F ⟧ P) p
⟨_⟩_≈_ F = Setoid._≈_ (setoid F _)
-- ⟦ F ⟧ is functorial.
map : ∀ {p} (F : PropF p) {P Q} → (P → Q) → ⟦ F ⟧ P → ⟦ F ⟧ Q
map Id f p = f p
map (K P) f p = p
map (F₁ ∨ F₂) f FP = Sum.map (map F₁ f) (map F₂ f) FP
map (F₁ ∧ F₂) f FP = Product.map (map F₁ f) (map F₂ f) FP
map (P₁ ⇒ F₂) f FP = map F₂ f ∘ FP
map (¬¬ F) f FP = ¬¬-map (map F f) FP
map-id : ∀ {p} (F : PropF p) {P} → ⟨ ⟦ F ⟧ P ⇒ F ⟩ map F id ≈ id
map-id Id x = refl
map-id (K P) x = refl
map-id (F₁ ∨ F₂) (inj₁ x) = inj₁ (map-id F₁ x)
map-id (F₁ ∨ F₂) (inj₂ y) = inj₂ (map-id F₂ y)
map-id (F₁ ∧ F₂) (x , y) = (map-id F₁ x , map-id F₂ y)
map-id (P₁ ⇒ F₂) f = λ x → map-id F₂ (f x)
map-id (¬¬ F) ¬¬x = _
map-∘ : ∀ {p} (F : PropF p) {P Q R} (f : Q → R) (g : P → Q) →
⟨ ⟦ F ⟧ P ⇒ F ⟩ map F f ∘ map F g ≈ map F (f ∘ g)
map-∘ Id f g x = refl
map-∘ (K P) f g x = refl
map-∘ (F₁ ∨ F₂) f g (inj₁ x) = inj₁ (map-∘ F₁ f g x)
map-∘ (F₁ ∨ F₂) f g (inj₂ y) = inj₂ (map-∘ F₂ f g y)
map-∘ (F₁ ∧ F₂) f g x = (map-∘ F₁ f g (proj₁ x) ,
map-∘ F₂ f g (proj₂ x))
map-∘ (P₁ ⇒ F₂) f g h = λ x → map-∘ F₂ f g (h x)
map-∘ (¬¬ F) f g x = _
-- A variant of sequence can be implemented for ⟦ F ⟧.
sequence : ∀ {p AF} → RawApplicative AF →
(AF (Lift p ⊥) → ⊥) →
({A B : Set p} → (A → AF B) → AF (A → B)) →
∀ F {P} → ⟦ F ⟧ (AF P) → AF (⟦ F ⟧ P)
sequence {AF = AF} A extract-⊥ sequence-⇒ = helper
where
open RawApplicative A
helper : ∀ F {P} → ⟦ F ⟧ (AF P) → AF (⟦ F ⟧ P)
helper Id x = x
helper (K P) x = pure x
helper (F₁ ∨ F₂) (inj₁ x) = inj₁ <$> helper F₁ x
helper (F₁ ∨ F₂) (inj₂ y) = inj₂ <$> helper F₂ y
helper (F₁ ∧ F₂) (x , y) = _,_ <$> helper F₁ x ⊛ helper F₂ y
helper (P₁ ⇒ F₂) f = sequence-⇒ (helper F₂ ∘ f)
helper (¬¬ F) x =
pure (λ ¬FP → x (λ fp → extract-⊥ (lift ∘ ¬FP <$> helper F fp)))
-- Some lemmas about double negation.
private
open module M {a} = RawMonad (¬¬-Monad {a = a})
¬¬-pull : ∀ {p} (F : PropF p) {P} →
⟦ F ⟧ (¬ ¬ P) → ¬ ¬ ⟦ F ⟧ P
¬¬-pull = sequence rawApplicative
(λ f → f lower)
(λ f g → g (λ x → contradiction (λ y → g (λ _ → y)) (f x)))
¬¬-remove : ∀ {p} (F : PropF p) {P} →
¬ ¬ ⟦ F ⟧ (¬ ¬ P) → ¬ ¬ ⟦ F ⟧ P
¬¬-remove F = negated-stable ∘ ¬¬-pull (¬¬ 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