C : Type u
inst✝⁷ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category D
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
⊢ ∀ (X : C) (S : Cover J X), IsIso (Cover.toMultiequalizer S (plusObj J P))
C : Type u
inst✝⁷ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category D
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
⊢ Presheaf.IsSheaf J (plusObj J P)
rw [Presheaf.isSheaf_iff_multiequalizer]
C : Type u
inst✝⁷ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category D
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
S : Cover J X
⊢ IsIso (Cover.toMultiequalizer S (plusObj J P))
C : Type u
inst✝⁷ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category D
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
⊢ ∀ (X : C) (S : Cover J X), IsIso (Cover.toMultiequalizer S (plusObj J P))
intro X S
C : Type u
inst✝⁷ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category D
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
S : Cover J X
⊢ IsIso ((forget D).map (Cover.toMultiequalizer S (plusObj J P)))
C : Type u
inst✝⁷ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category D
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
S : Cover J X
⊢ IsIso (Cover.toMultiequalizer S (plusObj J P))
apply @isIso_of_reflects_iso _ _ _ _ _ _ _ (forget D) ?_
C : Type u
inst✝⁷ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category D
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
S : Cover J X
⊢ Function.Bijective ((forget D).map (Cover.toMultiequalizer S (plusObj J P)))
C : Type u
inst✝⁷ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category D
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
S : Cover J X
⊢ IsIso ((forget D).map (Cover.toMultiequalizer S (plusObj J P)))
rw [isIso_iff_bijective]
case left
C : Type u
inst✝⁷ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category D
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
S : Cover J X
⊢ Function.Injective ((forget D).map (Cover.toMultiequalizer S (plusObj J P)))

case right
C : Type u
inst✝⁷ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category D
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
S : Cover J X
⊢ Function.Surjective ((forget D).map (Cover.toMultiequalizer S (plusObj J P)))
C : Type u
inst✝⁷ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category D
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
S : Cover J X
⊢ Function.Bijective ((forget D).map (Cover.toMultiequalizer S (plusObj J P)))
constructor
case left
C : Type u
inst✝⁷ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category D
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
S : Cover J X
x y : (forget D).obj ((plusObj J P).obj X.op)
h :
  (forget D).map (Cover.toMultiequalizer S (plusObj J P)) x = (forget D).map (Cover.toMultiequalizer S (plusObj J P)) y
⊢ x = y
case left
C : Type u
inst✝⁷ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category D
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
S : Cover J X
⊢ Function.Injective ((forget D).map (Cover.toMultiequalizer S (plusObj J P)))
intro x y h
case left
C : Type u
inst✝⁷ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category D
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
S : Cover J X
x y : (forget D).obj ((plusObj J P).obj X.op)
h :
  (forget D).map (Cover.toMultiequalizer S (plusObj J P)) x = (forget D).map (Cover.toMultiequalizer S (plusObj J P)) y
⊢ ∀ (I : Cover.Arrow S), (forget D).map ((plusObj J P).map I.f.op) x = (forget D).map ((plusObj J P).map I.f.op) y
case left
C : Type u
inst✝⁷ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category D
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
S : Cover J X
x y : (forget D).obj ((plusObj J P).obj X.op)
h :
  (forget D).map (Cover.toMultiequalizer S (plusObj J P)) x = (forget D).map (Cover.toMultiequalizer S (plusObj J P)) y
⊢ x = y
apply sep P S _ _
case left
C : Type u
inst✝⁷ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category D
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
S : Cover J X
x y : (forget D).obj ((plusObj J P).obj X.op)
h :
  (forget D).map (Cover.toMultiequalizer S (plusObj J P)) x = (forget D).map (Cover.toMultiequalizer S (plusObj J P)) y
I : Cover.Arrow S
⊢ (forget D).map ((plusObj J P).map I.f.op) x = (forget D).map ((plusObj J P).map I.f.op) y
case left
C : Type u
inst✝⁷ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category D
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
S : Cover J X
x y : (forget D).obj ((plusObj J P).obj X.op)
h :
  (forget D).map (Cover.toMultiequalizer S (plusObj J P)) x = (forget D).map (Cover.toMultiequalizer S (plusObj J P)) y
