[GOAL]
B : Type u
⊢ [inst : Inhabited B] → Inhabited (FreeBicategory B)
[PROOFSTEP]
intro h
[GOAL]
B : Type u
h : Inhabited B
⊢ Inhabited (FreeBicategory B)
[PROOFSTEP]
exact id h
[GOAL]
B : Type u
inst✝ : Quiver B
a b : FreeBicategory B
⊢ ∀ {X Y : a ⟶ b} (f : X ⟶ Y), 𝟙 X ≫ f = f
[PROOFSTEP]
rintro f g ⟨η⟩
[GOAL]
case mk
B : Type u
inst✝ : Quiver B
a b : FreeBicategory B
f g : a ⟶ b
f✝ : f ⟶ g
η : Hom₂ f g
⊢ 𝟙 f ≫ Quot.mk Rel η = Quot.mk Rel η
[PROOFSTEP]
exact Quot.sound (Rel.id_comp η)
[GOAL]
B : Type u
inst✝ : Quiver B
a b : FreeBicategory B
⊢ ∀ {X Y : a ⟶ b} (f : X ⟶ Y), f ≫ 𝟙 Y = f
[PROOFSTEP]
rintro f g ⟨η⟩
[GOAL]
case mk
B : Type u
inst✝ : Quiver B
a b : FreeBicategory B
f g : a ⟶ b
f✝ : f ⟶ g
η : Hom₂ f g
⊢ Quot.mk Rel η ≫ 𝟙 g = Quot.mk Rel η
[PROOFSTEP]
exact Quot.sound (Rel.comp_id η)
[GOAL]
B : Type u
inst✝ : Quiver B
a b : FreeBicategory B
⊢ ∀ {W X Y Z : a ⟶ b} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
rintro f g h i ⟨η⟩ ⟨θ⟩ ⟨ι⟩
[GOAL]
case mk.mk.mk
B : Type u
inst✝ : Quiver B
a b : FreeBicategory B
f g h i : a ⟶ b
f✝ : f ⟶ g
η : Hom₂ f g
g✝ : g ⟶ h
θ : Hom₂ g h
h✝ : h ⟶ i
ι : Hom₂ h i
⊢ (Quot.mk Rel η ≫ Quot.mk Rel θ) ≫ Quot.mk Rel ι = Quot.mk Rel η ≫ Quot.mk Rel θ ≫ Quot.mk Rel ι
[PROOFSTEP]
exact Quot.sound (Rel.assoc η θ ι)
[GOAL]
B : Type u
inst✝ : Quiver B
⊢ ∀ {a b c : FreeBicategory B} (f : a ⟶ b) {g h i : b ⟶ c} (η : g ⟶ h) (θ : h ⟶ i),
    (fun a b c f g h η =>
          Quot.map (Hom₂.whisker_left f)
            (_ : ∀ (η η' : Hom₂ g h), Rel η η' → Rel (Hom₂.whisker_left f η) (Hom₂.whisker_left f η')) η)
        a b c f g i (η ≫ θ) =
      (fun a b c f g h η =>
            Quot.map (Hom₂.whisker_left f)
              (_ : ∀ (η η' : Hom₂ g h), Rel η η' → Rel (Hom₂.whisker_left f η) (Hom₂.whisker_left f η')) η)
          a b c f g h η ≫
        (fun a b c f g h η =>
            Quot.map (Hom₂.whisker_left f)
              (_ : ∀ (η η' : Hom₂ g h), Rel η η' → Rel (Hom₂.whisker_left f η) (Hom₂.whisker_left f η')) η)
          a b c f h i θ
[PROOFSTEP]
rintro a b c f g h i ⟨η⟩ ⟨θ⟩
[GOAL]
case mk.mk
B : Type u
inst✝ : Quiver B
a b c : FreeBicategory B
f : a ⟶ b
g h i : b ⟶ c
η✝ : g ⟶ h
η : Hom₂ g h
θ✝ : h ⟶ i
θ : Hom₂ h i
⊢ (fun a b c f g h η =>
        Quot.map (Hom₂.whisker_left f)
          (_ : ∀ (η η' : Hom₂ g h), Rel η η' → Rel (Hom₂.whisker_left f η) (Hom₂.whisker_left f η')) η)
      a b c f g i (Quot.mk Rel η ≫ Quot.mk Rel θ) =
    (fun a b c f g h η =>
          Quot.map (Hom₂.whisker_left f)
            (_ : ∀ (η η' : Hom₂ g h), Rel η η' → Rel (Hom₂.whisker_left f η) (Hom₂.whisker_left f η')) η)
        a b c f g h (Quot.mk Rel η) ≫
      (fun a b c f g h η =>
          Quot.map (Hom₂.whisker_left f)
            (_ : ∀ (η η' : Hom₂ g h), Rel η η' → Rel (Hom₂.whisker_left f η) (Hom₂.whisker_left f η')) η)
        a b c f h i (Quot.mk Rel θ)
[PROOFSTEP]
exact Quot.sound (Rel.whisker_left_comp f η θ)
[GOAL]
B : Type u
inst✝ : Quiver B
⊢ ∀ {a b : FreeBicategory B} {f g : a ⟶ b} (η : f ⟶ g),
    (fun a b c f g h η =>
          Quot.map (Hom₂.whisker_left f)
            (_ : ∀ (η η' : Hom₂ g h), Rel η η' → Rel (Hom₂.whisker_left f η) (Hom₂.whisker_left f η')) η)
        a a b (𝟙 a) f g η =
      ((fun a b f => Iso.mk (Quot.mk Rel (Hom₂.left_unitor f)) (Quot.mk Rel (Hom₂.left_unitor_inv f))) a b f).hom ≫
        η ≫ ((fun a b f => Iso.mk (Quot.mk Rel (Hom₂.left_unitor f)) (Quot.mk Rel (Hom₂.left_unitor_inv f))) a b g).inv
[PROOFSTEP]
rintro a b f g ⟨η⟩
[GOAL]
case mk
B : Type u
inst✝ : Quiver B
a b : FreeBicategory B
f g : a ⟶ b
η✝ : f ⟶ g
η : Hom₂ f g
⊢ (fun a b c f g h η =>
        Quot.map (Hom₂.whisker_left f)
          (_ : ∀ (η η' : Hom₂ g h), Rel η η' → Rel (Hom₂.whisker_left f η) (Hom₂.whisker_left f η')) η)
      a a b (𝟙 a) f g (Quot.mk Rel η) =
    ((fun a b f => Iso.mk (Quot.mk Rel (Hom₂.left_unitor f)) (Quot.mk Rel (Hom₂.left_unitor_inv f))) a b f).hom ≫
      Quot.mk Rel η ≫
        ((fun a b f => Iso.mk (Quot.mk Rel (Hom₂.left_unitor f)) (Quot.mk Rel (Hom₂.left_unitor_inv f))) a b g).inv
[PROOFSTEP]
exact Quot.sound (Rel.id_whisker_left η)
[GOAL]
B : Type u
inst✝ : Quiver B
⊢ ∀ {a b c d : FreeBicategory B} (f : a ⟶ b) (g : b ⟶ c) {h h' : c ⟶ d} (η : h ⟶ h'),
    (fun a b c f g h η =>
          Quot.map (Hom₂.whisker_left f)
            (_ : ∀ (η η' : Hom₂ g h), Rel η η' → Rel (Hom₂.whisker_left f η) (Hom₂.whisker_left f η')) η)
        a c d (f ≫ g) h h' η =
      ((fun a b c d f g h => Iso.mk (Quot.mk Rel (Hom₂.associator f g h)) (Quot.mk Rel (Hom₂.associator_inv f g h))) a b
            c d f g h).hom ≫
        (fun a b c f g h η =>
              Quot.map (Hom₂.whisker_left f)
                (_ : ∀ (η η' : Hom₂ g h), Rel η η' → Rel (Hom₂.whisker_left f η) (Hom₂.whisker_left f η')) η)
            a b d f (g ≫ h) (g ≫ h')
            ((fun a b c f g h η =>
                Quot.map (Hom₂.whisker_left f)
                  (_ : ∀ (η η' : Hom₂ g h), Rel η η' → Rel (Hom₂.whisker_left f η) (Hom₂.whisker_left f η')) η)
              b c d g h h' η) ≫
          ((fun a b c d f g h => Iso.mk (Quot.mk Rel (Hom₂.associator f g h)) (Quot.mk Rel (Hom₂.associator_inv f g h)))
              a b c d f g h').inv
[PROOFSTEP]
rintro a b c d f g h h' ⟨η⟩
[GOAL]
case mk
B : Type u
inst✝ : Quiver B
a b c d : FreeBicategory B
f : a ⟶ b
g : b ⟶ c
h h' : c ⟶ d
η✝ : h ⟶ h'
η : Hom₂ h h'
⊢ (fun a b c f g h η =>
        Quot.map (Hom₂.whisker_left f)
          (_ : ∀ (η η' : Hom₂ g h), Rel η η' → Rel (Hom₂.whisker_left f η) (Hom₂.whisker_left f η')) η)
      a c d (f ≫ g) h h' (Quot.mk Rel η) =
    ((fun a b c d f g h => Iso.mk (Quot.mk Rel (Hom₂.associator f g h)) (Quot.mk Rel (Hom₂.associator_inv f g h))) a b c
          d f g h).hom ≫
      (fun a b c f g h η =>
            Quot.map (Hom₂.whisker_left f)
              (_ : ∀ (η η' : Hom₂ g h), Rel η η' → Rel (Hom₂.whisker_left f η) (Hom₂.whisker_left f η')) η)
          a b d f (g ≫ h) (g ≫ h')
          ((fun a b c f g h η =>
              Quot.map (Hom₂.whisker_left f)
                (_ : ∀ (η η' : Hom₂ g h), Rel η η' → Rel (Hom₂.whisker_left f η) (Hom₂.whisker_left f η')) η)
            b c d g h h' (Quot.mk Rel η)) ≫
        ((fun a b c d f g h => Iso.mk (Quot.mk Rel (Hom₂.associator f g h)) (Quot.mk Rel (Hom₂.associator_inv f g h))) a
            b c d f g h').inv
[PROOFSTEP]
exact Quot.sound (Rel.comp_whisker_left f g η)
[GOAL]
B : Type u
inst✝ : Quiver B
⊢ ∀ {a b c : FreeBicategory B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h) (i : b ⟶ c),
    (fun a b c f g η h =>
          Quot.map (Hom₂.whisker_right h)
            (_ : ∀ (η η' : Hom₂ f g), Rel η η' → Rel (Hom₂.whisker_right h η) (Hom₂.whisker_right h η')) η)
        a b c f h (η ≫ θ) i =
      (fun a b c f g η h =>
            Quot.map (Hom₂.whisker_right h)
              (_ : ∀ (η η' : Hom₂ f g), Rel η η' → Rel (Hom₂.whisker_right h η) (Hom₂.whisker_right h η')) η)
          a b c f g η i ≫
        (fun a b c f g η h =>
            Quot.map (Hom₂.whisker_right h)
              (_ : ∀ (η η' : Hom₂ f g), Rel η η' → Rel (Hom₂.whisker_right h η) (Hom₂.whisker_right h η')) η)
          a b c g h θ i
[PROOFSTEP]
rintro a b c f g h ⟨η⟩ ⟨θ⟩ i
[GOAL]
case mk.mk
B : Type u
inst✝ : Quiver B
a b c : FreeBicategory B
f g h : a ⟶ b
η✝ : f ⟶ g
η : Hom₂ f g
θ✝ : g ⟶ h
θ : Hom₂ g h
i : b ⟶ c
⊢ (fun a b c f g η h =>
        Quot.map (Hom₂.whisker_right h)
          (_ : ∀ (η η' : Hom₂ f g), Rel η η' → Rel (Hom₂.whisker_right h η) (Hom₂.whisker_right h η')) η)
      a b c f h (Quot.mk Rel η ≫ Quot.mk Rel θ) i =
    (fun a b c f g η h =>
          Quot.map (Hom₂.whisker_right h)
            (_ : ∀ (η η' : Hom₂ f g), Rel η η' → Rel (Hom₂.whisker_right h η) (Hom₂.whisker_right h η')) η)
        a b c f g (Quot.mk Rel η) i ≫
      (fun a b c f g η h =>
          Quot.map (Hom₂.whisker_right h)
            (_ : ∀ (η η' : Hom₂ f g), Rel η η' → Rel (Hom₂.whisker_right h η) (Hom₂.whisker_right h η')) η)
        a b c g h (Quot.mk Rel θ) i
[PROOFSTEP]
exact Quot.sound (Rel.comp_whisker_right i η θ)
[GOAL]
B : Type u
inst✝ : Quiver B
⊢ ∀ {a b : FreeBicategory B} {f g : a ⟶ b} (η : f ⟶ g),
    (fun a b c f g η h =>
          Quot.map (Hom₂.whisker_right h)
            (_ : ∀ (η η' : Hom₂ f g), Rel η η' → Rel (Hom₂.whisker_right h η) (Hom₂.whisker_right h η')) η)
        a b b f g η (𝟙 b) =
      ((fun a b f => Iso.mk (Quot.mk Rel (Hom₂.right_unitor f)) (Quot.mk Rel (Hom₂.right_unitor_inv f))) a b f).hom ≫
        η ≫
          ((fun a b f => Iso.mk (Quot.mk Rel (Hom₂.right_unitor f)) (Quot.mk Rel (Hom₂.right_unitor_inv f))) a b g).inv
[PROOFSTEP]
rintro a b f g ⟨η⟩
[GOAL]
case mk
B : Type u
inst✝ : Quiver B
a b : FreeBicategory B
f g : a ⟶ b
η✝ : f ⟶ g
η : Hom₂ f g
⊢ (fun a b c f g η h =>
        Quot.map (Hom₂.whisker_right h)
          (_ : ∀ (η η' : Hom₂ f g), Rel η η' → Rel (Hom₂.whisker_right h η) (Hom₂.whisker_right h η')) η)
      a b b f g (Quot.mk Rel η) (𝟙 b) =
    ((fun a b f => Iso.mk (Quot.mk Rel (Hom₂.right_unitor f)) (Quot.mk Rel (Hom₂.right_unitor_inv f))) a b f).hom ≫
      Quot.mk Rel η ≫
        ((fun a b f => Iso.mk (Quot.mk Rel (Hom₂.right_unitor f)) (Quot.mk Rel (Hom₂.right_unitor_inv f))) a b g).inv
[PROOFSTEP]
exact Quot.sound (Rel.whisker_right_id η)
[GOAL]
B : Type u
inst✝ : Quiver B
⊢ ∀ {a b c d : FreeBicategory B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d),
    (fun a b c f g η h =>
          Quot.map (Hom₂.whisker_right h)
            (_ : ∀ (η η' : Hom₂ f g), Rel η η' → Rel (Hom₂.whisker_right h η) (Hom₂.whisker_right h η')) η)
        a b d f f' η (g ≫ h) =
      ((fun a b c d f g h => Iso.mk (Quot.mk Rel (Hom₂.associator f g h)) (Quot.mk Rel (Hom₂.associator_inv f g h))) a b
            c d f g h).inv ≫
        (fun a b c f g η h =>
              Quot.map (Hom₂.whisker_right h)
                (_ : ∀ (η η' : Hom₂ f g), Rel η η' → Rel (Hom₂.whisker_right h η) (Hom₂.whisker_right h η')) η)
            a c d (f ≫ g) (f' ≫ g)
            ((fun a b c f g η h =>
                Quot.map (Hom₂.whisker_right h)
                  (_ : ∀ (η η' : Hom₂ f g), Rel η η' → Rel (Hom₂.whisker_right h η) (Hom₂.whisker_right h η')) η)
              a b c f f' η g)
            h ≫
          ((fun a b c d f g h => Iso.mk (Quot.mk Rel (Hom₂.associator f g h)) (Quot.mk Rel (Hom₂.associator_inv f g h)))
              a b c d f' g h).hom
[PROOFSTEP]
rintro a b c d f f' ⟨η⟩ g h
[GOAL]
case mk
B : Type u
inst✝ : Quiver B
a b c d : FreeBicategory B
f f' : a ⟶ b
η✝ : f ⟶ f'
η : Hom₂ f f'
g : b ⟶ c
h : c ⟶ d
⊢ (fun a b c f g η h =>
        Quot.map (Hom₂.whisker_right h)
          (_ : ∀ (η η' : Hom₂ f g), Rel η η' → Rel (Hom₂.whisker_right h η) (Hom₂.whisker_right h η')) η)
      a b d f f' (Quot.mk Rel η) (g ≫ h) =
    ((fun a b c d f g h => Iso.mk (Quot.mk Rel (Hom₂.associator f g h)) (Quot.mk Rel (Hom₂.associator_inv f g h))) a b c
          d f g h).inv ≫
      (fun a b c f g η h =>
            Quot.map (Hom₂.whisker_right h)
              (_ : ∀ (η η' : Hom₂ f g), Rel η η' → Rel (Hom₂.whisker_right h η) (Hom₂.whisker_right h η')) η)
          a c d (f ≫ g) (f' ≫ g)
          ((fun a b c f g η h =>
              Quot.map (Hom₂.whisker_right h)
                (_ : ∀ (η η' : Hom₂ f g), Rel η η' → Rel (Hom₂.whisker_right h η) (Hom₂.whisker_right h η')) η)
            a b c f f' (Quot.mk Rel η) g)
          h ≫
        ((fun a b c d f g h => Iso.mk (Quot.mk Rel (Hom₂.associator f g h)) (Quot.mk Rel (Hom₂.associator_inv f g h))) a
            b c d f' g h).hom
[PROOFSTEP]
exact Quot.sound (Rel.whisker_right_comp g h η)
[GOAL]
B : Type u
inst✝ : Quiver B
⊢ ∀ {a b c d : FreeBicategory B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d),
    (fun a b c f g η h =>
          Quot.map (Hom₂.whisker_right h)
            (_ : ∀ (η η' : Hom₂ f g), Rel η η' → Rel (Hom₂.whisker_right h η) (Hom₂.whisker_right h η')) η)
        a c d (f ≫ g) (f ≫ g')
        ((fun a b c f g h η =>
            Quot.map (Hom₂.whisker_left f)
              (_ : ∀ (η η' : Hom₂ g h), Rel η η' → Rel (Hom₂.whisker_left f η) (Hom₂.whisker_left f η')) η)
          a b c f g g' η)
        h =
      ((fun a b c d f g h => Iso.mk (Quot.mk Rel (Hom₂.associator f g h)) (Quot.mk Rel (Hom₂.associator_inv f g h))) a b
            c d f g h).hom ≫
        (fun a b c f g h η =>
              Quot.map (Hom₂.whisker_left f)
                (_ : ∀ (η η' : Hom₂ g h), Rel η η' → Rel (Hom₂.whisker_left f η) (Hom₂.whisker_left f η')) η)
            a b d f (g ≫ h) (g' ≫ h)
            ((fun a b c f g η h =>
                Quot.map (Hom₂.whisker_right h)
                  (_ : ∀ (η η' : Hom₂ f g), Rel η η' → Rel (Hom₂.whisker_right h η) (Hom₂.whisker_right h η')) η)
              b c d g g' η h) ≫
          ((fun a b c d f g h => Iso.mk (Quot.mk Rel (Hom₂.associator f g h)) (Quot.mk Rel (Hom₂.associator_inv f g h)))
              a b c d f g' h).inv
[PROOFSTEP]
rintro a b c d f g g' ⟨η⟩ h
[GOAL]
case mk
B : Type u
inst✝ : Quiver B
a b c d : FreeBicategory B
f : a ⟶ b
g g' : b ⟶ c
η✝ : g ⟶ g'
η : Hom₂ g g'
h : c ⟶ d
⊢ (fun a b c f g η h =>
        Quot.map (Hom₂.whisker_right h)
          (_ : ∀ (η η' : Hom₂ f g), Rel η η' → Rel (Hom₂.whisker_right h η) (Hom₂.whisker_right h η')) η)
      a c d (f ≫ g) (f ≫ g')
      ((fun a b c f g h η =>
          Quot.map (Hom₂.whisker_left f)
            (_ : ∀ (η η' : Hom₂ g h), Rel η η' → Rel (Hom₂.whisker_left f η) (Hom₂.whisker_left f η')) η)
        a b c f g g' (Quot.mk Rel η))
      h =
    ((fun a b c d f g h => Iso.mk (Quot.mk Rel (Hom₂.associator f g h)) (Quot.mk Rel (Hom₂.associator_inv f g h))) a b c
          d f g h).hom ≫
      (fun a b c f g h η =>
            Quot.map (Hom₂.whisker_left f)
              (_ : ∀ (η η' : Hom₂ g h), Rel η η' → Rel (Hom₂.whisker_left f η) (Hom₂.whisker_left f η')) η)
          a b d f (g ≫ h) (g' ≫ h)
          ((fun a b c f g η h =>
              Quot.map (Hom₂.whisker_right h)
                (_ : ∀ (η η' : Hom₂ f g), Rel η η' → Rel (Hom₂.whisker_right h η) (Hom₂.whisker_right h η')) η)
            b c d g g' (Quot.mk Rel η) h) ≫
        ((fun a b c d f g h => Iso.mk (Quot.mk Rel (Hom₂.associator f g h)) (Quot.mk Rel (Hom₂.associator_inv f g h))) a
            b c d f g' h).inv
[PROOFSTEP]
exact Quot.sound (Rel.whisker_assoc f η h)
[GOAL]
B : Type u
inst✝ : Quiver B
⊢ ∀ {a b c : FreeBicategory B} {f g : a ⟶ b} {h i : b ⟶ c} (η : f ⟶ g) (θ : h ⟶ i),
    (fun a b c f g h η =>
            Quot.map (Hom₂.whisker_left f)
              (_ : ∀ (η η' : Hom₂ g h), Rel η η' → Rel (Hom₂.whisker_left f η) (Hom₂.whisker_left f η')) η)
          a b c f h i θ ≫
        (fun a b c f g η h =>
            Quot.map (Hom₂.whisker_right h)
              (_ : ∀ (η η' : Hom₂ f g), Rel η η' → Rel (Hom₂.whisker_right h η) (Hom₂.whisker_right h η')) η)
          a b c f g η i =
      (fun a b c f g η h =>
            Quot.map (Hom₂.whisker_right h)
              (_ : ∀ (η η' : Hom₂ f g), Rel η η' → Rel (Hom₂.whisker_right h η) (Hom₂.whisker_right h η')) η)
          a b c f g η h ≫
        (fun a b c f g h η =>
            Quot.map (Hom₂.whisker_left f)
              (_ : ∀ (η η' : Hom₂ g h), Rel η η' → Rel (Hom₂.whisker_left f η) (Hom₂.whisker_left f η')) η)
          a b c g h i θ
[PROOFSTEP]
rintro a b c f g h i ⟨η⟩ ⟨θ⟩
[GOAL]
case mk.mk
B : Type u
inst✝ : Quiver B
a b c : FreeBicategory B
f g : a ⟶ b
h i : b ⟶ c
η✝ : f ⟶ g
η : Hom₂ f g
θ✝ : h ⟶ i
θ : Hom₂ h i
⊢ (fun a b c f g h η =>
          Quot.map (Hom₂.whisker_left f)
            (_ : ∀ (η η' : Hom₂ g h), Rel η η' → Rel (Hom₂.whisker_left f η) (Hom₂.whisker_left f η')) η)
        a b c f h i (Quot.mk Rel θ) ≫
      (fun a b c f g η h =>
          Quot.map (Hom₂.whisker_right h)
            (_ : ∀ (η η' : Hom₂ f g), Rel η η' → Rel (Hom₂.whisker_right h η) (Hom₂.whisker_right h η')) η)
        a b c f g (Quot.mk Rel η) i =
    (fun a b c f g η h =>
          Quot.map (Hom₂.whisker_right h)
            (_ : ∀ (η η' : Hom₂ f g), Rel η η' → Rel (Hom₂.whisker_right h η) (Hom₂.whisker_right h η')) η)
        a b c f g (Quot.mk Rel η) h ≫
      (fun a b c f g h η =>
          Quot.map (Hom₂.whisker_left f)
            (_ : ∀ (η η' : Hom₂ g h), Rel η η' → Rel (Hom₂.whisker_left f η) (Hom₂.whisker_left f η')) η)
        a b c g h i (Quot.mk Rel θ)
[PROOFSTEP]
exact Quot.sound (Rel.whisker_exchange η θ)
[GOAL]
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
H : Rel η θ
⊢ liftHom₂ F η = liftHom₂ F θ
[PROOFSTEP]
induction H
[GOAL]
case vcomp_right
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝¹ b✝ : B
f✝ g✝ h✝ : Hom a✝¹ b✝
η✝ : Hom₂ f✝ g✝
θ₁✝ θ₂✝ : Hom₂ g✝ h✝
a✝ : Rel θ₁✝ θ₂✝
a_ih✝ : liftHom₂ F θ₁✝ = liftHom₂ F θ₂✝
⊢ liftHom₂ F (Hom₂.vcomp η✝ θ₁✝) = liftHom₂ F (Hom₂.vcomp η✝ θ₂✝)
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case vcomp_right
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝¹ b✝ : B
f✝ g✝ h✝ : Hom a✝¹ b✝
η✝ : Hom₂ f✝ g✝
θ₁✝ θ₂✝ : Hom₂ g✝ h✝
a✝ : Rel θ₁✝ θ₂✝
a_ih✝ : liftHom₂ F θ₁✝ = liftHom₂ F θ₂✝
⊢ liftHom₂ F η✝ ≫ liftHom₂ F θ₁✝ = liftHom₂ F η✝ ≫ liftHom₂ F θ₂✝
[PROOFSTEP]
aesop_cat
[GOAL]
case vcomp_left
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝¹ b✝ : B
f✝ g✝ h✝ : Hom a✝¹ b✝
η₁✝ η₂✝ : Hom₂ f✝ g✝
θ✝ : Hom₂ g✝ h✝
a✝ : Rel η₁✝ η₂✝
a_ih✝ : liftHom₂ F η₁✝ = liftHom₂ F η₂✝
⊢ liftHom₂ F (Hom₂.vcomp η₁✝ θ✝) = liftHom₂ F (Hom₂.vcomp η₂✝ θ✝)
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case vcomp_left
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝¹ b✝ : B
f✝ g✝ h✝ : Hom a✝¹ b✝
η₁✝ η₂✝ : Hom₂ f✝ g✝
θ✝ : Hom₂ g✝ h✝
a✝ : Rel η₁✝ η₂✝
a_ih✝ : liftHom₂ F η₁✝ = liftHom₂ F η₂✝
⊢ liftHom₂ F η₁✝ ≫ liftHom₂ F θ✝ = liftHom₂ F η₂✝ ≫ liftHom₂ F θ✝
[PROOFSTEP]
aesop_cat
[GOAL]
case id_comp
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ g✝ : Hom a✝ b✝
η✝ : Hom₂ f✝ g✝
⊢ liftHom₂ F (Hom₂.vcomp (Hom₂.id f✝) η✝) = liftHom₂ F η✝
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case id_comp
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ g✝ : Hom a✝ b✝
η✝ : Hom₂ f✝ g✝
⊢ 𝟙 (liftHom F f✝) ≫ liftHom₂ F η✝ = liftHom₂ F η✝
[PROOFSTEP]
aesop_cat
[GOAL]
case comp_id
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ g✝ : Hom a✝ b✝
η✝ : Hom₂ f✝ g✝
⊢ liftHom₂ F (Hom₂.vcomp η✝ (Hom₂.id g✝)) = liftHom₂ F η✝
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case comp_id
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ g✝ : Hom a✝ b✝
η✝ : Hom₂ f✝ g✝
⊢ liftHom₂ F η✝ ≫ 𝟙 (liftHom F g✝) = liftHom₂ F η✝
[PROOFSTEP]
aesop_cat
[GOAL]
case assoc
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ g✝ h✝ i✝ : Hom a✝ b✝
η✝ : Hom₂ f✝ g✝
θ✝ : Hom₂ g✝ h✝
ι✝ : Hom₂ h✝ i✝
⊢ liftHom₂ F (Hom₂.vcomp (Hom₂.vcomp η✝ θ✝) ι✝) = liftHom₂ F (Hom₂.vcomp η✝ (Hom₂.vcomp θ✝ ι✝))
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case assoc
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ g✝ h✝ i✝ : Hom a✝ b✝
η✝ : Hom₂ f✝ g✝
θ✝ : Hom₂ g✝ h✝
ι✝ : Hom₂ h✝ i✝
⊢ (liftHom₂ F η✝ ≫ liftHom₂ F θ✝) ≫ liftHom₂ F ι✝ = liftHom₂ F η✝ ≫ liftHom₂ F θ✝ ≫ liftHom₂ F ι✝
[PROOFSTEP]
aesop_cat
[GOAL]
case whisker_left
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝¹ b✝ c✝ : B
f✝ : Hom a✝¹ b✝
g✝ h✝ : Hom b✝ c✝
η✝ η'✝ : Hom₂ g✝ h✝
a✝ : Rel η✝ η'✝
a_ih✝ : liftHom₂ F η✝ = liftHom₂ F η'✝
⊢ liftHom₂ F (Hom₂.whisker_left f✝ η✝) = liftHom₂ F (Hom₂.whisker_left f✝ η'✝)
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case whisker_left
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝¹ b✝ c✝ : B
f✝ : Hom a✝¹ b✝
g✝ h✝ : Hom b✝ c✝
η✝ η'✝ : Hom₂ g✝ h✝
a✝ : Rel η✝ η'✝
a_ih✝ : liftHom₂ F η✝ = liftHom₂ F η'✝
⊢ liftHom F f✝ ◁ liftHom₂ F η✝ = liftHom F f✝ ◁ liftHom₂ F η'✝
[PROOFSTEP]
aesop_cat
[GOAL]
case whisker_left_id
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ : B
f✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
⊢ liftHom₂ F (Hom₂.whisker_left f✝ (Hom₂.id g✝)) = liftHom₂ F (Hom₂.id (Hom.comp f✝ g✝))
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case whisker_left_id
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ : B
f✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
⊢ liftHom F f✝ ◁ 𝟙 (liftHom F g✝) = 𝟙 (liftHom F f✝ ≫ liftHom F g✝)
[PROOFSTEP]
aesop_cat
[GOAL]
case whisker_left_comp
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ : B
f✝ : Hom a✝ b✝
g✝ h✝ i✝ : Hom b✝ c✝
η✝ : Hom₂ g✝ h✝
θ✝ : Hom₂ h✝ i✝
⊢ liftHom₂ F (Hom₂.whisker_left f✝ (Hom₂.vcomp η✝ θ✝)) =
    liftHom₂ F (Hom₂.vcomp (Hom₂.whisker_left f✝ η✝) (Hom₂.whisker_left f✝ θ✝))
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case whisker_left_comp
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ : B
f✝ : Hom a✝ b✝
g✝ h✝ i✝ : Hom b✝ c✝
η✝ : Hom₂ g✝ h✝
θ✝ : Hom₂ h✝ i✝
⊢ liftHom F f✝ ◁ (liftHom₂ F η✝ ≫ liftHom₂ F θ✝) = liftHom F f✝ ◁ liftHom₂ F η✝ ≫ liftHom F f✝ ◁ liftHom₂ F θ✝
[PROOFSTEP]
aesop_cat
[GOAL]
case id_whisker_left
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ g✝ : Hom a✝ b✝
η✝ : Hom₂ f✝ g✝
⊢ liftHom₂ F (Hom₂.whisker_left (Hom.id a✝) η✝) =
    liftHom₂ F (Hom₂.vcomp (Hom₂.left_unitor f✝) (Hom₂.vcomp η✝ (Hom₂.left_unitor_inv g✝)))
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case id_whisker_left
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ g✝ : Hom a✝ b✝
η✝ : Hom₂ f✝ g✝
⊢ 𝟙 (F.obj a✝) ◁ liftHom₂ F η✝ = (λ_ (liftHom F f✝)).hom ≫ liftHom₂ F η✝ ≫ (λ_ (liftHom F g✝)).inv
[PROOFSTEP]
aesop_cat
[GOAL]
case comp_whisker_left
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ d✝ : B
f✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
h✝ h'✝ : Hom c✝ d✝
η✝ : Hom₂ h✝ h'✝
⊢ liftHom₂ F (Hom₂.whisker_left (Hom.comp f✝ g✝) η✝) =
    liftHom₂ F
      (Hom₂.vcomp (Hom₂.associator f✝ g✝ h✝)
        (Hom₂.vcomp (Hom₂.whisker_left f✝ (Hom₂.whisker_left g✝ η✝)) (Hom₂.associator_inv f✝ g✝ h'✝)))
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case comp_whisker_left
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ d✝ : B
f✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
h✝ h'✝ : Hom c✝ d✝
η✝ : Hom₂ h✝ h'✝
⊢ (liftHom F f✝ ≫ liftHom F g✝) ◁ liftHom₂ F η✝ =
    (α_ (liftHom F f✝) (liftHom F g✝) (liftHom F h✝)).hom ≫
      liftHom F f✝ ◁ liftHom F g✝ ◁ liftHom₂ F η✝ ≫ (α_ (liftHom F f✝) (liftHom F g✝) (liftHom F h'✝)).inv
[PROOFSTEP]
aesop_cat
[GOAL]
case whisker_right
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝¹ b✝ c✝ : B
f✝ g✝ : Hom a✝¹ b✝
h✝ : Hom b✝ c✝
η✝ η'✝ : Hom₂ f✝ g✝
a✝ : Rel η✝ η'✝
a_ih✝ : liftHom₂ F η✝ = liftHom₂ F η'✝
⊢ liftHom₂ F (Hom₂.whisker_right h✝ η✝) = liftHom₂ F (Hom₂.whisker_right h✝ η'✝)
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case whisker_right
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝¹ b✝ c✝ : B
f✝ g✝ : Hom a✝¹ b✝
h✝ : Hom b✝ c✝
η✝ η'✝ : Hom₂ f✝ g✝
a✝ : Rel η✝ η'✝
a_ih✝ : liftHom₂ F η✝ = liftHom₂ F η'✝
⊢ liftHom₂ F η✝ ▷ liftHom F h✝ = liftHom₂ F η'✝ ▷ liftHom F h✝
[PROOFSTEP]
aesop_cat
[GOAL]
case id_whisker_right
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ : B
f✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
⊢ liftHom₂ F (Hom₂.whisker_right g✝ (Hom₂.id f✝)) = liftHom₂ F (Hom₂.id (Hom.comp f✝ g✝))
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case id_whisker_right
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ : B
f✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
⊢ 𝟙 (liftHom F f✝) ▷ liftHom F g✝ = 𝟙 (liftHom F f✝ ≫ liftHom F g✝)
[PROOFSTEP]
aesop_cat
[GOAL]
case comp_whisker_right
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ : B
f✝ g✝ h✝ : Hom a✝ b✝
i✝ : Hom b✝ c✝
η✝ : Hom₂ f✝ g✝
θ✝ : Hom₂ g✝ h✝
⊢ liftHom₂ F (Hom₂.whisker_right i✝ (Hom₂.vcomp η✝ θ✝)) =
    liftHom₂ F (Hom₂.vcomp (Hom₂.whisker_right i✝ η✝) (Hom₂.whisker_right i✝ θ✝))
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case comp_whisker_right
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ : B
f✝ g✝ h✝ : Hom a✝ b✝
i✝ : Hom b✝ c✝
η✝ : Hom₂ f✝ g✝
θ✝ : Hom₂ g✝ h✝
⊢ (liftHom₂ F η✝ ≫ liftHom₂ F θ✝) ▷ liftHom F i✝ = liftHom₂ F η✝ ▷ liftHom F i✝ ≫ liftHom₂ F θ✝ ▷ liftHom F i✝
[PROOFSTEP]
aesop_cat
[GOAL]
case whisker_right_id
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ g✝ : Hom a✝ b✝
η✝ : Hom₂ f✝ g✝
⊢ liftHom₂ F (Hom₂.whisker_right (Hom.id b✝) η✝) =
    liftHom₂ F (Hom₂.vcomp (Hom₂.right_unitor f✝) (Hom₂.vcomp η✝ (Hom₂.right_unitor_inv g✝)))
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case whisker_right_id
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ g✝ : Hom a✝ b✝
η✝ : Hom₂ f✝ g✝
⊢ liftHom₂ F η✝ ▷ 𝟙 (F.obj b✝) = (ρ_ (liftHom F f✝)).hom ≫ liftHom₂ F η✝ ≫ (ρ_ (liftHom F g✝)).inv
[PROOFSTEP]
aesop_cat
[GOAL]
case whisker_right_comp
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ d✝ : B
f✝ f'✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
h✝ : Hom c✝ d✝
η✝ : Hom₂ f✝ f'✝
⊢ liftHom₂ F (Hom₂.whisker_right (Hom.comp g✝ h✝) η✝) =
    liftHom₂ F
      (Hom₂.vcomp (Hom₂.associator_inv f✝ g✝ h✝)
        (Hom₂.vcomp (Hom₂.whisker_right h✝ (Hom₂.whisker_right g✝ η✝)) (Hom₂.associator f'✝ g✝ h✝)))
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case whisker_right_comp
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ d✝ : B
f✝ f'✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
h✝ : Hom c✝ d✝
η✝ : Hom₂ f✝ f'✝
⊢ liftHom₂ F η✝ ▷ (liftHom F g✝ ≫ liftHom F h✝) =
    (α_ (liftHom F f✝) (liftHom F g✝) (liftHom F h✝)).inv ≫
      liftHom₂ F η✝ ▷ liftHom F g✝ ▷ liftHom F h✝ ≫ (α_ (liftHom F f'✝) (liftHom F g✝) (liftHom F h✝)).hom
[PROOFSTEP]
aesop_cat
[GOAL]
case whisker_assoc
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ d✝ : B
f✝ : Hom a✝ b✝
g✝ g'✝ : Hom b✝ c✝
η✝ : Hom₂ g✝ g'✝
h✝ : Hom c✝ d✝
⊢ liftHom₂ F (Hom₂.whisker_right h✝ (Hom₂.whisker_left f✝ η✝)) =
    liftHom₂ F
      (Hom₂.vcomp (Hom₂.associator f✝ g✝ h✝)
        (Hom₂.vcomp (Hom₂.whisker_left f✝ (Hom₂.whisker_right h✝ η✝)) (Hom₂.associator_inv f✝ g'✝ h✝)))
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case whisker_assoc
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ d✝ : B
f✝ : Hom a✝ b✝
g✝ g'✝ : Hom b✝ c✝
η✝ : Hom₂ g✝ g'✝
h✝ : Hom c✝ d✝
⊢ (liftHom F f✝ ◁ liftHom₂ F η✝) ▷ liftHom F h✝ =
    (α_ (liftHom F f✝) (liftHom F g✝) (liftHom F h✝)).hom ≫
      liftHom F f✝ ◁ liftHom₂ F η✝ ▷ liftHom F h✝ ≫ (α_ (liftHom F f✝) (liftHom F g'✝) (liftHom F h✝)).inv
[PROOFSTEP]
aesop_cat
[GOAL]
case whisker_exchange
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ : B
f✝ g✝ : Hom a✝ b✝
h✝ i✝ : Hom b✝ c✝
η✝ : Hom₂ f✝ g✝
θ✝ : Hom₂ h✝ i✝
⊢ liftHom₂ F (Hom₂.vcomp (Hom₂.whisker_left f✝ θ✝) (Hom₂.whisker_right i✝ η✝)) =
    liftHom₂ F (Hom₂.vcomp (Hom₂.whisker_right h✝ η✝) (Hom₂.whisker_left g✝ θ✝))
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case whisker_exchange
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ : B
f✝ g✝ : Hom a✝ b✝
h✝ i✝ : Hom b✝ c✝
η✝ : Hom₂ f✝ g✝
θ✝ : Hom₂ h✝ i✝
⊢ liftHom F f✝ ◁ liftHom₂ F θ✝ ≫ liftHom₂ F η✝ ▷ liftHom F i✝ =
    liftHom₂ F η✝ ▷ liftHom F h✝ ≫ liftHom F g✝ ◁ liftHom₂ F θ✝
[PROOFSTEP]
aesop_cat
[GOAL]
case associator_hom_inv
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ d✝ : B
f✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
h✝ : Hom c✝ d✝
⊢ liftHom₂ F (Hom₂.vcomp (Hom₂.associator f✝ g✝ h✝) (Hom₂.associator_inv f✝ g✝ h✝)) =
    liftHom₂ F (Hom₂.id (Hom.comp (Hom.comp f✝ g✝) h✝))
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case associator_hom_inv
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ d✝ : B
f✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
h✝ : Hom c✝ d✝
⊢ (α_ (liftHom F f✝) (liftHom F g✝) (liftHom F h✝)).hom ≫ (α_ (liftHom F f✝) (liftHom F g✝) (liftHom F h✝)).inv =
    𝟙 ((liftHom F f✝ ≫ liftHom F g✝) ≫ liftHom F h✝)
[PROOFSTEP]
aesop_cat
[GOAL]
case associator_inv_hom
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ d✝ : B
f✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
h✝ : Hom c✝ d✝
⊢ liftHom₂ F (Hom₂.vcomp (Hom₂.associator_inv f✝ g✝ h✝) (Hom₂.associator f✝ g✝ h✝)) =
    liftHom₂ F (Hom₂.id (Hom.comp f✝ (Hom.comp g✝ h✝)))
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case associator_inv_hom
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ d✝ : B
f✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
h✝ : Hom c✝ d✝
⊢ (α_ (liftHom F f✝) (liftHom F g✝) (liftHom F h✝)).inv ≫ (α_ (liftHom F f✝) (liftHom F g✝) (liftHom F h✝)).hom =
    𝟙 (liftHom F f✝ ≫ liftHom F g✝ ≫ liftHom F h✝)
[PROOFSTEP]
aesop_cat
[GOAL]
case left_unitor_hom_inv
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ : Hom a✝ b✝
⊢ liftHom₂ F (Hom₂.vcomp (Hom₂.left_unitor f✝) (Hom₂.left_unitor_inv f✝)) =
    liftHom₂ F (Hom₂.id (Hom.comp (Hom.id a✝) f✝))
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case left_unitor_hom_inv
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ : Hom a✝ b✝
⊢ (λ_ (liftHom F f✝)).hom ≫ (λ_ (liftHom F f✝)).inv = 𝟙 (𝟙 (F.obj a✝) ≫ liftHom F f✝)
[PROOFSTEP]
aesop_cat
[GOAL]
case left_unitor_inv_hom
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ : Hom a✝ b✝
⊢ liftHom₂ F (Hom₂.vcomp (Hom₂.left_unitor_inv f✝) (Hom₂.left_unitor f✝)) = liftHom₂ F (Hom₂.id f✝)
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case left_unitor_inv_hom
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ : Hom a✝ b✝
⊢ (λ_ (liftHom F f✝)).inv ≫ (λ_ (liftHom F f✝)).hom = 𝟙 (liftHom F f✝)
[PROOFSTEP]
aesop_cat
[GOAL]
case right_unitor_hom_inv
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ : Hom a✝ b✝
⊢ liftHom₂ F (Hom₂.vcomp (Hom₂.right_unitor f✝) (Hom₂.right_unitor_inv f✝)) =
    liftHom₂ F (Hom₂.id (Hom.comp f✝ (Hom.id b✝)))
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case right_unitor_hom_inv
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ : Hom a✝ b✝
⊢ (ρ_ (liftHom F f✝)).hom ≫ (ρ_ (liftHom F f✝)).inv = 𝟙 (liftHom F f✝ ≫ 𝟙 (F.obj b✝))
[PROOFSTEP]
aesop_cat
[GOAL]
case right_unitor_inv_hom
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ : Hom a✝ b✝
⊢ liftHom₂ F (Hom₂.vcomp (Hom₂.right_unitor_inv f✝) (Hom₂.right_unitor f✝)) = liftHom₂ F (Hom₂.id f✝)
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case right_unitor_inv_hom
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ : B
f✝ : Hom a✝ b✝
⊢ (ρ_ (liftHom F f✝)).inv ≫ (ρ_ (liftHom F f✝)).hom = 𝟙 (liftHom F f✝)
[PROOFSTEP]
aesop_cat
[GOAL]
case pentagon
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ d✝ e✝ : B
f✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
h✝ : Hom c✝ d✝
i✝ : Hom d✝ e✝
⊢ liftHom₂ F
      (Hom₂.vcomp (Hom₂.whisker_right i✝ (Hom₂.associator f✝ g✝ h✝))
        (Hom₂.vcomp (Hom₂.associator f✝ (Hom.comp g✝ h✝) i✝) (Hom₂.whisker_left f✝ (Hom₂.associator g✝ h✝ i✝)))) =
    liftHom₂ F (Hom₂.vcomp (Hom₂.associator (Hom.comp f✝ g✝) h✝ i✝) (Hom₂.associator f✝ g✝ (Hom.comp h✝ i✝)))
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case pentagon
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ d✝ e✝ : B
f✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
h✝ : Hom c✝ d✝
i✝ : Hom d✝ e✝
⊢ (α_ (liftHom F f✝) (liftHom F g✝) (liftHom F h✝)).hom ▷ liftHom F i✝ ≫
      (α_ (liftHom F f✝) (liftHom F g✝ ≫ liftHom F h✝) (liftHom F i✝)).hom ≫
        liftHom F f✝ ◁ (α_ (liftHom F g✝) (liftHom F h✝) (liftHom F i✝)).hom =
    (α_ (liftHom F f✝ ≫ liftHom F g✝) (liftHom F h✝) (liftHom F i✝)).hom ≫
      (α_ (liftHom F f✝) (liftHom F g✝) (liftHom F h✝ ≫ liftHom F i✝)).hom
[PROOFSTEP]
aesop_cat
[GOAL]
case triangle
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ : B
f✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
⊢ liftHom₂ F (Hom₂.vcomp (Hom₂.associator f✝ (Hom.id b✝) g✝) (Hom₂.whisker_left f✝ (Hom₂.left_unitor g✝))) =
    liftHom₂ F (Hom₂.whisker_right g✝ (Hom₂.right_unitor f✝))
[PROOFSTEP]
dsimp [liftHom₂]
[GOAL]
case triangle
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g : a ⟶ b
η θ : Hom₂ f g
a✝ b✝ c✝ : B
f✝ : Hom a✝ b✝
g✝ : Hom b✝ c✝
⊢ (α_ (liftHom F f✝) (𝟙 (F.obj b✝)) (liftHom F g✝)).hom ≫ liftHom F f✝ ◁ (λ_ (liftHom F g✝)).hom =
    (ρ_ (liftHom F f✝)).hom ▷ liftHom F g✝
[PROOFSTEP]
aesop_cat
[GOAL]
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
⊢ ∀ {a b : FreeBicategory B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h),
    PrelaxFunctor.map₂
        { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
          map₂ := fun {a b} {f g} =>
            Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
        (η ≫ θ) =
      PrelaxFunctor.map₂
          { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
            map₂ := fun {a b} {f g} =>
              Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
          η ≫
        PrelaxFunctor.map₂
          { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
            map₂ := fun {a b} {f g} =>
              Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
          θ
[PROOFSTEP]
intros a b f g h η θ
[GOAL]
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g h : a ⟶ b
η : f ⟶ g
θ : g ⟶ h
⊢ PrelaxFunctor.map₂
      { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
        map₂ := fun {a b} {f g} =>
          Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
      (η ≫ θ) =
    PrelaxFunctor.map₂
        { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
          map₂ := fun {a b} {f g} =>
            Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
        η ≫
      PrelaxFunctor.map₂
        { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
          map₂ := fun {a b} {f g} =>
            Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
        θ
[PROOFSTEP]
apply Quot.rec _ _ η
[GOAL]
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g h : a ⟶ b
η : f ⟶ g
θ : g ⟶ h
⊢ ∀ (a_1 : Hom₂ f g),
    PrelaxFunctor.map₂
        { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
          map₂ := fun {a b} {f g} =>
            Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
        (Quot.mk Rel a_1 ≫ θ) =
      PrelaxFunctor.map₂
          { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
            map₂ := fun {a b} {f g} =>
              Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
          (Quot.mk Rel a_1) ≫
        PrelaxFunctor.map₂
          { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
            map₂ := fun {a b} {f g} =>
              Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
          θ
[PROOFSTEP]
intro η
[GOAL]
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g h : a ⟶ b
η✝ : f ⟶ g
θ : g ⟶ h
η : Hom₂ f g
⊢ PrelaxFunctor.map₂
      { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
        map₂ := fun {a b} {f g} =>
          Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
      (Quot.mk Rel η ≫ θ) =
    PrelaxFunctor.map₂
        { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
          map₂ := fun {a b} {f g} =>
            Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
        (Quot.mk Rel η) ≫
      PrelaxFunctor.map₂
        { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
          map₂ := fun {a b} {f g} =>
            Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
        θ
[PROOFSTEP]
apply Quot.rec _ _ θ
[GOAL]
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g h : a ⟶ b
η✝ : f ⟶ g
θ : g ⟶ h
η : Hom₂ f g
⊢ ∀ (a_1 : Hom₂ g h),
    PrelaxFunctor.map₂
        { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
          map₂ := fun {a b} {f g} =>
            Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
        (Quot.mk Rel η ≫ Quot.mk Rel a_1) =
      PrelaxFunctor.map₂
          { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
            map₂ := fun {a b} {f g} =>
              Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
          (Quot.mk Rel η) ≫
        PrelaxFunctor.map₂
          { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
            map₂ := fun {a b} {f g} =>
              Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
          (Quot.mk Rel a_1)
[PROOFSTEP]
intro θ
[GOAL]
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g h : a ⟶ b
η✝ : f ⟶ g
θ✝ : g ⟶ h
η : Hom₂ f g
θ : Hom₂ g h
⊢ PrelaxFunctor.map₂
      { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
        map₂ := fun {a b} {f g} =>
          Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
      (Quot.mk Rel η ≫ Quot.mk Rel θ) =
    PrelaxFunctor.map₂
        { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
          map₂ := fun {a b} {f g} =>
            Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
        (Quot.mk Rel η) ≫
      PrelaxFunctor.map₂
        { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
          map₂ := fun {a b} {f g} =>
            Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
        (Quot.mk Rel θ)
[PROOFSTEP]
rfl
[GOAL]
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g h : a ⟶ b
η✝ : f ⟶ g
θ : g ⟶ h
η : Hom₂ f g
⊢ ∀ (a_1 b_1 : Hom₂ g h) (p : Rel a_1 b_1),
    (_ :
        PrelaxFunctor.map₂
            { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
              map₂ := fun {a b} {f g} =>
                Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
            (Quot.mk Rel η ≫ Quot.mk Rel b_1) =
          PrelaxFunctor.map₂
              { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                map₂ := fun {a b} {f g} =>
                  Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
              (Quot.mk Rel η) ≫
            PrelaxFunctor.map₂
              { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                map₂ := fun {a b} {f g} =>
                  Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
              (Quot.mk Rel b_1)) =
      (_ :
        PrelaxFunctor.map₂
            { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
              map₂ := fun {a b} {f g} =>
                Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
            (Quot.mk Rel η ≫ Quot.mk Rel b_1) =
          PrelaxFunctor.map₂
            { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
              map₂ := fun {a b} {f g} =>
                Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
            (Quot.mk Rel η ≫ Quot.mk Rel b_1))
[PROOFSTEP]
intros
[GOAL]
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g h : a ⟶ b
η✝ : f ⟶ g
θ : g ⟶ h
η : Hom₂ f g
a✝ b✝ : Hom₂ g h
p✝ : Rel a✝ b✝
⊢ (_ :
      PrelaxFunctor.map₂
          { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
            map₂ := fun {a b} {f g} =>
              Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
          (Quot.mk Rel η ≫ Quot.mk Rel b✝) =
        PrelaxFunctor.map₂
            { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
              map₂ := fun {a b} {f g} =>
                Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
            (Quot.mk Rel η) ≫
          PrelaxFunctor.map₂
            { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
              map₂ := fun {a b} {f g} =>
                Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
            (Quot.mk Rel b✝)) =
    (_ :
      PrelaxFunctor.map₂
          { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
            map₂ := fun {a b} {f g} =>
              Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
          (Quot.mk Rel η ≫ Quot.mk Rel b✝) =
        PrelaxFunctor.map₂
          { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
            map₂ := fun {a b} {f g} =>
              Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
          (Quot.mk Rel η ≫ Quot.mk Rel b✝))
[PROOFSTEP]
rfl
[GOAL]
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g h : a ⟶ b
η : f ⟶ g
θ : g ⟶ h
⊢ ∀ (a_1 b_1 : Hom₂ f g) (p : Rel a_1 b_1),
    (_ :
        PrelaxFunctor.map₂
            { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
              map₂ := fun {a b} {f g} =>
                Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
            (Quot.mk Rel b_1 ≫ θ) =
          PrelaxFunctor.map₂
              { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                map₂ := fun {a b} {f g} =>
                  Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
              (Quot.mk Rel b_1) ≫
            PrelaxFunctor.map₂
              { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                map₂ := fun {a b} {f g} =>
                  Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
              θ) =
      (_ :
        PrelaxFunctor.map₂
            { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
              map₂ := fun {a b} {f g} =>
                Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
            (Quot.mk Rel b_1 ≫ θ) =
          PrelaxFunctor.map₂
              { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                map₂ := fun {a b} {f g} =>
                  Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
              (Quot.mk Rel b_1) ≫
            PrelaxFunctor.map₂
              { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                map₂ := fun {a b} {f g} =>
                  Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
              θ)
[PROOFSTEP]
intros
[GOAL]
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b : FreeBicategory B
f g h : a ⟶ b
η : f ⟶ g
θ : g ⟶ h
a✝ b✝ : Hom₂ f g
p✝ : Rel a✝ b✝
⊢ (_ :
      PrelaxFunctor.map₂
          { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
            map₂ := fun {a b} {f g} =>
              Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
          (Quot.mk Rel b✝ ≫ θ) =
        PrelaxFunctor.map₂
            { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
              map₂ := fun {a b} {f g} =>
                Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
            (Quot.mk Rel b✝) ≫
          PrelaxFunctor.map₂
            { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
              map₂ := fun {a b} {f g} =>
                Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
            θ) =
    (_ :
      PrelaxFunctor.map₂
          { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
            map₂ := fun {a b} {f g} =>
              Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
          (Quot.mk Rel b✝ ≫ θ) =
        PrelaxFunctor.map₂
            { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
              map₂ := fun {a b} {f g} =>
                Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
            (Quot.mk Rel b✝) ≫
          PrelaxFunctor.map₂
            { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
              map₂ := fun {a b} {f g} =>
                Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
            θ)
[PROOFSTEP]
rfl
  -- Porting note: still borked from here. The infoview doesn't update properly for me.
[GOAL]
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
⊢ ∀ {a b c : FreeBicategory B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h),
    PrelaxFunctor.map₂
        { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
          map₂ := fun {a b} {f g} =>
            Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
        (f ◁ η) =
      ((fun {a b c} f g =>
              Iso.refl
                ((↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                        map₂ := fun {a b} {f g} =>
                          Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
                  (f ≫ g)))
            f g).hom ≫
        (↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                    map₂ := fun {a b} {f g} =>
                      Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
              f ◁
            PrelaxFunctor.map₂
              { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                map₂ := fun {a b} {f g} =>
                  Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
              η ≫
          ((fun {a b c} f g =>
                Iso.refl
                  ((↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                          map₂ := fun {a b} {f g} =>
                            Quot.lift (liftHom₂ F)
                              (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
                    (f ≫ g)))
              f h).inv
[PROOFSTEP]
intro a b c f g h η
[GOAL]
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b c : FreeBicategory B
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ h
⊢ PrelaxFunctor.map₂
      { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
        map₂ := fun {a b} {f g} =>
          Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
      (f ◁ η) =
    ((fun {a b c} f g =>
            Iso.refl
              ((↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                      map₂ := fun {a b} {f g} =>
                        Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
                (f ≫ g)))
          f g).hom ≫
      (↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                  map₂ := fun {a b} {f g} =>
                    Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
            f ◁
          PrelaxFunctor.map₂
            { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
              map₂ := fun {a b} {f g} =>
                Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
            η ≫
        ((fun {a b c} f g =>
              Iso.refl
                ((↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                        map₂ := fun {a b} {f g} =>
                          Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
                  (f ≫ g)))
            f h).inv
[PROOFSTEP]
apply Quot.rec _ _ η
[GOAL]
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b c : FreeBicategory B
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ h
⊢ ∀ (a_1 : Hom₂ g h),
    PrelaxFunctor.map₂
        { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
          map₂ := fun {a b} {f g} =>
            Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
        (f ◁ Quot.mk Rel a_1) =
      ((fun {a b c} f g =>
              Iso.refl
                ((↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                        map₂ := fun {a b} {f g} =>
                          Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
                  (f ≫ g)))
            f g).hom ≫
        (↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                    map₂ := fun {a b} {f g} =>
                      Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
              f ◁
            PrelaxFunctor.map₂
              { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                map₂ := fun {a b} {f g} =>
                  Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
              (Quot.mk Rel a_1) ≫
          ((fun {a b c} f g =>
                Iso.refl
                  ((↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                          map₂ := fun {a b} {f g} =>
                            Quot.lift (liftHom₂ F)
                              (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
                    (f ≫ g)))
              f h).inv
[PROOFSTEP]
intros
[GOAL]
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b c : FreeBicategory B
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ h
a✝ : Hom₂ g h
⊢ PrelaxFunctor.map₂
      { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
        map₂ := fun {a b} {f g} =>
          Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
      (f ◁ Quot.mk Rel a✝) =
    ((fun {a b c} f g =>
            Iso.refl
              ((↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                      map₂ := fun {a b} {f g} =>
                        Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
                (f ≫ g)))
          f g).hom ≫
      (↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                  map₂ := fun {a b} {f g} =>
                    Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
            f ◁
          PrelaxFunctor.map₂
            { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
              map₂ := fun {a b} {f g} =>
                Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
            (Quot.mk Rel a✝) ≫
        ((fun {a b c} f g =>
              Iso.refl
                ((↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                        map₂ := fun {a b} {f g} =>
                          Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
                  (f ≫ g)))
            f h).inv
[PROOFSTEP]
aesop_cat
[GOAL]
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b c : FreeBicategory B
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ h
⊢ ∀ (a_1 b_1 : Hom₂ g h) (p : Rel a_1 b_1),
    (_ :
        PrelaxFunctor.map₂
            { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
              map₂ := fun {a b} {f g} =>
                Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
            (f ◁ Quot.mk Rel b_1) =
          ((fun {a b c} f g =>
                  Iso.refl
                    ((↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                            map₂ := fun {a b} {f g} =>
                              Quot.lift (liftHom₂ F)
                                (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
                      (f ≫ g)))
                f g).hom ≫
            (↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                        map₂ := fun {a b} {f g} =>
                          Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
                  f ◁
                PrelaxFunctor.map₂
                  { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                    map₂ := fun {a b} {f g} =>
                      Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
                  (Quot.mk Rel b_1) ≫
              ((fun {a b c} f g =>
                    Iso.refl
                      ((↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                              map₂ := fun {a b} {f g} =>
                                Quot.lift (liftHom₂ F)
                                  (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
                        (f ≫ g)))
                  f h).inv) =
      (_ :
        PrelaxFunctor.map₂
            { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
              map₂ := fun {a b} {f g} =>
                Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
            (f ◁ Quot.mk Rel b_1) =
          ((fun {a b c} f g =>
                  Iso.refl
                    ((↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                            map₂ := fun {a b} {f g} =>
                              Quot.lift (liftHom₂ F)
                                (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
                      (f ≫ g)))
                f g).hom ≫
            (↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                        map₂ := fun {a b} {f g} =>
                          Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
                  f ◁
                PrelaxFunctor.map₂
                  { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                    map₂ := fun {a b} {f g} =>
                      Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
                  (Quot.mk Rel b_1) ≫
              ((fun {a b c} f g =>
                    Iso.refl
                      ((↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                              map₂ := fun {a b} {f g} =>
                                Quot.lift (liftHom₂ F)
                                  (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
                        (f ≫ g)))
                  f h).inv)
[PROOFSTEP]
intros
[GOAL]
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a b c : FreeBicategory B
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ h
a✝ b✝ : Hom₂ g h
p✝ : Rel a✝ b✝
⊢ (_ :
      PrelaxFunctor.map₂
          { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
            map₂ := fun {a b} {f g} =>
              Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
          (f ◁ Quot.mk Rel b✝) =
        ((fun {a b c} f g =>
                Iso.refl
                  ((↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                          map₂ := fun {a b} {f g} =>
                            Quot.lift (liftHom₂ F)
                              (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
                    (f ≫ g)))
              f g).hom ≫
          (↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                      map₂ := fun {a b} {f g} =>
                        Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
                f ◁
              PrelaxFunctor.map₂
                { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                  map₂ := fun {a b} {f g} =>
                    Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
                (Quot.mk Rel b✝) ≫
            ((fun {a b c} f g =>
                  Iso.refl
                    ((↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                            map₂ := fun {a b} {f g} =>
                              Quot.lift (liftHom₂ F)
                                (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
                      (f ≫ g)))
                f h).inv) =
    (_ :
      PrelaxFunctor.map₂
          { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
            map₂ := fun {a b} {f g} =>
              Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
          (f ◁ Quot.mk Rel b✝) =
        ((fun {a b c} f g =>
                Iso.refl
                  ((↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                          map₂ := fun {a b} {f g} =>
                            Quot.lift (liftHom₂ F)
                              (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
                    (f ≫ g)))
              f g).hom ≫
          (↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                      map₂ := fun {a b} {f g} =>
                        Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
                f ◁
              PrelaxFunctor.map₂
                { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                  map₂ := fun {a b} {f g} =>
                    Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
                (Quot.mk Rel b✝) ≫
            ((fun {a b c} f g =>
                  Iso.refl
                    ((↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                            map₂ := fun {a b} {f g} =>
                              Quot.lift (liftHom₂ F)
                                (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
                      (f ≫ g)))
                f h).inv)
[PROOFSTEP]
rfl
[GOAL]
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
⊢ ∀ {a b c : FreeBicategory B} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c),
    PrelaxFunctor.map₂
        { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
          map₂ := fun {a b} {f g} =>
            Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
        (η ▷ h) =
      ((fun {a b c} f g =>
              Iso.refl
                ((↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                        map₂ := fun {a b} {f g} =>
                          Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
                  (f ≫ g)))
            f h).hom ≫
        PrelaxFunctor.map₂
              { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                map₂ := fun {a b} {f g} =>
                  Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
              η ▷
            (↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                    map₂ := fun {a b} {f g} =>
                      Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
              h ≫
          ((fun {a b c} f g =>
                Iso.refl
                  ((↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                          map₂ := fun {a b} {f g} =>
                            Quot.lift (liftHom₂ F)
                              (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
                    (f ≫ g)))
              g h).inv
[PROOFSTEP]
intro _ _ _ _ _ η h
[GOAL]
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a✝ b✝ c✝ : FreeBicategory B
f✝ g✝ : a✝ ⟶ b✝
η : f✝ ⟶ g✝
h : b✝ ⟶ c✝
⊢ PrelaxFunctor.map₂
      { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
        map₂ := fun {a b} {f g} =>
          Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
      (η ▷ h) =
    ((fun {a b c} f g =>
            Iso.refl
              ((↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                      map₂ := fun {a b} {f g} =>
                        Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
                (f ≫ g)))
          f✝ h).hom ≫
      PrelaxFunctor.map₂
            { toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
              map₂ := fun {a b} {f g} =>
                Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }
            η ▷
          (↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                  map₂ := fun {a b} {f g} =>
                    Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
            h ≫
        ((fun {a b c} f g =>
              Iso.refl
                ((↑{ toPrefunctor := { obj := F.obj, map := fun {X Y} => liftHom F },
                        map₂ := fun {a b} {f g} =>
                          Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f g), Rel η θ → liftHom₂ F η = liftHom₂ F θ) }).map
                  (f ≫ g)))
            g✝ h).inv
[PROOFSTEP]
dsimp
[GOAL]
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a✝ b✝ c✝ : FreeBicategory B
f✝ g✝ : a✝ ⟶ b✝
η : f✝ ⟶ g✝
h : b✝ ⟶ c✝
⊢ Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ (f✝ ≫ h) (g✝ ≫ h)), Rel η θ → liftHom₂ F η = liftHom₂ F θ) (η ▷ h) =
    𝟙 (liftHom F f✝ ≫ liftHom F h) ≫
      Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f✝ g✝), Rel η θ → liftHom₂ F η = liftHom₂ F θ) η ▷ liftHom F h ≫
        𝟙 (liftHom F g✝ ≫ liftHom F h)
[PROOFSTEP]
apply Quot.rec _ _ η
[GOAL]
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a✝ b✝ c✝ : FreeBicategory B
f✝ g✝ : a✝ ⟶ b✝
η : f✝ ⟶ g✝
h : b✝ ⟶ c✝
⊢ ∀ (a : Hom₂ f✝ g✝),
    Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ (f✝ ≫ h) (g✝ ≫ h)), Rel η θ → liftHom₂ F η = liftHom₂ F θ)
        (Quot.mk Rel a ▷ h) =
      𝟙 (liftHom F f✝ ≫ liftHom F h) ≫
        Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f✝ g✝), Rel η θ → liftHom₂ F η = liftHom₂ F θ) (Quot.mk Rel a) ▷
            liftHom F h ≫
          𝟙 (liftHom F g✝ ≫ liftHom F h)
[PROOFSTEP]
aesop_cat
[GOAL]
B : Type u₁
inst✝¹ : Quiver B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤q C
a✝ b✝ c✝ : FreeBicategory B
f✝ g✝ : a✝ ⟶ b✝
η : f✝ ⟶ g✝
h : b✝ ⟶ c✝
⊢ ∀ (a b : Hom₂ f✝ g✝) (p : Rel a b),
    (_ :
        Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ (f✝ ≫ h) (g✝ ≫ h)), Rel η θ → liftHom₂ F η = liftHom₂ F θ)
            (Quot.mk Rel b ▷ h) =
          𝟙 (liftHom F f✝ ≫ liftHom F h) ≫
            Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f✝ g✝), Rel η θ → liftHom₂ F η = liftHom₂ F θ) (Quot.mk Rel b) ▷
                liftHom F h ≫
              𝟙 (liftHom F g✝ ≫ liftHom F h)) =
      (_ :
        Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ (f✝ ≫ h) (g✝ ≫ h)), Rel η θ → liftHom₂ F η = liftHom₂ F θ)
            (Quot.mk Rel b ▷ h) =
          𝟙 (liftHom F f✝ ≫ liftHom F h) ≫
            Quot.lift (liftHom₂ F) (_ : ∀ (η θ : Hom₂ f✝ g✝), Rel η θ → liftHom₂ F η = liftHom₂ F θ) (Quot.mk Rel b) ▷
                liftHom F h ≫
              𝟙 (liftHom F g✝ ≫ liftHom F h))
[PROOFSTEP]
aesop_cat
