Is recursively defined type considerable?

Stream: mathlib4

[Guo Zixun]

For example, if we want to take about MvPolynomial (Fin n) R is equivant with Polynomial (Polynomial ... (Polynomial R)) , the following strange codes seem to work:

-- we use the product because the `CommSemiring` instance can't be found automatically
@[reducible]
noncomputable def nthPolynomial.{u} (R : Type u) [CommSemiring R] (n : ℕ) : (T : Type u) × (CommSemiring T) :=
  match n with
  | 0 => ⟨R, inferInstance⟩
  | Nat.succ m =>
    letI commSemiring := (nthPolynomial R m).2
    ⟨Polynomial ((nthPolynomial R m).1), inferInstance⟩
termination_by n


noncomputable instance {R : Type*} [CommSemiring R] (n : ℕ) : CommSemiring (nthPolynomial R n).1 :=
  (nthPolynomial R n).2

noncomputable instance alg_instance {R : Type*} [CommSemiring R] (n : ℕ) : Algebra R (nthPolynomial R n).1 :=
  match n with
  | 0 => by show Algebra R R; infer_instance
  | Nat.succ m =>
    letI commSemiring := (nthPolynomial R m).2
    letI algebra := alg_instance  m (R := R)
    by show Algebra R (Polynomial ((nthPolynomial R m).1)); infer_instance

@[reducible]
noncomputable def nthPolynomialEval {R : Type*} [CommSemiring R] (n : ℕ) (σ : Fin n -> R) : (nthPolynomial R n).1 →+* R :=
  match n with
  | 0 => RingHom.id R
  | Nat.succ m =>
    let eval := nthPolynomialEval m
    fun p => Polynomial.eval (fun i => eval (Polynomial.coeff p i)) p

noncomputable def finEquiv (R : Type*) [CommSemiring R] (n : ℕ) : (MvPolynomial (Fin n) R) ≃ₐ[R] (nthPolynomial R n).1 :=
  match n with
  | 0 => isEmptyAlgEquiv R (Fin 0)
  | Nat.succ m =>
    let equiv1 := finSuccEquiv R m
    let equiv2 := finEquiv R m
    by
      show (MvPolynomial (Fin (Nat.succ m)) R) ≃ₐ[R] Polynomial (nthPolynomial R m).1
      exact equiv1.trans (Polynomial.mapAlgEquiv equiv2)

noncomputable def finEquiv_zero {R : Type*} [CommSemiring R] : (MvPolynomial (Fin 0) R) ≃ₐ[R] R := finEquiv R 0
noncomputable def finEquiv_one {R : Type*} [CommSemiring R] : (MvPolynomial (Fin 1) R) ≃ₐ[R] Polynomial R := finEquiv R 1
noncomputable def finEquiv_two {R : Type*} [CommSemiring R] : (MvPolynomial (Fin 2) R) ≃ₐ[R] Polynomial (Polynomial R) := finEquiv R 2

But I think using a recusive funtion to define type may also bring terrible things like equiv1.trans (Polynomial.mapAlgEquiv equiv2) failing in type checking unless mannuly show the type is definitionally equal. Is there any other way to generally say a similar results?

[Edward van de Meent]

perhaps what we really need here is a kind of LawfulMonad that is able to consider type class requirements...

[Edward van de Meent]

(since the thing here basically is that there is Polynomial.join : (Polynomial (Polynomial R)) -> Polynomial R which together with Polynomial.C as pure gives a monad)

[Edward van de Meent]

i suppose the real level to express this fact would be in category theory?

[Guo Zixun]

Edward van de Meent said:

perhaps what we really need here is a kind of LawfulMonad that is able to consider type class requirements...

Sorry but I don't quite understand how the fact that Polynomial is a LawfunMonad can help here?

[Edward van de Meent]

looking back, it seems that indeed i was confused

[Guo Zixun]

Edward van de Meent said:

looking back, it seems that indeed i was confused

Oh, sorry.