⊢ ∀ (I : Cover.Arrow S), (forget D).map ((plusObj J P).map I.f.op) x = (forget D).map ((plusObj J P).map I.f.op) y
intro I
case left
C : Type u
inst✝⁷ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category D
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
S : Cover J X
x y : (forget D).obj ((plusObj J P).obj X.op)
I : Cover.Arrow S
h :
  ↑(Meq.equiv (plusObj J P) S) ((forget D).map (Cover.toMultiequalizer S (plusObj J P)) x) =
    ↑(Meq.equiv (plusObj J P) S) ((forget D).map (Cover.toMultiequalizer S (plusObj J P)) y)
⊢ (forget D).map ((plusObj J P).map I.f.op) x = (forget D).map ((plusObj J P).map I.f.op) y
case left
C : Type u
inst✝⁷ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category D
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
S : Cover J X
x y : (forget D).obj ((plusObj J P).obj X.op)
h :
  (forget D).map (Cover.toMultiequalizer S (plusObj J P)) x = (forget D).map (Cover.toMultiequalizer S (plusObj J P)) y
I : Cover.Arrow S
⊢ (forget D).map ((plusObj J P).map I.f.op) x = (forget D).map ((plusObj J P).map I.f.op) y
apply_fun Meq.equiv _ _  at h
case left
C : Type u
inst✝⁷ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category D
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
S : Cover J X
x y : (forget D).obj ((plusObj J P).obj X.op)
I : Cover.Arrow S
h :
  ↑(↑(Meq.equiv (plusObj J P) S) ((forget D).map (Cover.toMultiequalizer S (plusObj J P)) x)) I =
    ↑(↑(Meq.equiv (plusObj J P) S) ((forget D).map (Cover.toMultiequalizer S (plusObj J P)) y)) I
⊢ (forget D).map ((plusObj J P).map I.f.op) x = (forget D).map ((plusObj J P).map I.f.op) y
case left
C : Type u
inst✝⁷ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category D
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
S : Cover J X
x y : (forget D).obj ((plusObj J P).obj X.op)
I : Cover.Arrow S
h :
  ↑(Meq.equiv (plusObj J P) S) ((forget D).map (Cover.toMultiequalizer S (plusObj J P)) x) =
    ↑(Meq.equiv (plusObj J P) S) ((forget D).map (Cover.toMultiequalizer S (plusObj J P)) y)
⊢ (forget D).map ((plusObj J P).map I.f.op) x = (forget D).map ((plusObj J P).map I.f.op) y
apply_fun fun e => e I  at h
no goals
case left
C : Type u
inst✝⁷ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category D
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
S : Cover J X
x y : (forget D).obj ((plusObj J P).obj X.op)
I : Cover.Arrow S
h :
  ↑(↑(Meq.equiv (plusObj J P) S) ((forget D).map (Cover.toMultiequalizer S (plusObj J P)) x)) I =
    ↑(↑(Meq.equiv (plusObj J P) S) ((forget D).map (Cover.toMultiequalizer S (plusObj J P)) y)) I
