Function with domain (Fin n -> Quotient r)

Stream: general

[Jiatong Yang]

variable (A : Type) (r : Setoid A)
variable (n : Nat) (B : Type)

variable (map₀ : (Fin n → A) → B)
variable (mapEq : ∀ (f g : Fin n → A), (∀ i, r.r (f i) (g i)) → map₀ f = map₀ g)

def map : (Fin n → Quotient r) → B := sorry

How to fill in this "sorry"?
I think use of Choice can be avoided because of finiteness of Fin n.

[Filippo A. E. Nuccio]

Are you aware of these results?

[Jiatong Yang]

Do you mean I should do induction on n?

[Jiatong Yang]

Or does it hold if Fin n is replaced by any X?

[Trebor Huang]

#5576 ?

[Filippo A. E. Nuccio]

No, the "induction" that you see there is not the "natural induction" you might be used to. It rather refers to an "induction" used to define a function out of a certain type. The point here is that docs#Quotient.lift allows yo to define a function on a quotient if you know that it sends congruent elements to the same image. You can upgrade your r to an equivalence relation on Fin n -> A and then apply this result.

[Jiatong Yang]

Thank you and I can fill it now.