Investigations on graph-theoretical constructions in Homotopy type theory

{-# OPTIONS --without-K --exact-split #-}

module foundations.FunExtTransport where
open import foundations.Transport
open import foundations.EquivalenceType
open import foundations.FunExtAxiom

module
  _ {ℓ₁ ℓ₂ : Level}{X : Type ℓ₁} {A B : X → Type ℓ₂} {x y : X}
  where

  funext-transport
    : (p : x ≡ y) → (f : A x → B x) → (g : A y → B y)
    ------------------------------------------------------------
    → (tr (λ z₁ → (x : A z₁) → B z₁) p f ≡ g)
    ≃ ((a : A(x)) → tr B p (f a) ≡ g (tr A p a))

  funext-transport idp f g = eqFunExt

  funext-transport-l
    : (p : x ≡ y)
    → (f : A x → B x)
    → (g : A y → B y)
    → ((tr (λ z₁ → (x : A z₁) → B z₁) p f ≡ g)
    -------------------------------------------
    → ((a : A(x)) → tr B p (f a) ≡ g (tr A p a)))

  funext-transport-l p f g = lemap (funext-transport p _ _)

  funext-transport-r
    : (p : x ≡ y)
    → (f : A x → B x)
    → (g : A y → B y)
    → ((a : A(x)) → tr B p (f a) ≡ g (tr A p a))
    -------------------------------------------
    → (tr (λ z₁ → (x : A z₁) → B z₁) p f ≡ g)

  funext-transport-r p f g = remap (funext-transport p _ _)

Latest changes

(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