[gallais]

New iteration on #2821

Please hold off on commenting for now

[gallais]

Maybe is standing for minus infinity so we should probably use
Relation.Nullary.Construct.Add.Infimum to make our intent more explicit.

This should probably be called degree and be moved to Base.

[gallais]

This should be using the name of the unit polynomial

[gallais]

I think this ought to work?

Suggested change

	≈⟨ B.+-congˡ (-‿distribʳ-* (CR.ring B) β (eval β p)) ⟨
	≈⟨ B.+-congˡ (B.-‿distribʳ-* β (eval β p)) ⟨

[gallais]

Suggested change

	module B = CR B
	open B
	using (distrib)
	renaming
	(_≈_ to _≈B_
	; _+_ to _+B_
	; _*_ to _*B_
	; -_ to -B_
	; setoid to B-Set)
	using (0#; 1#)
	module B = CR B
	open B
	using ()
	renaming
	(Carrier to B)

And then you can use B instead of CR.Carrier B and e.g. _B.+_ instead of _B+_.

[gallais]

Suggested change

	eval-inverse-homomorphic : (β : CR.Carrier B) → (p : Poly) →
	eval‿- : (β : CR.Carrier B) → (p : Poly) →

[gallais]

Define id# (?) and

Suggested change

	x-mapsto-β : (β : CR.Carrier B) → eval β (A0# ∷ A1# ∷ []) ≈B β
	eval-id# : (β : CR.Carrier B) → eval β id# ≈B β

[gallais]

This should go in Poly.Base.Semiring; and be called inject maybe?

[gallais]

Suggested change

	eval-comm : (β : CR.Carrier B) → ∀ (r : A.Carrier) → ⟦ r ⟧ ≈B eval β (ı r)
	eval-inject : (β : CR.Carrier B) → ∀ (r : A.Carrier) → eval β (ı r) B.≈ ⟦ r ⟧

[gallais]

We could lift the constant parameters to an anonymous module.
It should look something like (modulo indentation, etc.)

open RingHomo

-- Now proving the universal property of eval
module _
  (ϕ : RingHomo {ℓ₁} {ℓ₁ L.⊔ ℓ₂} PolyrawRing B.rawRing)
  (ϕ-inject : (r : A) → ⟦ ϕ ⟧ (ı r) ≈B (⟦ r ⟧))
  (β : B) (ϕ-id# : ⟦ ϕ ⟧ id# ≈B β)
  where

  eval-unique : (p : Poly) → ⟦ ϕ ⟧ p ≈B eval β p

[gallais]

Mostly cosmetic changes