-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
φ : nerveFunctor₂.obj (Cat.of C) ⟶ nerveFunctor₂.obj (Cat.of D)
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
obtain :
  ∀ (h : (edgeMk f).CompStruct (edgeMk g) (edgeMk (f ≫ g))),
    Eq (α :=
      Quiver.Hom (V := D)
        ((nerveEquiv : (a : ComposableArrows D 0) → D)
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (φ.app
                      (op
                        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                          _root_._proof_1))) :
                  (a :
                      (fun (X : Type u) ↦ X)
                        ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                    (fun (X : Type u) ↦ X)
                      ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
                ((Equiv.symm nerveEquiv : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) X :
                  ComposableArrows (↑(Cat.of C) : Type u) 0) :
              (fun (X : Type u) ↦ X)
                ((nerveFunctor₂.obj (Cat.of D)).obj
                  (op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      _root_._proof_1)))) :
          D)
        ((nerveEquiv : (a : ComposableArrows D 0) → D)
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (φ.app
                      (op
                        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                          _root_._proof_1))) :
                  (a :
                      (fun (X : Type u) ↦ X)
                        ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                    (fun (X : Type u) ↦ X)
                      ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
                ((Equiv.symm nerveEquiv : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) Z :
                  ComposableArrows (↑(Cat.of C) : Type u) 0) :
              (fun (X : Type u) ↦ X)
                ((nerveFunctor₂.obj (Cat.of D)).obj
                  (op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      _root_._proof_1)))) :
          D))
      ((homEquiv :
            (a :
                SSet.Edge
                  ((ConcreteCategory.hom (φ.app (op { obj := ⦋0⦌, property := _root_._proof_1 })) :
                      (a :
                          (fun (X : Type u) ↦ X)
                            ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                        (fun (X : Type u) ↦ X)
                          ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
                    ((nerveEquiv.symm : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) X))
                  ((ConcreteCategory.hom (φ.app (op { obj := ⦋0⦌, property := _root_._proof_1 })) :
                      (a :
                          (fun (X : Type u) ↦ X)
                            ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                        (fun (X : Type u) ↦ X)
                          ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
                    ((nerveEquiv.symm : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) Z))) →
              (nerveEquiv : (a : ComposableArrows D 0) → D)
                  ((ConcreteCategory.hom (φ.app (op { obj := ⦋0⦌, property := _root_._proof_1 })) :
                      (a :
                          (fun (X : Type u) ↦ X)
                            ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                        (fun (X : Type u) ↦ X)
                          ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
                    ((nerveEquiv.symm : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) X)) ⟶
                (nerveEquiv : (a : ComposableArrows D 0) → D)
                  ((ConcreteCategory.hom (φ.app (op { obj := ⦋0⦌, property := _root_._proof_1 })) :
                      (a :
                          (fun (X : Type u) ↦ X)
                            ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                        (fun (X : Type u) ↦ X)
                          ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
                    ((nerveEquiv.symm : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) Z)))
          ((edgeMk (f ≫ g)).toTruncated.map φ) :
        Quiver.Hom (V := D)
          ((nerveEquiv : (a : ComposableArrows D 0) → D)
              ((ConcreteCategory.hom (FC := TypeCat.Fun)
                      (φ.app
                        (op
                          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                            _root_._proof_1))) :
                    (a :
                        (fun (X : Type u) ↦ X)
                          ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                      (fun (X : Type u) ↦ X)
                        ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
                  ((Equiv.symm nerveEquiv : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0)
                      X :
                    ComposableArrows (↑(Cat.of C) : Type u) 0) :
                (fun (X : Type u) ↦ X)
                  ((nerveFunctor₂.obj (Cat.of D)).obj
                    (op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        _root_._proof_1)))) :
            D)
          ((nerveEquiv : (a : ComposableArrows D 0) → D)
              ((ConcreteCategory.hom (FC := TypeCat.Fun)
                      (φ.app
                        (op
                          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                            _root_._proof_1))) :
                    (a :
                        (fun (X : Type u) ↦ X)
                          ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                      (fun (X : Type u) ↦ X)
                        ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
                  ((Equiv.symm nerveEquiv : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0)
                      Z :
                    ComposableArrows (↑(Cat.of C) : Type u) 0) :
                (fun (X : Type u) ↦ X)
                  ((nerveFunctor₂.obj (Cat.of D)).obj
                    (op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        _root_._proof_1)))) :
            D))
      (CategoryStruct.comp (Y :=
          (nerveEquiv : (a : ComposableArrows D 0) → D)
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (φ.app
                      (op
                        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                          _root_._proof_1))) :
                  (a :
                      (fun (X : Type u) ↦ X)
                        ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                    (fun (X : Type u) ↦ X)
                      ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
                ((Equiv.symm nerveEquiv : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) Y :
                  ComposableArrows (↑(Cat.of C) : Type u) 0) :
              (fun (X : Type u) ↦ X)
                ((nerveFunctor₂.obj (Cat.of D)).obj
                  (op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      _root_._proof_1)))))
          ((homEquiv :
              (a :
                  SSet.Edge
                    ((ConcreteCategory.hom (φ.app (op { obj := ⦋0⦌, property := _root_._proof_1 })) :
                        (a :
                            (fun (X : Type u) ↦ X)
                              ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                          (fun (X : Type u) ↦ X)
                            ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
                      ((nerveEquiv.symm : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) X))
                    ((ConcreteCategory.hom (φ.app (op { obj := ⦋0⦌, property := _root_._proof_1 })) :
                        (a :
                            (fun (X : Type u) ↦ X)
                              ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                          (fun (X : Type u) ↦ X)
                            ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
                      ((nerveEquiv.symm : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0)
                        Y))) →
                (nerveEquiv : (a : ComposableArrows D 0) → D)
                    ((ConcreteCategory.hom (φ.app (op { obj := ⦋0⦌, property := _root_._proof_1 })) :
                        (a :
                            (fun (X : Type u) ↦ X)
                              ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                          (fun (X : Type u) ↦ X)
                            ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
                      ((nerveEquiv.symm : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0)
                        X)) ⟶
                  (nerveEquiv : (a : ComposableArrows D 0) → D)
                    ((ConcreteCategory.hom (φ.app (op { obj := ⦋0⦌, property := _root_._proof_1 })) :
                        (a :
                            (fun (X : Type u) ↦ X)
                              ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                          (fun (X : Type u) ↦ X)
                            ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
                      ((nerveEquiv.symm : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) Y)))
            ((edgeMk f).toTruncated.map φ))
          ((homEquiv :
              (a :
                  SSet.Edge
                    ((ConcreteCategory.hom (φ.app (op { obj := ⦋0⦌, property := _root_._proof_1 })) :
                        (a :
                            (fun (X : Type u) ↦ X)
                              ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                          (fun (X : Type u) ↦ X)
                            ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
                      ((nerveEquiv.symm : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) Y))
                    ((ConcreteCategory.hom (φ.app (op { obj := ⦋0⦌, property := _root_._proof_1 })) :
                        (a :
                            (fun (X : Type u) ↦ X)
                              ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                          (fun (X : Type u) ↦ X)
                            ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
                      ((nerveEquiv.symm : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0)
                        Z))) →
                (nerveEquiv : (a : ComposableArrows D 0) → D)
                    ((ConcreteCategory.hom (φ.app (op { obj := ⦋0⦌, property := _root_._proof_1 })) :
                        (a :
                            (fun (X : Type u) ↦ X)
                              ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                          (fun (X : Type u) ↦ X)
                            ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
                      ((nerveEquiv.symm : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0)
                        Y)) ⟶
                  (nerveEquiv : (a : ComposableArrows D 0) → D)
                    ((ConcreteCategory.hom (φ.app (op { obj := ⦋0⦌, property := _root_._proof_1 })) :
                        (a :
                            (fun (X : Type u) ↦ X)
                              ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                          (fun (X : Type u) ↦ X)
                            ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
                      ((nerveEquiv.symm : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) Z)))
            ((edgeMk g).toTruncated.map φ)) :
        Quiver.Hom (V := D)
          ((nerveEquiv : (a : ComposableArrows D 0) → D)
              ((ConcreteCategory.hom (FC := TypeCat.Fun)
                      (φ.app
                        (op
                          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                            _root_._proof_1))) :
                    (a :
                        (fun (X : Type u) ↦ X)
                          ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                      (fun (X : Type u) ↦ X)
                        ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
                  ((Equiv.symm nerveEquiv : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0)
                      X :
                    ComposableArrows (↑(Cat.of C) : Type u) 0) :
                (fun (X : Type u) ↦ X)
                  ((nerveFunctor₂.obj (Cat.of D)).obj
                    (op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        _root_._proof_1)))) :
            D)
          ((nerveEquiv : (a : ComposableArrows D 0) → D)
              ((ConcreteCategory.hom (FC := TypeCat.Fun)
                      (φ.app
                        (op
                          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                            _root_._proof_1))) :
                    (a :
                        (fun (X : Type u) ↦ X)
                          ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                      (fun (X : Type u) ↦ X)
                        ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
                  ((Equiv.symm nerveEquiv : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0)
                      Z :
                    ComposableArrows (↑(Cat.of C) : Type u) 0) :
                (fun (X : Type u) ↦ X)
                  ((nerveFunctor₂.obj (Cat.of D)).obj
                    (op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        _root_._proof_1)))) :
            D))
⊢ Eq (α :=
    Quiver.Hom (V := D)
      ((nerveEquiv : (a : ComposableArrows D 0) → D)
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (φ.app
                    (op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        _root_._proof_1))) :
                (a :
                    (fun (X : Type u) ↦ X)
                      ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                  (fun (X : Type u) ↦ X)
                    ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
              ((Equiv.symm nerveEquiv : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) X :
                ComposableArrows (↑(Cat.of C) : Type u) 0) :
            (fun (X : Type u) ↦ X)
              ((nerveFunctor₂.obj (Cat.of D)).obj
                (op
                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                    _root_._proof_1)))) :
        D)
      ((nerveEquiv : (a : ComposableArrows D 0) → D)
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (φ.app
                    (op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        _root_._proof_1))) :
                (a :
                    (fun (X : Type u) ↦ X)
                      ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                  (fun (X : Type u) ↦ X)
                    ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
              ((Equiv.symm nerveEquiv : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) Z :
                ComposableArrows (↑(Cat.of C) : Type u) 0) :
            (fun (X : Type u) ↦ X)
              ((nerveFunctor₂.obj (Cat.of D)).obj
                (op
                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                    _root_._proof_1)))) :
        D))
    ((homEquiv :
          (a :
              SSet.Edge
                ((ConcreteCategory.hom (φ.app (op { obj := ⦋0⦌, property := _root_._proof_1 })) :
                    (a :
                        (fun (X : Type u) ↦ X)
                          ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                      (fun (X : Type u) ↦ X)
                        ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
                  ((nerveEquiv.symm : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) X))
                ((ConcreteCategory.hom (φ.app (op { obj := ⦋0⦌, property := _root_._proof_1 })) :
                    (a :
                        (fun (X : Type u) ↦ X)
                          ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                      (fun (X : Type u) ↦ X)
                        ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
                  ((nerveEquiv.symm : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) Z))) →
            (nerveEquiv : (a : ComposableArrows D 0) → D)
                ((ConcreteCategory.hom (φ.app (op { obj := ⦋0⦌, property := _root_._proof_1 })) :
                    (a :
                        (fun (X : Type u) ↦ X)
                          ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                      (fun (X : Type u) ↦ X)
                        ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
                  ((nerveEquiv.symm : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) X)) ⟶
              (nerveEquiv : (a : ComposableArrows D 0) → D)
                ((ConcreteCategory.hom (φ.app (op { obj := ⦋0⦌, property := _root_._proof_1 })) :
                    (a :
                        (fun (X : Type u) ↦ X)
                          ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                      (fun (X : Type u) ↦ X)
                        ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
                  ((nerveEquiv.symm : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) Z)))
        ((edgeMk (f ≫ g)).toTruncated.map φ) :
      Quiver.Hom (V := D)
        ((nerveEquiv : (a : ComposableArrows D 0) → D)
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (φ.app
                      (op
                        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                          _root_._proof_1))) :
                  (a :
                      (fun (X : Type u) ↦ X)
                        ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                    (fun (X : Type u) ↦ X)
                      ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
                ((Equiv.symm nerveEquiv : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) X :
                  ComposableArrows (↑(Cat.of C) : Type u) 0) :
              (fun (X : Type u) ↦ X)
                ((nerveFunctor₂.obj (Cat.of D)).obj
                  (op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      _root_._proof_1)))) :
          D)
        ((nerveEquiv : (a : ComposableArrows D 0) → D)
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (φ.app
                      (op
                        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                          _root_._proof_1))) :
                  (a :
                      (fun (X : Type u) ↦ X)
                        ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                    (fun (X : Type u) ↦ X)
                      ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
                ((Equiv.symm nerveEquiv : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) Z :
                  ComposableArrows (↑(Cat.of C) : Type u) 0) :
              (fun (X : Type u) ↦ X)
                ((nerveFunctor₂.obj (Cat.of D)).obj
                  (op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      _root_._proof_1)))) :
          D))
    (CategoryStruct.comp (Y :=
        (nerveEquiv : (a : ComposableArrows D 0) → D)
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (φ.app
                    (op
                      (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                        _root_._proof_1))) :
                (a :
                    (fun (X : Type u) ↦ X)
                      ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                  (fun (X : Type u) ↦ X)
                    ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
              ((Equiv.symm nerveEquiv : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) Y :
                ComposableArrows (↑(Cat.of C) : Type u) 0) :
            (fun (X : Type u) ↦ X)
              ((nerveFunctor₂.obj (Cat.of D)).obj
                (op
                  (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                    _root_._proof_1)))))
        ((homEquiv :
            (a :
                SSet.Edge
                  ((ConcreteCategory.hom (φ.app (op { obj := ⦋0⦌, property := _root_._proof_1 })) :
                      (a :
                          (fun (X : Type u) ↦ X)
                            ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                        (fun (X : Type u) ↦ X)
                          ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
                    ((nerveEquiv.symm : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) X))
                  ((ConcreteCategory.hom (φ.app (op { obj := ⦋0⦌, property := _root_._proof_1 })) :
                      (a :
                          (fun (X : Type u) ↦ X)
                            ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                        (fun (X : Type u) ↦ X)
                          ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
                    ((nerveEquiv.symm : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) Y))) →
              (nerveEquiv : (a : ComposableArrows D 0) → D)
                  ((ConcreteCategory.hom (φ.app (op { obj := ⦋0⦌, property := _root_._proof_1 })) :
                      (a :
                          (fun (X : Type u) ↦ X)
                            ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                        (fun (X : Type u) ↦ X)
                          ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
                    ((nerveEquiv.symm : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) X)) ⟶
                (nerveEquiv : (a : ComposableArrows D 0) → D)
                  ((ConcreteCategory.hom (φ.app (op { obj := ⦋0⦌, property := _root_._proof_1 })) :
                      (a :
                          (fun (X : Type u) ↦ X)
                            ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                        (fun (X : Type u) ↦ X)
                          ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
                    ((nerveEquiv.symm : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) Y)))
          ((edgeMk f).toTruncated.map φ))
        ((homEquiv :
            (a :
                SSet.Edge
                  ((ConcreteCategory.hom (φ.app (op { obj := ⦋0⦌, property := _root_._proof_1 })) :
                      (a :
                          (fun (X : Type u) ↦ X)
                            ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                        (fun (X : Type u) ↦ X)
                          ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
                    ((nerveEquiv.symm : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) Y))
                  ((ConcreteCategory.hom (φ.app (op { obj := ⦋0⦌, property := _root_._proof_1 })) :
                      (a :
                          (fun (X : Type u) ↦ X)
                            ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                        (fun (X : Type u) ↦ X)
                          ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
                    ((nerveEquiv.symm : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) Z))) →
              (nerveEquiv : (a : ComposableArrows D 0) → D)
                  ((ConcreteCategory.hom (φ.app (op { obj := ⦋0⦌, property := _root_._proof_1 })) :
                      (a :
                          (fun (X : Type u) ↦ X)
                            ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                        (fun (X : Type u) ↦ X)
                          ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
                    ((nerveEquiv.symm : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) Y)) ⟶
                (nerveEquiv : (a : ComposableArrows D 0) → D)
                  ((ConcreteCategory.hom (φ.app (op { obj := ⦋0⦌, property := _root_._proof_1 })) :
                      (a :
                          (fun (X : Type u) ↦ X)
                            ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                        (fun (X : Type u) ↦ X)
                          ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
                    ((nerveEquiv.symm : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) Z)))
          ((edgeMk g).toTruncated.map φ)) :
      Quiver.Hom (V := D)
        ((nerveEquiv : (a : ComposableArrows D 0) → D)
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (φ.app
                      (op
                        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                          _root_._proof_1))) :
                  (a :
                      (fun (X : Type u) ↦ X)
                        ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                    (fun (X : Type u) ↦ X)
                      ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
                ((Equiv.symm nerveEquiv : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) X :
                  ComposableArrows (↑(Cat.of C) : Type u) 0) :
              (fun (X : Type u) ↦ X)
                ((nerveFunctor₂.obj (Cat.of D)).obj
                  (op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      _root_._proof_1)))) :
          D)
        ((nerveEquiv : (a : ComposableArrows D 0) → D)
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (φ.app
                      (op
                        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                          _root_._proof_1))) :
                  (a :
                      (fun (X : Type u) ↦ X)
                        ((nerveFunctor₂.obj (Cat.of C)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 }))) →
                    (fun (X : Type u) ↦ X)
                      ((nerveFunctor₂.obj (Cat.of D)).obj (op { obj := ⦋0⦌, property := _root_._proof_1 })))
                ((Equiv.symm nerveEquiv : (a : (↑(Cat.of C) : Type u)) → ComposableArrows (↑(Cat.of C) : Type u) 0) Z :
                  ComposableArrows (↑(Cat.of C) : Type u) 0) :
              (fun (X : Type u) ↦ X)
                ((nerveFunctor₂.obj (Cat.of D)).obj
                  (op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                      _root_._proof_1)))) :
          D))

Tactic:
obtain ⟨h⟩ := (nerve.nonempty_compStruct_iff f g (f ≫ g)).2 rfl

Premises used: Iff.mpr, CategoryTheory.nerve.nonempty_compStruct_iff, CategoryTheory.CategoryStruct.comp, rfl