Investigations on graph-theoretical constructions in Homotopy type theory

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

module lib.graph-definitions.Alternative-definition-is-equiv
  where

  open import foundations.Core

  Def₁ : (ℓ : Level) → Type (lsuc ℓ)
  Def₁ ℓ = ∑[ N ∶ Type ℓ ] ∑[ E ∶ (N → N → Type ℓ)]
           (N is-set) × ((x y : N) → (E x y) is-set)

  Def₂ : (ℓ : Level) → Type (lsuc ℓ)
  Def₂ ℓ = ∑[ N ∶ Type ℓ ] ∑[ E ∶ Type ℓ ]
           ∑[ sc ∶ (E → N) ] ∑[ tg ∶ (E → N) ] (N is-set) × (E is-set)

Remark. The definitions above are for demostrative purposes. First they are not general concerning the universes level where they lie on. Such levels can be different. Note also that the last two ∑-types used in the second definition are not needed.

  variable
    ℓ : Level

  Def₁≃Def₂ : Def₁ ℓ ≃ Def₂ ℓ
  Def₁≃Def₂ = qinv-≃ f (g , H₁ , H₂)
    where
    f : Def₁ ℓ → Def₂ ℓ
    f (N , E , Node-is-set , Edge-is-set)
      = N
        , (∑[ x ] ∑[ y ] (E x y))
        , π₁ , π₁ ∘ π₂
        , Node-is-set
        , ∑-set Node-is-set (λ x → ∑-set Node-is-set (λ y → Edge-is-set x y))

    g : Def₂ ℓ → Def₁ ℓ
    g (N , E , sc , tg , N-is-set ,  E-is-set)
      = N
        , (λ x y → ∑[ e ∶ E ] ((sc e ≡ x) × (tg e ≡ y)))
        , N-is-set
        , λ x y → ∑-set E-is-set (λ _ → prop-is-set
          (∑-prop (N-is-set _ _) (λ _ → N-is-set _ _)))

    open import foundations.UnivalenceAxiom
    open import foundations.UnivalenceTransport
    open import foundations.FunExtAxiom

    H₁ : (G : Def₂ ℓ) → f (g G) ≡ G
    H₁ t@(N , E , sc , tg , N-is-set ,  E-is-set)
      = pair=  (idp , pair= (ua (∑∑∑-st≡×tg≡-≃-E N E sc tg) , helper₂))
      where
      ∑∑∑-st≡×tg≡-≃-E
        : (N : Type ℓ) → (E : Type ℓ) → (sc tg : E → N)
        → (∑[ x ] ∑[ y ] ∑[ e ∶ E ] ((sc e ≡ x) × (tg e ≡ y))) ≃ E
      ∑∑∑-st≡×tg≡-≃-E N E sc tg =
            qinv-≃ (λ {(x , y , e , t1 , t2) → e})
                  (( λ {e → (sc e , tg e , e , idp , idp)})
                  , (λ {_ → idp})
                  , λ {(x , y , e , idp , idp) → idp})

      p = ∑∑∑-st≡×tg≡-≃-E N E sc tg

      F₁ : Type ℓ → Type _
      F₁ E' = ∑[ sc ∶ (E' → N) ] ∑[ tg ∶ (E' → N) ] (N is-set) × (E' is-set)

      F₂ : Type ℓ → Type (lsuc ℓ)
      F₂ N' = ∑[ E' ] ∑[ sc' ∶ (E' → N') ] ∑[ tg' ∶ (E' → N') ] (N' is-set) × (E' is-set)

      helper₂ : tr F₁ (ua p) (π₁ , π₁ ∘ π₂ , _ , _) ≡ (sc , tg , _ , _)
      helper₂ = ↓-Σ-in {p = ua p} sc-e
        (↓-Σ-in {p = pair= (ua p , sc-e)} tg-e
        (∑-prop set-is-prop (λ _ → set-is-prop) _ _))
        where
        sc-e : tr (λ z → z → N) (ua p) π₁ ≡ sc
        sc-e = funext λ e →
          begin
              tr (λ z → z → N) (ua p) π₁ e
                 ≡⟨ transport-fun-h {A = λ X → X}{B = λ _ → N} (ua p) π₁ e ⟩
              tr (λ _ → N) (ua p) (π₁ (tr (λ X → X) (! ua p) e))
                 ≡⟨ transport-const (ua p) _ ⟩
              π₁ (tr (λ X → X) (! ua p) e)
                 ≡⟨⟩
              π₁ (coe (! ua p) e)
                 ≡⟨ ap π₁ (coe-!-ua p e) ⟩
              π₁ (rapply p e)
                 ≡⟨⟩
              sc e ∎


        tg-e : PathOver (λ v → π₁ v → N) (π₁ ∘ π₂) (pair= (ua p , sc-e)) tg
        tg-e =  funext λ e →
          begin
            tr (λ v → π₁ v → N) (pair= (ua p , sc-e)) (π₁ ∘ π₂) e
              ≡⟨ transport-fun-h {A = λ X → π₁ X}{B = λ _ → N}
                                 ((pair= (ua p , sc-e))) (π₁ ∘ π₂) e ⟩
            tr (λ _ → N) (pair= (ua p , sc-e)) ((π₁ ∘ π₂) (tr (λ X → π₁ X)
                         (! ((pair= (ua p , sc-e)))) e))
              ≡⟨ transport-const ((pair= (ua p , sc-e))) _ ⟩
            (π₁ ∘ π₂) (tr (λ X → π₁ X) (! ((pair= (ua p , sc-e)))) e)
              ≡⟨ ap (π₁ ∘ π₂) (transport-family-ap π₁ (! (pair= (ua p , sc-e))) e) ⟩
            (π₁ ∘ π₂) (tr (λ X → X) (ap π₁ (! (pair= (ua p , sc-e)))) e)
              ≡⟨ ap (λ o → (π₁ ∘ π₂) (tr (λ X → X) o e)) (ap-π₁-!pair= (ua p) sc-e) ⟩
            (π₁ ∘ π₂) (tr (λ X → X) (! (ua p)) e)
              ≡⟨ ap (π₁ ∘ π₂) (coe-!-ua p e) ⟩
            (π₁ ∘ π₂) (rapply p e)
              ≡⟨⟩
            tg e
            ∎


    ∑∑∑E≃E'
      : (N : Type ℓ) → (E : N → N → Type ℓ) → ∀ x y
      → (∑[ e ∶ (∑[ x₁ ] ∑[ y₁ ] E x₁ y₁) ] ∑[ p ∶ (π₁ e ≡ x) ] (π₁ (π₂ e) ≡ y)) ≃ E x y
    ∑∑∑E≃E' N E x y
        = qinv-≃ (λ { ((_ , _ , e) , idp , idp)  → e})
                (( λ{ e → (((_ , _ , e)) , idp , idp)})
                , (λ {_ → idp})
                , λ {((_ , _ , _) , idp , idp) → idp})

    H₂ : g ∘ f ∼ id
    H₂ (N , E , N-is-set , E-is-set)
      = pair= (idp
      , pair= (funext (λ x → funext (λ y → ua (∑∑∑E≃E' N E x y )))
      , pair= (set-is-prop _ N-is-set
      , funext (λ x → funext (λ y → set-is-prop _ (E-is-set _ _))))))

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