\begin{code}
{-# OPTIONS --without-K #-}
module Preliminaries.SetsAndFunctions where
open import Agda.Primitive using (Level ; lzero ; lsuc ; _⊔_)
\end{code}
\begin{code}
id : {i : Level}{X : Set i} → X → X
id x = x
infixl 30 _∘_
_∘_ : {i j k : Level}{X : Set i}{Y : X → Set j}{Z : (x : X) → Y x → Set k} →
({x : X} → (y : Y x) → Z x y) → (f : (x : X) → Y x) →
(x : X) → Z x (f x)
g ∘ f = λ x → g(f x)
\end{code}
\begin{code}
Subset : {i : Level} → Set i → Set(lsuc i)
Subset {i} X = X → Set i
_∈_ : {i : Level}{X : Set i} → X → Subset X → Set i
x ∈ A = A x
\end{code}
\begin{code}
infixr 3 _,_
record Σ {i j : Level} {A : Set i} (B : A → Set j) : Set (i ⊔ j) where
constructor _,_
field
pr₁ : A
pr₂ : B pr₁
open Σ public
\end{code}
\begin{code}
infixr 20 _×_
_×_ : {i j : Level} → Set i → Set j → Set(i ⊔ j)
X × Y = Σ \(x : X) → Y
\end{code}
\begin{code}
infix 30 _≡_
infixr 40 _·_
infixl 50 _⁻¹
data _≡_ {i : Level} {A : Set i} : A → A → Set i where
refl : {a : A} → a ≡ a
J : {i j : Level} {A : Set i} (C : (a b : A) → a ≡ b → Set j)
→ ((a : A) → C a a refl)
→ (a b : A) → (p : a ≡ b) → C a b p
J C c a .a refl = c a
_⁻¹ : {i : Level}{A : Set i} → {x y : A} → x ≡ y → y ≡ x
refl ⁻¹ = refl
_·_ : {i : Level}{A : Set i} → {x y z : A} → x ≡ y → y ≡ z → x ≡ z
refl · refl = refl
transport : {i j : Level}{X : Set i}{x x' : X} → (Y : X → Set j) → x ≡ x' → Y x → Y x'
transport Y refl y = y
transport² : {i j k : Level} {X : Set i} (Y : X → Set j) (Z : (x : X) → Y x → Set k) {x x' : X} {y : Y x}
→ (p : x ≡ x') → Z x y → Z x' (transport Y p y)
transport² Y Z refl z = z
ap : {i j : Level}{X : Set i}{Y : Set j} → ∀(f : X → Y) → {x₀ x₁ : X} → x₀ ≡ x₁ → f x₀ ≡ f x₁
ap f refl = refl
fun-ap : {i j : Level}{X : Set i}{Y : X → Set j} → ∀{f g : (x : X) → Y x} → f ≡ g → ∀(x : X) → f x ≡ g x
fun-ap r x = ap (λ h → h x) r
apd² : {i j k : Level} {X : Set i} {Y : X → Set j} {Z : Set k}
{x₀ x₁ : X} {y₀ : Y x₀} {y₁ : Y x₁}
→ (f : (x : X) → Y x → Z) → (p : x₀ ≡ x₁) → transport Y p y₀ ≡ y₁
→ f x₀ y₀ ≡ f x₁ y₁
apd² f refl refl = refl
sym-is-inverse : {X : Set} {x y : X} (p : x ≡ y) → refl ≡ p ⁻¹ · p
sym-is-inverse refl = refl
pair⁼ : {i j : Level}{X : Set i}{Y : X → Set j}{x x' : X}{y : Y x}{y' : Y x'}
→ (p : x ≡ x') → transport Y p y ≡ y' → (x , y) ≡ (x' , y')
pair⁼ refl refl = refl
pairˣ⁼ : {i : Level}{A₀ A₁ : Set i}{a₀ a₀' : A₀}{a₁ a₁' : A₁}
→ a₀ ≡ a₀' → a₁ ≡ a₁' → (a₀ , a₁) ≡ (a₀' , a₁')
pairˣ⁼ refl refl = refl
pr₁⁼ : {i j : Level}{X : Set i}{Y : X → Set j}{w w' : Σ \(x : X) → Y x}
→ w ≡ w' → pr₁ w ≡ pr₁ w'
pr₁⁼ refl = refl
pr₂⁼ : {i j : Level}{X : Set i}{Y : X → Set j}{w w' : Σ \(x : X) → Y x}
→ (p : w ≡ w') → transport Y (pr₁⁼ p) (pr₂ w) ≡ pr₂ w'
pr₂⁼ refl = refl
pair⁼-η : {i j : Level} {A : Set i} {B : A → Set j} {w₀ w₁ : Σ B}
→ (p : w₀ ≡ w₁) → p ≡ pair⁼ (pr₁⁼ p) (pr₂⁼ p)
pair⁼-η refl = refl
pr₂ˣ⁼ : {i : Level}{A₀ A₁ : Set i}{w w' : A₀ × A₁}
→ w ≡ w' → pr₂ w ≡ pr₂ w'
pr₂ˣ⁼ refl = refl
\end{code}
\begin{code}
constant : {i j : Level} {X : Set i} {Y : Set j} → (X → Y) → Set(i ⊔ j)
constant f = ∀ x x' → f x ≡ f x'
Lemma[∘-constant] : {X Y Z : Set} → (f : X → Y) → (g : Y → Z)
→ constant f → constant (g ∘ f)
Lemma[∘-constant] f g cf x x' = ap g (cf x x')
\end{code}
\begin{code}
data ∅ : Set where
∅-elim : {i : Level}{A : Set i} → ∅ → A
∅-elim ()
¬ : {i : Level} → Set i → Set i
¬ X = X → ∅
infix 30 _≠_
_≠_ : {i : Level} {A : Set i} → A → A → Set i
x ≠ y = ¬ (x ≡ y)
\end{code}
\begin{code}
data ⒈ : Set where
⋆ : ⒈
unit : {X : Set} → X → ⒈
unit x = ⋆
singleton : ∀(x x' : ⒈) → x ≡ x'
singleton ⋆ ⋆ = refl
\end{code}
\begin{code}
infixr 20 _+_
data _+_ (X₀ X₁ : Set) : Set where
inl : X₀ → X₀ + X₁
inr : X₁ → X₀ + X₁
case : {X₀ X₁ Y : Set} → (X₀ → Y) → (X₁ → Y) → X₀ + X₁ → Y
case f₀ f₁ (inl x₀) = f₀ x₀
case f₀ f₁ (inr x₁) = f₁ x₁
equality-cases : {X₀ X₁ : Set} → {A : Set} →
∀(y : X₀ + X₁) → (∀ x₀ → y ≡ inl x₀ → A) → (∀ x₁ → y ≡ inr x₁ → A) → A
equality-cases (inl x₀) f₀ f₁ = f₀ x₀ refl
equality-cases (inr x₁) f₀ f₁ = f₁ x₁ refl
cases : {X₀ X₁ Y₀ Y₁ : Set} → (X₀ → Y₀) → (X₁ → Y₁) → X₀ + X₁ → Y₀ + Y₁
cases f₀ f₁ (inl x₀) = inl (f₀ x₀)
cases f₀ f₁ (inr x₁) = inr (f₁ x₁)
Lemma[+] : {X₀ X₁ : Set} → (x : X₀ + X₁) →
(Σ \(x₀ : X₀) → x ≡ inl x₀) + (Σ \(x₁ : X₁) → x ≡ inr x₁)
Lemma[+] (inl x₀) = inl (x₀ , refl)
Lemma[+] (inr x₁) = inr (x₁ , refl)
\end{code}
\begin{code}
decidable : Set → Set
decidable A = A + ¬ A
discrete : Set → Set
discrete A = ∀(a a' : A) → decidable (a ≡ a')
hprop : Set → Set
hprop X = (x y : X) → x ≡ y
hprop-valued : {A : Set} → (A → Set) → Set
hprop-valued P = ∀ a → hprop(P a)
⒈-hprop : hprop ⒈
⒈-hprop ⋆ ⋆ = refl
Σ-hprop : {A : Set} {B : A → Set}
→ hprop A → hprop-valued B → hprop (Σ B)
Σ-hprop {A} {B} hA hB (a₀ , b₀) (a₁ , b₁) = pair⁼ (hA a₀ a₁) (hB a₁ (transport B (hA a₀ a₁) b₀) b₁)
hset : Set → Set
hset X = {x y : X} → hprop (x ≡ y)
hset-valued : {A : Set} → (A → Set) → Set
hset-valued P = ∀ a → hset(P a)
Σ-hset : {A : Set} {B : A → Set}
→ hset A → hset-valued B → hset (Σ B)
Σ-hset {A} {B} hA hB {w₀} {w₁} p q = (pair⁼-η p) · claim₂ · (pair⁼-η q)⁻¹
where
□ : pr₁ w₀ ≡ pr₁ w₁ → Set
□ r = transport B r (pr₂ w₀) ≡ pr₂ w₁
claim₀ : pr₁⁼ p ≡ pr₁⁼ q
claim₀ = hA (pr₁⁼ p) (pr₁⁼ q)
claim₁ : transport □ claim₀ (pr₂⁼ p) ≡ pr₂⁼ q
claim₁ = hB (pr₁ w₁) (transport □ claim₀ (pr₂⁼ p)) (pr₂⁼ q)
claim₂ : pair⁼ (pr₁⁼ p) (pr₂⁼ p) ≡ pair⁼ (pr₁⁼ q) (pr₂⁼ q)
claim₂ = apd² pair⁼ claim₀ claim₁
\end{code}
\begin{code}
Funext : Set₁
Funext = {X : Set} {Y : X → Set} {f g : (x : X) → Y x}
→ (∀(x : X) → f x ≡ g x) → f ≡ g
\end{code}