Graph.lean → Quotient.lean, Quotient.lean → Setquot.lean

GroundZero.lean

@@ -43,7 +43,6 @@ import GroundZero.HITs.Coequalizer
 import GroundZero.HITs.Colimit
 import GroundZero.HITs.Flattening
 import GroundZero.HITs.Generalized
-import GroundZero.HITs.Graph
 import GroundZero.HITs.Int
 import GroundZero.HITs.Interval
 import GroundZero.HITs.Join
@@ -52,6 +51,7 @@ import GroundZero.HITs.Moebius
 import GroundZero.HITs.Pushout
 import GroundZero.HITs.Quotient
 import GroundZero.HITs.Reals
+import GroundZero.HITs.Setquot
 import GroundZero.HITs.Simplicial
 import GroundZero.HITs.Sphere
 import GroundZero.HITs.Suspension

GroundZero/Algebra/Group/Absolutizer.lean

@@ -1,5 +1,5 @@
 import GroundZero.Algebra.Group.Basic
-import GroundZero.HITs.Quotient
+import GroundZero.HITs.Setquot
 
 open GroundZero.Types.Id (ap)
 open GroundZero.Types

GroundZero/Algebra/Group/Action.lean

@@ -1,5 +1,5 @@
 import GroundZero.Algebra.Group.Symmetric
-import GroundZero.HITs.Quotient
+import GroundZero.HITs.Setquot
 
 open GroundZero.Types.Id (ap)
 open GroundZero.Structures

GroundZero/Algebra/Group/Factor.lean

@@ -1,5 +1,5 @@
 import GroundZero.Algebra.Group.Subgroup
-import GroundZero.HITs.Quotient
+import GroundZero.HITs.Setquot
 
 open GroundZero.Types.Equiv (biinv transport)
 open GroundZero.Types.Id (ap)

GroundZero/HITs/Coequalizer.lean

@@ -1,4 +1,4 @@
-import GroundZero.HITs.Graph
+import GroundZero.HITs.Quotient
 
 open GroundZero.Types.Id (ap)
 open GroundZero.Types.Equiv

GroundZero/HITs/Colimit.lean

@@ -1,4 +1,4 @@
-import GroundZero.HITs.Graph
+import GroundZero.HITs.Quotient
 open GroundZero.Types.Equiv (pathoverOfEq)
 
 /-

GroundZero/HITs/Generalized.lean

@@ -1,4 +1,4 @@
-import GroundZero.HITs.Graph
+import GroundZero.HITs.Quotient
 open GroundZero.Types.Equiv (pathoverOfEq)
 
 /-

GroundZero/HITs/Pushout.lean

@@ -1,4 +1,4 @@
-import GroundZero.HITs.Graph
+import GroundZero.HITs.Quotient
 
 open GroundZero.Types.Id (ap)
 open GroundZero.Types.Equiv

GroundZero/HITs/Quotient.lean

@@ -1,104 +1,60 @@
-import GroundZero.HITs.Trunc
+import GroundZero.Types.HEq
 
+open GroundZero.Types.Equiv (apd)
 open GroundZero.Types.Id (ap)
-open GroundZero.Types.Equiv
-open GroundZero.Structures
-open GroundZero.Theorems
 open GroundZero.Types
-open GroundZero
 
 namespace GroundZero.HITs
