search

JetBrains / arend-lib

Apache License 2.0
79 stars 23 forks source link

Proven that the radical of the ideal generated by two elements is equal to the radical of the ideal generated by powers of these elements #52

Closed TurtlePU closed 2 years ago

TurtlePU commented 2 years ago

Closes #41

ice1000 commented 2 years ago 
--- Checking arend-lib ---
Error:  Category.Subobj:12:18: The sort \hType of 'subobj' does not fit into the expected sort \Set
  In: Subobj
Error:  Category.Subobj:34:18: The sort \hType of 'regSubobj' does not fit into the expected sort \Set
  In: RegularSubobj
Error:  Category.Topos.Sheaf:277:8: Type mismatch
  Expected type: Precat
    Actual type:
    Precat (\Sigma (y : ObOver {framePresPreorder P} j.1)
      (TruncP (\Sigma (j : \Sigma (j : J) (x : P.E) ((g j).1.1 x)) (Cover1 {P} y.1 j.2)))) {
      | Hom => \lam (x : \Sigma (y : ObOver {framePresPreorder P} j.1)
        (TruncP (\Sigma (j : \Sigma (j : J) (x : P.E) ((g j).1.1 x)) (Cover1 {P} y.1 j.2))))
        (y : \Sigma (y : ObOver {framePresPreorder P} j.1)
          (TruncP (\Sigma (j : \Sigma (j : J) (x : P.E) ((g j).1.1 x)) (Cover1 {P} y.1 j.2)))) => Hom x.1 y.1
      | id => \lam (x : \Sigma (y : ObOver {framePresPreorder P} j.1)
        (TruncP (\Sigma (j : \Sigma (j : J) (x : P.E) ((g j).1.1 x)) (Cover1 {P} y.1 j.2)))) => id x.1
      | o => \lam {X Y Z : \Sigma (y : ObOver {framePresPreorder P} j.1)
        (TruncP (\Sigma (j : \Sigma (j : J) (x : P.E) ((g j).1.1 x)) (Cover1 {P} y.1 j.2)))} => (∘) {X.1} {Y.1} {Z.1}
    }
  In: subPrecat {slicePrecat {framePresPreorder P} j.1} {\Sigma (y : ObOver {framePresPreorder P} j.1)
        (TruncP (\Sigma (j : \Sigma (j : J) (x : P.E) ((g j).1.1 x)) (Cover1 {P} y.1 j.2)))}
        (\lam (p : \Sigma (y : ObOver {framePresPreorder P} j.1)
          (TruncP (\Sigma (j : \Sigma (j : J) (x : P.E) ((g j).1.1 x)) (Cover1 {P} y.1 j.2)))) => p.1)
Error:  Category.Topos.Sheaf:312:12: Type mismatch
  Expected type: Precat
    Actual type:
    Precat (\Sigma (y : ObOver {framePresPreorder P} a) (TruncP (\Sigma (j : J) (Cover1 {P} y.1 (g j))))) {
      | Hom => \lam (x : \Sigma (y : ObOver {framePresPreorder P} a) (TruncP (\Sigma (j : J) (Cover1 {P} y.1 (g j)))))
        (y : \Sigma (y : ObOver {framePresPreorder P} a) (TruncP (\Sigma (j : J) (Cover1 {P} y.1 (g j))))) => Hom x.1 y.1
      | id => \lam (x : \Sigma (y : ObOver {framePresPreorder P} a) (TruncP (\Sigma (j : J) (Cover1 {P} y.1 (g j))))) => id x.1
      | o => \lam {X Y Z : \Sigma (y : ObOver {framePresPreorder P} a) (TruncP (\Sigma (j : J) (Cover1 {P} y.1 (g j))))} =>
        (∘) {X.1} {Y.1} {Z.1}
    }
  In: subPrecat {slicePrecat {framePresPreorder P} a}
        {\Sigma (y : ObOver {framePresPreorder P} a) (TruncP (\Sigma (j : J) (Cover1 {P} y.1 (g j))))}
        (\lam (p : \Sigma (y : ObOver {framePresPreorder P} a) (TruncP (\Sigma (j : J) (Cover1 {P} y.1 (g j))))) => p.1)
Error:  Category.Topos.Sheaf:316:12: Type mismatch
  Expected type: Precat
    Actual type:
    Precat (\Sigma (y : ObOver {framePresPreorder P} a) (TruncP (\Sigma (j : J) (Cover1 {P} y.1 (g j))))) {
      | Hom => \lam (x : \Sigma (y : ObOver {framePresPreorder P} a) (TruncP (\Sigma (j : J) (Cover1 {P} y.1 (g j)))))
        (y : \Sigma (y : ObOver {framePresPreorder P} a) (TruncP (\Sigma (j : J) (Cover1 {P} y.1 (g j))))) => Hom x.1 y.1
      | id => \lam (x : \Sigma (y : ObOver {framePresPreorder P} a) (TruncP (\Sigma (j : J) (Cover1 {P} y.1 (g j))))) => id x.1
      | o => \lam {X Y Z : \Sigma (y : ObOver {framePresPreorder P} a) (TruncP (\Sigma (j : J) (Cover1 {P} y.1 (g j))))} =>
        (∘) {X.1} {Y.1} {Z.1}
    }
  In: subPrecat {slicePrecat {framePresPreorder P} a}
        {\Sigma (y : ObOver {framePresPreorder P} a) (TruncP (\Sigma (j : J) (Cover1 {P} y.1 (g j))))}
        (\lam (p : \Sigma (y : ObOver {framePresPreorder P} a) (TruncP (\Sigma (j : J) (Cover1 {P} y.1 (g j))))) => p.1)
Error:  Category.Topos.Sheaf:319:12: Type mismatch
  Expected type: Precat
    Actual type:
    Precat (\Sigma (y : ObOver {framePresPreorder P} b) (TruncP (\Sigma (j : J) (Cover1 {P} y.1 (g j))))) {
      | Hom => \lam (x : \Sigma (y : ObOver {framePresPreorder P} b) (TruncP (\Sigma (j : J) (Cover1 {P} y.1 (g j)))))
        (y : \Sigma (y : ObOver {framePresPreorder P} b) (TruncP (\Sigma (j : J) (Cover1 {P} y.1 (g j))))) => Hom x.1 y.1
      | id => \lam (x : \Sigma (y : ObOver {framePresPreorder P} b) (TruncP (\Sigma (j : J) (Cover1 {P} y.1 (g j))))) => id x.1
      | o => \lam {X Y Z : \Sigma (y : ObOver {framePresPreorder P} b) (TruncP (\Sigma (j : J) (Cover1 {P} y.1 (g j))))} =>
        (∘) {X.1} {Y.1} {Z.1}
    }
  In: subPrecat {slicePrecat {framePresPreorder P} b}
        {\Sigma (y : ObOver {framePresPreorder P} b) (TruncP (\Sigma (j : J) (Cover1 {P} y.1 (g j))))}
        (\lam (p : \Sigma (y : ObOver {framePresPreorder P} b) (TruncP (\Sigma (j : J) (Cover1 {P} y.1 (g j))))) => p.1)