F : PFunctor
X : Type ?u.20790
f✝ : X → Obj F X
xs : Path F
a 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 → a = a'
F : PFunctor
X : Type ?u.20790
f✝ : X → Obj F X
xs : Path F
a 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 }) → a = a'
generalize h : M.mk ⟨a, f⟩ = x
case cons
F : PFunctor
X : Type ?u.20790
f✝¹ : X → Obj F X
xs : Path F
a a' : F.A
f : B F a → M F
i : B F a'
f✝ : B F a' → M F
a✝ : IsPath xs (f✝ i)
h : M.mk { fst := a, snd := f } = M.mk { fst := a', snd := f✝ }
⊢ a = a'
F : PFunctor
X : Type ?u.20790
f✝ : X → Obj F X
xs : Path F
a 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 → a = a'
rintro (_ | ⟨_, _, _, _, rfl, _⟩)
case cons.refl
F : PFunctor
X : Type ?u.20790
f✝ : X → Obj F X
xs : Path F
a : F.A
f : B F a → M F
i : B F a
a✝ : IsPath xs (f i)
h : M.mk { fst := a, snd := f } = M.mk { fst := a, snd := f }
⊢ a = a
case cons
F : PFunctor
X : Type ?u.20790
f✝¹ : X → Obj F X
xs : Path F
a a' : F.A
f : B F a → M F
i : B F a'
f✝ : B F a' → M F
a✝ : IsPath xs (f✝ i)
h : M.mk { fst := a, snd := f } = M.mk { fst := a', snd := f✝ }
⊢ a = a'
cases mk_inj h
no goals
case cons.refl
F : PFunctor
X : Type ?u.20790
f✝ : X → Obj F X
xs : Path F
a : F.A
f : B F a → M F
i : B F a
a✝ : IsPath xs (f i)
h : M.mk { fst := a, snd := f } = M.mk { fst := a, snd := f }
⊢ a = a
rfl