-universe u v w u' v' w'
-
-hott definition Setquot {A : Type u} (R : A → A → Prop v) := ∥Quotient (λ x y, (R x y).1)∥₀
-
-hott definition Setquot.elem {A : Type u} {R : A → A → Prop v} : A → Setquot R :=
-Trunc.elem ∘ Quotient.elem
-
-hott definition Setquot.sound {A : Type u} {R : A → A → Prop v} {a b : A} :
-  (R a b).1 → @Id (Setquot R) (Setquot.elem a) (Setquot.elem b) :=
-begin intro; dsimp [elem]; apply ap Trunc.elem; apply Quotient.line; assumption end
-
-hott lemma Setquot.set {A : Type u} {R : A → A → Prop v} : hset (Setquot R) :=
-zeroEqvSet.forward (Trunc.uniq 0)
-
-hott definition Setquot.ind {A : Type u} {R : A → A → Prop u'} {π : Setquot R → Type v}
-  (elemπ : Π x, π (Setquot.elem x))
-  (lineπ : Π x y H, elemπ x =[Setquot.sound H] elemπ y)
-  (set   : Π x, hset (π x)) : Π x, π x :=
-begin
-  fapply Trunc.ind;
-  { fapply Quotient.ind; apply elemπ;
-    { intros x y H; apply Id.trans;
-      apply transportComp;
-      apply lineπ } };
-  { intro; apply zeroEqvSet.left; apply set }
-end
-
-attribute [eliminator] Setquot.ind
-
-hott definition Setquot.rec {A : Type u} {R : A → A → Prop u'} {B : Type v}
-  (elemπ : A → B) (lineπ : Π x y, (R x y).fst → elemπ x = elemπ y) (set : hset B) : Setquot R → B :=
-@Setquot.ind A R (λ _, B) elemπ (λ x y H, pathoverOfEq (Setquot.sound H) (lineπ x y H)) (λ _, set)
-
-hott definition Setquot.lift₂ {A : Type u} {R₁ : A → A → Prop u'} {B : Type v} {R₂ : B → B → Prop v'}
-  {γ : Type w} (R₁refl : Π x, (R₁ x x).fst) (R₂refl : Π x, (R₂ x x).fst) (f : A → B → γ)
-  (h : hset γ) (p : Π a₁ a₂ b₁ b₂, (R₁ a₁ b₁).fst → (R₂ a₂ b₂).fst → f a₁ a₂ = f b₁ b₂) : Setquot R₁ → Setquot R₂ → γ :=
-begin
-  fapply @Setquot.rec A R₁ (Setquot R₂ → γ);
-  { intro x; fapply Setquot.rec; exact f x;
-    { intros y₁ y₂ H; apply p; apply R₁refl; exact H };
-    { assumption } };
-  { intros x y H; apply Theorems.funext; fapply Setquot.ind;
-    { intro z; apply p; assumption; apply R₂refl };
-    { intros; apply h };
-    { intros; apply Structures.propIsSet; apply h } };
-  { apply zeroEqvSet.forward; apply Structures.piRespectsNType 0;
-    intros; apply zeroEqvSet.left; apply h }
-end
-
-hott definition Relquot {A : Type u} (s : eqrel A) := Setquot s.rel
-
-hott definition Relquot.elem {A : Type u} {s : eqrel A} : A → Relquot s :=
-Setquot.elem
-
-hott definition Relquot.sound {A : Type u} {s : eqrel A} {a b : A} :
-  s.apply a b → @Id (Relquot s) (Relquot.elem a) (Relquot.elem b) :=
-Setquot.sound
-
-hott corollary Relquot.set {A : Type u} {s : eqrel A} : hset (Relquot s) :=
-by apply Setquot.set
-
-hott definition Relquot.ind {A : Type u} {s : eqrel A}
-  {π : Relquot s → Type v}
-  (elemπ : Π x, π (Relquot.elem x))
-  (lineπ : Π x y H, elemπ x =[Relquot.sound H] elemπ y)
-  (set   : Π x, hset (π x)) : Π x, π x :=
-Setquot.ind elemπ lineπ set
-
-attribute [eliminator] Relquot.ind
-
-hott definition Relquot.indProp {A : Type u} {s : eqrel A}
-  {π : Relquot s → Type v} (elemπ : Π x, π (Relquot.elem x))
-  (propπ : Π x, prop (π x)) : Π x, π x :=
-begin
-  intro x; induction x; apply elemπ; apply propπ;
-  apply Structures.propIsSet; apply propπ
-end
-
-hott definition Relquot.rec {A : Type u} {B : Type v} {s : eqrel A}
-  (elemπ : A → B)
-  (lineπ : Π x y, s.apply x y → elemπ x = elemπ y)
-  (set   : hset B) : Relquot s → B :=
-by apply Setquot.rec <;> assumption
-
-hott definition Relquot.lift₂ {A : Type u} {B : Type v} {γ : Type w}
-  {s₁ : eqrel A} {s₂ : eqrel B} (f : A → B → γ) (h : hset γ)
-  (p : Π a₁ a₂ b₁ b₂, s₁.apply a₁ b₁ → s₂.apply a₂ b₂ → f a₁ a₂ = f b₁ b₂) :
-  Relquot s₁ → Relquot s₂ → γ :=
-begin
-  fapply Setquot.lift₂; apply s₁.iseqv.fst; apply s₂.iseqv.fst;
-  repeat { assumption }
-end
+universe u v w
+
+inductive Quotient.rel {A : Type u} (R : A → A → Type v) : A → A → Prop
+| line {n m : A} : R n m → rel R n m
+
+hott axiom Quotient {A : Type u} (R : A → A → Type v) : Type (max u v) :=
+Resize.{u, v} (Quot (Quotient.rel R))
+
+namespace Quotient
+  hott axiom elem {A : Type u} {R : A → A → Type w} : A → Quotient R :=
+  Resize.intro ∘ Quot.mk (rel R)
+
+  hott opaque line {A : Type u} {R : A → A → Type w} {x y : A}
+    (H : R x y) : @elem A R x = @elem A R y :=
+  trustHigherCtor (congrArg Resize.intro (Quot.sound (rel.line H)))
+
+  hott axiom rec {A : Type u} {B : Type v} {R : A → A → Type w}
+    (f : A → B) (H : Π x y, R x y → f x = f y) : Quotient R → B :=
+  λ x, Quot.withUseOf H (Quot.lift f (λ a b, λ (rel.line ε), elimEq (H a b ε)) x.elim) x.elim
+
+  @[eliminator] hott axiom ind {A : Type u} {R : A → A → Type v} {B : Quotient R → Type w}
+    (f : Π x, B (elem x)) (ε : Π x y H, f x =[line H] f y) : Π x, B x :=
+  λ x, Quot.withUseOf ε (@Quot.hrecOn A (rel R) (B ∘ Resize.intro) x.elim f
+    (λ a b, λ (rel.line H), HEq.fromPathover (line H) (ε a b H))) x.elim
+
+  hott opaque recβrule {A : Type u} {B : Type v} {R : A → A → Type w}
+    (f : A → B) (ε : Π x y, R x y → f x = f y) {x y : A}
+    (g : R x y) : ap (rec f ε) (line g) = ε x y g :=
+  trustCoherence
+
+  hott opaque indβrule {A : Type u} {R : A → A → Type v} {B : Quotient R → Type w}
+    (f : Π x, B (elem x)) (ε : Π x y H, f x =[line H] f y)
+    {x y : A} (g : R x y) : apd (ind f ε) (line g) = ε x y g :=
+  trustCoherence
+
+  attribute [irreducible] Quotient
+
+  section
+    variable {A : Type u} {R : A → A → Type v} {B : Quotient R → Type w}
+             (f : Π x, B (elem x)) (ε₁ ε₂ : Π x y H, f x =[line H] f y)
+
+    #failure ind f ε₁ ≡ ind f ε₂
+  end
+
+  section
+    variable {A : Type u} {R : A → A → Type v} {B : Type w}
+             (f : A → B) (ε₁ ε₂ : Π x y, R x y → f x = f y)
+
+    #failure rec f ε₁ ≡ rec f ε₂
+  end
+end Quotient
 
 end GroundZero.HITs

GroundZero/HITs/Setquot.lean

@@ -0,0 +1,104 @@
+import GroundZero.HITs.Trunc
+
+open GroundZero.Types.Id (ap)
+open GroundZero.Types.Equiv
+open GroundZero.Structures
+open GroundZero.Theorems
+open GroundZero.Types
+open GroundZero
+
+namespace GroundZero.HITs
+universe u v w u' v' w'
+
+hott definition Setquot {A : Type u} (R : A → A → Prop v) := ∥Quotient (λ x y, (R x y).1)∥₀
+
+hott definition Setquot.elem {A : Type u} {R : A → A → Prop v} : A → Setquot R :=
+Trunc.elem ∘ Quotient.elem
+
+hott definition Setquot.sound {A : Type u} {R : A → A → Prop v} {a b : A} :
+  (R a b).1 → @Id (Setquot R) (Setquot.elem a) (Setquot.elem b) :=
+begin intro; dsimp [elem]; apply ap Trunc.elem; apply Quotient.line; assumption end
+
+hott lemma Setquot.set {A : Type u} {R : A → A → Prop v} : hset (Setquot R) :=
+zeroEqvSet.forward (Trunc.uniq 0)
+
+hott definition Setquot.ind {A : Type u} {R : A → A → Prop u'} {π : Setquot R → Type v}
+  (elemπ : Π x, π (Setquot.elem x))
+  (lineπ : Π x y H, elemπ x =[Setquot.sound H] elemπ y)
+  (set   : Π x, hset (π x)) : Π x, π x :=
+begin
+  fapply Trunc.ind;
+  { fapply Quotient.ind; apply elemπ;
+    { intros x y H; apply Id.trans;
+      apply transportComp;
+      apply lineπ } };
+  { intro; apply zeroEqvSet.left; apply set }
+end
+
+attribute [eliminator] Setquot.ind
+
+hott definition Setquot.rec {A : Type u} {R : A → A → Prop u'} {B : Type v}
+  (elemπ : A → B) (lineπ : Π x y, (R x y).fst → elemπ x = elemπ y) (set : hset B) : Setquot R → B :=
+@Setquot.ind A R (λ _, B) elemπ (λ x y H, pathoverOfEq (Setquot.sound H) (lineπ x y H)) (λ _, set)
+
+hott definition Setquot.lift₂ {A : Type u} {R₁ : A → A → Prop u'} {B : Type v} {R₂ : B → B → Prop v'}
+  {γ : Type w} (R₁refl : Π x, (R₁ x x).fst) (R₂refl : Π x, (R₂ x x).fst) (f : A → B → γ)
+  (h : hset γ) (p : Π a₁ a₂ b₁ b₂, (R₁ a₁ b₁).fst → (R₂ a₂ b₂).fst → f a₁ a₂ = f b₁ b₂) : Setquot R₁ → Setquot R₂ → γ :=
+begin
+  fapply @Setquot.rec A R₁ (Setquot R₂ → γ);
+  { intro x; fapply Setquot.rec; exact f x;
+    { intros y₁ y₂ H; apply p; apply R₁refl; exact H };
+    { assumption } };
+  { intros x y H; apply Theorems.funext; fapply Setquot.ind;
+    { intro z; apply p; assumption; apply R₂refl };
+    { intros; apply h };
+    { intros; apply Structures.propIsSet; apply h } };
+  { apply zeroEqvSet.forward; apply Structures.piRespectsNType 0;
+    intros; apply zeroEqvSet.left; apply h }
+end
+
+hott definition Relquot {A : Type u} (s : eqrel A) := Setquot s.rel
+
+hott definition Relquot.elem {A : Type u} {s : eqrel A} : A → Relquot s :=
+Setquot.elem
+
+hott definition Relquot.sound {A : Type u} {s : eqrel A} {a b : A} :
+  s.apply a b → @Id (Relquot s) (Relquot.elem a) (Relquot.elem b) :=
+Setquot.sound
+
+hott corollary Relquot.set {A : Type u} {s : eqrel A} : hset (Relquot s) :=
+by apply Setquot.set
+
+hott definition Relquot.ind {A : Type u} {s : eqrel A}
+  {π : Relquot s → Type v}
+  (elemπ : Π x, π (Relquot.elem x))
+  (lineπ : Π x y H, elemπ x =[Relquot.sound H] elemπ y)
+  (set   : Π x, hset (π x)) : Π x, π x :=
+Setquot.ind elemπ lineπ set
+
+attribute [eliminator] Relquot.ind
+
+hott definition Relquot.indProp {A : Type u} {s : eqrel A}
+  {π : Relquot s → Type v} (elemπ : Π x, π (Relquot.elem x))
+  (propπ : Π x, prop (π x)) : Π x, π x :=
+begin
+  intro x; induction x; apply elemπ; apply propπ;
+  apply Structures.propIsSet; apply propπ
+end
+
+hott definition Relquot.rec {A : Type u} {B : Type v} {s : eqrel A}
+  (elemπ : A → B)
+  (lineπ : Π x y, s.apply x y → elemπ x = elemπ y)
+  (set   : hset B) : Relquot s → B :=
+by apply Setquot.rec <;> assumption
+
+hott definition Relquot.lift₂ {A : Type u} {B : Type v} {γ : Type w}
+  {s₁ : eqrel A} {s₂ : eqrel B} (f : A → B → γ) (h : hset γ)
+  (p : Π a₁ a₂ b₁ b₂, s₁.apply a₁ b₁ → s₂.apply a₂ b₂ → f a₁ a₂ = f b₁ b₂) :
+  Relquot s₁ → Relquot s₂ → γ :=
+begin
+  fapply Setquot.lift₂; apply s₁.iseqv.fst; apply s₂.iseqv.fst;
+  repeat { assumption }
+end
+
+end GroundZero.HITs