Session 28: The category of pointed sets
1. An example of a non-distributive category
Exercise 1 (p. 298)
Both parts of the distributive law are false in the category of pointed sets:
(a) Find an object A for which the map
\mathbf{0} \rightarrow \mathbf{0} \times A
is not an isomorphism.
(b) Find objects A, B_1, and B_2 for which the standard map
A \times B_1 + A \times B_2 \rightarrow A \times (B_1 + B_2)
is not an isomorphism.
Solution: Exercise 1
For part (a), taking A to be
def A : Pointed := {
X := Fin 2
point := 0
}
we can show that the map {\mathbf{0} \rightarrow \mathbf{0} \times A} is not an isomorphism, as follows:
example [HasInitial Pointed] [HasBinaryProduct (β₯_ Pointed) A] :
IsEmpty ((β₯_ Pointed) β
(β₯_ Pointed) β¨― A) := instβΒΉ:HasInitial Pointedinstβ:HasBinaryProduct (β₯_ Pointed) Aβ’ IsEmpty (β₯_ Pointed β
(β₯_ Pointed) β¨― A)
instβΒΉ:HasInitial Pointedinstβ:HasBinaryProduct (β₯_ Pointed) Aβ’ β (a : β₯_ Pointed β
(β₯_ Pointed) β¨― A), False
instβΒΉ:HasInitial Pointedinstβ:HasBinaryProduct (β₯_ Pointed) Ae:β₯_ Pointed β
(β₯_ Pointed) β¨― Aβ’ False
instβΒΉ:HasInitial Pointedinstβ:HasBinaryProduct (β₯_ Pointed) Ae:β₯_ Pointed β
(β₯_ Pointed) β¨― Aaβ:β₯_ Pointed βΆ A := { toFun := fun x β¦ A.point, map_point := β― }β’ False
instβΒΉ:HasInitial Pointedinstβ:HasBinaryProduct (β₯_ Pointed) Ae:β₯_ Pointed β
(β₯_ Pointed) β¨― Aaβ:β₯_ Pointed βΆ A := { toFun := fun x β¦ A.point, map_point := β― }pA:(β₯_ Pointed) β¨― A βΆ A := prod.sndβ’ False
instβΒΉ:HasInitial Pointedinstβ:HasBinaryProduct (β₯_ Pointed) Ae:β₯_ Pointed β
(β₯_ Pointed) β¨― Aaβ:β₯_ Pointed βΆ A := { toFun := fun x β¦ A.point, map_point := β― }pA:(β₯_ Pointed) β¨― A βΆ A := prod.snds:A βΆ (β₯_ Pointed) β¨― A := prod.lift { toFun := fun x β¦ (β₯_ Pointed).point, map_point := β― } (π A)β’ False
instβΒΉ:HasInitial Pointedinstβ:HasBinaryProduct (β₯_ Pointed) Ae:β₯_ Pointed β
(β₯_ Pointed) β¨― Aaβ:β₯_ Pointed βΆ A := { toFun := fun x β¦ A.point, map_point := β― }pA:(β₯_ Pointed) β¨― A βΆ A := prod.snds:A βΆ (β₯_ Pointed) β¨― A := prod.lift { toFun := fun x β¦ (β₯_ Pointed).point, map_point := β― } (π A)h_comm:pA β e.hom = aββ’ False
instβΒΉ:HasInitial Pointedinstβ:HasBinaryProduct (β₯_ Pointed) Ae:β₯_ Pointed β
(β₯_ Pointed) β¨― Aaβ:β₯_ Pointed βΆ A := { toFun := fun x β¦ A.point, map_point := β― }pA:(β₯_ Pointed) β¨― A βΆ A := prod.snds:A βΆ (β₯_ Pointed) β¨― A := prod.lift { toFun := fun x β¦ (β₯_ Pointed).point, map_point := β― } (π A)h_comm:pA β e.hom = aβone:A.X := 1β’ False
have h_contra : one = A.point := calc one
_ = (π A) one := rfl
_ = (pA β s) one := instβΒΉ:HasInitial Pointedinstβ:HasBinaryProduct (β₯_ Pointed) Ae:β₯_ Pointed β
(β₯_ Pointed) β¨― Aaβ:β₯_ Pointed βΆ A := { toFun := fun x β¦ A.point, map_point := β― }pA:(β₯_ Pointed) β¨― A βΆ A := prod.snds:A βΆ (β₯_ Pointed) β¨― A := prod.lift { toFun := fun x β¦ (β₯_ Pointed).point, map_point := β― } (π A)h_comm:pA β e.hom = aβone:A.X := 1β’ (ConcreteCategory.hom (π A)) one = (ConcreteCategory.hom (pA β s)) one All goals completed! π
_ = pA ((π ((β₯_ Pointed) β¨― A)) (s one)) := rfl
_ = pA ((e.hom β e.inv) (s one)) := instβΒΉ:HasInitial Pointedinstβ:HasBinaryProduct (β₯_ Pointed) Ae:β₯_ Pointed β
(β₯_ Pointed) β¨― Aaβ:β₯_ Pointed βΆ A := { toFun := fun x β¦ A.point, map_point := β― }pA:(β₯_ Pointed) β¨― A βΆ A := prod.snds:A βΆ (β₯_ Pointed) β¨― A := prod.lift { toFun := fun x β¦ (β₯_ Pointed).point, map_point := β― } (π A)h_comm:pA β e.hom = aβone:A.X := 1β’ (ConcreteCategory.hom pA) ((ConcreteCategory.hom (π ((β₯_ Pointed) β¨― A))) ((ConcreteCategory.hom s) one)) =
(ConcreteCategory.hom pA) ((ConcreteCategory.hom (e.hom β e.inv)) ((ConcreteCategory.hom s) one)) All goals completed! π
_ = (pA β e.hom) (e.inv (s one)) := rfl
_ = aβ (e.inv (s one)) := instβΒΉ:HasInitial Pointedinstβ:HasBinaryProduct (β₯_ Pointed) Ae:β₯_ Pointed β
(β₯_ Pointed) β¨― Aaβ:β₯_ Pointed βΆ A := { toFun := fun x β¦ A.point, map_point := β― }pA:(β₯_ Pointed) β¨― A βΆ A := prod.snds:A βΆ (β₯_ Pointed) β¨― A := prod.lift { toFun := fun x β¦ (β₯_ Pointed).point, map_point := β― } (π A)h_comm:pA β e.hom = aβone:A.X := 1β’ (ConcreteCategory.hom (pA β e.hom)) ((ConcreteCategory.hom e.inv) ((ConcreteCategory.hom s) one)) =
(ConcreteCategory.hom aβ) ((ConcreteCategory.hom e.inv) ((ConcreteCategory.hom s) one)) All goals completed! π
_ = A.point := rfl
All goals completed! π
For part (b), taking A, B_1, and B_2 to be, respectively,
def A : Pointed := {
X := Fin 2
point := 0
}
def Bβ : Pointed := {
X := Unit
point := ()
}
def Bβ : Pointed := {
X := Unit
point := ()
}
we can use the pigeonhole principle (and grind to aid readability) to show that the map {A \times B_1 + A \times B_2 \rightarrow A \times (B_1 + B_2)} is not an isomorphism, as follows:
instance : OfNat A.X 0 where
ofNat := (0 : Fin 2)
instance : OfNat A.X 1 where
ofNat := (1 : Fin 2)
example [HasBinaryProduct A Bβ] [HasBinaryProduct A Bβ]
[HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)]
[HasBinaryCoproduct Bβ Bβ] [HasBinaryProduct A (Bβ β¨Ώ Bβ)] :
IsEmpty ((A β¨― Bβ) β¨Ώ (A β¨― Bβ) β
A β¨― (Bβ β¨Ώ Bβ)) := instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)β’ IsEmpty ((A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ Bβ)
instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)β’ β (a : (A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ Bβ), False
instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ Bββ’ False
-- Alias longer types for convenience
instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― Bββ’ False
instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ Bββ’ False
-- Define constant basepoint endomorphism of A
instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }β’ False
-- Construct 3 distinct pathways from A to L
instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }β’ False
instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }jβ:A βΆ L := coprod.inl β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }β’ False
instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }jβ:A βΆ L := coprod.inl β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }jβ:A βΆ L := coprod.inr β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }β’ False
-- Push pathways through isomorphism to obtain 3 target elements
instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }jβ:A βΆ L := coprod.inl β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }jβ:A βΆ L := coprod.inr β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β cAL)) 1β’ False
instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }jβ:A βΆ L := coprod.inl β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }jβ:A βΆ L := coprod.inr β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β cAL)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1β’ False
instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }jβ:A βΆ L := coprod.inl β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }jβ:A βΆ L := coprod.inr β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β cAL)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1β’ False
-- Define 'detector' morphisms
instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }jβ:A βΆ L := coprod.inl β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }jβ:A βΆ L := coprod.inr β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β cAL)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1m10:L βΆ A := coprod.desc prod.fst (cAA β prod.fst)β’ False
instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }jβ:A βΆ L := coprod.inl β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }jβ:A βΆ L := coprod.inr β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β cAL)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1m10:L βΆ A := coprod.desc prod.fst (cAA β prod.fst)m01:L βΆ A := coprod.desc (cAA β prod.fst) prod.fstβ’ False
-- Evaluate detector compositions for each pathway
have h10β : m10 β cAL = cAA := instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)β’ IsEmpty ((A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ Bβ)
instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }jβ:A βΆ L := coprod.inl β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }jβ:A βΆ L := coprod.inr β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β cAL)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1m10:L βΆ A := coprod.desc prod.fst (cAA β prod.fst)m01:L βΆ A := coprod.desc (cAA β prod.fst) prod.fstxβ:A.Xβ’ β(ConcreteCategory.hom (m10 β cAL)) xβ = β(ConcreteCategory.hom cAA) xβ
All goals completed! π
have h01β : m01 β cAL = cAA := instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)β’ IsEmpty ((A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ Bβ)
instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }jβ:A βΆ L := coprod.inl β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }jβ:A βΆ L := coprod.inr β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β cAL)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1m10:L βΆ A := coprod.desc prod.fst (cAA β prod.fst)m01:L βΆ A := coprod.desc (cAA β prod.fst) prod.fsth10β:m10 β cAL = cAAxβ:A.Xβ’ β(ConcreteCategory.hom (m01 β cAL)) xβ = β(ConcreteCategory.hom cAA) xβ
All goals completed! π
have h10β : m10 β jβ = π A := instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)β’ IsEmpty ((A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ Bβ)
All goals completed! π
have h01β : m01 β jβ = cAA := instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)β’ IsEmpty ((A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ Bβ)
instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }jβ:A βΆ L := coprod.inl β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }jβ:A βΆ L := coprod.inr β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β cAL)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1m10:L βΆ A := coprod.desc prod.fst (cAA β prod.fst)m01:L βΆ A := coprod.desc (cAA β prod.fst) prod.fsth01β:m01 β cAL = cAAh10β:m10 β jβ = π Aβ’ m01 β jβ = cAA
All goals completed! π
have h10β : m10 β jβ = cAA := instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)β’ IsEmpty ((A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ Bβ)
instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }jβ:A βΆ L := coprod.inl β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }jβ:A βΆ L := coprod.inr β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β cAL)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1m10:L βΆ A := coprod.desc prod.fst (cAA β prod.fst)m01:L βΆ A := coprod.desc (cAA β prod.fst) prod.fsth10β:m10 β cAL = cAAh01β:m01 β cAL = cAAβ’ m10 β jβ = cAA
All goals completed! π
have h01β : m01 β jβ = π A := instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)β’ IsEmpty ((A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ Bβ)
instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }jβ:A βΆ L := coprod.inl β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }jβ:A βΆ L := coprod.inr β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β cAL)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1m10:L βΆ A := coprod.desc prod.fst (cAA β prod.fst)m01:L βΆ A := coprod.desc (cAA β prod.fst) prod.fsth10β:m10 β cAL = cAAh01β:m01 β cAL = cAAh10β:m10 β jβ = cAAβ’ m01 β jβ = π A
All goals completed! π
-- Prove all morphisms into Z map to basepoint
have h_fXZ {X : Pointed} (f : X βΆ Z) :
f = β¨fun _ β¦ Z.point, rflβ© := instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)β’ IsEmpty ((A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ Bβ)
have : π Z = β¨fun _ β¦ Z.point, rflβ© := instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)β’ IsEmpty ((A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ Bβ)
have ext_Bβ {Y : Pointed} (f g : Bβ βΆ Y) : f = g := instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)β’ IsEmpty ((A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ Bβ)
instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }jβ:A βΆ L := coprod.inl β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }jβ:A βΆ L := coprod.inr β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β cAL)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1m10:L βΆ A := coprod.desc prod.fst (cAA β prod.fst)m01:L βΆ A := coprod.desc (cAA β prod.fst) prod.fsth10β:m10 β cAL = cAAh01β:m01 β cAL = cAAh10β:m10 β jβ = π Ah01β:m01 β jβ = cAAh10β:m10 β jβ = cAAh01β:m01 β jβ = π AX:Pointedfβ:X βΆ ZY:Pointedf:Bβ βΆ Yg:Bβ βΆ Yxβ:Bβ.Xβ’ β(ConcreteCategory.hom f) xβ = β(ConcreteCategory.hom g) xβ
All goals completed! π
have ext_Bβ {Y : Pointed} (f g : Bβ βΆ Y) : f = g := instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)β’ IsEmpty ((A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ Bβ)
instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }jβ:A βΆ L := coprod.inl β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }jβ:A βΆ L := coprod.inr β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β cAL)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1m10:L βΆ A := coprod.desc prod.fst (cAA β prod.fst)m01:L βΆ A := coprod.desc (cAA β prod.fst) prod.fsth10β:m10 β cAL = cAAh01β:m01 β cAL = cAAh10β:m10 β jβ = π Ah01β:m01 β jβ = cAAh10β:m10 β jβ = cAAh01β:m01 β jβ = π AX:Pointedfβ:X βΆ Zext_Bβ:β {Y : Pointed} (f g : Bβ βΆ Y), f = gY:Pointedf:Bβ βΆ Yg:Bβ βΆ Yxβ:Bβ.Xβ’ β(ConcreteCategory.hom f) xβ = β(ConcreteCategory.hom g) xβ
All goals completed! π
instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }jβ:A βΆ L := coprod.inl β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }jβ:A βΆ L := coprod.inr β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β cAL)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1m10:L βΆ A := coprod.desc prod.fst (cAA β prod.fst)m01:L βΆ A := coprod.desc (cAA β prod.fst) prod.fsth10β:m10 β cAL = cAAh01β:m01 β cAL = cAAh10β:m10 β jβ = π Ah01β:m01 β jβ = cAAh10β:m10 β jβ = cAAh01β:m01 β jβ = π AX:Pointedf:X βΆ Zext_Bβ:β {Y : Pointed} (f g : Bβ βΆ Y), f = gext_Bβ:β {Y : Pointed} (f g : Bβ βΆ Y), f = gβ’ π Z β coprod.inl = { toFun := fun x β¦ Z.point, map_point := β― } β coprod.inlinstββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }jβ:A βΆ L := coprod.inl β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }jβ:A βΆ L := coprod.inr β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β cAL)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1m10:L βΆ A := coprod.desc prod.fst (cAA β prod.fst)m01:L βΆ A := coprod.desc (cAA β prod.fst) prod.fsth10β:m10 β cAL = cAAh01β:m01 β cAL = cAAh10β:m10 β jβ = π Ah01β:m01 β jβ = cAAh10β:m10 β jβ = cAAh01β:m01 β jβ = π AX:Pointedf:X βΆ Zext_Bβ:β {Y : Pointed} (f g : Bβ βΆ Y), f = gext_Bβ:β {Y : Pointed} (f g : Bβ βΆ Y), f = gβ’ π Z β coprod.inr = { toFun := fun x β¦ Z.point, map_point := β― } β coprod.inr
instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }jβ:A βΆ L := coprod.inl β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }jβ:A βΆ L := coprod.inr β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β cAL)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1m10:L βΆ A := coprod.desc prod.fst (cAA β prod.fst)m01:L βΆ A := coprod.desc (cAA β prod.fst) prod.fsth10β:m10 β cAL = cAAh01β:m01 β cAL = cAAh10β:m10 β jβ = π Ah01β:m01 β jβ = cAAh10β:m10 β jβ = cAAh01β:m01 β jβ = π AX:Pointedf:X βΆ Zext_Bβ:β {Y : Pointed} (f g : Bβ βΆ Y), f = gext_Bβ:β {Y : Pointed} (f g : Bβ βΆ Y), f = gβ’ π Z β coprod.inl = { toFun := fun x β¦ Z.point, map_point := β― } β coprod.inl All goals completed! π
instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }jβ:A βΆ L := coprod.inl β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }jβ:A βΆ L := coprod.inr β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β cAL)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1m10:L βΆ A := coprod.desc prod.fst (cAA β prod.fst)m01:L βΆ A := coprod.desc (cAA β prod.fst) prod.fsth10β:m10 β cAL = cAAh01β:m01 β cAL = cAAh10β:m10 β jβ = π Ah01β:m01 β jβ = cAAh10β:m10 β jβ = cAAh01β:m01 β jβ = π AX:Pointedf:X βΆ Zext_Bβ:β {Y : Pointed} (f g : Bβ βΆ Y), f = gext_Bβ:β {Y : Pointed} (f g : Bβ βΆ Y), f = gβ’ π Z β coprod.inr = { toFun := fun x β¦ Z.point, map_point := β― } β coprod.inr All goals completed! π
calc
f = π Z β f := instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }jβ:A βΆ L := coprod.inl β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }jβ:A βΆ L := coprod.inr β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β cAL)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1m10:L βΆ A := coprod.desc prod.fst (cAA β prod.fst)m01:L βΆ A := coprod.desc (cAA β prod.fst) prod.fsth10β:m10 β cAL = cAAh01β:m01 β cAL = cAAh10β:m10 β jβ = π Ah01β:m01 β jβ = cAAh10β:m10 β jβ = cAAh01β:m01 β jβ = π AX:Pointedf:X βΆ Zthis:π Z = { toFun := fun x β¦ Z.point, map_point := β― }β’ f = π Z β f All goals completed! π
_ = β¨fun _ β¦ Z.point, rflβ© β f := instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }jβ:A βΆ L := coprod.inl β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }jβ:A βΆ L := coprod.inr β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β cAL)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1m10:L βΆ A := coprod.desc prod.fst (cAA β prod.fst)m01:L βΆ A := coprod.desc (cAA β prod.fst) prod.fsth10β:m10 β cAL = cAAh01β:m01 β cAL = cAAh10β:m10 β jβ = π Ah01β:m01 β jβ = cAAh10β:m10 β jβ = cAAh01β:m01 β jβ = π AX:Pointedf:X βΆ Zthis:π Z = { toFun := fun x β¦ Z.point, map_point := β― }β’ π Z β f = { toFun := fun x β¦ Z.point, map_point := β― } β f All goals completed! π
_ = β¨fun _ β¦ Z.point, rflβ© := rfl
-- Lift element equality to morphism equality for morphisms A βΆ L
have h_fAL {a b : A βΆ L}
(h_v : (prod.fst β e.hom β a) 1 =
(prod.fst β e.hom β b) 1) : a = b := instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)β’ IsEmpty ((A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ Bβ)
have : e.hom β a = e.hom β b := instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)β’ IsEmpty ((A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ Bβ)
have ext_A {f g : A βΆ A} (h : f 1 = g 1) : f = g := instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)β’ IsEmpty ((A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ Bβ)
instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }jβ:A βΆ L := coprod.inl β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }jβ:A βΆ L := coprod.inr β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β cAL)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1m10:L βΆ A := coprod.desc prod.fst (cAA β prod.fst)m01:L βΆ A := coprod.desc (cAA β prod.fst) prod.fsth10β:m10 β cAL = cAAh01β:m01 β cAL = cAAh10β:m10 β jβ = π Ah01β:m01 β jβ = cAAh10β:m10 β jβ = cAAh01β:m01 β jβ = π Ah_fXZ:β {X : Pointed} (f : X βΆ Z), f = { toFun := fun x β¦ Z.point, map_point := β― }a:A βΆ Lb:A βΆ Lh_v:(ConcreteCategory.hom (prod.fst β e.hom β a)) 1 = (ConcreteCategory.hom (prod.fst β e.hom β b)) 1f:A βΆ Ag:A βΆ Ah:(ConcreteCategory.hom f) 1 = (ConcreteCategory.hom g) 1x:A.Xβ’ β(ConcreteCategory.hom f) x = β(ConcreteCategory.hom g) x
instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }jβ:A βΆ L := coprod.inl β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }jβ:A βΆ L := coprod.inr β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β cAL)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1m10:L βΆ A := coprod.desc prod.fst (cAA β prod.fst)m01:L βΆ A := coprod.desc (cAA β prod.fst) prod.fsth10β:m10 β cAL = cAAh01β:m01 β cAL = cAAh10β:m10 β jβ = π Ah01β:m01 β jβ = cAAh10β:m10 β jβ = cAAh01β:m01 β jβ = π Ah_fXZ:β {X : Pointed} (f : X βΆ Z), f = { toFun := fun x β¦ Z.point, map_point := β― }a:A βΆ Lb:A βΆ Lh_v:(ConcreteCategory.hom (prod.fst β e.hom β a)) 1 = (ConcreteCategory.hom (prod.fst β e.hom β b)) 1f:A βΆ Ag:A βΆ Ah:(ConcreteCategory.hom f) 1 = (ConcreteCategory.hom g) 1x:Fin 2β’ β(ConcreteCategory.hom f) x = β(ConcreteCategory.hom g) x
instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }jβ:A βΆ L := coprod.inl β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }jβ:A βΆ L := coprod.inr β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β cAL)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1m10:L βΆ A := coprod.desc prod.fst (cAA β prod.fst)m01:L βΆ A := coprod.desc (cAA β prod.fst) prod.fsth10β:m10 β cAL = cAAh01β:m01 β cAL = cAAh10β:m10 β jβ = π Ah01β:m01 β jβ = cAAh10β:m10 β jβ = cAAh01β:m01 β jβ = π Ah_fXZ:β {X : Pointed} (f : X βΆ Z), f = { toFun := fun x β¦ Z.point, map_point := β― }a:A βΆ Lb:A βΆ Lh_v:(ConcreteCategory.hom (prod.fst β e.hom β a)) 1 = (ConcreteCategory.hom (prod.fst β e.hom β b)) 1f:A βΆ Ag:A βΆ Ah:(ConcreteCategory.hom f) 1 = (ConcreteCategory.hom g) 1β’ β(ConcreteCategory.hom f) ((fun i β¦ i) β¨0, β―β©) = β(ConcreteCategory.hom g) ((fun i β¦ i) β¨0, β―β©)instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }jβ:A βΆ L := coprod.inl β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }jβ:A βΆ L := coprod.inr β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β cAL)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1m10:L βΆ A := coprod.desc prod.fst (cAA β prod.fst)m01:L βΆ A := coprod.desc (cAA β prod.fst) prod.fsth10β:m10 β cAL = cAAh01β:m01 β cAL = cAAh10β:m10 β jβ = π Ah01β:m01 β jβ = cAAh10β:m10 β jβ = cAAh01β:m01 β jβ = π Ah_fXZ:β {X : Pointed} (f : X βΆ Z), f = { toFun := fun x β¦ Z.point, map_point := β― }a:A βΆ Lb:A βΆ Lh_v:(ConcreteCategory.hom (prod.fst β e.hom β a)) 1 = (ConcreteCategory.hom (prod.fst β e.hom β b)) 1f:A βΆ Ag:A βΆ Ah:(ConcreteCategory.hom f) 1 = (ConcreteCategory.hom g) 1β’ β(ConcreteCategory.hom f) ((fun i β¦ i) β¨1, β―β©) = β(ConcreteCategory.hom g) ((fun i β¦ i) β¨1, β―β©)
instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }jβ:A βΆ L := coprod.inl β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }jβ:A βΆ L := coprod.inr β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β cAL)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1m10:L βΆ A := coprod.desc prod.fst (cAA β prod.fst)m01:L βΆ A := coprod.desc (cAA β prod.fst) prod.fsth10β:m10 β cAL = cAAh01β:m01 β cAL = cAAh10β:m10 β jβ = π Ah01β:m01 β jβ = cAAh10β:m10 β jβ = cAAh01β:m01 β jβ = π Ah_fXZ:β {X : Pointed} (f : X βΆ Z), f = { toFun := fun x β¦ Z.point, map_point := β― }a:A βΆ Lb:A βΆ Lh_v:(ConcreteCategory.hom (prod.fst β e.hom β a)) 1 = (ConcreteCategory.hom (prod.fst β e.hom β b)) 1f:A βΆ Ag:A βΆ Ah:(ConcreteCategory.hom f) 1 = (ConcreteCategory.hom g) 1β’ β(ConcreteCategory.hom f) ((fun i β¦ i) β¨0, β―β©) = β(ConcreteCategory.hom g) ((fun i β¦ i) β¨0, β―β©) All goals completed! π
instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }jβ:A βΆ L := coprod.inl β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }jβ:A βΆ L := coprod.inr β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β cAL)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1m10:L βΆ A := coprod.desc prod.fst (cAA β prod.fst)m01:L βΆ A := coprod.desc (cAA β prod.fst) prod.fsth10β:m10 β cAL = cAAh01β:m01 β cAL = cAAh10β:m10 β jβ = π Ah01β:m01 β jβ = cAAh10β:m10 β jβ = cAAh01β:m01 β jβ = π Ah_fXZ:β {X : Pointed} (f : X βΆ Z), f = { toFun := fun x β¦ Z.point, map_point := β― }a:A βΆ Lb:A βΆ Lh_v:(ConcreteCategory.hom (prod.fst β e.hom β a)) 1 = (ConcreteCategory.hom (prod.fst β e.hom β b)) 1f:A βΆ Ag:A βΆ Ah:(ConcreteCategory.hom f) 1 = (ConcreteCategory.hom g) 1β’ β(ConcreteCategory.hom f) ((fun i β¦ i) β¨1, β―β©) = β(ConcreteCategory.hom g) ((fun i β¦ i) β¨1, β―β©) All goals completed! π
instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }jβ:A βΆ L := coprod.inl β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }jβ:A βΆ L := coprod.inr β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β cAL)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1m10:L βΆ A := coprod.desc prod.fst (cAA β prod.fst)m01:L βΆ A := coprod.desc (cAA β prod.fst) prod.fsth10β:m10 β cAL = cAAh01β:m01 β cAL = cAAh10β:m10 β jβ = π Ah01β:m01 β jβ = cAAh10β:m10 β jβ = cAAh01β:m01 β jβ = π Ah_fXZ:β {X : Pointed} (f : X βΆ Z), f = { toFun := fun x β¦ Z.point, map_point := β― }a:A βΆ Lb:A βΆ Lh_v:(ConcreteCategory.hom (prod.fst β e.hom β a)) 1 = (ConcreteCategory.hom (prod.fst β e.hom β b)) 1ext_A:β {f g : A βΆ A}, (ConcreteCategory.hom f) 1 = (ConcreteCategory.hom g) 1 β f = gβ’ prod.fst β e.hom β a = prod.fst β e.hom β binstββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }jβ:A βΆ L := coprod.inl β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }jβ:A βΆ L := coprod.inr β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β cAL)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1m10:L βΆ A := coprod.desc prod.fst (cAA β prod.fst)m01:L βΆ A := coprod.desc (cAA β prod.fst) prod.fsth10β:m10 β cAL = cAAh01β:m01 β cAL = cAAh10β:m10 β jβ = π Ah01β:m01 β jβ = cAAh10β:m10 β jβ = cAAh01β:m01 β jβ = π Ah_fXZ:β {X : Pointed} (f : X βΆ Z), f = { toFun := fun x β¦ Z.point, map_point := β― }a:A βΆ Lb:A βΆ Lh_v:(ConcreteCategory.hom (prod.fst β e.hom β a)) 1 = (ConcreteCategory.hom (prod.fst β e.hom β b)) 1ext_A:β {f g : A βΆ A}, (ConcreteCategory.hom f) 1 = (ConcreteCategory.hom g) 1 β f = gβ’ prod.snd β e.hom β a = prod.snd β e.hom β b
instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }jβ:A βΆ L := coprod.inl β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }jβ:A βΆ L := coprod.inr β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β cAL)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1m10:L βΆ A := coprod.desc prod.fst (cAA β prod.fst)m01:L βΆ A := coprod.desc (cAA β prod.fst) prod.fsth10β:m10 β cAL = cAAh01β:m01 β cAL = cAAh10β:m10 β jβ = π Ah01β:m01 β jβ = cAAh10β:m10 β jβ = cAAh01β:m01 β jβ = π Ah_fXZ:β {X : Pointed} (f : X βΆ Z), f = { toFun := fun x β¦ Z.point, map_point := β― }a:A βΆ Lb:A βΆ Lh_v:(ConcreteCategory.hom (prod.fst β e.hom β a)) 1 = (ConcreteCategory.hom (prod.fst β e.hom β b)) 1ext_A:β {f g : A βΆ A}, (ConcreteCategory.hom f) 1 = (ConcreteCategory.hom g) 1 β f = gβ’ prod.fst β e.hom β a = prod.fst β e.hom β b All goals completed! π
instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }jβ:A βΆ L := coprod.inl β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }jβ:A βΆ L := coprod.inr β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β cAL)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1m10:L βΆ A := coprod.desc prod.fst (cAA β prod.fst)m01:L βΆ A := coprod.desc (cAA β prod.fst) prod.fsth10β:m10 β cAL = cAAh01β:m01 β cAL = cAAh10β:m10 β jβ = π Ah01β:m01 β jβ = cAAh10β:m10 β jβ = cAAh01β:m01 β jβ = π Ah_fXZ:β {X : Pointed} (f : X βΆ Z), f = { toFun := fun x β¦ Z.point, map_point := β― }a:A βΆ Lb:A βΆ Lh_v:(ConcreteCategory.hom (prod.fst β e.hom β a)) 1 = (ConcreteCategory.hom (prod.fst β e.hom β b)) 1ext_A:β {f g : A βΆ A}, (ConcreteCategory.hom f) 1 = (ConcreteCategory.hom g) 1 β f = gβ’ prod.snd β e.hom β a = prod.snd β e.hom β b All goals completed! π
All goals completed! π
-- Apply pigeonhole principle
have h_pigeon : vβ = vβ β¨ vβ = vβ β¨ vβ = vβ := instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)β’ IsEmpty ((A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ Bβ)
instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }jβ:A βΆ L := coprod.inl β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }jβ:A βΆ L := coprod.inr β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β cAL)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1m10:L βΆ A := coprod.desc prod.fst (cAA β prod.fst)m01:L βΆ A := coprod.desc (cAA β prod.fst) prod.fsth10β:m10 β cAL = cAAh01β:m01 β cAL = cAAh10β:m10 β jβ = π Ah01β:m01 β jβ = cAAh10β:m10 β jβ = cAAh01β:m01 β jβ = π Ah_fXZ:β {X : Pointed} (f : X βΆ Z), f = { toFun := fun x β¦ Z.point, map_point := β― }h_fAL:β {a b : A βΆ L},
(ConcreteCategory.hom (prod.fst β e.hom β a)) 1 = (ConcreteCategory.hom (prod.fst β e.hom β b)) 1 β a = bvalβ:βisLtβ:valβ < 2β’ β¨valβ, isLtββ© = vβ β¨ β¨valβ, isLtββ© = vβ β¨ vβ = vβ; instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }jβ:A βΆ L := coprod.inl β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }jβ:A βΆ L := coprod.inr β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β cAL)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1m10:L βΆ A := coprod.desc prod.fst (cAA β prod.fst)m01:L βΆ A := coprod.desc (cAA β prod.fst) prod.fsth10β:m10 β cAL = cAAh01β:m01 β cAL = cAAh10β:m10 β jβ = π Ah01β:m01 β jβ = cAAh10β:m10 β jβ = cAAh01β:m01 β jβ = π Ah_fXZ:β {X : Pointed} (f : X βΆ Z), f = { toFun := fun x β¦ Z.point, map_point := β― }h_fAL:β {a b : A βΆ L},
(ConcreteCategory.hom (prod.fst β e.hom β a)) 1 = (ConcreteCategory.hom (prod.fst β e.hom β b)) 1 β a = bvalβΒΉ:βisLtβΒΉ:valβ < 2valβ:βisLtβ:valβ < 2β’ β¨valβΒΉ, isLtβΒΉβ© = β¨valβ, isLtββ© β¨ β¨valβΒΉ, isLtβΒΉβ© = vβ β¨ β¨valβ, isLtββ© = vβ; instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }jβ:A βΆ L := coprod.inl β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }jβ:A βΆ L := coprod.inr β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β cAL)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1m10:L βΆ A := coprod.desc prod.fst (cAA β prod.fst)m01:L βΆ A := coprod.desc (cAA β prod.fst) prod.fsth10β:m10 β cAL = cAAh01β:m01 β cAL = cAAh10β:m10 β jβ = π Ah01β:m01 β jβ = cAAh10β:m10 β jβ = cAAh01β:m01 β jβ = π Ah_fXZ:β {X : Pointed} (f : X βΆ Z), f = { toFun := fun x β¦ Z.point, map_point := β― }h_fAL:β {a b : A βΆ L},
(ConcreteCategory.hom (prod.fst β e.hom β a)) 1 = (ConcreteCategory.hom (prod.fst β e.hom β b)) 1 β a = bvalβΒ²:βisLtβΒ²:valβ < 2valβΒΉ:βisLtβΒΉ:valβ < 2valβ:βisLtβ:valβ < 2β’ β¨valβΒ², isLtβΒ²β© = β¨valβΒΉ, isLtβΒΉβ© β¨ β¨valβΒ², isLtβΒ²β© = β¨valβ, isLtββ© β¨ β¨valβΒΉ, isLtβΒΉβ© = β¨valβ, isLtββ©; All goals completed! π
-- Derive contradiction for each collision
instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }jβ:A βΆ L := coprod.inl β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }jβ:A βΆ L := coprod.inr β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β cAL)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1m10:L βΆ A := coprod.desc prod.fst (cAA β prod.fst)m01:L βΆ A := coprod.desc (cAA β prod.fst) prod.fsth10β:m10 β cAL = cAAh01β:m01 β cAL = cAAh10β:m10 β jβ = π Ah01β:m01 β jβ = cAAh10β:m10 β jβ = cAAh01β:m01 β jβ = π Ah_fXZ:β {X : Pointed} (f : X βΆ Z), f = { toFun := fun x β¦ Z.point, map_point := β― }h_fAL:β {a b : A βΆ L},
(ConcreteCategory.hom (prod.fst β e.hom β a)) 1 = (ConcreteCategory.hom (prod.fst β e.hom β b)) 1 β a = bh01:vβ = vββ’ Falseinstββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }jβ:A βΆ L := coprod.inl β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }jβ:A βΆ L := coprod.inr β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β cAL)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1m10:L βΆ A := coprod.desc prod.fst (cAA β prod.fst)m01:L βΆ A := coprod.desc (cAA β prod.fst) prod.fsth10β:m10 β cAL = cAAh01β:m01 β cAL = cAAh10β:m10 β jβ = π Ah01β:m01 β jβ = cAAh10β:m10 β jβ = cAAh01β:m01 β jβ = π Ah_fXZ:β {X : Pointed} (f : X βΆ Z), f = { toFun := fun x β¦ Z.point, map_point := β― }h_fAL:β {a b : A βΆ L},
(ConcreteCategory.hom (prod.fst β e.hom β a)) 1 = (ConcreteCategory.hom (prod.fst β e.hom β b)) 1 β a = bh02:vβ = vββ’ Falseinstββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }jβ:A βΆ L := coprod.inl β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }jβ:A βΆ L := coprod.inr β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β cAL)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1m10:L βΆ A := coprod.desc prod.fst (cAA β prod.fst)m01:L βΆ A := coprod.desc (cAA β prod.fst) prod.fsth10β:m10 β cAL = cAAh01β:m01 β cAL = cAAh10β:m10 β jβ = π Ah01β:m01 β jβ = cAAh10β:m10 β jβ = cAAh01β:m01 β jβ = π Ah_fXZ:β {X : Pointed} (f : X βΆ Z), f = { toFun := fun x β¦ Z.point, map_point := β― }h_fAL:β {a b : A βΆ L},
(ConcreteCategory.hom (prod.fst β e.hom β a)) 1 = (ConcreteCategory.hom (prod.fst β e.hom β b)) 1 β a = bh12:vβ = vββ’ False
instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }jβ:A βΆ L := coprod.inl β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }jβ:A βΆ L := coprod.inr β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β cAL)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1m10:L βΆ A := coprod.desc prod.fst (cAA β prod.fst)m01:L βΆ A := coprod.desc (cAA β prod.fst) prod.fsth10β:m10 β cAL = cAAh01β:m01 β cAL = cAAh10β:m10 β jβ = π Ah01β:m01 β jβ = cAAh10β:m10 β jβ = cAAh01β:m01 β jβ = π Ah_fXZ:β {X : Pointed} (f : X βΆ Z), f = { toFun := fun x β¦ Z.point, map_point := β― }h_fAL:β {a b : A βΆ L},
(ConcreteCategory.hom (prod.fst β e.hom β a)) 1 = (ConcreteCategory.hom (prod.fst β e.hom β b)) 1 β a = bh01:vβ = vββ’ False have h_contra : (1 : Fin 2) = 0 := calc
1 = (π A) 1 := rfl
_ = (m10 β jβ) 1 := instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }jβ:A βΆ L := coprod.inl β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }jβ:A βΆ L := coprod.inr β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β cAL)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1m10:L βΆ A := coprod.desc prod.fst (cAA β prod.fst)m01:L βΆ A := coprod.desc (cAA β prod.fst) prod.fsth10β:m10 β cAL = cAAh01β:m01 β cAL = cAAh10β:m10 β jβ = π Ah01β:m01 β jβ = cAAh10β:m10 β jβ = cAAh01β:m01 β jβ = π Ah_fXZ:β {X : Pointed} (f : X βΆ Z), f = { toFun := fun x β¦ Z.point, map_point := β― }h_fAL:β {a b : A βΆ L},
(ConcreteCategory.hom (prod.fst β e.hom β a)) 1 = (ConcreteCategory.hom (prod.fst β e.hom β b)) 1 β a = bh01:vβ = vββ’ (ConcreteCategory.hom (π A)) 1 = (ConcreteCategory.hom (m10 β jβ)) 1 All goals completed! π
_ = (m10 β cAL) 1 := instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }jβ:A βΆ L := coprod.inl β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }jβ:A βΆ L := coprod.inr β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β cAL)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1m10:L βΆ A := coprod.desc prod.fst (cAA β prod.fst)m01:L βΆ A := coprod.desc (cAA β prod.fst) prod.fsth10β:m10 β cAL = cAAh01β:m01 β cAL = cAAh10β:m10 β jβ = π Ah01β:m01 β jβ = cAAh10β:m10 β jβ = cAAh01β:m01 β jβ = π Ah_fXZ:β {X : Pointed} (f : X βΆ Z), f = { toFun := fun x β¦ Z.point, map_point := β― }h_fAL:β {a b : A βΆ L},
(ConcreteCategory.hom (prod.fst β e.hom β a)) 1 = (ConcreteCategory.hom (prod.fst β e.hom β b)) 1 β a = bh01:vβ = vββ’ (ConcreteCategory.hom (m10 β jβ)) 1 = (ConcreteCategory.hom (m10 β cAL)) 1 All goals completed! π
_ = cAA 1 := instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }jβ:A βΆ L := coprod.inl β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }jβ:A βΆ L := coprod.inr β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β cAL)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1m10:L βΆ A := coprod.desc prod.fst (cAA β prod.fst)m01:L βΆ A := coprod.desc (cAA β prod.fst) prod.fsth10β:m10 β cAL = cAAh01β:m01 β cAL = cAAh10β:m10 β jβ = π Ah01β:m01 β jβ = cAAh10β:m10 β jβ = cAAh01β:m01 β jβ = π Ah_fXZ:β {X : Pointed} (f : X βΆ Z), f = { toFun := fun x β¦ Z.point, map_point := β― }h_fAL:β {a b : A βΆ L},
(ConcreteCategory.hom (prod.fst β e.hom β a)) 1 = (ConcreteCategory.hom (prod.fst β e.hom β b)) 1 β a = bh01:vβ = vββ’ (ConcreteCategory.hom (m10 β cAL)) 1 = (ConcreteCategory.hom cAA) 1 All goals completed! π
_ = 0 := rfl
All goals completed! π
instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }jβ:A βΆ L := coprod.inl β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }jβ:A βΆ L := coprod.inr β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β cAL)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1m10:L βΆ A := coprod.desc prod.fst (cAA β prod.fst)m01:L βΆ A := coprod.desc (cAA β prod.fst) prod.fsth10β:m10 β cAL = cAAh01β:m01 β cAL = cAAh10β:m10 β jβ = π Ah01β:m01 β jβ = cAAh10β:m10 β jβ = cAAh01β:m01 β jβ = π Ah_fXZ:β {X : Pointed} (f : X βΆ Z), f = { toFun := fun x β¦ Z.point, map_point := β― }h_fAL:β {a b : A βΆ L},
(ConcreteCategory.hom (prod.fst β e.hom β a)) 1 = (ConcreteCategory.hom (prod.fst β e.hom β b)) 1 β a = bh02:vβ = vββ’ False have h_contra : (1 : Fin 2) = 0 := calc
1 = (π A) 1 := rfl
_ = (m01 β jβ) 1 := instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }jβ:A βΆ L := coprod.inl β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }jβ:A βΆ L := coprod.inr β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β cAL)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1m10:L βΆ A := coprod.desc prod.fst (cAA β prod.fst)m01:L βΆ A := coprod.desc (cAA β prod.fst) prod.fsth10β:m10 β cAL = cAAh01β:m01 β cAL = cAAh10β:m10 β jβ = π Ah01β:m01 β jβ = cAAh10β:m10 β jβ = cAAh01β:m01 β jβ = π Ah_fXZ:β {X : Pointed} (f : X βΆ Z), f = { toFun := fun x β¦ Z.point, map_point := β― }h_fAL:β {a b : A βΆ L},
(ConcreteCategory.hom (prod.fst β e.hom β a)) 1 = (ConcreteCategory.hom (prod.fst β e.hom β b)) 1 β a = bh02:vβ = vββ’ (ConcreteCategory.hom (π A)) 1 = (ConcreteCategory.hom (m01 β jβ)) 1 All goals completed! π
_ = (m01 β cAL) 1 := instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }jβ:A βΆ L := coprod.inl β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }jβ:A βΆ L := coprod.inr β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β cAL)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1m10:L βΆ A := coprod.desc prod.fst (cAA β prod.fst)m01:L βΆ A := coprod.desc (cAA β prod.fst) prod.fsth10β:m10 β cAL = cAAh01β:m01 β cAL = cAAh10β:m10 β jβ = π Ah01β:m01 β jβ = cAAh10β:m10 β jβ = cAAh01β:m01 β jβ = π Ah_fXZ:β {X : Pointed} (f : X βΆ Z), f = { toFun := fun x β¦ Z.point, map_point := β― }h_fAL:β {a b : A βΆ L},
(ConcreteCategory.hom (prod.fst β e.hom β a)) 1 = (ConcreteCategory.hom (prod.fst β e.hom β b)) 1 β a = bh02:vβ = vββ’ (ConcreteCategory.hom (m01 β jβ)) 1 = (ConcreteCategory.hom (m01 β cAL)) 1 All goals completed! π
_ = cAA 1 := instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }jβ:A βΆ L := coprod.inl β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }jβ:A βΆ L := coprod.inr β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β cAL)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1m10:L βΆ A := coprod.desc prod.fst (cAA β prod.fst)m01:L βΆ A := coprod.desc (cAA β prod.fst) prod.fsth10β:m10 β cAL = cAAh01β:m01 β cAL = cAAh10β:m10 β jβ = π Ah01β:m01 β jβ = cAAh10β:m10 β jβ = cAAh01β:m01 β jβ = π Ah_fXZ:β {X : Pointed} (f : X βΆ Z), f = { toFun := fun x β¦ Z.point, map_point := β― }h_fAL:β {a b : A βΆ L},
(ConcreteCategory.hom (prod.fst β e.hom β a)) 1 = (ConcreteCategory.hom (prod.fst β e.hom β b)) 1 β a = bh02:vβ = vββ’ (ConcreteCategory.hom (m01 β cAL)) 1 = (ConcreteCategory.hom cAA) 1 All goals completed! π
_ = 0 := rfl
All goals completed! π
instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }jβ:A βΆ L := coprod.inl β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }jβ:A βΆ L := coprod.inr β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β cAL)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1m10:L βΆ A := coprod.desc prod.fst (cAA β prod.fst)m01:L βΆ A := coprod.desc (cAA β prod.fst) prod.fsth10β:m10 β cAL = cAAh01β:m01 β cAL = cAAh10β:m10 β jβ = π Ah01β:m01 β jβ = cAAh10β:m10 β jβ = cAAh01β:m01 β jβ = π Ah_fXZ:β {X : Pointed} (f : X βΆ Z), f = { toFun := fun x β¦ Z.point, map_point := β― }h_fAL:β {a b : A βΆ L},
(ConcreteCategory.hom (prod.fst β e.hom β a)) 1 = (ConcreteCategory.hom (prod.fst β e.hom β b)) 1 β a = bh12:vβ = vββ’ False have h_contra : (1 : Fin 2) = 0 := calc
1 = (π A) 1 := rfl
_ = (m10 β jβ) 1 := instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }jβ:A βΆ L := coprod.inl β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }jβ:A βΆ L := coprod.inr β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β cAL)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1m10:L βΆ A := coprod.desc prod.fst (cAA β prod.fst)m01:L βΆ A := coprod.desc (cAA β prod.fst) prod.fsth10β:m10 β cAL = cAAh01β:m01 β cAL = cAAh10β:m10 β jβ = π Ah01β:m01 β jβ = cAAh10β:m10 β jβ = cAAh01β:m01 β jβ = π Ah_fXZ:β {X : Pointed} (f : X βΆ Z), f = { toFun := fun x β¦ Z.point, map_point := β― }h_fAL:β {a b : A βΆ L},
(ConcreteCategory.hom (prod.fst β e.hom β a)) 1 = (ConcreteCategory.hom (prod.fst β e.hom β b)) 1 β a = bh12:vβ = vββ’ (ConcreteCategory.hom (π A)) 1 = (ConcreteCategory.hom (m10 β jβ)) 1 All goals completed! π
_ = (m10 β jβ) 1 := instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }jβ:A βΆ L := coprod.inl β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }jβ:A βΆ L := coprod.inr β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β cAL)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1m10:L βΆ A := coprod.desc prod.fst (cAA β prod.fst)m01:L βΆ A := coprod.desc (cAA β prod.fst) prod.fsth10β:m10 β cAL = cAAh01β:m01 β cAL = cAAh10β:m10 β jβ = π Ah01β:m01 β jβ = cAAh10β:m10 β jβ = cAAh01β:m01 β jβ = π Ah_fXZ:β {X : Pointed} (f : X βΆ Z), f = { toFun := fun x β¦ Z.point, map_point := β― }h_fAL:β {a b : A βΆ L},
(ConcreteCategory.hom (prod.fst β e.hom β a)) 1 = (ConcreteCategory.hom (prod.fst β e.hom β b)) 1 β a = bh12:vβ = vββ’ (ConcreteCategory.hom (m10 β jβ)) 1 = (ConcreteCategory.hom (m10 β jβ)) 1 All goals completed! π
_ = cAA 1 := instββ΄:HasBinaryProduct A BβinstβΒ³:HasBinaryProduct A BβinstβΒ²:HasBinaryCoproduct (A β¨― Bβ) (A β¨― Bβ)instβΒΉ:HasBinaryCoproduct Bβ Bβinstβ:HasBinaryProduct A (Bβ β¨Ώ Bβ)e:(A β¨― Bβ) β¨Ώ A β¨― Bβ β
A β¨― Bβ β¨Ώ BβL:Pointed := (A β¨― Bβ) β¨Ώ A β¨― BβZ:Pointed := Bβ β¨Ώ BβcAA:A βΆ A := { toFun := fun x β¦ A.point, map_point := β― }cAL:A βΆ L := { toFun := fun x β¦ L.point, map_point := β― }jβ:A βΆ L := coprod.inl β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }jβ:A βΆ L := coprod.inr β prod.lift (π A) { toFun := fun x β¦ Bβ.point, map_point := β― }vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β cAL)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1vβ:A.X := (ConcreteCategory.hom (prod.fst β e.hom β jβ)) 1m10:L βΆ A := coprod.desc prod.fst (cAA β prod.fst)m01:L βΆ A := coprod.desc (cAA β prod.fst) prod.fsth10β:m10 β cAL = cAAh01β:m01 β cAL = cAAh10β:m10 β jβ = π Ah01β:m01 β jβ = cAAh10β:m10 β jβ = cAAh01β:m01 β jβ = π Ah_fXZ:β {X : Pointed} (f : X βΆ Z), f = { toFun := fun x β¦ Z.point, map_point := β― }h_fAL:β {a b : A βΆ L},
(ConcreteCategory.hom (prod.fst β e.hom β a)) 1 = (ConcreteCategory.hom (prod.fst β e.hom β b)) 1 β a = bh12:vβ = vββ’ (ConcreteCategory.hom (m10 β jβ)) 1 = (ConcreteCategory.hom cAA) 1 All goals completed! π
_ = 0 := rfl
All goals completed! π
Exercise 2 (p. 298)
As we saw, in the category of pointed sets, the (only) map {\mathbf{0} \rightarrow \mathbf{1}} is an isomorphism. Show that the other clause in the definition of linear category fails, i.e. find objects A and B in \mathbf{1}/πΊ for which the 'identity matrix'
A + B \rightarrow A \times B
is not an isomorphism.
Solution: Exercise 2
Taking A and B to be, respectively,
def A : Pointed := {
X := Fin 2
point := 0
}
def B : Pointed := {
X := Fin 2
point := 0
}
we can show that the identity matrix is not an isomorphism, as follows:
instance : OfNat A.X 0 where
ofNat := (0 : Fin 2)
instance : OfNat A.X 1 where
ofNat := (1 : Fin 2)
instance : OfNat B.X 0 where
ofNat := (0 : Fin 2)
instance : OfNat B.X 1 where
ofNat := (1 : Fin 2)
-- Define helper functions
lemma eval_zero {X Y : Pointed} [HasZeroMorphisms Pointed] (x : X.X) :
(0 : X βΆ Y) x = Y.point := X:PointedY:Pointedinstβ:HasZeroMorphisms Pointedx:X.Xβ’ (ConcreteCategory.hom 0) x = Y.point
X:PointedY:Pointedinstβ:HasZeroMorphisms Pointedx:X.Xthis:{ toFun := fun x β¦ Y.point, map_point := β― } β 0 = 0β’ (ConcreteCategory.hom 0) x = Y.point
X:PointedY:Pointedinstβ:HasZeroMorphisms Pointedx:X.Xthis:{ toFun := fun x β¦ Y.point, map_point := β― } β 0 = 0β’ (ConcreteCategory.hom ({ toFun := fun x β¦ Y.point, map_point := β― } β 0)) x = Y.point; All goals completed! π
abbrev d11 : Fin 2 β Fin 2 β Fin 2
| 1, 1 => 1
| _, _ => 0
example [HasZeroMorphisms Pointed]
[HasBinaryProduct A B] [HasBinaryCoproduct A B] :
IsEmpty (IsIso
(coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B)))) := instβΒ²:HasZeroMorphisms PointedinstβΒΉ:HasBinaryProduct A Binstβ:HasBinaryCoproduct A Bβ’ IsEmpty (IsIso (coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B))))
instβΒ²:HasZeroMorphisms PointedinstβΒΉ:HasBinaryProduct A Binstβ:HasBinaryCoproduct A Bβ’ IsIso (coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B))) β False
instβΒ²:HasZeroMorphisms PointedinstβΒΉ:HasBinaryProduct A Binstβ:HasBinaryCoproduct A Bh_iso:IsIso (coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B)))β’ False
-- Construct identity matrix
instβΒ²:HasZeroMorphisms PointedinstβΒΉ:HasBinaryProduct A Binstβ:HasBinaryCoproduct A Bh_iso:IsIso (coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B)))I:A β¨Ώ B βΆ A β¨― B := coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B))β’ False
-- Construct morphism v mapping (1, 1) to 1 and everything else to 0
let v : A β¨― B βΆ A := {
toFun := fun x β¦
d11 ((prod.fst : A β¨― B βΆ A).toFun x)
((prod.snd : A β¨― B βΆ B).toFun x)
map_point := instβΒ²:HasZeroMorphisms PointedinstβΒΉ:HasBinaryProduct A Binstβ:HasBinaryCoproduct A Bh_iso:IsIso (coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B)))I:A β¨Ώ B βΆ A β¨― B := coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B))β’ d11 (prod.fst.toFun (A β¨― B).point) (prod.snd.toFun (A β¨― B).point) = A.point
instβΒ²:HasZeroMorphisms PointedinstβΒΉ:HasBinaryProduct A Binstβ:HasBinaryCoproduct A Bh_iso:IsIso (coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B)))I:A β¨Ώ B βΆ A β¨― B := coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B))β’ d11 A.point B.point = A.point; All goals completed! π
}
-- Construct diagonal morphism mapping 1 to (1, 1)
instβΒ²:HasZeroMorphisms PointedinstβΒΉ:HasBinaryProduct A Binstβ:HasBinaryCoproduct A Bh_iso:IsIso (coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B)))I:A β¨Ώ B βΆ A β¨― B := coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B))v:A β¨― B βΆ A := { toFun := fun x β¦ d11 (prod.fst.toFun x) (prod.snd.toFun x), map_point := β― }f11:A βΆ A β¨― B := prod.lift (π A) { toFun := fun x β¦ x, map_point := β― }β’ False
-- Evaluate projections on left (a, 0) and right (0, b) axes
have eval_inl_fst (x : A.X) :
((prod.fst : A β¨― B βΆ A) β prod.lift (π A) 0) x = x := instβΒ²:HasZeroMorphisms PointedinstβΒΉ:HasBinaryProduct A Binstβ:HasBinaryCoproduct A Bβ’ IsEmpty (IsIso (coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B))))
instβΒ²:HasZeroMorphisms PointedinstβΒΉ:HasBinaryProduct A Binstβ:HasBinaryCoproduct A Bh_iso:IsIso (coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B)))I:A β¨Ώ B βΆ A β¨― B := coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B))v:A β¨― B βΆ A := { toFun := fun x β¦ d11 (prod.fst.toFun x) (prod.snd.toFun x), map_point := β― }f11:A βΆ A β¨― B := prod.lift (π A) { toFun := fun x β¦ x, map_point := β― }x:A.Xβ’ (ConcreteCategory.hom (π A)) x = x; All goals completed! π
have eval_inl_snd (x : A.X) :
((prod.snd : A β¨― B βΆ B) β prod.lift (π A) 0) x = 0 := instβΒ²:HasZeroMorphisms PointedinstβΒΉ:HasBinaryProduct A Binstβ:HasBinaryCoproduct A Bβ’ IsEmpty (IsIso (coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B))))
instβΒ²:HasZeroMorphisms PointedinstβΒΉ:HasBinaryProduct A Binstβ:HasBinaryCoproduct A Bh_iso:IsIso (coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B)))I:A β¨Ώ B βΆ A β¨― B := coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B))v:A β¨― B βΆ A := { toFun := fun x β¦ d11 (prod.fst.toFun x) (prod.snd.toFun x), map_point := β― }f11:A βΆ A β¨― B := prod.lift (π A) { toFun := fun x β¦ x, map_point := β― }eval_inl_fst:β (x : A.X), (ConcreteCategory.hom (prod.fst β prod.lift (π A) 0)) x = xx:A.Xβ’ (ConcreteCategory.hom 0) x = 0
All goals completed! π
have eval_inr_fst (x : B.X) :
((prod.fst : A β¨― B βΆ A) β prod.lift 0 (π B)) x = 0 := instβΒ²:HasZeroMorphisms PointedinstβΒΉ:HasBinaryProduct A Binstβ:HasBinaryCoproduct A Bβ’ IsEmpty (IsIso (coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B))))
instβΒ²:HasZeroMorphisms PointedinstβΒΉ:HasBinaryProduct A Binstβ:HasBinaryCoproduct A Bh_iso:IsIso (coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B)))I:A β¨Ώ B βΆ A β¨― B := coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B))v:A β¨― B βΆ A := { toFun := fun x β¦ d11 (prod.fst.toFun x) (prod.snd.toFun x), map_point := β― }f11:A βΆ A β¨― B := prod.lift (π A) { toFun := fun x β¦ x, map_point := β― }eval_inl_fst:β (x : A.X), (ConcreteCategory.hom (prod.fst β prod.lift (π A) 0)) x = xeval_inl_snd:β (x : A.X), (ConcreteCategory.hom (prod.snd β prod.lift (π A) 0)) x = 0x:B.Xβ’ (ConcreteCategory.hom 0) x = 0
All goals completed! π
have eval_inr_snd (x : B.X) :
((prod.snd : A β¨― B βΆ B) β prod.lift 0 (π B)) x = x := instβΒ²:HasZeroMorphisms PointedinstβΒΉ:HasBinaryProduct A Binstβ:HasBinaryCoproduct A Bβ’ IsEmpty (IsIso (coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B))))
instβΒ²:HasZeroMorphisms PointedinstβΒΉ:HasBinaryProduct A Binstβ:HasBinaryCoproduct A Bh_iso:IsIso (coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B)))I:A β¨Ώ B βΆ A β¨― B := coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B))v:A β¨― B βΆ A := { toFun := fun x β¦ d11 (prod.fst.toFun x) (prod.snd.toFun x), map_point := β― }f11:A βΆ A β¨― B := prod.lift (π A) { toFun := fun x β¦ x, map_point := β― }eval_inl_fst:β (x : A.X), (ConcreteCategory.hom (prod.fst β prod.lift (π A) 0)) x = xeval_inl_snd:β (x : A.X), (ConcreteCategory.hom (prod.snd β prod.lift (π A) 0)) x = 0eval_inr_fst:β (x : B.X), (ConcreteCategory.hom (prod.fst β prod.lift 0 (π B))) x = 0x:B.Xβ’ (ConcreteCategory.hom (π B)) x = x; All goals completed! π
-- Show v acts exactly like zero morphism on left axis
have hv_inl :
(v β I) β coprod.inl = (0 β I) β coprod.inl := instβΒ²:HasZeroMorphisms PointedinstβΒΉ:HasBinaryProduct A Binstβ:HasBinaryCoproduct A Bβ’ IsEmpty (IsIso (coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B))))
instβΒ²:HasZeroMorphisms PointedinstβΒΉ:HasBinaryProduct A Binstβ:HasBinaryCoproduct A Bh_iso:IsIso (coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B)))I:A β¨Ώ B βΆ A β¨― B := coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B))v:A β¨― B βΆ A := { toFun := fun x β¦ d11 (prod.fst.toFun x) (prod.snd.toFun x), map_point := β― }f11:A βΆ A β¨― B := prod.lift (π A) { toFun := fun x β¦ x, map_point := β― }eval_inl_fst:β (x : A.X), (ConcreteCategory.hom (prod.fst β prod.lift (π A) 0)) x = xeval_inl_snd:β (x : A.X), (ConcreteCategory.hom (prod.snd β prod.lift (π A) 0)) x = 0eval_inr_fst:β (x : B.X), (ConcreteCategory.hom (prod.fst β prod.lift 0 (π B))) x = 0eval_inr_snd:β (x : B.X), (ConcreteCategory.hom (prod.snd β prod.lift 0 (π B))) x = xthis:I β coprod.inl = prod.lift (π A) 0β’ (v β I) β coprod.inl = (0 β I) β coprod.inl
instβΒ²:HasZeroMorphisms PointedinstβΒΉ:HasBinaryProduct A Binstβ:HasBinaryCoproduct A Bh_iso:IsIso (coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B)))I:A β¨Ώ B βΆ A β¨― B := coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B))v:A β¨― B βΆ A := { toFun := fun x β¦ d11 (prod.fst.toFun x) (prod.snd.toFun x), map_point := β― }f11:A βΆ A β¨― B := prod.lift (π A) { toFun := fun x β¦ x, map_point := β― }eval_inl_fst:β (x : A.X), (ConcreteCategory.hom (prod.fst β prod.lift (π A) 0)) x = xeval_inl_snd:β (x : A.X), (ConcreteCategory.hom (prod.snd β prod.lift (π A) 0)) x = 0eval_inr_fst:β (x : B.X), (ConcreteCategory.hom (prod.fst β prod.lift 0 (π B))) x = 0eval_inr_snd:β (x : B.X), (ConcreteCategory.hom (prod.snd β prod.lift 0 (π B))) x = xthis:I β coprod.inl = prod.lift (π A) 0β’ v β prod.lift (π A) 0 = 0 β prod.lift (π A) 0
instβΒ²:HasZeroMorphisms PointedinstβΒΉ:HasBinaryProduct A Binstβ:HasBinaryCoproduct A Bh_iso:IsIso (coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B)))I:A β¨Ώ B βΆ A β¨― B := coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B))v:A β¨― B βΆ A := { toFun := fun x β¦ d11 (prod.fst.toFun x) (prod.snd.toFun x), map_point := β― }f11:A βΆ A β¨― B := prod.lift (π A) { toFun := fun x β¦ x, map_point := β― }eval_inl_fst:β (x : A.X), (ConcreteCategory.hom (prod.fst β prod.lift (π A) 0)) x = xeval_inl_snd:β (x : A.X), (ConcreteCategory.hom (prod.snd β prod.lift (π A) 0)) x = 0eval_inr_fst:β (x : B.X), (ConcreteCategory.hom (prod.fst β prod.lift 0 (π B))) x = 0eval_inr_snd:β (x : B.X), (ConcreteCategory.hom (prod.snd β prod.lift 0 (π B))) x = xthis:I β coprod.inl = prod.lift (π A) 0x:A.Xβ’ β(ConcreteCategory.hom (v β prod.lift (π A) 0)) x = β(ConcreteCategory.hom (0 β prod.lift (π A) 0)) x
instβΒ²:HasZeroMorphisms PointedinstβΒΉ:HasBinaryProduct A Binstβ:HasBinaryCoproduct A Bh_iso:IsIso (coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B)))I:A β¨Ώ B βΆ A β¨― B := coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B))v:A β¨― B βΆ A := { toFun := fun x β¦ d11 (prod.fst.toFun x) (prod.snd.toFun x), map_point := β― }f11:A βΆ A β¨― B := prod.lift (π A) { toFun := fun x β¦ x, map_point := β― }eval_inl_fst:β (x : A.X), (ConcreteCategory.hom (prod.fst β prod.lift (π A) 0)) x = xeval_inl_snd:β (x : A.X), (ConcreteCategory.hom (prod.snd β prod.lift (π A) 0)) x = 0eval_inr_fst:β (x : B.X), (ConcreteCategory.hom (prod.fst β prod.lift 0 (π B))) x = 0eval_inr_snd:β (x : B.X), (ConcreteCategory.hom (prod.snd β prod.lift 0 (π B))) x = xthis:I β coprod.inl = prod.lift (π A) 0x:A.Xβ’ d11 ((ConcreteCategory.hom (prod.fst β prod.lift (π A) 0)) x)
((ConcreteCategory.hom (prod.snd β prod.lift (π A) 0)) x) =
(ConcreteCategory.hom 0) ((ConcreteCategory.hom (prod.lift (π A) 0)) x)
instβΒ²:HasZeroMorphisms PointedinstβΒΉ:HasBinaryProduct A Binstβ:HasBinaryCoproduct A Bh_iso:IsIso (coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B)))I:A β¨Ώ B βΆ A β¨― B := coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B))v:A β¨― B βΆ A := { toFun := fun x β¦ d11 (prod.fst.toFun x) (prod.snd.toFun x), map_point := β― }f11:A βΆ A β¨― B := prod.lift (π A) { toFun := fun x β¦ x, map_point := β― }eval_inl_fst:β (x : A.X), (ConcreteCategory.hom (prod.fst β prod.lift (π A) 0)) x = xeval_inl_snd:β (x : A.X), (ConcreteCategory.hom (prod.snd β prod.lift (π A) 0)) x = 0eval_inr_fst:β (x : B.X), (ConcreteCategory.hom (prod.fst β prod.lift 0 (π B))) x = 0eval_inr_snd:β (x : B.X), (ConcreteCategory.hom (prod.snd β prod.lift 0 (π B))) x = xthis:I β coprod.inl = prod.lift (π A) 0x:A.Xβ’ d11 x 0 = A.point
instβΒ²:HasZeroMorphisms PointedinstβΒΉ:HasBinaryProduct A Binstβ:HasBinaryCoproduct A Bh_iso:IsIso (coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B)))I:A β¨Ώ B βΆ A β¨― B := coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B))v:A β¨― B βΆ A := { toFun := fun x β¦ d11 (prod.fst.toFun x) (prod.snd.toFun x), map_point := β― }f11:A βΆ A β¨― B := prod.lift (π A) { toFun := fun x β¦ x, map_point := β― }eval_inl_fst:β (x : A.X), (ConcreteCategory.hom (prod.fst β prod.lift (π A) 0)) x = xeval_inl_snd:β (x : A.X), (ConcreteCategory.hom (prod.snd β prod.lift (π A) 0)) x = 0eval_inr_fst:β (x : B.X), (ConcreteCategory.hom (prod.fst β prod.lift 0 (π B))) x = 0eval_inr_snd:β (x : B.X), (ConcreteCategory.hom (prod.snd β prod.lift 0 (π B))) x = xthis:I β coprod.inl = prod.lift (π A) 0x:Fin 2β’ d11 x 0 = A.point
instβΒ²:HasZeroMorphisms PointedinstβΒΉ:HasBinaryProduct A Binstβ:HasBinaryCoproduct A Bh_iso:IsIso (coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B)))I:A β¨Ώ B βΆ A β¨― B := coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B))v:A β¨― B βΆ A := { toFun := fun x β¦ d11 (prod.fst.toFun x) (prod.snd.toFun x), map_point := β― }f11:A βΆ A β¨― B := prod.lift (π A) { toFun := fun x β¦ x, map_point := β― }eval_inl_fst:β (x : A.X), (ConcreteCategory.hom (prod.fst β prod.lift (π A) 0)) x = xeval_inl_snd:β (x : A.X), (ConcreteCategory.hom (prod.snd β prod.lift (π A) 0)) x = 0eval_inr_fst:β (x : B.X), (ConcreteCategory.hom (prod.fst β prod.lift 0 (π B))) x = 0eval_inr_snd:β (x : B.X), (ConcreteCategory.hom (prod.snd β prod.lift 0 (π B))) x = xthis:I β coprod.inl = prod.lift (π A) 0β’ d11 ((fun i β¦ i) β¨0, β―β©) 0 = A.pointinstβΒ²:HasZeroMorphisms PointedinstβΒΉ:HasBinaryProduct A Binstβ:HasBinaryCoproduct A Bh_iso:IsIso (coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B)))I:A β¨Ώ B βΆ A β¨― B := coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B))v:A β¨― B βΆ A := { toFun := fun x β¦ d11 (prod.fst.toFun x) (prod.snd.toFun x), map_point := β― }f11:A βΆ A β¨― B := prod.lift (π A) { toFun := fun x β¦ x, map_point := β― }eval_inl_fst:β (x : A.X), (ConcreteCategory.hom (prod.fst β prod.lift (π A) 0)) x = xeval_inl_snd:β (x : A.X), (ConcreteCategory.hom (prod.snd β prod.lift (π A) 0)) x = 0eval_inr_fst:β (x : B.X), (ConcreteCategory.hom (prod.fst β prod.lift 0 (π B))) x = 0eval_inr_snd:β (x : B.X), (ConcreteCategory.hom (prod.snd β prod.lift 0 (π B))) x = xthis:I β coprod.inl = prod.lift (π A) 0β’ d11 ((fun i β¦ i) β¨1, β―β©) 0 = A.point instβΒ²:HasZeroMorphisms PointedinstβΒΉ:HasBinaryProduct A Binstβ:HasBinaryCoproduct A Bh_iso:IsIso (coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B)))I:A β¨Ώ B βΆ A β¨― B := coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B))v:A β¨― B βΆ A := { toFun := fun x β¦ d11 (prod.fst.toFun x) (prod.snd.toFun x), map_point := β― }f11:A βΆ A β¨― B := prod.lift (π A) { toFun := fun x β¦ x, map_point := β― }eval_inl_fst:β (x : A.X), (ConcreteCategory.hom (prod.fst β prod.lift (π A) 0)) x = xeval_inl_snd:β (x : A.X), (ConcreteCategory.hom (prod.snd β prod.lift (π A) 0)) x = 0eval_inr_fst:β (x : B.X), (ConcreteCategory.hom (prod.fst β prod.lift 0 (π B))) x = 0eval_inr_snd:β (x : B.X), (ConcreteCategory.hom (prod.snd β prod.lift 0 (π B))) x = xthis:I β coprod.inl = prod.lift (π A) 0β’ d11 ((fun i β¦ i) β¨0, β―β©) 0 = A.pointinstβΒ²:HasZeroMorphisms PointedinstβΒΉ:HasBinaryProduct A Binstβ:HasBinaryCoproduct A Bh_iso:IsIso (coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B)))I:A β¨Ώ B βΆ A β¨― B := coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B))v:A β¨― B βΆ A := { toFun := fun x β¦ d11 (prod.fst.toFun x) (prod.snd.toFun x), map_point := β― }f11:A βΆ A β¨― B := prod.lift (π A) { toFun := fun x β¦ x, map_point := β― }eval_inl_fst:β (x : A.X), (ConcreteCategory.hom (prod.fst β prod.lift (π A) 0)) x = xeval_inl_snd:β (x : A.X), (ConcreteCategory.hom (prod.snd β prod.lift (π A) 0)) x = 0eval_inr_fst:β (x : B.X), (ConcreteCategory.hom (prod.fst β prod.lift 0 (π B))) x = 0eval_inr_snd:β (x : B.X), (ConcreteCategory.hom (prod.snd β prod.lift 0 (π B))) x = xthis:I β coprod.inl = prod.lift (π A) 0β’ d11 ((fun i β¦ i) β¨1, β―β©) 0 = A.point All goals completed! π
-- Show v acts exactly like zero morphism on right axis
have hv_inr :
(v β I) β coprod.inr = (0 β I) β coprod.inr := instβΒ²:HasZeroMorphisms PointedinstβΒΉ:HasBinaryProduct A Binstβ:HasBinaryCoproduct A Bβ’ IsEmpty (IsIso (coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B))))
instβΒ²:HasZeroMorphisms PointedinstβΒΉ:HasBinaryProduct A Binstβ:HasBinaryCoproduct A Bh_iso:IsIso (coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B)))I:A β¨Ώ B βΆ A β¨― B := coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B))v:A β¨― B βΆ A := { toFun := fun x β¦ d11 (prod.fst.toFun x) (prod.snd.toFun x), map_point := β― }f11:A βΆ A β¨― B := prod.lift (π A) { toFun := fun x β¦ x, map_point := β― }eval_inl_fst:β (x : A.X), (ConcreteCategory.hom (prod.fst β prod.lift (π A) 0)) x = xeval_inl_snd:β (x : A.X), (ConcreteCategory.hom (prod.snd β prod.lift (π A) 0)) x = 0eval_inr_fst:β (x : B.X), (ConcreteCategory.hom (prod.fst β prod.lift 0 (π B))) x = 0eval_inr_snd:β (x : B.X), (ConcreteCategory.hom (prod.snd β prod.lift 0 (π B))) x = xhv_inl:(v β I) β coprod.inl = (0 β I) β coprod.inlthis:I β coprod.inr = prod.lift 0 (π B)β’ (v β I) β coprod.inr = (0 β I) β coprod.inr
instβΒ²:HasZeroMorphisms PointedinstβΒΉ:HasBinaryProduct A Binstβ:HasBinaryCoproduct A Bh_iso:IsIso (coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B)))I:A β¨Ώ B βΆ A β¨― B := coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B))v:A β¨― B βΆ A := { toFun := fun x β¦ d11 (prod.fst.toFun x) (prod.snd.toFun x), map_point := β― }f11:A βΆ A β¨― B := prod.lift (π A) { toFun := fun x β¦ x, map_point := β― }eval_inl_fst:β (x : A.X), (ConcreteCategory.hom (prod.fst β prod.lift (π A) 0)) x = xeval_inl_snd:β (x : A.X), (ConcreteCategory.hom (prod.snd β prod.lift (π A) 0)) x = 0eval_inr_fst:β (x : B.X), (ConcreteCategory.hom (prod.fst β prod.lift 0 (π B))) x = 0eval_inr_snd:β (x : B.X), (ConcreteCategory.hom (prod.snd β prod.lift 0 (π B))) x = xhv_inl:(v β I) β coprod.inl = (0 β I) β coprod.inlthis:I β coprod.inr = prod.lift 0 (π B)β’ v β prod.lift 0 (π B) = 0 β prod.lift 0 (π B)
instβΒ²:HasZeroMorphisms PointedinstβΒΉ:HasBinaryProduct A Binstβ:HasBinaryCoproduct A Bh_iso:IsIso (coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B)))I:A β¨Ώ B βΆ A β¨― B := coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B))v:A β¨― B βΆ A := { toFun := fun x β¦ d11 (prod.fst.toFun x) (prod.snd.toFun x), map_point := β― }f11:A βΆ A β¨― B := prod.lift (π A) { toFun := fun x β¦ x, map_point := β― }eval_inl_fst:β (x : A.X), (ConcreteCategory.hom (prod.fst β prod.lift (π A) 0)) x = xeval_inl_snd:β (x : A.X), (ConcreteCategory.hom (prod.snd β prod.lift (π A) 0)) x = 0eval_inr_fst:β (x : B.X), (ConcreteCategory.hom (prod.fst β prod.lift 0 (π B))) x = 0eval_inr_snd:β (x : B.X), (ConcreteCategory.hom (prod.snd β prod.lift 0 (π B))) x = xhv_inl:(v β I) β coprod.inl = (0 β I) β coprod.inlthis:I β coprod.inr = prod.lift 0 (π B)x:B.Xβ’ β(ConcreteCategory.hom (v β prod.lift 0 (π B))) x = β(ConcreteCategory.hom (0 β prod.lift 0 (π B))) x
instβΒ²:HasZeroMorphisms PointedinstβΒΉ:HasBinaryProduct A Binstβ:HasBinaryCoproduct A Bh_iso:IsIso (coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B)))I:A β¨Ώ B βΆ A β¨― B := coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B))v:A β¨― B βΆ A := { toFun := fun x β¦ d11 (prod.fst.toFun x) (prod.snd.toFun x), map_point := β― }f11:A βΆ A β¨― B := prod.lift (π A) { toFun := fun x β¦ x, map_point := β― }eval_inl_fst:β (x : A.X), (ConcreteCategory.hom (prod.fst β prod.lift (π A) 0)) x = xeval_inl_snd:β (x : A.X), (ConcreteCategory.hom (prod.snd β prod.lift (π A) 0)) x = 0eval_inr_fst:β (x : B.X), (ConcreteCategory.hom (prod.fst β prod.lift 0 (π B))) x = 0eval_inr_snd:β (x : B.X), (ConcreteCategory.hom (prod.snd β prod.lift 0 (π B))) x = xhv_inl:(v β I) β coprod.inl = (0 β I) β coprod.inlthis:I β coprod.inr = prod.lift 0 (π B)x:B.Xβ’ d11 ((ConcreteCategory.hom (prod.fst β prod.lift 0 (π B))) x)
((ConcreteCategory.hom (prod.snd β prod.lift 0 (π B))) x) =
(ConcreteCategory.hom 0) ((ConcreteCategory.hom (prod.lift 0 (π B))) x)
instβΒ²:HasZeroMorphisms PointedinstβΒΉ:HasBinaryProduct A Binstβ:HasBinaryCoproduct A Bh_iso:IsIso (coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B)))I:A β¨Ώ B βΆ A β¨― B := coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B))v:A β¨― B βΆ A := { toFun := fun x β¦ d11 (prod.fst.toFun x) (prod.snd.toFun x), map_point := β― }f11:A βΆ A β¨― B := prod.lift (π A) { toFun := fun x β¦ x, map_point := β― }eval_inl_fst:β (x : A.X), (ConcreteCategory.hom (prod.fst β prod.lift (π A) 0)) x = xeval_inl_snd:β (x : A.X), (ConcreteCategory.hom (prod.snd β prod.lift (π A) 0)) x = 0eval_inr_fst:β (x : B.X), (ConcreteCategory.hom (prod.fst β prod.lift 0 (π B))) x = 0eval_inr_snd:β (x : B.X), (ConcreteCategory.hom (prod.snd β prod.lift 0 (π B))) x = xhv_inl:(v β I) β coprod.inl = (0 β I) β coprod.inlthis:I β coprod.inr = prod.lift 0 (π B)x:B.Xβ’ d11 0 x = A.point
instβΒ²:HasZeroMorphisms PointedinstβΒΉ:HasBinaryProduct A Binstβ:HasBinaryCoproduct A Bh_iso:IsIso (coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B)))I:A β¨Ώ B βΆ A β¨― B := coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B))v:A β¨― B βΆ A := { toFun := fun x β¦ d11 (prod.fst.toFun x) (prod.snd.toFun x), map_point := β― }f11:A βΆ A β¨― B := prod.lift (π A) { toFun := fun x β¦ x, map_point := β― }eval_inl_fst:β (x : A.X), (ConcreteCategory.hom (prod.fst β prod.lift (π A) 0)) x = xeval_inl_snd:β (x : A.X), (ConcreteCategory.hom (prod.snd β prod.lift (π A) 0)) x = 0eval_inr_fst:β (x : B.X), (ConcreteCategory.hom (prod.fst β prod.lift 0 (π B))) x = 0eval_inr_snd:β (x : B.X), (ConcreteCategory.hom (prod.snd β prod.lift 0 (π B))) x = xhv_inl:(v β I) β coprod.inl = (0 β I) β coprod.inlthis:I β coprod.inr = prod.lift 0 (π B)x:Fin 2β’ d11 0 x = A.point
instβΒ²:HasZeroMorphisms PointedinstβΒΉ:HasBinaryProduct A Binstβ:HasBinaryCoproduct A Bh_iso:IsIso (coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B)))I:A β¨Ώ B βΆ A β¨― B := coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B))v:A β¨― B βΆ A := { toFun := fun x β¦ d11 (prod.fst.toFun x) (prod.snd.toFun x), map_point := β― }f11:A βΆ A β¨― B := prod.lift (π A) { toFun := fun x β¦ x, map_point := β― }eval_inl_fst:β (x : A.X), (ConcreteCategory.hom (prod.fst β prod.lift (π A) 0)) x = xeval_inl_snd:β (x : A.X), (ConcreteCategory.hom (prod.snd β prod.lift (π A) 0)) x = 0eval_inr_fst:β (x : B.X), (ConcreteCategory.hom (prod.fst β prod.lift 0 (π B))) x = 0eval_inr_snd:β (x : B.X), (ConcreteCategory.hom (prod.snd β prod.lift 0 (π B))) x = xhv_inl:(v β I) β coprod.inl = (0 β I) β coprod.inlthis:I β coprod.inr = prod.lift 0 (π B)β’ d11 0 ((fun i β¦ i) β¨0, β―β©) = A.pointinstβΒ²:HasZeroMorphisms PointedinstβΒΉ:HasBinaryProduct A Binstβ:HasBinaryCoproduct A Bh_iso:IsIso (coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B)))I:A β¨Ώ B βΆ A β¨― B := coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B))v:A β¨― B βΆ A := { toFun := fun x β¦ d11 (prod.fst.toFun x) (prod.snd.toFun x), map_point := β― }f11:A βΆ A β¨― B := prod.lift (π A) { toFun := fun x β¦ x, map_point := β― }eval_inl_fst:β (x : A.X), (ConcreteCategory.hom (prod.fst β prod.lift (π A) 0)) x = xeval_inl_snd:β (x : A.X), (ConcreteCategory.hom (prod.snd β prod.lift (π A) 0)) x = 0eval_inr_fst:β (x : B.X), (ConcreteCategory.hom (prod.fst β prod.lift 0 (π B))) x = 0eval_inr_snd:β (x : B.X), (ConcreteCategory.hom (prod.snd β prod.lift 0 (π B))) x = xhv_inl:(v β I) β coprod.inl = (0 β I) β coprod.inlthis:I β coprod.inr = prod.lift 0 (π B)β’ d11 0 ((fun i β¦ i) β¨1, β―β©) = A.point instβΒ²:HasZeroMorphisms PointedinstβΒΉ:HasBinaryProduct A Binstβ:HasBinaryCoproduct A Bh_iso:IsIso (coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B)))I:A β¨Ώ B βΆ A β¨― B := coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B))v:A β¨― B βΆ A := { toFun := fun x β¦ d11 (prod.fst.toFun x) (prod.snd.toFun x), map_point := β― }f11:A βΆ A β¨― B := prod.lift (π A) { toFun := fun x β¦ x, map_point := β― }eval_inl_fst:β (x : A.X), (ConcreteCategory.hom (prod.fst β prod.lift (π A) 0)) x = xeval_inl_snd:β (x : A.X), (ConcreteCategory.hom (prod.snd β prod.lift (π A) 0)) x = 0eval_inr_fst:β (x : B.X), (ConcreteCategory.hom (prod.fst β prod.lift 0 (π B))) x = 0eval_inr_snd:β (x : B.X), (ConcreteCategory.hom (prod.snd β prod.lift 0 (π B))) x = xhv_inl:(v β I) β coprod.inl = (0 β I) β coprod.inlthis:I β coprod.inr = prod.lift 0 (π B)β’ d11 0 ((fun i β¦ i) β¨0, β―β©) = A.pointinstβΒ²:HasZeroMorphisms PointedinstβΒΉ:HasBinaryProduct A Binstβ:HasBinaryCoproduct A Bh_iso:IsIso (coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B)))I:A β¨Ώ B βΆ A β¨― B := coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B))v:A β¨― B βΆ A := { toFun := fun x β¦ d11 (prod.fst.toFun x) (prod.snd.toFun x), map_point := β― }f11:A βΆ A β¨― B := prod.lift (π A) { toFun := fun x β¦ x, map_point := β― }eval_inl_fst:β (x : A.X), (ConcreteCategory.hom (prod.fst β prod.lift (π A) 0)) x = xeval_inl_snd:β (x : A.X), (ConcreteCategory.hom (prod.snd β prod.lift (π A) 0)) x = 0eval_inr_fst:β (x : B.X), (ConcreteCategory.hom (prod.fst β prod.lift 0 (π B))) x = 0eval_inr_snd:β (x : B.X), (ConcreteCategory.hom (prod.snd β prod.lift 0 (π B))) x = xhv_inl:(v β I) β coprod.inl = (0 β I) β coprod.inlthis:I β coprod.inr = prod.lift 0 (π B)β’ d11 0 ((fun i β¦ i) β¨1, β―β©) = A.point All goals completed! π
-- Hence v must be zero morphism
have hv_eq : v = 0 := instβΒ²:HasZeroMorphisms PointedinstβΒΉ:HasBinaryProduct A Binstβ:HasBinaryCoproduct A Bβ’ IsEmpty (IsIso (coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B))))
instβΒ²:HasZeroMorphisms PointedinstβΒΉ:HasBinaryProduct A Binstβ:HasBinaryCoproduct A Bh_iso:IsIso (coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B)))I:A β¨Ώ B βΆ A β¨― B := coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B))v:A β¨― B βΆ A := { toFun := fun x β¦ d11 (prod.fst.toFun x) (prod.snd.toFun x), map_point := β― }f11:A βΆ A β¨― B := prod.lift (π A) { toFun := fun x β¦ x, map_point := β― }eval_inl_fst:β (x : A.X), (ConcreteCategory.hom (prod.fst β prod.lift (π A) 0)) x = xeval_inl_snd:β (x : A.X), (ConcreteCategory.hom (prod.snd β prod.lift (π A) 0)) x = 0eval_inr_fst:β (x : B.X), (ConcreteCategory.hom (prod.fst β prod.lift 0 (π B))) x = 0eval_inr_snd:β (x : B.X), (ConcreteCategory.hom (prod.snd β prod.lift 0 (π B))) x = xhv_inl:(v β I) β coprod.inl = (0 β I) β coprod.inlhv_inr:(v β I) β coprod.inr = (0 β I) β coprod.inrβ’ v β π (A β¨― B) = 0 β π (A β¨― B)
instβΒ²:HasZeroMorphisms PointedinstβΒΉ:HasBinaryProduct A Binstβ:HasBinaryCoproduct A Bh_iso:IsIso (coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B)))I:A β¨Ώ B βΆ A β¨― B := coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B))v:A β¨― B βΆ A := { toFun := fun x β¦ d11 (prod.fst.toFun x) (prod.snd.toFun x), map_point := β― }f11:A βΆ A β¨― B := prod.lift (π A) { toFun := fun x β¦ x, map_point := β― }eval_inl_fst:β (x : A.X), (ConcreteCategory.hom (prod.fst β prod.lift (π A) 0)) x = xeval_inl_snd:β (x : A.X), (ConcreteCategory.hom (prod.snd β prod.lift (π A) 0)) x = 0eval_inr_fst:β (x : B.X), (ConcreteCategory.hom (prod.fst β prod.lift 0 (π B))) x = 0eval_inr_snd:β (x : B.X), (ConcreteCategory.hom (prod.snd β prod.lift 0 (π B))) x = xhv_inl:(v β I) β coprod.inl = (0 β I) β coprod.inlhv_inr:(v β I) β coprod.inr = (0 β I) β coprod.inrβ’ v β I β inv I = 0 β I β inv I
repeat instβΒ²:HasZeroMorphisms PointedinstβΒΉ:HasBinaryProduct A Binstβ:HasBinaryCoproduct A Bh_iso:IsIso (coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B)))I:A β¨Ώ B βΆ A β¨― B := coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B))v:A β¨― B βΆ A := { toFun := fun x β¦ d11 (prod.fst.toFun x) (prod.snd.toFun x), map_point := β― }f11:A βΆ A β¨― B := prod.lift (π A) { toFun := fun x β¦ x, map_point := β― }eval_inl_fst:β (x : A.X), (ConcreteCategory.hom (prod.fst β prod.lift (π A) 0)) x = xeval_inl_snd:β (x : A.X), (ConcreteCategory.hom (prod.snd β prod.lift (π A) 0)) x = 0eval_inr_fst:β (x : B.X), (ConcreteCategory.hom (prod.fst β prod.lift 0 (π B))) x = 0eval_inr_snd:β (x : B.X), (ConcreteCategory.hom (prod.snd β prod.lift 0 (π B))) x = xhv_inl:(v β I) β coprod.inl = (0 β I) β coprod.inlhv_inr:(v β I) β coprod.inr = (0 β I) β coprod.inrβ’ (v β I) β inv I = (0 β I) β inv I
All goals completed! π
-- Derive 1 = 0 contradiction by evaluating v at (1, 1)
have h_contra : (1 : Fin 2) = 0 := calc
1 = d11 1 1 := rfl
_ = d11 (((prod.fst : A β¨― B βΆ A) β f11) 1)
(((prod.snd : A β¨― B βΆ B) β f11) 1) := instβΒ²:HasZeroMorphisms PointedinstβΒΉ:HasBinaryProduct A Binstβ:HasBinaryCoproduct A Bh_iso:IsIso (coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B)))I:A β¨Ώ B βΆ A β¨― B := coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B))v:A β¨― B βΆ A := { toFun := fun x β¦ d11 (prod.fst.toFun x) (prod.snd.toFun x), map_point := β― }f11:A βΆ A β¨― B := prod.lift (π A) { toFun := fun x β¦ x, map_point := β― }eval_inl_fst:β (x : A.X), (ConcreteCategory.hom (prod.fst β prod.lift (π A) 0)) x = xeval_inl_snd:β (x : A.X), (ConcreteCategory.hom (prod.snd β prod.lift (π A) 0)) x = 0eval_inr_fst:β (x : B.X), (ConcreteCategory.hom (prod.fst β prod.lift 0 (π B))) x = 0eval_inr_snd:β (x : B.X), (ConcreteCategory.hom (prod.snd β prod.lift 0 (π B))) x = xhv_inl:(v β I) β coprod.inl = (0 β I) β coprod.inlhv_inr:(v β I) β coprod.inr = (0 β I) β coprod.inrhv_eq:v = 0β’ d11 1 1 = d11 ((ConcreteCategory.hom (prod.fst β f11)) 1) ((ConcreteCategory.hom (prod.snd β f11)) 1)
instβΒ²:HasZeroMorphisms PointedinstβΒΉ:HasBinaryProduct A Binstβ:HasBinaryCoproduct A Bh_iso:IsIso (coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B)))I:A β¨Ώ B βΆ A β¨― B := coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B))v:A β¨― B βΆ A := { toFun := fun x β¦ d11 (prod.fst.toFun x) (prod.snd.toFun x), map_point := β― }f11:A βΆ A β¨― B := prod.lift (π A) { toFun := fun x β¦ x, map_point := β― }eval_inl_fst:β (x : A.X), (ConcreteCategory.hom (prod.fst β prod.lift (π A) 0)) x = xeval_inl_snd:β (x : A.X), (ConcreteCategory.hom (prod.snd β prod.lift (π A) 0)) x = 0eval_inr_fst:β (x : B.X), (ConcreteCategory.hom (prod.fst β prod.lift 0 (π B))) x = 0eval_inr_snd:β (x : B.X), (ConcreteCategory.hom (prod.snd β prod.lift 0 (π B))) x = xhv_inl:(v β I) β coprod.inl = (0 β I) β coprod.inlhv_inr:(v β I) β coprod.inr = (0 β I) β coprod.inrhv_eq:v = 0β’ d11 1 1 = d11 ((ConcreteCategory.hom (π A)) 1) ((ConcreteCategory.hom { toFun := fun x β¦ x, map_point := β― }) 1); All goals completed! π
_ = v (f11 1) := rfl
_ = (0 : A β¨― B βΆ A) (f11 1) := instβΒ²:HasZeroMorphisms PointedinstβΒΉ:HasBinaryProduct A Binstβ:HasBinaryCoproduct A Bh_iso:IsIso (coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B)))I:A β¨Ώ B βΆ A β¨― B := coprod.desc (prod.lift (π A) 0) (prod.lift 0 (π B))v:A β¨― B βΆ A := { toFun := fun x β¦ d11 (prod.fst.toFun x) (prod.snd.toFun x), map_point := β― }f11:A βΆ A β¨― B := prod.lift (π A) { toFun := fun x β¦ x, map_point := β― }eval_inl_fst:β (x : A.X), (ConcreteCategory.hom (prod.fst β prod.lift (π A) 0)) x = xeval_inl_snd:β (x : A.X), (ConcreteCategory.hom (prod.snd β prod.lift (π A) 0)) x = 0eval_inr_fst:β (x : B.X), (ConcreteCategory.hom (prod.fst β prod.lift 0 (π B))) x = 0eval_inr_snd:β (x : B.X), (ConcreteCategory.hom (prod.snd β prod.lift 0 (π B))) x = xhv_inl:(v β I) β coprod.inl = (0 β I) β coprod.inlhv_inr:(v β I) β coprod.inr = (0 β I) β coprod.inrhv_eq:v = 0β’ (ConcreteCategory.hom v) ((ConcreteCategory.hom f11) 1) = (ConcreteCategory.hom 0) ((ConcreteCategory.hom f11) 1) All goals completed! π
_ = 0 := eval_zero (f11 1)
All goals completed! π