------------------------------------------------------------------------
-- The Agda standard library
--
-- Quotients for Heterogeneous equality
------------------------------------------------------------------------
{-# OPTIONS --with-K --safe #-}
module Relation.Binary.HeterogeneousEquality.Quotients where
open import Function.Base using (_$_; const; _∘_)
open import Level hiding (lift)
open import Relation.Binary.Bundles using (Setoid)
open import Relation.Binary.HeterogeneousEquality
open ≅-Reasoning
record Quotient {c ℓ} (S : Setoid c ℓ) : Set (suc (c ⊔ ℓ)) where
open Setoid S renaming (Carrier to A)
field
Q : Set c
abs : A → Q
compat : (B : Q → Set c) (f : ∀ a → B (abs a)) → Set (c ⊔ ℓ)
compat _ f = {a a′ : A} → a ≈ a′ → f a ≅ f a′
field
compat-abs : compat _ abs
lift : (B : Q → Set c) (f : ∀ a → B (abs a)) → compat B f → ∀ q → B q
lift-conv : {B : Q → Set c} (f : ∀ a → B (abs a)) (p : compat B f) →
∀ a → lift B f p (abs a) ≅ f a
Quotients : ∀ c ℓ → Set (suc (c ⊔ ℓ))
Quotients c ℓ = (S : Setoid c ℓ) → Quotient S
module Properties {c ℓ} {S : Setoid c ℓ} (Qu : Quotient S) where
open Setoid S renaming (Carrier to A) hiding (refl; sym; trans)
open Quotient Qu
module _ {B B′ : Q → Set c} {f : ∀ a → B (abs a)} {p : compat B f} where
lift-unique : {g : ∀ q → B′ q} → (∀ a → g (abs a) ≅ f a) →
∀ x → lift B f p x ≅ g x
lift-unique {g} ext = lift _ liftf≅g liftf≅g-ext where
liftf≅g : ∀ a → lift B f p (abs a) ≅ g (abs a)
liftf≅g x = begin
lift _ f p (abs x) ≅⟨ lift-conv f p x ⟩
f x ≅⟨ sym (ext x) ⟩
g (abs x) ∎
liftf≅g-ext : ∀ {a a′} → a ≈ a′ → liftf≅g a ≅ liftf≅g a′
liftf≅g-ext eq = ≅-heterogeneous-irrelevantˡ _ _
$ cong (lift B f p) (compat-abs eq)
lift-ext : {g : ∀ a → B′ (abs a)} {p′ : compat B′ g} → (∀ x → f x ≅ g x) →
∀ x → lift B f p x ≅ lift B′ g p′ x
lift-ext {g} {p′} h = lift-unique $ λ a → begin
lift B′ g p′ (abs a) ≅⟨ lift-conv g p′ a ⟩
g a ≅⟨ sym (h a) ⟩
f a ∎
lift-conv-abs : ∀ a → lift (const Q) abs compat-abs a ≅ a
lift-conv-abs = lift-unique (λ _ → refl)
lift-fold : {B : Q → Set c} (f : ∀ q → B q) →
∀ a → lift B (f ∘ abs) (cong f ∘ compat-abs) a ≅ f a
lift-fold f = lift-unique (λ _ → refl)
abs-epimorphism : {B : Q → Set c} {f g : ∀ q → B q} →
(∀ x → f (abs x) ≅ g (abs x)) → ∀ q → f q ≅ g q
abs-epimorphism {B} {f} {g} p q = begin
f q ≅⟨ sym (lift-fold f q) ⟩
lift B (f ∘ abs) (cong f ∘ compat-abs) q ≅⟨ lift-ext p q ⟩
lift B (g ∘ abs) (cong g ∘ compat-abs) q ≅⟨ lift-fold g q ⟩
g q ∎
------------------------------------------------------------------------
-- Properties provable with extensionality
module _ (ext : ∀ {a b} {A : Set a} {B₁ B₂ : A → Set b} {f₁ : ∀ a → B₁ a}
{f₂ : ∀ a → B₂ a} → (∀ a → f₁ a ≅ f₂ a) → f₁ ≅ f₂) where
module Properties₂
{c ℓ} {S₁ S₂ : Setoid c ℓ} (Qu₁ : Quotient S₁) (Qu₂ : Quotient S₂)
where
module S₁ = Setoid S₁
module S₂ = Setoid S₂
module Qu₁ = Quotient Qu₁
module Qu₂ = Quotient Qu₂
module _ {B : _ → _ → Set c} (f : ∀ s₁ s₂ → B (Qu₁.abs s₁) (Qu₂.abs s₂)) where
compat₂ : Set _
compat₂ = ∀ {a b a′ b′} → a S₁.≈ a′ → b S₂.≈ b′ → f a b ≅ f a′ b′
lift₂ : compat₂ → ∀ q q′ → B q q′
lift₂ p = Qu₁.lift _ g (ext ∘ g-ext) module Lift₂ where
g : ∀ a q → B (Qu₁.abs a) q
g a = Qu₂.lift (B (Qu₁.abs a)) (f a) (p S₁.refl)
g-ext : ∀ {a a′} → a S₁.≈ a′ → ∀ q → g a q ≅ g a′ q
g-ext a≈a′ = Properties.lift-ext Qu₂ (λ _ → p a≈a′ S₂.refl)
lift₂-conv : (p : compat₂) → ∀ a a′ → lift₂ p (Qu₁.abs a) (Qu₂.abs a′) ≅ f a a′
lift₂-conv p a a′ = begin
lift₂ p (Qu₁.abs a) (Qu₂.abs a′)
≅⟨ cong (_$ (Qu₂.abs a′)) (Qu₁.lift-conv (Lift₂.g p) (ext ∘ Lift₂.g-ext p) a) ⟩
Lift₂.g p a (Qu₂.abs a′)
≡⟨⟩
Qu₂.lift (B (Qu₁.abs a)) (f a) (p S₁.refl) (Qu₂.abs a′)
≅⟨ Qu₂.lift-conv (f a) (p S₁.refl) a′ ⟩
f a a′
∎
module Properties₃ {c ℓ} {S₁ S₂ S₃ : Setoid c ℓ}
(Qu₁ : Quotient S₁) (Qu₂ : Quotient S₂) (Qu₃ : Quotient S₃)
where
module S₁ = Setoid S₁
module S₂ = Setoid S₂
module S₃ = Setoid S₃
module Qu₁ = Quotient Qu₁
module Qu₂ = Quotient Qu₂
module Qu₃ = Quotient Qu₃
module _ {B : _ → _ → _ → Set c}
(f : ∀ s₁ s₂ s₃ → B (Qu₁.abs s₁) (Qu₂.abs s₂) (Qu₃.abs s₃)) where
compat₃ : Set _
compat₃ = ∀ {a b c a′ b′ c′} → a S₁.≈ a′ → b S₂.≈ b′ → c S₃.≈ c′ →
f a b c ≅ f a′ b′ c′
lift₃ : compat₃ → ∀ q₁ q₂ q₃ → B q₁ q₂ q₃
lift₃ p = Qu₁.lift _ h (ext ∘ h-ext) module Lift₃ where
g : ∀ a b q → B (Qu₁.abs a) (Qu₂.abs b) q
g a b = Qu₃.lift (B (Qu₁.abs a) (Qu₂.abs b)) (f a b) (p S₁.refl S₂.refl)
g-ext : ∀ {a a′ b b′} → a S₁.≈ a′ → b S₂.≈ b′ → ∀ c → g a b c ≅ g a′ b′ c
g-ext a≈a′ b≈b′ = Properties.lift-ext Qu₃ (λ _ → p a≈a′ b≈b′ S₃.refl)
h : ∀ a q₂ q₃ → B (Qu₁.abs a) q₂ q₃
h a = Qu₂.lift (λ b → ∀ q → B (Qu₁.abs a) b q) (g a) (ext ∘ g-ext S₁.refl)
h-ext : ∀ {a a′} → a S₁.≈ a′ → ∀ b → h a b ≅ h a′ b
h-ext a≈a′ = Properties.lift-ext Qu₂ $ λ _ → ext (g-ext a≈a′ S₂.refl)
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