extracted_peanoSurface

formal source

 199  initial := realization_initial R
 200
 201/-- Peano surface for the extracted arithmetic of any realization. -/
 202theorem extracted_peanoSurface (R : LogicRealization) :
 203    PeanoSurface (extracted R) where
 204  zero_ne_step := R.orbit_no_confusion
 205  step_injective := R.orbit_step_injective
 206  induction := R.orbit_induction
 207
 208/-- The natural equivalence between two initial Peano objects. -/
 209noncomputable def equivOfInitial {R S : LogicRealization}
 210    (A : ArithmeticOf R) (B : ArithmeticOf S) : A.peano.carrier ≃ B.peano.carrier where
 211  toFun := (A.initial.lift B.peano).toFun
 212  invFun := (B.initial.lift A.peano).toFun
 213  left_inv := by
 214    intro x
 215    have hcomp :
 216        (PeanoObject.Hom.comp (B.initial.lift A.peano) (A.initial.lift B.peano)).toFun =
 217          (PeanoObject.Hom.id A.peano).toFun :=
 218      A.initial.uniq A.peano
 219        (PeanoObject.Hom.comp (B.initial.lift A.peano) (A.initial.lift B.peano))
 220        (PeanoObject.Hom.id A.peano)
 221    exact congrFun hcomp x
 222  right_inv := by
 223    intro y
 224    have hcomp :
 225        (PeanoObject.Hom.comp (A.initial.lift B.peano) (B.initial.lift A.peano)).toFun =
 226          (PeanoObject.Hom.id B.peano).toFun :=
 227      B.initial.uniq B.peano
 228        (PeanoObject.Hom.comp (A.initial.lift B.peano) (B.initial.lift A.peano))
 229        (PeanoObject.Hom.id B.peano)
 230    exact congrFun hcomp y
 231
 232/-- Canonical arithmetic object for any realization: the initial Peano object.