case h_obj
V : Type u_1
inst✝¹ : Quiver V
W : Type u_5
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
⊢ ∀ (X : V), (of σ ⋙q lift σ φ τ h).obj X = φ.obj X

case h_map
V : Type u_1
inst✝¹ : Quiver V
W : Type u_5
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
⊢ ∀ (X Y : V) (f : X ⟶ Y),
    (of σ ⋙q lift σ φ τ h).map f =
      Eq.recOn (_ : φ.obj Y = (of σ ⋙q lift σ φ τ h).obj Y)
        (Eq.recOn (_ : φ.obj X = (of σ ⋙q lift σ φ τ h).obj X) (φ.map f))
V : Type u_1
inst✝¹ : Quiver V
W : Type u_5
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
⊢ of σ ⋙q lift σ φ τ h = φ
fapply Prefunctor.ext
case h_obj
V : Type u_1
inst✝¹ : Quiver V
W : Type u_5
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X : V
⊢ (of σ ⋙q lift σ φ τ h).obj X = φ.obj X
case h_obj
V : Type u_1
inst✝¹ : Quiver V
W : Type u_5
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
⊢ ∀ (X : V), (of σ ⋙q lift σ φ τ h).obj X = φ.obj X
rintro X
case h_obj
V : Type u_1
inst✝¹ : Quiver V
W : Type u_5
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X : V
⊢ (lift σ φ τ h).obj ((of σ).obj X) = φ.obj X
case h_obj
V : Type u_1
inst✝¹ : Quiver V
W : Type u_5
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X : V
⊢ (of σ ⋙q lift σ φ τ h).obj X = φ.obj X
simp only [Prefunctor.comp_obj]
case h_obj.h
V : Type u_1
inst✝¹ : Quiver V
W : Type u_5
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X : V
⊢ φ.obj X = (lift σ φ τ h).obj ((of σ).obj X)
case h_obj
V : Type u_1
inst✝¹ : Quiver V
W : Type u_5
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X : V
⊢ (lift σ φ τ h).obj ((of σ).obj X) = φ.obj X
apply Eq.symm
no goals
case h_obj.h
V : Type u_1
inst✝¹ : Quiver V
W : Type u_5
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X : V
⊢ φ.obj X = (lift σ φ τ h).obj ((of σ).obj X)
exact h X
case h_map
V : Type u_1
inst✝¹ : Quiver V
W : Type u_5
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ (of σ ⋙q lift σ φ τ h).map f =
    Eq.recOn (_ : φ.obj Y = (of σ ⋙q lift σ φ τ h).obj Y)
      (Eq.recOn (_ : φ.obj X = (of σ ⋙q lift σ φ τ h).obj X) (φ.map f))
case h_map
V : Type u_1
inst✝¹ : Quiver V
W : Type u_5
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
⊢ ∀ (X Y : V) (f : X ⟶ Y),
    (of σ ⋙q lift σ φ τ h).map f =
      Eq.recOn (_ : φ.obj Y = (of σ ⋙q lift σ φ τ h).obj Y)
        (Eq.recOn (_ : φ.obj X = (of σ ⋙q lift σ φ τ h).obj X) (φ.map f))
rintro X Y f
case h_map
V : Type u_1
inst✝¹ : Quiver V
W : Type u_5
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ (lift σ φ τ h).map ((of σ).map f) =
    (_ : φ.obj Y = (of σ ⋙q lift σ φ τ h).obj Y) ▸ (_ : φ.obj X = (of σ ⋙q lift σ φ τ h).obj X) ▸ φ.map f
case h_map
V : Type u_1
inst✝¹ : Quiver V
W : Type u_5
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ (of σ ⋙q lift σ φ τ h).map f =
    Eq.recOn (_ : φ.obj Y = (of σ ⋙q lift σ φ τ h).obj Y)
      (Eq.recOn (_ : φ.obj X = (of σ ⋙q lift σ φ τ h).obj X) (φ.map f))
simp only [Prefunctor.comp_map]
case h_map.h
V : Type u_1
inst✝¹ : Quiver V
W : Type u_5
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ HEq ((lift σ φ τ h).map ((of σ).map f))
    ((_ : φ.obj Y = (of σ ⋙q lift σ φ τ h).obj Y) ▸ (_ : φ.obj X = (of σ ⋙q lift σ φ τ h).obj X) ▸ φ.map f)
case h_map
V : Type u_1
inst✝¹ : Quiver V
W : Type u_5
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ (lift σ φ τ h).map ((of σ).map f) =
    (_ : φ.obj Y = (of σ ⋙q lift σ φ τ h).obj Y) ▸ (_ : φ.obj X = (of σ ⋙q lift σ φ τ h).obj X) ▸ φ.map f
apply eq_of_heq
case h_map.h
V : Type u_1
inst✝¹ : Quiver V
W : Type u_5
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ HEq (φ.map f) ((_ : φ.obj Y = (of σ ⋙q lift σ φ τ h).obj Y) ▸ (_ : φ.obj X = (of σ ⋙q lift σ φ τ h).obj X) ▸ φ.map f)
case h_map.h
V : Type u_1
inst✝¹ : Quiver V
W : Type u_5
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ HEq ((lift σ φ τ h).map ((of σ).map f))
    ((_ : φ.obj Y = (of σ ⋙q lift σ φ τ h).obj Y) ▸ (_ : φ.obj X = (of σ ⋙q lift σ φ τ h).obj X) ▸ φ.map f)
