module SOAS.Common where
open import Categories.Category.Instance.Sets public
open import Axiom.Extensionality.Propositional
using (Extensionality; ExtensionalityImplicit)
open import Relation.Binary.PropositionalEquality public
hiding (Extensionality)
renaming (subst to ≡subst; [_] to ≡[_])
open import Categories.Category public
open import Categories.Category.Helper public
open import Categories.Functor public
renaming (id to idF)
open import Categories.NaturalTransformation public
using (ntHelper)
renaming (NaturalTransformation to NT; id to idN; _∘ᵥ_ to _∘N_)
open import Categories.NaturalTransformation.Equivalence using (_≃_) public
open import Categories.Morphism using (Iso) public
open import Level as L hiding (lift) renaming (suc to lsuc) public
open import Function using (flip; case_of_; _∋_) public renaming (_$_ to _$ᶠ_)
open import Data.Product public using (_×_; proj₁; proj₂; _,_; Σ; module Σ; Σ-syntax; swap)
open import Data.Sum public using (_⊎_ ; inj₁; inj₂)
open import Data.Unit public using (tt)
data *T : Set where
* : *T
1ℓ : Level
1ℓ = lsuc 0ℓ
postulate
ext : Extensionality 0ℓ 0ℓ
iext : ExtensionalityImplicit 0ℓ 0ℓ
ext² : {A : Set} {B : A → Set}{C : (x : A) → B x → Set}
{f g : (x : A) → (y : B x) → C x y} →
(∀ x y → f x y ≡ g x y) →
(λ x y → f x y) ≡ (λ x y → g x y)
ext² p = ext (λ x → ext (λ y → p x y))
dext : {A : Set} {B : A → Set}{C : (x : A) → B x → Set}
{f g : {x : A} → (y : B x) → C x y} →
(∀ {x} y → f {x} y ≡ g {x} y) →
(λ {x} y → f {x} y) ≡ (λ {x} y → g {x} y)
dext p = iext (ext p)
dext² : {A : Set}{B : A → Set}{C : A → A → Set}
{D : (x : A) → B x → (y : A) → C x y → Set}
{f g : {x : A} → (b : B x) → {y : A} → (c : C x y) → D x b y c} →
(∀ {x} b {y} c → f {x} b {y} c ≡ g {x} b {y} c) →
(λ {x} b {y} c → f {x} b {y} c) ≡
(λ {x} b {y} c → g {x} b {y} c)
dext² p = dext (λ {x} y → dext (p {x} y))
dext′ : {A : Set} {B : A → Set}{C : (x : A) → B x → Set}
{f g : {x : A} → (y : B x) → C x y} →
(∀ {x} {y} → f {x} y ≡ g {x} y) →
(λ {x} y → f {x} y) ≡ (λ {x} y → g {x} y)
dext′ p = dext (λ {x} y → p {x}{y})
𝕊ets : Category 1ℓ 0ℓ 0ℓ
𝕊ets = Sets 0ℓ
module 𝕊et = Category 𝕊ets
open Category (Sets 0ℓ) public using (_∘_; id)
open import Categories.Morphism 𝕊ets public using ()
renaming ( _≅_ to _≅ₛ_ ; module ≅ to ≅ₛ ; ≅-setoid to ≅ₛ-setoid)
congr : ∀{ℓ}{A B : Set ℓ}{x y : A} → x ≡ y → (f : A → B) → f x ≡ f y
congr refl f = refl