{-# OPTIONS --without-K #-}
open import library.Basics hiding (Type ; Σ)
open import library.types.Sigma
module Sec2preliminaries where
Type = Type₀
Σ = library.Basics.Σ {lzero} {lzero}
_+_ : Type → Type → Type
X + Y = Coprod X Y
const : {X Y : Type} → (f : X → Y) → Type
const {X} f = (x₁ x₂ : X) → (f x₁) == (f x₂)
coll : Type → Type
coll X = Σ (X → X) const
pathColl : Type → Type
pathColl X = (x₁ x₂ : X) → coll (x₁ == x₂)
LEM : Type₁
LEM = (P : Type) → is-prop P → P + (¬ P)
LEM∞ : Type₁
LEM∞ = (X : Type) → X + (¬ X)
Funext : {X Y : Type} → Type
Funext {X} {Y} = (f g : X → Y) → ((x : X) → (f x) == (g x)) → f == g
_↔_ : Type → Type → Type
X ↔ Y = (X → Y) × (Y → X)
_↔₀₁_ : Type → Type₁ → Type₁
A ↔₀₁ B = (A → B) × (B → A)
_↔₁₁_ : Type₁ → Type₁ → Type₁
X ↔₁₁ Y = (X → Y) × (Y → X)
_◎_ : {X Y Z : Type} → (X ↔ Y) → (Y ↔ Z) → (X ↔ Z)
e₁ ◎ e₂ = fst e₂ ∘ fst e₁ , snd e₁ ∘ snd e₂
prop-eq-triv : {P : Type} → {p₁ p₂ : P} → is-prop P → p₁ == p₂
prop-eq-triv h = prop-has-all-paths h _ _
second-comp-triv : {X : Type} → {P : X → Type} → ((x : X) → is-prop (P x)) → (a b : Σ X P) → (fst a == fst b) → a == b
second-comp-triv {X} {P} h a b q = pair= q (from-transp P q (prop-eq-triv (h (fst b))))
open import library.types.Pi
neutral-codomain : {X : Type} → {Y : X → Type} → ((x : X) → is-contr (Y x)) → Π X Y ≃ Unit
neutral-codomain = contr-equiv-Unit ∘ Π-level
path-to-equiv : {X Y : Type} → X == Y → X ≃ Y
path-to-equiv {X} idp = ide X
delete-idp : {X : Type} → {x₁ x₂ : X} → (p q : x₁ == x₂) → (p ∙ idp == q) ≃ (p == q)
delete-idp idp q = ide _
add-path : {X : Type} → {x₁ x₂ x₃ : X} → (p q : x₁ == x₂) → (r : x₂ == x₃) → (p == q) == (p ∙ r == q ∙ r)
add-path idp q idp = transport (λ q₁ → (idp == q₁) == (idp == q ∙ idp)) {x = q ∙ idp} {y = q} (∙-unit-r _) idp
open import library.types.Paths
reverse-paths : {X : Type} → {x₁ x₂ : X} → (p : x₂ == x₁) → (q : x₁ == x₂) → (! p == q) ≃ (p == ! q)
reverse-paths p idp =
! p == idp ≃⟨ path-to-equiv (add-path _ _ _) ⟩
! p ∙ p == p ≃⟨ path-to-equiv (transport (λ p₁ → (! p ∙ p == p) == (p₁ == p)) (!-inv-l p) idp) ⟩
idp == p ≃⟨ !-equiv ⟩
p == idp ≃∎
switch-args : {X Y : Type} → {Z : X → Y → Type} → ((x : X) → (y : Y) → Z x y) ≃ ((y : Y) → (x : X) → Z x y)
switch-args = equiv f g h₁ h₂ where
f = λ k y x → k x y
g = λ i x y → i y x
h₁ = λ _ → idp
h₂ = λ _ → idp
set-lemma : {X : Type} → (is-set X) → {Y : X → Type} → (x₀ : X) → (y₁ y₂ : Y x₀) → _==_ {A = Σ X Y} (x₀ , y₁) (x₀ , y₂) → y₁ == y₂
set-lemma {X} h {Y} x₀ y₁ y₂ p =
y₁ =⟨ idp ⟩
transport Y idp y₁ =⟨ transport {A = x₀ == x₀} (λ q → y₁ == transport Y q y₁)
{x = idp} {y = ap fst p}
(prop-has-all-paths (h x₀ x₀) _ _)
idp ⟩
transport Y (ap fst p) y₁ =⟨ snd-of-p ⟩
y₂ ∎ where
pairs : =Σ {B = Y} (x₀ , y₁) (x₀ , y₂)
pairs = <– (=Σ-eqv _ _) p
paov : y₁ == y₂ [ Y ↓ fst (pairs) ]
paov = snd pairs
snd-of-p : transport Y (ap fst p) y₁ == y₂
snd-of-p = to-transp paov