Investigations on graph-theoretical constructions in Homotopy type theory

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

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

module
  _
  {ℓ₁ ℓ₂ : Level}
  {A : Type ℓ₁} {B : A → Type ℓ₂}
  {f g : (a : A) → B a}
  where

Application of an homotopy

  happly
    : f ≡ g
    ------------------------
    → ((x : A) → f x ≡ g x)

  happly idp x = refl (f x)
  ≡-app = happly

  postulate axiomFunExt : isEquiv happly

  eqFunExt : (f ≡ g) ≃ ((x : A) → f x ≡ g x)
  eqFunExt = happly , axiomFunExt

From this, the usual notion of function extensionality follows.

  funext
    : ((x : A) → f x ≡ g x)
    ------------------------
    → f ≡ g

  funext = remap eqFunExt

Beta and eta rules for function extensionality

  funext-β
    : (h : ((x : A) → f x ≡ g x))
    ------------------------------
    → happly (funext h) ≡ h

  funext-β h = lrmap-inverse eqFunExt

  funext-η
    : (p : f ≡ g)
    ------------------------
    → funext (happly p) ≡ p

  funext-η p = rlmap-inverse eqFunExt

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