F : PFunctor
X : Type ?u.21403
f✝ : X → Obj F X
xs : Path F
a : F.A
f : B F a → M F
i : B F a
x : M F
h : M.mk { fst := a, snd := f } = x
⊢ IsPath ({ fst := a, snd := i } :: xs) x → IsPath xs (f i)
F : PFunctor
X : Type ?u.21403
f✝ : X → Obj F X
xs : Path F
a : F.A
f : B F a → M F
i : B F a
⊢ IsPath ({ fst := a, snd := i } :: xs) (M.mk { fst := a, snd := f }) → IsPath xs (f i)
generalize h : M.mk ⟨a, f⟩ = x
case cons
F : PFunctor
X : Type ?u.21403
f✝¹ : X → Obj F X
xs : Path F
a : F.A
f : B F a → M F
i : B F a
f✝ : B F a → M F
hp : IsPath xs (f✝ i)
h : M.mk { fst := a, snd := f } = M.mk { fst := a, snd := f✝ }
⊢ IsPath xs (f i)
F : PFunctor
X : Type ?u.21403
f✝ : X → Obj F X
xs : Path F
a : F.A
f : B F a → M F
i : B F a
x : M F
h : M.mk { fst := a, snd := f } = x
⊢ IsPath ({ fst := a, snd := i } :: xs) x → IsPath xs (f i)
rintro (_ | ⟨_, _, _, _, rfl, hp⟩)
case cons.refl
F : PFunctor
X : Type ?u.21403
f✝ : X → Obj F X
xs : Path F
a : F.A
f : B F a → M F
i : B F a
hp : IsPath xs (f i)
h : M.mk { fst := a, snd := f } = M.mk { fst := a, snd := f }
⊢ IsPath xs (f i)
case cons
F : PFunctor
X : Type ?u.21403
f✝¹ : X → Obj F X
xs : Path F
a : F.A
f : B F a → M F
i : B F a
f✝ : B F a → M F
hp : IsPath xs (f✝ i)
h : M.mk { fst := a, snd := f } = M.mk { fst := a, snd := f✝ }
⊢ IsPath xs (f i)
cases mk_inj h
no goals
case cons.refl
F : PFunctor
X : Type ?u.21403
f✝ : X → Obj F X
xs : Path F
a : F.A
f : B F a → M F
i : B F a
hp : IsPath xs (f i)
h : M.mk { fst := a, snd := f } = M.mk { fst := a, snd := f }
⊢ IsPath xs (f i)
exact hp