⊢ (forget D).map ((plusObj J P).map I.f.op) x = (forget D).map ((plusObj J P).map I.f.op) y
convert h <;> erw [Meq.equiv_apply, ← comp_apply, Multiequalizer.lift_ι]
case right
C : Type u
inst✝⁷ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category D
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
S : Cover J X
x : (forget D).obj (multiequalizer (Cover.index S (plusObj J P)))
⊢ ∃ a, (forget D).map (Cover.toMultiequalizer S (plusObj J P)) a = x
case right
C : Type u
inst✝⁷ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category D
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
S : Cover J X
⊢ Function.Surjective ((forget D).map (Cover.toMultiequalizer S (plusObj J P)))
rintro (x : (multiequalizer (S.index _) : D))
case right.intro
C : Type u
inst✝⁷ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category D
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
S : Cover J X
x : (forget D).obj (multiequalizer (Cover.index S (plusObj J P)))
t : (forget D).obj ((plusObj J P).obj X.op)
ht : Meq.mk S t = ↑(Meq.equiv (plusObj J P) S) x
⊢ ∃ a, (forget D).map (Cover.toMultiequalizer S (plusObj J P)) a = x
case right
C : Type u
inst✝⁷ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category D
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
S : Cover J X
x : (forget D).obj (multiequalizer (Cover.index S (plusObj J P)))
⊢ ∃ a, (forget D).map (Cover.toMultiequalizer S (plusObj J P)) a = x
obtain ⟨t, ht⟩ := exists_of_sep P hsep X S (Meq.equiv _ _ x)
case right.intro
C : Type u
inst✝⁷ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category D
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
S : Cover J X
x : (forget D).obj (multiequalizer (Cover.index S (plusObj J P)))
t : (forget D).obj ((plusObj J P).obj X.op)
ht : Meq.mk S t = ↑(Meq.equiv (plusObj J P) S) x
⊢ (forget D).map (Cover.toMultiequalizer S (plusObj J P)) t = x
case right.intro
C : Type u
inst✝⁷ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category D
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
S : Cover J X
x : (forget D).obj (multiequalizer (Cover.index S (plusObj J P)))
t : (forget D).obj ((plusObj J P).obj X.op)
ht : Meq.mk S t = ↑(Meq.equiv (plusObj J P) S) x
⊢ ∃ a, (forget D).map (Cover.toMultiequalizer S (plusObj J P)) a = x
use t
case right.intro.a
C : Type u
inst✝⁷ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category D
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
S : Cover J X
x : (forget D).obj (multiequalizer (Cover.index S (plusObj J P)))
t : (forget D).obj ((plusObj J P).obj X.op)
ht : Meq.mk S t = ↑(Meq.equiv (plusObj J P) S) x
⊢ ↑(Meq.equiv (plusObj J P) S) ((forget D).map (Cover.toMultiequalizer S (plusObj J P)) t) =
    ↑(Meq.equiv (plusObj J P) S) x
case right.intro
C : Type u
inst✝⁷ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category D
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
S : Cover J X
x : (forget D).obj (multiequalizer (Cover.index S (plusObj J P)))
t : (forget D).obj ((plusObj J P).obj X.op)
ht : Meq.mk S t = ↑(Meq.equiv (plusObj J P) S) x
⊢ (forget D).map (Cover.toMultiequalizer S (plusObj J P)) t = x
apply (Meq.equiv _ _).injective
case right.intro.a
C : Type u
inst✝⁷ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category D
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
S : Cover J X
x : (forget D).obj (multiequalizer (Cover.index S (plusObj J P)))
t : (forget D).obj ((plusObj J P).obj X.op)
ht : Meq.mk S t = ↑(Meq.equiv (plusObj J P) S) x
⊢ ↑(Meq.equiv (plusObj J P) S) ((forget D).map (Cover.toMultiequalizer S (plusObj J P)) t) = Meq.mk S t
case right.intro.a
C : Type u
inst✝⁷ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category D
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
S : Cover J X
x : (forget D).obj (multiequalizer (Cover.index S (plusObj J P)))
t : (forget D).obj ((plusObj J P).obj X.op)
ht : Meq.mk S t = ↑(Meq.equiv (plusObj J P) S) x
⊢ ↑(Meq.equiv (plusObj J P) S) ((forget D).map (Cover.toMultiequalizer S (plusObj J P)) t) =
    ↑(Meq.equiv (plusObj J P) S) x
