[GOAL]
V : QuivCat
⊢ { obj := fun V => of (Paths ↑V),
          map := fun {X Y} F =>
            Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
      (𝟙 V) =
    𝟙
      ({ obj := fun V => of (Paths ↑V),
            map := fun {X Y} F =>
              Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.obj
        V)
[PROOFSTEP]
change (show Paths V ⥤ _ from _) = _
[GOAL]
V : QuivCat
⊢ (let_fun this :=
      { obj := fun V => of (Paths ↑V),
            map := fun {X Y} F =>
              Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
        (𝟙 V);
    this) =
    𝟙
      ({ obj := fun V => of (Paths ↑V),
            map := fun {X Y} F =>
              Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.obj
        V)
[PROOFSTEP]
ext
[GOAL]
case h_obj.h
V : QuivCat
x✝ : Paths ↑V
⊢ (let_fun this :=
          { obj := fun V => of (Paths ↑V),
                map := fun {X Y} F =>
                  Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
            (𝟙 V);
        this).obj
      x✝ =
    (𝟙
          ({ obj := fun V => of (Paths ↑V),
                map := fun {X Y} F =>
                  Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.obj
            V)).obj
      x✝
case h
V : QuivCat
a✝ b✝ : ↑V
e✝ : a✝ ⟶ b✝
⊢ (let_fun this :=
          { obj := fun V => of (Paths ↑V),
                map := fun {X Y} F =>
                  Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
            (𝟙 V);
        this).map
      (Quiver.Hom.toPath e✝) =
    eqToHom
        (_ :
          (let_fun this :=
                  { obj := fun V => of (Paths ↑V),
                        map := fun {X Y} F =>
                          Functor.mk
                            { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
                    (𝟙 V);
                this).obj
              a✝ =
            (𝟙
                  ({ obj := fun V => of (Paths ↑V),
                        map := fun {X Y} F =>
                          Functor.mk
                            { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.obj
                    V)).obj
              a✝) ≫
      (𝟙
              ({ obj := fun V => of (Paths ↑V),
                    map := fun {X Y} F =>
                      Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.obj
                V)).map
          (Quiver.Hom.toPath e✝) ≫
        eqToHom
          (_ :
            (𝟙
                    ({ obj := fun V => of (Paths ↑V),
                          map := fun {X Y} F =>
                            Functor.mk
                              { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.obj
                      V)).obj
                b✝ =
              (let_fun this :=
                    { obj := fun V => of (Paths ↑V),
                          map := fun {X Y} F =>
                            Functor.mk
                              { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
                      (𝟙 V);
                  this).obj
                b✝)
[PROOFSTEP]
swap
[GOAL]
case h
V : QuivCat
a✝ b✝ : ↑V
e✝ : a✝ ⟶ b✝
⊢ (let_fun this :=
          { obj := fun V => of (Paths ↑V),
                map := fun {X Y} F =>
                  Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
            (𝟙 V);
        this).map
      (Quiver.Hom.toPath e✝) =
    eqToHom
        (_ :
          (let_fun this :=
                  { obj := fun V => of (Paths ↑V),
                        map := fun {X Y} F =>
                          Functor.mk
                            { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
                    (𝟙 V);
                this).obj
              a✝ =
            (𝟙
                  ({ obj := fun V => of (Paths ↑V),
                        map := fun {X Y} F =>
                          Functor.mk
                            { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.obj
                    V)).obj
              a✝) ≫
      (𝟙
              ({ obj := fun V => of (Paths ↑V),
                    map := fun {X Y} F =>
                      Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.obj
                V)).map
          (Quiver.Hom.toPath e✝) ≫
        eqToHom
          (_ :
            (𝟙
                    ({ obj := fun V => of (Paths ↑V),
                          map := fun {X Y} F =>
                            Functor.mk
                              { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.obj
                      V)).obj
                b✝ =
              (let_fun this :=
                    { obj := fun V => of (Paths ↑V),
                          map := fun {X Y} F =>
                            Functor.mk
                              { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
                      (𝟙 V);
                  this).obj
                b✝)
case h_obj.h
V : QuivCat
x✝ : Paths ↑V
⊢ (let_fun this :=
          { obj := fun V => of (Paths ↑V),
                map := fun {X Y} F =>
                  Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
            (𝟙 V);
        this).obj
      x✝ =
    (𝟙
          ({ obj := fun V => of (Paths ↑V),
                map := fun {X Y} F =>
                  Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.obj
            V)).obj
      x✝
[PROOFSTEP]
apply eq_conj_eqToHom
[GOAL]
case h_obj.h
V : QuivCat
x✝ : Paths ↑V
⊢ (let_fun this :=
          { obj := fun V => of (Paths ↑V),
                map := fun {X Y} F =>
                  Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
            (𝟙 V);
        this).obj
      x✝ =
    (𝟙
          ({ obj := fun V => of (Paths ↑V),
                map := fun {X Y} F =>
                  Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.obj
            V)).obj
      x✝
[PROOFSTEP]
rfl
[GOAL]
U x✝¹ x✝ : QuivCat
F : U ⟶ x✝¹
G : x✝¹ ⟶ x✝
⊢ { obj := fun V => of (Paths ↑V),
          map := fun {X Y} F =>
            Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
      (F ≫ G) =
    { obj := fun V => of (Paths ↑V),
            map := fun {X Y} F =>
              Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
        F ≫
      { obj := fun V => of (Paths ↑V),
            map := fun {X Y} F =>
              Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
        G
[PROOFSTEP]
change (show Paths U ⥤ _ from _) = _
[GOAL]
U x✝¹ x✝ : QuivCat
F : U ⟶ x✝¹
G : x✝¹ ⟶ x✝
⊢ (let_fun this :=
      { obj := fun V => of (Paths ↑V),
            map := fun {X Y} F =>
              Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
        (F ≫ G);
    this) =
    { obj := fun V => of (Paths ↑V),
            map := fun {X Y} F =>
              Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
        F ≫
      { obj := fun V => of (Paths ↑V),
            map := fun {X Y} F =>
              Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
        G
[PROOFSTEP]
ext
[GOAL]
case h_obj.h
U x✝² x✝¹ : QuivCat
F : U ⟶ x✝²
G : x✝² ⟶ x✝¹
x✝ : Paths ↑U
⊢ (let_fun this :=
          { obj := fun V => of (Paths ↑V),
                map := fun {X Y} F =>
                  Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
            (F ≫ G);
        this).obj
      x✝ =
    ({ obj := fun V => of (Paths ↑V),
                map := fun {X Y} F =>
                  Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
            F ≫
          { obj := fun V => of (Paths ↑V),
                map := fun {X Y} F =>
                  Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
            G).obj
      x✝
case h
U x✝¹ x✝ : QuivCat
F : U ⟶ x✝¹
G : x✝¹ ⟶ x✝
a✝ b✝ : ↑U
e✝ : a✝ ⟶ b✝
⊢ (let_fun this :=
          { obj := fun V => of (Paths ↑V),
                map := fun {X Y} F =>
                  Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
            (F ≫ G);
        this).map
      (Quiver.Hom.toPath e✝) =
    eqToHom
        (_ :
          (let_fun this :=
                  { obj := fun V => of (Paths ↑V),
                        map := fun {X Y} F =>
                          Functor.mk
                            { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
                    (F ≫ G);
                this).obj
              a✝ =
            ({ obj := fun V => of (Paths ↑V),
                        map := fun {X Y} F =>
                          Functor.mk
                            { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
                    F ≫
                  { obj := fun V => of (Paths ↑V),
                        map := fun {X Y} F =>
                          Functor.mk
                            { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
                    G).obj
              a✝) ≫
      ({ obj := fun V => of (Paths ↑V),
                    map := fun {X Y} F =>
                      Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
                F ≫
              { obj := fun V => of (Paths ↑V),
                    map := fun {X Y} F =>
                      Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
                G).map
          (Quiver.Hom.toPath e✝) ≫
        eqToHom
          (_ :
            ({ obj := fun V => of (Paths ↑V),
                          map := fun {X Y} F =>
                            Functor.mk
                              { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
                      F ≫
                    { obj := fun V => of (Paths ↑V),
                          map := fun {X Y} F =>
                            Functor.mk
                              { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
                      G).obj
                b✝ =
              (let_fun this :=
                    { obj := fun V => of (Paths ↑V),
                          map := fun {X Y} F =>
                            Functor.mk
                              { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
                      (F ≫ G);
                  this).obj
                b✝)
[PROOFSTEP]
swap
[GOAL]
case h
U x✝¹ x✝ : QuivCat
F : U ⟶ x✝¹
G : x✝¹ ⟶ x✝
a✝ b✝ : ↑U
e✝ : a✝ ⟶ b✝
⊢ (let_fun this :=
          { obj := fun V => of (Paths ↑V),
                map := fun {X Y} F =>
                  Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
            (F ≫ G);
        this).map
      (Quiver.Hom.toPath e✝) =
    eqToHom
        (_ :
          (let_fun this :=
                  { obj := fun V => of (Paths ↑V),
                        map := fun {X Y} F =>
                          Functor.mk
                            { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
                    (F ≫ G);
                this).obj
              a✝ =
            ({ obj := fun V => of (Paths ↑V),
                        map := fun {X Y} F =>
                          Functor.mk
                            { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
                    F ≫
                  { obj := fun V => of (Paths ↑V),
                        map := fun {X Y} F =>
                          Functor.mk
                            { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
                    G).obj
              a✝) ≫
      ({ obj := fun V => of (Paths ↑V),
                    map := fun {X Y} F =>
                      Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
                F ≫
              { obj := fun V => of (Paths ↑V),
                    map := fun {X Y} F =>
                      Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
                G).map
          (Quiver.Hom.toPath e✝) ≫
        eqToHom
          (_ :
            ({ obj := fun V => of (Paths ↑V),
                          map := fun {X Y} F =>
                            Functor.mk
                              { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
                      F ≫
                    { obj := fun V => of (Paths ↑V),
                          map := fun {X Y} F =>
                            Functor.mk
                              { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
                      G).obj
                b✝ =
              (let_fun this :=
                    { obj := fun V => of (Paths ↑V),
                          map := fun {X Y} F =>
                            Functor.mk
                              { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
                      (F ≫ G);
                  this).obj
                b✝)
case h_obj.h
U x✝² x✝¹ : QuivCat
F : U ⟶ x✝²
G : x✝² ⟶ x✝¹
x✝ : Paths ↑U
⊢ (let_fun this :=
          { obj := fun V => of (Paths ↑V),
                map := fun {X Y} F =>
                  Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
            (F ≫ G);
        this).obj
      x✝ =
    ({ obj := fun V => of (Paths ↑V),
                map := fun {X Y} F =>
                  Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
            F ≫
          { obj := fun V => of (Paths ↑V),
                map := fun {X Y} F =>
                  Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
            G).obj
      x✝
[PROOFSTEP]
apply eq_conj_eqToHom
[GOAL]
case h_obj.h
U x✝² x✝¹ : QuivCat
F : U ⟶ x✝²
G : x✝² ⟶ x✝¹
x✝ : Paths ↑U
⊢ (let_fun this :=
          { obj := fun V => of (Paths ↑V),
                map := fun {X Y} F =>
                  Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
            (F ≫ G);
        this).obj
      x✝ =
    ({ obj := fun V => of (Paths ↑V),
                map := fun {X Y} F =>
                  Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
            F ≫
          { obj := fun V => of (Paths ↑V),
                map := fun {X Y} F =>
                  Functor.mk { obj := fun X_1 => F.obj X_1, map := fun {X_1 Y_1} f => Prefunctor.mapPath F f } }.map
            G).obj
      x✝
[PROOFSTEP]
rfl
[GOAL]
V : QuivCat
C : Cat
F : Cat.free.obj V ⟶ C
⊢ ∀ (a b : ↑V) (e : a ⟶ b),
    ((fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F)).map (Quiver.Hom.toPath e) =
      eqToHom (_ : ((fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F)).obj a = F.obj a) ≫
        F.map (Quiver.Hom.toPath e) ≫
          eqToHom (_ : F.obj b = ((fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F)).obj b)
[PROOFSTEP]
simp
[GOAL]
V : QuivCat
C : Cat
⊢ Function.RightInverse (fun F => lift F) fun F => Paths.of ⋙q F.toPrefunctor
[PROOFSTEP]
rintro ⟨obj, map⟩
[GOAL]
case mk
V : QuivCat
C : Cat
obj : ↑V → ↑(forget.obj C)
map : {X Y : ↑V} → (X ⟶ Y) → (obj X ⟶ obj Y)
⊢ (fun F => Paths.of ⋙q F.toPrefunctor) ((fun F => lift F) { obj := obj, map := map }) = { obj := obj, map := map }
[PROOFSTEP]
dsimp only [Prefunctor.comp]
[GOAL]
case mk
V : QuivCat
C : Cat
obj : ↑V → ↑(forget.obj C)
map : {X Y : ↑V} → (X ⟶ Y) → (obj X ⟶ obj Y)
⊢ { obj := fun X => (lift { obj := obj, map := map }).obj (Paths.of.obj X),
      map := fun {X Y} f => (lift { obj := obj, map := map }).map (Paths.of.map f) } =
    { obj := obj, map := map }
[PROOFSTEP]
congr
[GOAL]
case mk.e_map
V : QuivCat
C : Cat
obj : ↑V → ↑(forget.obj C)
map : {X Y : ↑V} → (X ⟶ Y) → (obj X ⟶ obj Y)
⊢ (fun {X Y} f => (lift { obj := obj, map := map }).map (Paths.of.map f)) = map
[PROOFSTEP]
funext X Y f
[GOAL]
case mk.e_map.h.h.h
V : QuivCat
C : Cat
obj : ↑V → ↑(forget.obj C)
map : {X Y : ↑V} → (X ⟶ Y) → (obj X ⟶ obj Y)
X Y : ↑V
f : X ⟶ Y
⊢ (lift { obj := obj, map := map }).map (Paths.of.map f) = map f
[PROOFSTEP]
exact Category.id_comp _
[GOAL]
V x✝¹ : QuivCat
x✝ : Cat
f : V ⟶ x✝¹
g : x✝¹ ⟶ forget.obj x✝
⊢ ↑((fun V C =>
              { toFun := fun F => Paths.of ⋙q F.toPrefunctor, invFun := fun F => lift F,
                left_inv :=
                  (_ : ∀ (F : Cat.free.obj V ⟶ C), (fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F) = F),
                right_inv :=
                  (_ : ∀ (x : V ⟶ forget.obj C), (fun F => Paths.of ⋙q F.toPrefunctor) ((fun F => lift F) x) = x) })
            V x✝).symm
      (f ≫ g) =
    Cat.free.map f ≫
      ↑((fun V C =>
                { toFun := fun F => Paths.of ⋙q F.toPrefunctor, invFun := fun F => lift F,
                  left_inv :=
                    (_ : ∀ (F : Cat.free.obj V ⟶ C), (fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F) = F),
                  right_inv :=
                    (_ : ∀ (x : V ⟶ forget.obj C), (fun F => Paths.of ⋙q F.toPrefunctor) ((fun F => lift F) x) = x) })
              x✝¹ x✝).symm
        g
[PROOFSTEP]
change (show Paths V ⥤ _ from _) = _
[GOAL]
V x✝¹ : QuivCat
x✝ : Cat
f : V ⟶ x✝¹
g : x✝¹ ⟶ forget.obj x✝
⊢ (let_fun this :=
      ↑((fun V C =>
                { toFun := fun F => Paths.of ⋙q F.toPrefunctor, invFun := fun F => lift F,
                  left_inv :=
                    (_ : ∀ (F : Cat.free.obj V ⟶ C), (fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F) = F),
                  right_inv :=
                    (_ : ∀ (x : V ⟶ forget.obj C), (fun F => Paths.of ⋙q F.toPrefunctor) ((fun F => lift F) x) = x) })
              V x✝).symm
        (f ≫ g);
    this) =
    Cat.free.map f ≫
      ↑((fun V C =>
                { toFun := fun F => Paths.of ⋙q F.toPrefunctor, invFun := fun F => lift F,
                  left_inv :=
                    (_ : ∀ (F : Cat.free.obj V ⟶ C), (fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F) = F),
                  right_inv :=
                    (_ : ∀ (x : V ⟶ forget.obj C), (fun F => Paths.of ⋙q F.toPrefunctor) ((fun F => lift F) x) = x) })
              x✝¹ x✝).symm
        g
[PROOFSTEP]
ext
[GOAL]
case h_obj.h
V x✝² : QuivCat
x✝¹ : Cat
f : V ⟶ x✝²
g : x✝² ⟶ forget.obj x✝¹
x✝ : Paths ↑V
⊢ (let_fun this :=
          ↑((fun V C =>
                    { toFun := fun F => Paths.of ⋙q F.toPrefunctor, invFun := fun F => lift F,
                      left_inv :=
                        (_ :
                          ∀ (F : Cat.free.obj V ⟶ C), (fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F) = F),
                      right_inv :=
                        (_ :
                          ∀ (x : V ⟶ forget.obj C), (fun F => Paths.of ⋙q F.toPrefunctor) ((fun F => lift F) x) = x) })
                  V x✝¹).symm
            (f ≫ g);
        this).obj
      x✝ =
    (Cat.free.map f ≫
          ↑((fun V C =>
                    { toFun := fun F => Paths.of ⋙q F.toPrefunctor, invFun := fun F => lift F,
                      left_inv :=
                        (_ :
                          ∀ (F : Cat.free.obj V ⟶ C), (fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F) = F),
                      right_inv :=
                        (_ :
                          ∀ (x : V ⟶ forget.obj C), (fun F => Paths.of ⋙q F.toPrefunctor) ((fun F => lift F) x) = x) })
                  x✝² x✝¹).symm
            g).obj
      x✝
case h
V x✝¹ : QuivCat
x✝ : Cat
f : V ⟶ x✝¹
g : x✝¹ ⟶ forget.obj x✝
a✝ b✝ : ↑V
e✝ : a✝ ⟶ b✝
⊢ (let_fun this :=
          ↑((fun V C =>
                    { toFun := fun F => Paths.of ⋙q F.toPrefunctor, invFun := fun F => lift F,
                      left_inv :=
                        (_ :
                          ∀ (F : Cat.free.obj V ⟶ C), (fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F) = F),
                      right_inv :=
                        (_ :
                          ∀ (x : V ⟶ forget.obj C), (fun F => Paths.of ⋙q F.toPrefunctor) ((fun F => lift F) x) = x) })
                  V x✝).symm
            (f ≫ g);
        this).map
      (Quiver.Hom.toPath e✝) =
    eqToHom
        (_ :
          (let_fun this :=
                  ↑((fun V C =>
                            { toFun := fun F => Paths.of ⋙q F.toPrefunctor, invFun := fun F => lift F,
                              left_inv :=
                                (_ :
                                  ∀ (F : Cat.free.obj V ⟶ C),
                                    (fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F) = F),
                              right_inv :=
                                (_ :
                                  ∀ (x : V ⟶ forget.obj C),
                                    (fun F => Paths.of ⋙q F.toPrefunctor) ((fun F => lift F) x) = x) })
                          V x✝).symm
                    (f ≫ g);
                this).obj
              a✝ =
            (Cat.free.map f ≫
                  ↑((fun V C =>
                            { toFun := fun F => Paths.of ⋙q F.toPrefunctor, invFun := fun F => lift F,
                              left_inv :=
                                (_ :
                                  ∀ (F : Cat.free.obj V ⟶ C),
                                    (fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F) = F),
                              right_inv :=
                                (_ :
                                  ∀ (x : V ⟶ forget.obj C),
                                    (fun F => Paths.of ⋙q F.toPrefunctor) ((fun F => lift F) x) = x) })
                          x✝¹ x✝).symm
                    g).obj
              a✝) ≫
      (Cat.free.map f ≫
              ↑((fun V C =>
                        { toFun := fun F => Paths.of ⋙q F.toPrefunctor, invFun := fun F => lift F,
                          left_inv :=
                            (_ :
                              ∀ (F : Cat.free.obj V ⟶ C),
                                (fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F) = F),
                          right_inv :=
                            (_ :
                              ∀ (x : V ⟶ forget.obj C),
                                (fun F => Paths.of ⋙q F.toPrefunctor) ((fun F => lift F) x) = x) })
                      x✝¹ x✝).symm
                g).map
          (Quiver.Hom.toPath e✝) ≫
        eqToHom
          (_ :
            (Cat.free.map f ≫
                    ↑((fun V C =>
                              { toFun := fun F => Paths.of ⋙q F.toPrefunctor, invFun := fun F => lift F,
                                left_inv :=
                                  (_ :
                                    ∀ (F : Cat.free.obj V ⟶ C),
                                      (fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F) = F),
                                right_inv :=
                                  (_ :
                                    ∀ (x : V ⟶ forget.obj C),
                                      (fun F => Paths.of ⋙q F.toPrefunctor) ((fun F => lift F) x) = x) })
                            x✝¹ x✝).symm
                      g).obj
                b✝ =
              (let_fun this :=
                    ↑((fun V C =>
                              { toFun := fun F => Paths.of ⋙q F.toPrefunctor, invFun := fun F => lift F,
                                left_inv :=
                                  (_ :
                                    ∀ (F : Cat.free.obj V ⟶ C),
                                      (fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F) = F),
                                right_inv :=
                                  (_ :
                                    ∀ (x : V ⟶ forget.obj C),
                                      (fun F => Paths.of ⋙q F.toPrefunctor) ((fun F => lift F) x) = x) })
                            V x✝).symm
                      (f ≫ g);
                  this).obj
                b✝)
[PROOFSTEP]
swap
[GOAL]
case h
V x✝¹ : QuivCat
x✝ : Cat
f : V ⟶ x✝¹
g : x✝¹ ⟶ forget.obj x✝
a✝ b✝ : ↑V
e✝ : a✝ ⟶ b✝
⊢ (let_fun this :=
          ↑((fun V C =>
                    { toFun := fun F => Paths.of ⋙q F.toPrefunctor, invFun := fun F => lift F,
                      left_inv :=
                        (_ :
                          ∀ (F : Cat.free.obj V ⟶ C), (fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F) = F),
                      right_inv :=
                        (_ :
                          ∀ (x : V ⟶ forget.obj C), (fun F => Paths.of ⋙q F.toPrefunctor) ((fun F => lift F) x) = x) })
                  V x✝).symm
            (f ≫ g);
        this).map
      (Quiver.Hom.toPath e✝) =
    eqToHom
        (_ :
          (let_fun this :=
                  ↑((fun V C =>
                            { toFun := fun F => Paths.of ⋙q F.toPrefunctor, invFun := fun F => lift F,
                              left_inv :=
                                (_ :
                                  ∀ (F : Cat.free.obj V ⟶ C),
                                    (fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F) = F),
                              right_inv :=
                                (_ :
                                  ∀ (x : V ⟶ forget.obj C),
                                    (fun F => Paths.of ⋙q F.toPrefunctor) ((fun F => lift F) x) = x) })
                          V x✝).symm
                    (f ≫ g);
                this).obj
              a✝ =
            (Cat.free.map f ≫
                  ↑((fun V C =>
                            { toFun := fun F => Paths.of ⋙q F.toPrefunctor, invFun := fun F => lift F,
                              left_inv :=
                                (_ :
                                  ∀ (F : Cat.free.obj V ⟶ C),
                                    (fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F) = F),
                              right_inv :=
                                (_ :
                                  ∀ (x : V ⟶ forget.obj C),
                                    (fun F => Paths.of ⋙q F.toPrefunctor) ((fun F => lift F) x) = x) })
                          x✝¹ x✝).symm
                    g).obj
              a✝) ≫
      (Cat.free.map f ≫
              ↑((fun V C =>
                        { toFun := fun F => Paths.of ⋙q F.toPrefunctor, invFun := fun F => lift F,
                          left_inv :=
                            (_ :
                              ∀ (F : Cat.free.obj V ⟶ C),
                                (fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F) = F),
                          right_inv :=
                            (_ :
                              ∀ (x : V ⟶ forget.obj C),
                                (fun F => Paths.of ⋙q F.toPrefunctor) ((fun F => lift F) x) = x) })
                      x✝¹ x✝).symm
                g).map
          (Quiver.Hom.toPath e✝) ≫
        eqToHom
          (_ :
            (Cat.free.map f ≫
                    ↑((fun V C =>
                              { toFun := fun F => Paths.of ⋙q F.toPrefunctor, invFun := fun F => lift F,
                                left_inv :=
                                  (_ :
                                    ∀ (F : Cat.free.obj V ⟶ C),
                                      (fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F) = F),
                                right_inv :=
                                  (_ :
                                    ∀ (x : V ⟶ forget.obj C),
                                      (fun F => Paths.of ⋙q F.toPrefunctor) ((fun F => lift F) x) = x) })
                            x✝¹ x✝).symm
                      g).obj
                b✝ =
              (let_fun this :=
                    ↑((fun V C =>
                              { toFun := fun F => Paths.of ⋙q F.toPrefunctor, invFun := fun F => lift F,
                                left_inv :=
                                  (_ :
                                    ∀ (F : Cat.free.obj V ⟶ C),
                                      (fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F) = F),
                                right_inv :=
                                  (_ :
                                    ∀ (x : V ⟶ forget.obj C),
                                      (fun F => Paths.of ⋙q F.toPrefunctor) ((fun F => lift F) x) = x) })
                            V x✝).symm
                      (f ≫ g);
                  this).obj
                b✝)
case h_obj.h
V x✝² : QuivCat
x✝¹ : Cat
f : V ⟶ x✝²
g : x✝² ⟶ forget.obj x✝¹
x✝ : Paths ↑V
⊢ (let_fun this :=
          ↑((fun V C =>
                    { toFun := fun F => Paths.of ⋙q F.toPrefunctor, invFun := fun F => lift F,
                      left_inv :=
                        (_ :
                          ∀ (F : Cat.free.obj V ⟶ C), (fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F) = F),
                      right_inv :=
                        (_ :
                          ∀ (x : V ⟶ forget.obj C), (fun F => Paths.of ⋙q F.toPrefunctor) ((fun F => lift F) x) = x) })
                  V x✝¹).symm
            (f ≫ g);
        this).obj
      x✝ =
    (Cat.free.map f ≫
          ↑((fun V C =>
                    { toFun := fun F => Paths.of ⋙q F.toPrefunctor, invFun := fun F => lift F,
                      left_inv :=
                        (_ :
                          ∀ (F : Cat.free.obj V ⟶ C), (fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F) = F),
                      right_inv :=
                        (_ :
                          ∀ (x : V ⟶ forget.obj C), (fun F => Paths.of ⋙q F.toPrefunctor) ((fun F => lift F) x) = x) })
                  x✝² x✝¹).symm
            g).obj
      x✝
[PROOFSTEP]
apply eq_conj_eqToHom
[GOAL]
case h_obj.h
V x✝² : QuivCat
x✝¹ : Cat
f : V ⟶ x✝²
g : x✝² ⟶ forget.obj x✝¹
x✝ : Paths ↑V
⊢ (let_fun this :=
          ↑((fun V C =>
                    { toFun := fun F => Paths.of ⋙q F.toPrefunctor, invFun := fun F => lift F,
                      left_inv :=
                        (_ :
                          ∀ (F : Cat.free.obj V ⟶ C), (fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F) = F),
                      right_inv :=
                        (_ :
                          ∀ (x : V ⟶ forget.obj C), (fun F => Paths.of ⋙q F.toPrefunctor) ((fun F => lift F) x) = x) })
                  V x✝¹).symm
            (f ≫ g);
        this).obj
      x✝ =
    (Cat.free.map f ≫
          ↑((fun V C =>
                    { toFun := fun F => Paths.of ⋙q F.toPrefunctor, invFun := fun F => lift F,
                      left_inv :=
                        (_ :
                          ∀ (F : Cat.free.obj V ⟶ C), (fun F => lift F) ((fun F => Paths.of ⋙q F.toPrefunctor) F) = F),
                      right_inv :=
                        (_ :
                          ∀ (x : V ⟶ forget.obj C), (fun F => Paths.of ⋙q F.toPrefunctor) ((fun F => lift F) x) = x) })
                  x✝² x✝¹).symm
            g).obj
      x✝
[PROOFSTEP]
rfl
