apply Trunc.lift_mk
α : Sort u_1
β : Sort u_2
s : Setoid α
a : α
f : (b : α) → ⟦b⟧ = ⟦a⟧ → β
h : ∀ (a_1 b : α) (ha : ⟦a_1⟧ = ⟦a⟧) (hb : ⟦b⟧ = ⟦a⟧), f a_1 ha = f b hb
⊢ Trunc.lift (fun x => f ↑x ⋯) ⋯ (toTrunc ⟦a⟧) = f a ⋯
no goals