rw [← ht]
case right.intro.a.h
C : Type u
inst✝⁷ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category D
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
S : Cover J X
x : (forget D).obj (multiequalizer (Cover.index S (plusObj J P)))
t : (forget D).obj ((plusObj J P).obj X.op)
ht : Meq.mk S t = ↑(Meq.equiv (plusObj J P) S) x
i : Cover.Arrow S
⊢ ↑(↑(Meq.equiv (plusObj J P) S) ((forget D).map (Cover.toMultiequalizer S (plusObj J P)) t)) i = ↑(Meq.mk S t) i
case right.intro.a
C : Type u
inst✝⁷ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category D
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
S : Cover J X
x : (forget D).obj (multiequalizer (Cover.index S (plusObj J P)))
t : (forget D).obj ((plusObj J P).obj X.op)
ht : Meq.mk S t = ↑(Meq.equiv (plusObj J P) S) x
⊢ ↑(Meq.equiv (plusObj J P) S) ((forget D).map (Cover.toMultiequalizer S (plusObj J P)) t) = Meq.mk S t
ext i
case right.intro.a.h
C : Type u
inst✝⁷ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category D
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
S : Cover J X
x : (forget D).obj (multiequalizer (Cover.index S (plusObj J P)))
t : (forget D).obj ((plusObj J P).obj X.op)
ht : Meq.mk S t = ↑(Meq.equiv (plusObj J P) S) x
i : Cover.Arrow S
⊢ (forget D).map (Multiequalizer.ι (Cover.index S (plusObj J P)) i)
      ((forget D).map (Cover.toMultiequalizer S (plusObj J P)) t) =
    ↑(Meq.mk S t) i
case right.intro.a.h
C : Type u
inst✝⁷ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category D
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
S : Cover J X
x : (forget D).obj (multiequalizer (Cover.index S (plusObj J P)))
t : (forget D).obj ((plusObj J P).obj X.op)
ht : Meq.mk S t = ↑(Meq.equiv (plusObj J P) S) x
i : Cover.Arrow S
⊢ ↑(↑(Meq.equiv (plusObj J P) S) ((forget D).map (Cover.toMultiequalizer S (plusObj J P)) t)) i = ↑(Meq.mk S t) i
dsimp
case right.intro.a.h
C : Type u
inst✝⁷ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category D
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
S : Cover J X
x : (forget D).obj (multiequalizer (Cover.index S (plusObj J P)))
t : (forget D).obj ((plusObj J P).obj X.op)
ht : Meq.mk S t = ↑(Meq.equiv (plusObj J P) S) x
i : Cover.Arrow S
⊢ (forget D).map ((plusObj J P).map i.f.op) t = ↑(Meq.mk S t) i
case right.intro.a.h
C : Type u
inst✝⁷ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category D
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
S : Cover J X
x : (forget D).obj (multiequalizer (Cover.index S (plusObj J P)))
t : (forget D).obj ((plusObj J P).obj X.op)
ht : Meq.mk S t = ↑(Meq.equiv (plusObj J P) S) x
i : Cover.Arrow S
⊢ (forget D).map (Multiequalizer.ι (Cover.index S (plusObj J P)) i)
      ((forget D).map (Cover.toMultiequalizer S (plusObj J P)) t) =
    ↑(Meq.mk S t) i
rw [← comp_apply, Multiequalizer.lift_ι]
no goals
case right.intro.a.h
C : Type u
inst✝⁷ : Category C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category D
inst✝⁵ : ConcreteCategory D
inst✝⁴ : PreservesLimits (forget D)
inst✝³ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : Cover J X), HasMultiequalizer (Cover.index S P)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : Cover J X) (x y : (forget D).obj (P.obj X.op)),
    (∀ (I : Cover.Arrow S), (forget D).map (P.map I.f.op) x = (forget D).map (P.map I.f.op) y) → x = y
X : C
S : Cover J X
x : (forget D).obj (multiequalizer (Cover.index S (plusObj J P)))
t : (forget D).obj ((plusObj J P).obj X.op)
ht : Meq.mk S t = ↑(Meq.equiv (plusObj J P) S) x
i : Cover.Arrow S
⊢ (forget D).map ((plusObj J P).map i.f.op) t = ↑(Meq.mk S t) i
rfl