Investigations on graph-theoretical constructions in Homotopy type theory

paso-a
  : (Path {A = ∑[ H ∶ Graph ℓ ] ∑[ h ∶ Hom H G ] isEdgeInj h}
       (A , (f , f-fact))
       (B , (g , g-fact)))
  ≃ (∑[ α ∶ A ≡ B ]
             (tr (λ H → ∑[ h ∶ Hom H G ] isEdgeInj h)
             α
             (f , f-fact)) ≡ g , g-fact)

paso-a = ≃-sym $ pair=Equiv (Graph ℓ) λ H → ∑[ h ∶ Hom H G ] isEdgeInj h

paso-d
  : (α : A ≡ B)
  → (∑[ p ∶ tr (λ H → Hom H G) α f ≡ g ]
             (Path {A = isEdgeInj g}
               (tr (λ h → isEdgeInj h) p
               (tr (λ p → isEdgeInj (π₂ p))
               (pair= ((α , refl (tr (λ X → Hom X G) α f)))) f-fact))
             g-fact))
  ≃ (tr (λ H → Hom H G) α f ≡ g)

paso-d idp = ∑-≃-base λ {idp →
       (being-edge-inj-is-prop g _ g-fact ,
           prop-is-set (being-edge-inj-is-prop g) _ g-fact
           (being-edge-inj-is-prop g _ g-fact))}


module _ (α : A ≡ B) where

  open Hom-Lemma-1 A B
  open Hom-Lemma-2 A B G f g

  cal :
      (Path {A = ∑[ H ∶ Graph ℓ ] ∑[ h ∶ Hom H G ] isEdgeInj h}
               (A , f , f-fact)
               (B , g , g-fact))
         ≃ (∑[ α ∶ A ≡ B ]
         (∑[ p ∶ Hom.α f ≡ Hom.α (g∘ α) ]
         (tr (λ e → (x y : Node A)
           → Edge A x y → Edge G (e x) (e y)) p
         (Hom.β f) ≡ Hom.β (g∘ α))))
  cal =
    begin≃
           (Path {A = ∑[ H ∶ Graph ℓ ] ∑[ h ∶ Hom H G ] isEdgeInj h}
               (A , (f , f-fact))
               (B , (g , g-fact)))
           ≃⟨ paso-a ⟩

           ((∑[ α ∶ A ≡ B ]
                (tr (λ H → ∑[ h ∶ Hom H G ] isEdgeInj h)
                α
                (f , f-fact)) ≡ g , g-fact))
           {-
             The following steps can be skiped until next comment.
           -}
             ≃⟨ sigma-preserves (λ {idp → idtoeqv idp }) ⟩
           (∑[ α ∶ A ≡ B ]
             (Path {A = ∑[ h ∶ Hom B G ] (isEdgeInj h)}
               (tr (λ H → Hom H G) α f , tr (λ p → isEdgeInj (π₂ p) )
               (pair= ((α , refl (tr (λ X → Hom X G) α f)))) f-fact)
             (g , g-fact)))
             ≃⟨ sigma-preserves (λ { idp → pair-≃-∑}) ⟩
           (∑[ α ∶ A ≡ B ] (∑[ p ∶ tr (λ H → Hom H G) α f ≡ g ]
               (Path {A = isEdgeInj g}
                     (tr (λ h → isEdgeInj h) p
                     (tr (λ p → isEdgeInj (π₂ p))
                       (pair= ((α , refl (tr (λ X → Hom X G) α f))))
                         f-fact))
                       g-fact)))
             ≃⟨ sigma-preserves paso-d ⟩
           (∑[ α ∶ A ≡ B ] ((tr (λ H → Hom H G) α f ≡ g)))

             ≃⟨ sigma-preserves (λ {idp → idEqv}) ⟩
           (∑[ α ∶ A ≡ B ] (f ≡ g∘ α) )
           {-
             From here, we must remember α is an equality between two graphs,
             and we have also an equality between two graph-morphisms.
             Now, in order to use the fiberwise equivalence, we need to
             unfold the base type A ≡ B.
           -}
               ≃⟨ sigma-preserves (λ α → Hom-Lemma-1.≡-of-homs-≃-≡-∑ A G f (g∘ α)) ⟩
           (∑[ α ∶ A ≡ B ]
             (∑[ p ∶ Hom.α f ≡ Hom.α (g∘ α) ]
               (tr (λ e → (x y : Node A)
               → Edge A x y
               → Edge G (e x) (e y)) p
               (Hom.β f) ≡ Hom.β (g∘ α))))
          ≃∎ where open import foundations.UnivalenceAxiom