iterate 2 apply (cast_heq _ _).trans
case h_map.h.h
V : Type u_1
inst✝¹ : Quiver V
W : Type u_5
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ HEq ((_ : φ.obj Y = (of σ ⋙q lift σ φ τ h).obj Y) ▸ (_ : φ.obj X = (of σ ⋙q lift σ φ τ h).obj X) ▸ φ.map f) (φ.map f)
case h_map.h
V : Type u_1
inst✝¹ : Quiver V
W : Type u_5
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ HEq (φ.map f) ((_ : φ.obj Y = (of σ ⋙q lift σ φ τ h).obj Y) ▸ (_ : φ.obj X = (of σ ⋙q lift σ φ τ h).obj X) ▸ φ.map f)
apply HEq.symm
case h_map.h.h
V : Type u_1
inst✝¹ : Quiver V
W : Type u_5
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ HEq ((_ : φ.obj X = (of σ ⋙q lift σ φ τ h).obj X) ▸ φ.map f) (φ.map f)
case h_map.h.h
V : Type u_1
inst✝¹ : Quiver V
W : Type u_5
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ HEq ((_ : φ.obj Y = (of σ ⋙q lift σ φ τ h).obj Y) ▸ (_ : φ.obj X = (of σ ⋙q lift σ φ τ h).obj X) ▸ φ.map f) (φ.map f)
apply (eqRec_heq _ _).trans
case h_map.h.h
V : Type u_1
inst✝¹ : Quiver V
W : Type u_5
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
this :
  ∀ {α : Sort ?u.2594} {γ : Sort ?u.2596} {β : α → γ → Sort ?u.2598} {a a' : α} (p : a = a') (g : γ) (b : β a g),
    HEq (p ▸ b) b
⊢ HEq ((_ : φ.obj X = (of σ ⋙q lift σ φ τ h).obj X) ▸ φ.map f) (φ.map f)
case h_map.h.h
V : Type u_1
inst✝¹ : Quiver V
W : Type u_5
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ HEq ((_ : φ.obj X = (of σ ⋙q lift σ φ τ h).obj X) ▸ φ.map f) (φ.map f)
have : ∀ {α γ} {β : α → γ → Sort _} {a a'} (p : a = a') g (b : β a g), HEq (p ▸ b) b := by
  intros
  subst_vars
  rfl
no goals
case h_map.h.h
V : Type u_1
inst✝¹ : Quiver V
W : Type u_5
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
this :
  ∀ {α : Sort ?u.2594} {γ : Sort ?u.2596} {β : α → γ → Sort ?u.2598} {a a' : α} (p : a = a') (g : γ) (b : β a g),
    HEq (p ▸ b) b
⊢ HEq ((_ : φ.obj X = (of σ ⋙q lift σ φ τ h).obj X) ▸ φ.map f) (φ.map f)
apply this
case h_map.h
V : Type u_1
inst✝¹ : Quiver V
W : Type u_5
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ HEq (φ.map f) ((_ : φ.obj Y = (of σ ⋙q lift σ φ τ h).obj Y) ▸ (_ : φ.obj X = (of σ ⋙q lift σ φ τ h).obj X) ▸ φ.map f)
case h_map.h
V : Type u_1
inst✝¹ : Quiver V
W : Type u_5
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ HEq (Eq.mpr (_ : (φ.obj X ⟶ τ (σ Y)) = (φ.obj X ⟶ φ.obj Y)) (φ.map f))
    ((_ : φ.obj Y = (of σ ⋙q lift σ φ τ h).obj Y) ▸ (_ : φ.obj X = (of σ ⋙q lift σ φ τ h).obj X) ▸ φ.map f)
apply (cast_heq _ _).trans
V : Type u_1
inst✝¹ : Quiver V
W : Type u_5
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
α✝ : Sort ?u.2594
γ✝ : Sort ?u.2596
β✝ : α✝ → γ✝ → Sort ?u.2598
a✝ a'✝ : α✝
p✝ : a✝ = a'✝
g✝ : γ✝
b✝ : β✝ a✝ g✝
⊢ HEq (p✝ ▸ b✝) b✝
V : Type u_1
inst✝¹ : Quiver V
W : Type u_5
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ ∀ {α : Sort ?u.2594} {γ : Sort ?u.2596} {β : α → γ → Sort ?u.2598} {a a' : α} (p : a = a') (g : γ) (b : β a g),
    HEq (p ▸ b) b
intros
V : Type u_1
inst✝¹ : Quiver V
W : Type u_5
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
α✝ : Sort ?u.2594
γ✝ : Sort ?u.2596
β✝ : α✝ → γ✝ → Sort ?u.2598
a'✝ : α✝
g✝ : γ✝
b✝ : β✝ a'✝ g✝
⊢ HEq ((_ : a'✝ = a'✝) ▸ b✝) b✝
V : Type u_1
inst✝¹ : Quiver V
W : Type u_5
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
α✝ : Sort ?u.2594
γ✝ : Sort ?u.2596
β✝ : α✝ → γ✝ → Sort ?u.2598
a✝ a'✝ : α✝
p✝ : a✝ = a'✝
g✝ : γ✝
b✝ : β✝ a✝ g✝
⊢ HEq (p✝ ▸ b✝) b✝
subst_vars
no goals
V : Type u_1
inst✝¹ : Quiver V
W : Type u_5
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
α✝ : Sort ?u.2594
γ✝ : Sort ?u.2596
β✝ : α✝ → γ✝ → Sort ?u.2598
a'✝ : α✝
g✝ : γ✝
b✝ : β✝ a'✝ g✝
⊢ HEq ((_ : a'✝ = a'✝) ▸ b✝) b✝
rfl