Investigations on graph-theoretical constructions in Homotopy type theory

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

module foundations.DependentAlgebra where

open import foundations.BasicTypes
open import foundations.BasicFunctions

open import foundations.EquivalenceType
open import foundations.QuasiinverseType

∑-comm
  : ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Type ℓ₁}
  → (B : A → Type ℓ₂) (C : A → Type ℓ₃)
    -----------------------------------------
  → Σ (Σ A B) (C ∘ fst) ≃ Σ (Σ A C) (B ∘ fst)

∑-comm {A = A} B C = qinv-≃ there (back , there-back , back-there)
  where
  there : Σ (Σ A B) (C ∘ fst) → Σ (Σ A C) (B ∘ fst)
  there ((a , b) , c) = ((a , c ) , b)

  back : Σ (Σ A C) (B ∘ fst) → Σ (Σ A B) (C ∘ fst)
  back  ((a , c ) , b) = ((a , b) , c)

  there-back : ∀ acb → there (back acb) ≡ acb
  there-back ((a , c) , b) = idp

  back-there : ∀ abc → back (there abc) ≡ abc
  back-there ((a , b) , c) = idp

sum-commute = ∑-comm

∏-comm
  : ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Type ℓ₁}
  → (B : A → Type ℓ₂)
  → (C : {a : A} → B a → Type ℓ₃)
  -----------------------------------------------------------
  → (Σ[ f ∶ Π A B ] Π[ x ∶ A ] (C (f x))) ≃ (Π[ x ∶ A ] Σ[ y ∶ B x ] C y)

∏-comm {A = A} B C = qinv-≃ there (back , there-back , back-there)
  where
  there : (Σ (Π A B) (\f → Π A (C ∘ f))) → (Π A (\x → Σ (B x) C))
  there (f , s) x = (f x , s x)

  back : (Π A (\x → Σ (B x) C)) → (Σ (Π A B) (\f → Π A (C ∘ f)))
  back  F = (\x → fst (F x)) , (\x → snd (F x))

  there-back : ∀ F → there (back F) ≡ F
  there-back F = idp

  back-there : ∀ fs → back (there fs) ≡ fs
  back-there fs = idp

:

prod-commute = ∏-comm

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