foundations.BasicEquivalences.md.
Version of Sunday, January 22, 2023, 10:42 PM
Powered by agda version 2.6.2.2-442c76b and pandoc 2.14.0.3
{-# OPTIONS --without-K --exact-split #-}
module foundations.BasicEquivalences where open import foundations.BasicTypes open import foundations.BasicFunctions open import foundations.AlgebraOnPaths open import foundations.EquivalenceType open import foundations.EquivalenceReasoning open import foundations.HomotopyType open import foundations.QuasiinverseType open import foundations.QuasiinverseLemmas
+-Σ×Σ
: ∀ {ℓ₁ ℓ₂} {A : Type ℓ₁}{B : Type ℓ₂}{C : A + B → Type (ℓ₁ ⊔ ℓ₂)}
→ (Σ[ x ∶ (A + B) ] C x) ≃ (Σ[ x ∶ A ] C (inl x)) + (Σ[ x ∶ B ] C (inr x))
+-Σ×Σ = qinv-≃ go (back , ((λ {(inl (a , c)) → idp
; (inr (b , c)) → idp})
, (λ {(inl a , c) → idp
; (inr b , c) → idp})))
where
go : _
go (inl a , c) = inl (a , c)
go (inr b , c) = inr (b , c)
back : _
back (inl (a , c)) = inl a , c
back (inr (b , c)) = inr b , c
postulate
∑-+-≃-+-∑ -- TODO: prove this in another time, np.
: ∀ {ℓ₁ ℓ₂ ℓ₃} {X : Type ℓ₁}{A : X → Type ℓ₂}{B : X → Type ℓ₃}
→ (∑[ x ∶ X ] (A x + B x)) ≃ ((∑[ x ∶ X ] (A x)) + (∑[ x ∶ X ] (B x)) )
equiv-+-fixed-left
: ∀ {ℓ₁ ℓ₂ ℓ₃} {A : Type ℓ₁}{B : Type ℓ₂}{X : Type ℓ₃}
→ A ≃ B
→ (X + A) ≃ (X + B)
equiv-+-fixed-right
: ∀ {ℓ₁ ℓ₂ ℓ₃} {A : Type ℓ₁}{B : Type ℓ₂}{X : Type ℓ₃}
→ A ≃ B
→ (A + X) ≃ (B + X)
-- Π+-Π×Π
-- : ∀ {ℓ₁ ℓ₂} {A : Type ℓ₁}{B : Type ℓ₂}{C : A + B → Type (ℓ₁ ⊔ ℓ₂)}
-- → ((x : A + B) → C x) ≃ ((x : A) → C (inl x)) × ((b : B) → C (inr b))
-- Π+-Π×Π {A = A}{B}{C} = qinv- go (back , (λ _ → idp) , retract-proof)
-- where
-- go : _
-- go f = (λ a → f (inl a)) , λ b → f (inr b)
-- back : _
-- back (f , g) = λ {(inl a) → f a; (inr b) → g b}
-- retract-proof : _
-- retract-proof f = funext (λ {(inl a) → idp ; (inr b) → idp})
Σℕ : ∀ {ℓ} {C : ℕ → Type ℓ}
→ (Σ[ n ∶ ℕ ] C n) ≃ ((C zero) + ( Σ[ n ∶ ℕ ] (C (succ n))))
Σℕ = qinv-≃ go (back , (λ {(inl c) → idp
; (inr (n , c)) → idp}) , retract-proof)
where
go : _
go (zero , c) = inl c
go (succ n , c) = inr (n , c)
back : _
back (inl c) = zero , c
back (inr (n , c)) = succ n , c
retract-proof : _
retract-proof (zero , c) = idp
retract-proof (succ n , c) = idp
-- Π-respects-≃
-- : ∀ {ℓ₁ ℓ₂ ℓ₃} {A : Type ℓ₁}{B : A → Type ℓ₂}{C : A → Type ℓ₃}
-- → ((a : A) → (B a ≃ C a))
-- → ((a : A) → B a) ≃ ((a : A) → C a)
-- Π-respects-≃ e = qinv-≃ go (back ,
-- (λ f → funext λ x → secEq (e x) (f x))
-- (λ f → funext λ x → retEq (e x) (f x)))
-- where
-- go : _
-- go f a = fst (e a) (f a)
-- back : _
-- back f a = rapply (e a) (f a)
-- Πℕ
-- : ∀ {ℓ} {C : ℕ → Type ℓ}
-- → ((n : ℕ) → C n) ≃ ((C zero) × ((n : ℕ) → C (succ n)))
-- Πℕ {C} = qinv- go (back , (λ _ → idp) retract-proof)
-- where
-- go : _
-- go f = f zero , λ n → f (succ n)
-- back : _
-- back (zero-case , succ-case) zero = zero-case
-- back (zero-case , succ-case) (succ z) = succ-case z
-- retract-proof : _
-- retract-proof f = funext (λ {zero → idp
-- ; (succ n) → idp})
-- Π+×Π4
-- : ∀ {ℓ₁ ℓ₂} {A : Type ℓ₁}{B : Type ℓ₂}{C : A + B → A + B → Type (ℓ₁ ⊔ ℓ₂)}
-- → ((x y : A + B) → C x y)
-- ≃ (((x y : A) → C (inl x) (inl y))
-- × ((x : A) (y : B) → C (inl x) (inr y))
-- × ((x : A) (y : B) → C (inr y) (inl x))
-- × ((x y : B) → C (inr x) (inr y)))
-- Π+×Π4 {A = A}{B}{C} = qinv- go (back , (λ _ → idp) retract-proof)
-- where
-- go : _
-- go f = (λ x y → f (inl x) (inl y))
-- , (λ x y → f (inl x) (inr y))
-- , (λ x y → f (inr y) (inl x))
-- , (λ x y → f (inr x) (inr y))
-- back : _
-- back (f1 , f2 , f3 , f4) (inl x) (inl y) = f1 x y
-- back (f1 , f2 , f3 , f4) (inl x) (inr y) = f2 x y
-- back (f1 , f2 , f3 , f4) (inr x) (inl y) = f3 y x
-- back (f1 , f2 , f3 , f4) (inr x) (inr y) = f4 x y
-- retract-proof : _
-- retract-proof f = funext (λ {(inl x) → funext (λ {(inl y) → idp
-- ; (inr y) → idp})
-- ; (inr x) → funext ((λ { (inl y) → idp
-- ; (inr y) → idp}))})
≃-+-comm
: ∀ {ℓ₁ ℓ₂ : Level} {X : Type ℓ₁}{Y : Type ℓ₂}
→ X + Y ≃ Y + X
≃-+-comm {X = X}{Y} = qinv-≃ f (g , H₁ , H₂ )
where
private
f : X + Y → Y + X
f (inl x) = inr x
f (inr x) = inl x
g : Y + X → X + Y
g (inl x) = inr x
g (inr x) = inl x
H₁ : (f ∘ g) ∼ id
H₁ (inl x) = idp
H₁ (inr x) = idp
H₂ : (g ∘ f) ∼ id
H₂ (inl x) = idp
H₂ (inr x) = idp
≃-+-assoc
: ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {X : Type ℓ₁}{Y : Type ℓ₂} {Z : Type ℓ₃}
→ X + (Y + Z) ≃ (X + Y) + Z
≃-+-assoc {X = X}{Y}{Z} = qinv-≃ f (g , (H₁ , H₂))
where
private
f : X + (Y + Z) → (X + Y) + Z
f (inl x) = inl (inl x)
f (inr (inl x)) = inl (inr x)
f (inr (inr x)) = inr x
g : (X + Y) + Z → X + (Y + Z)
g (inl (inl x)) = inl x
g (inl (inr x)) = inr (inl x)
g (inr x) = inr (inr x)
H₁ : (f ∘ g) ∼ id
H₁ (inl (inl x)) = idp
H₁ (inl (inr x)) = idp
H₁ (inr x) = idp
H₂ : g ∘ f ∼ id
H₂ (inl x) = idp
H₂ (inr (inl x)) = idp
H₂ (inr (inr x)) = idp
≃-+-runit
: ∀ {ℓ₁ ℓ₂ : Level}{X : Type ℓ₁}
→ X ≃ X + (𝟘 ℓ₂)
≃-+-runit {ℓ₁ = ℓ₁}{ℓ₂}{X} = qinv-≃ f (g , (H₁ , H₂ ))
where
private
f : X → X + (𝟘 ℓ₂)
f x = inl x
g : X + (𝟘 ℓ₂) → X
g (inl x) = x
H₁ : (f ∘ g) ∼ id
H₁ (inl x) = idp
H₂ : (x : X) → (g (f x)) ≡ x
H₂ x = idp
≃-+-lunit
: ∀ {ℓ₁ ℓ₂ : Level}{X : Type ℓ₁}
→ X ≃ 𝟘 ℓ₂ + X
≃-+-lunit {ℓ₂ = ℓ₂}{X} =
X ≃⟨ ≃-+-runit ⟩
X + 𝟘 ℓ₂ ≃⟨ ≃-+-comm ⟩
(𝟘 ℓ₂) + X ≃∎
≃-×-comm
: ∀ {ℓ₁ ℓ₂ : Level} {X : Type ℓ₁}{Y : Type ℓ₂}
→ X × Y ≃ Y × X
≃-×-comm {X = X}{Y} = qinv-≃ f (g , (H₁ , H₂))
where
private
f : X × Y → Y × X
f (x , y) = (y , x)
g : Y × X → X × Y
g (y , x) = (x , y)
H₁ : (f ∘ g) ∼ id
H₁ x = idp
H₂ : (g ∘ f) ∼ id
H₂ x = idp
≃-×-runit
: ∀ {ℓ₁ ℓ₂} {X : Type ℓ₁}
→ X ≃ X × (𝟙 ℓ₂)
≃-×-runit {ℓ₁}{ℓ₂}{X = X} = qinv-≃ f (g , (H₁ , H₂))
where
private
f : X → X × 𝟙 ℓ₂
f x = (x , unit)
g : X × 𝟙 ℓ₂ → X
g (x , _) = x
H₁ : (f ∘ g) ∼ id
H₁ x = idp
H₂ : (g ∘ f) ∼ id
H₂ x = idp
≃-×-lunit
: ∀ {ℓ₁ ℓ₂ : Level} {X : Type ℓ₁}
→ X ≃ 𝟙 ℓ₂ × X
≃-×-lunit {ℓ₁}{ℓ₂} {X = X} =
X ≃⟨ ≃-×-runit ⟩
X × (𝟙 ℓ₂) ≃⟨ ≃-×-comm ⟩
(𝟙 ℓ₂) × X ≃∎
≃-×-assoc
: ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {X : Type ℓ₁}{Y : Type ℓ₂} {Z : Type ℓ₃}
→ X × (Y × Z) ≃ (X × Y) × Z
≃-×-assoc {X = X}{Y}{Z} = qinv-≃ f (g , (H₁ , H₂))
where
private
f : X × (Y × Z) → (X × Y) × Z
f (x , (y , z)) = ( (x , y) , z)
g : (X × Y) × Z → X × (Y × Z)
g ((x , y) , z) = (x , (y , z))
H₁ : (f ∘ g) ∼ id
H₁ ((x , y) , z) = idp
H₂ : g ∘ f ∼ id
H₂ (x , (y , z)) = idp
≃-×-+-distr
: ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {X : Type ℓ₁}{Y : Type ℓ₂} {Z : Type ℓ₃}
→ (X × (Y + Z)) ≃ ((X × Y) + (X × Z))
≃-×-+-distr {X = X}{Y}{Z} = qinv-≃ f (g , (H₁ , H₂))
where
private
f : (X × (Y + Z)) → ((X × Y) + (X × Z))
f (x , inl y) = inl (x , y)
f (x , inr z) = inr (x , z)
g : ((X × Y) + (X × Z)) → (X × (Y + Z))
g (inl (x , y)) = x , inl y
g (inr (x , z)) = x , inr z
open import foundations.CoproductIdentities
H₁ : (f ∘ g) ∼ id
H₁ (inl x) = ap inl (uppt x )
H₁ (inr x) = ap inr (uppt x)
H₂ : (g ∘ f) ∼ id
H₂ (p , inl x) = pair= (idp , idp)
H₂ (p , inr x) = pair= (idp , idp)
A type and its lifting to some universe are equivalent as types.
lifting-equivalence
: ∀ {ℓ₁ ℓ₂ : Level}
→ (A : Type ℓ₁)
→ A ≃ (↑ ℓ₂ A)
lifting-equivalence {ℓ₁}{ℓ₂} A =
quasiinverse-to-≃ f (g , (λ { (Lift a) → idp}) , λ {p → idp})
where
f : A → ↑ ℓ₂ A
f a = Lift a
g : A ← ↑ ℓ₂ A
g (Lift a) = a
Some synomys:
≃-↑ = lifting-equivalence
move-right-from-composition
: ∀ {ℓ₁ ℓ₂ ℓ₃ : Level}{A : Type ℓ₁}{B : Type ℓ₂}{C : Type ℓ₃}
→ (f : A → B) → (e : B ≃ C) → (g : A → C)
→ f :> (e ∙→) ≡ g
--------------------------------------
→ f ≡ g :> (e ∙←)
move-right-from-composition f e .(λ x → π₁ e (f x)) idp =
begin
f
≡⟨⟩
f :> id
≡⟨ ap (λ w → f :> w) (funext (λ x → ! (rlmap-inverse-h e x))) ⟩
f :> ((e ∙→) :> (e ∙←))
≡⟨ :>-lassoc f (e ∙→) (e ∙←) ⟩
(f :> (e ∙→)) :> (e ∙←)
∎ where open import foundations.FunExtAxiom
move-left-from-composition
: ∀ {ℓ₁ ℓ₂ ℓ₃ : Level}{A : Type ℓ₁}{B : Type ℓ₂}{C : Type ℓ₃}
→ (f : A → B) → (e : B ≃ C) → (g : A → C)
→ f ≡ g :> (e ∙←)
--------------------------------------
→ f :> (e ∙→) ≡ g
move-left-from-composition .(λ x → π₁ (π₁ (π₂ e (g x)))) e g idp
= :>-rassoc g (e ∙←) (e ∙→)
· ap (λ w → g :> w) (funext (λ x → lrmap-inverse-h e x))
where open import foundations.FunExtAxiom
2-out-of-3-property
: ∀ {ℓ₁ ℓ₂ ℓ₃ : Level}{A : Type ℓ₁}{B : Type ℓ₂}{C : Type ℓ₃}
→ (f : A → C) → (e : A ≃ B) → (g : B ≃ C)
→ f ≡ (e ∙→) :> (g ∙→)
-------------------------
→ isEquiv f
2-out-of-3-property .(λ x → π₁ g (π₁ e x)) e g idp = comp-is-equiv
where
comp-is-equiv : isEquiv ((e ∙→) :> (g ∙→))
comp-is-equiv = π₂ (≃-trans e g)
inv-of-equiv-composition
: ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Type ℓ₁}{B : Type ℓ₂}{C : Type ℓ₃}
→ (f : A ≃ B)
→ (g : B ≃ C)
→ remap ((f ∙→) :> (g ∙→) , π₂ (≃-trans f g))
≡ (g ∙←) :> (f ∙←)
inv-of-equiv-composition f g = idp
(2022-12-28)(57c278b4) Last updated: 2021-09-16 15:00:00 by jonathan.cubides (2022-07-06)(d3a4a8cf) minors by jonathan.cubides (2022-01-26)(4aef326b) [ reports ] added some revisions by jonathan.cubides (2021-12-20)(049db6a8) Added code of cubical experiments. by jonathan.cubides (2021-12-20)(961730c9) [ html ] regular update by jonathan.cubides (2021-12-20)(e0ef9faa) Fixed compilation and format, remove hidden parts by jonathan.cubides (2021-12-20)(5120e5d1) Added cubical experiment to the master by jonathan.cubides (2021-12-17)(828fdd0a) More revisions added for CPP by jonathan.cubides (2021-12-15)(0d6a99d8) Fixed some broken links and descriptions by jonathan.cubides (2021-12-15)(662a1f2d) [ .gitignore ] add by jonathan.cubides (2021-12-15)(0630ce66) Minor fixes by jonathan.cubides (2021-12-13)(04f10eba) Fixed a lot of details by jonathan.cubides (2021-12-10)(24195c9f) [ .gitignore ] ignore .zip and arxiv related files by jonathan.cubides (2021-12-09)(538d2859) minor fixes before dinner by jonathan.cubides (2021-12-09)(36a1a69f) [ planar.pdf ] w.i.p revisions to share on arxiv first by jonathan.cubides