foundations.FunExtTransportDependent.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.FunExtTransportDependent where open import foundations.Transport open import foundations.TransportLemmas open import foundations.CoproductIdentities open import foundations.EquivalenceType open import foundations.FunExtAxiom open import foundations.FunExtTransport open import foundations.QuasiinverseLemmas
module
_
{ℓ₁ ℓ₂ : Level}{X : Type ℓ₁} {A : X → Type ℓ₂}{B : (x : X) → A x → Type ℓ₂}{x y : X}
where
funext-transport-dfun
: (p : x ≡ y)
→ (f : (a : A x) → B x a)
→ (g : (a : A y) → B y a)
----------------------------------------------------------------------------
→ (f ≡ g
[ (λ z₁ → (x : A z₁) → B z₁ x) ↓ p ])
≃ ((a : A x) →
(f a) ≡ g (tr A p a)
[ (λ w → B (π₁ w) (π₂ w)) ↓ (pair= (p , refl (tr A p a))) ])
funext-transport-dfun idp f g = eqFunExt
funext-transport-dfun-l
: (p : x ≡ y) → (f : (a : A x) → B x a) → (g : (a : A y) → B y a)
→ (tr (λ z₁ → (x : A z₁) → B z₁ x) p f ≡ g)
---------------------------------------------------------------------------
→ (a : A x) →
(f a) ≡ g (tr A p a)
[ (λ w → B (π₁ w) (π₂ w)) ↓ (pair= (p , refl (tr A p a))) ]
funext-transport-dfun-l p f g = lemap (funext-transport-dfun p _ _)
funext-transport-dfun-r
: (p : x ≡ y)
→ (f : (a : A x) → B x a)
→ (g : (a : A y) → B y a)
→ ((a : A x) → tr (λ w → B (π₁ w) (π₂ w)) (pair= (p , refl (tr A p a))) (f a) ≡ g (tr A p a))
--------------------------------------------------------------------------
→ (tr (λ z₁ → (x : A z₁) → B z₁ x) p f ≡ g)
funext-transport-dfun-r p f g = remap (funext-transport-dfun p _ _)
funext-transport-dfun-bezem
: ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {X : Type ℓ₁}{A : X → Type ℓ₂}{B : (x : X) → A x → Type ℓ₃} {x y : X}
→ (p : x ≡ y)
→ (f : (a : A x) → B x a)
→ (g : (a : A y) → B y a)
→ (a : A y)
------------------------------------------------------------------------------------
→ ((tr (λ x → (a : A x) → B x a) p f) a ≡ g a)
≃ (tr (λ w → B (π₁ w) (π₂ w)) (pair= (p , transport-inv p)) (f (tr A (! p)a)) ≡ g a)
funext-transport-dfun-bezem idp f g a = idEqv
funext-transport-dfun-bezem-l
: ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {X : Type ℓ₁}{A : X → Type ℓ₂}{B : (x : X) → A x → Type ℓ₃} {x y : X}
→ (p : x ≡ y)
→ (f : (a : A x) → B x a)
→ (g : (a : A y) → B y a)
→ (a : A y)
→ (tr (λ x → (a : A x) → B x a) p f) a ≡ g a
------------------------------------------------------------------------------------
→ tr (λ w → B (π₁ w) (π₂ w)) (pair= (p , transport-inv p)) (f (tr A (! p) a)) ≡ g a
funext-transport-dfun-bezem-l p f g a x₁ = lemap (funext-transport-dfun-bezem p f g a) x₁
funext-transport-dfun-bezem-r
: ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {X : Type ℓ₁}{A : X → Type ℓ₂}{B : (x : X) → A x → Type ℓ₃} {x y : X}
→ (p : x ≡ y)
→ (f : (a : A x) → B x a)
→ (g : (a : A y) → B y a)
→ (a : A y)
→ tr (λ w → B (π₁ w) (π₂ w)) (pair= (p , transport-inv p)) (f (tr A (! p) a)) ≡ g a
------------------------------------------------------------------------------------
→ (tr (λ x → (a : A x) → B x a) p f) a ≡ g a
funext-transport-dfun-bezem-r p f g a x₁ = remap (funext-transport-dfun-bezem p f g a) x₁
(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