Session 21: Products in categories
Definition: Product (p. 237)
Suppose that A and B are objects in a category π. A product of A and B (in π) is
-
an object
Pin π, and -
a pair of maps,
{P \xrightarrow{p_1} A},{P \xrightarrow{p_2} B}, in π satisfying:
for every object T and every pair of maps {T \xrightarrow{q_1} A}, {T \xrightarrow{q_2} B}, there is exactly one map {T \xrightarrow{q} P} for which {q_1 = p_1 \circ q} and {q_2 = p_2 \circ q}.
See the earlier definition of product on p. 217.
Theorem (p. 239)
Suppose that {A \xleftarrow{p_1} P \xrightarrow{p_2} B} and {A \xleftarrow{q_1} Q \xrightarrow{q_2} B}, are two products of A and B. Because {A \xleftarrow{p_1} P \xrightarrow{p_2} B} is a product, viewing Q as a 'test object' gives a map {Q \rightarrow P}; because {A \xleftarrow{q_1} Q \xrightarrow{q_2} B} is a product, we also get a map {P \rightarrow Q}. These two maps are necessarily inverse to each other, and therefore the two objects P, Q are isomorphic.
We provided a proof of this theorem in Exercise 12 of Article IV using the mathlib API for (binary) products. We repeat that proof here, but this time using only the book definition.
theorem uniqueness_of_products'
{π : Type u} [Category.{v, u} π] (A B P Q : π)
(pβ : P βΆ A) (pβ : P βΆ B)
(hP : β (T : π) (tβ : T βΆ A) (tβ : T βΆ B),
(β! t : T βΆ P, tβ = pβ β t β§ tβ = pβ β t))
(qβ : Q βΆ A) (qβ : Q βΆ B)
(hQ : β (T : π) (tβ : T βΆ A) (tβ : T βΆ B),
(β! t : T βΆ Q, tβ = qβ β t β§ tβ = qβ β t))
: Nonempty (P β
Q) := π:Type uinstβ:Category.{v, u} πA:πB:πP:πQ:πpβ:P βΆ Apβ:P βΆ BhP:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = pβ β t β§ tβ = pβ β tqβ:Q βΆ Aqβ:Q βΆ BhQ:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = qβ β t β§ tβ = qβ β tβ’ Nonempty (P β
Q)
π:Type uinstβ:Category.{v, u} πA:πB:πP:πQ:πpβ:P βΆ Apβ:P βΆ BhP:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = pβ β t β§ tβ = pβ β tqβ:Q βΆ Aqβ:Q βΆ BhQ:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = qβ β t β§ tβ = qβ β tf:P βΆ Qhf_comm:pβ = qβ β f β§ pβ = qβ β frightβ:β (y : P βΆ Q), (fun t β¦ pβ = qβ β t β§ pβ = qβ β t) y β y = fβ’ Nonempty (P β
Q)
π:Type uinstβ:Category.{v, u} πA:πB:πP:πQ:πpβ:P βΆ Apβ:P βΆ BhP:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = pβ β t β§ tβ = pβ β tqβ:Q βΆ Aqβ:Q βΆ BhQ:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = qβ β t β§ tβ = qβ β tf:P βΆ Qhf_comm:pβ = qβ β f β§ pβ = qβ β frightβΒΉ:β (y : P βΆ Q), (fun t β¦ pβ = qβ β t β§ pβ = qβ β t) y β y = fg:Q βΆ Phg_comm:qβ = pβ β g β§ qβ = pβ β grightβ:β (y : Q βΆ P), (fun t β¦ qβ = pβ β t β§ qβ = pβ β t) y β y = gβ’ Nonempty (P β
Q)
have hgf : g β f = π P := π:Type uinstβ:Category.{v, u} πA:πB:πP:πQ:πpβ:P βΆ Apβ:P βΆ BhP:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = pβ β t β§ tβ = pβ β tqβ:Q βΆ Aqβ:Q βΆ BhQ:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = qβ β t β§ tβ = qβ β tβ’ Nonempty (P β
Q)
π:Type uinstβ:Category.{v, u} πA:πB:πP:πQ:πpβ:P βΆ Apβ:P βΆ BhP:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = pβ β t β§ tβ = pβ β tqβ:Q βΆ Aqβ:Q βΆ BhQ:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = qβ β t β§ tβ = qβ β tf:P βΆ Qhf_comm:pβ = qβ β f β§ pβ = qβ β frightβΒΉ:β (y : P βΆ Q), (fun t β¦ pβ = qβ β t β§ pβ = qβ β t) y β y = fg:Q βΆ Phg_comm:qβ = pβ β g β§ qβ = pβ β grightβ:β (y : Q βΆ P), (fun t β¦ qβ = pβ β t β§ qβ = pβ β t) y β y = gβ’ pβ = pβ β g β f β§ pβ = pβ β g β fπ:Type uinstβ:Category.{v, u} πA:πB:πP:πQ:πpβ:P βΆ Apβ:P βΆ BhP:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = pβ β t β§ tβ = pβ β tqβ:Q βΆ Aqβ:Q βΆ BhQ:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = qβ β t β§ tβ = qβ β tf:P βΆ Qhf_comm:pβ = qβ β f β§ pβ = qβ β frightβΒΉ:β (y : P βΆ Q), (fun t β¦ pβ = qβ β t β§ pβ = qβ β t) y β y = fg:Q βΆ Phg_comm:qβ = pβ β g β§ qβ = pβ β grightβ:β (y : Q βΆ P), (fun t β¦ qβ = pβ β t β§ qβ = pβ β t) y β y = gβ’ pβ = pβ β π P β§ pβ = pβ β π P
π:Type uinstβ:Category.{v, u} πA:πB:πP:πQ:πpβ:P βΆ Apβ:P βΆ BhP:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = pβ β t β§ tβ = pβ β tqβ:Q βΆ Aqβ:Q βΆ BhQ:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = qβ β t β§ tβ = qβ β tf:P βΆ Qhf_comm:pβ = qβ β f β§ pβ = qβ β frightβΒΉ:β (y : P βΆ Q), (fun t β¦ pβ = qβ β t β§ pβ = qβ β t) y β y = fg:Q βΆ Phg_comm:qβ = pβ β g β§ qβ = pβ β grightβ:β (y : Q βΆ P), (fun t β¦ qβ = pβ β t β§ qβ = pβ β t) y β y = gβ’ pβ = pβ β g β f β§ pβ = pβ β g β f π:Type uinstβ:Category.{v, u} πA:πB:πP:πQ:πpβ:P βΆ Apβ:P βΆ BhP:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = pβ β t β§ tβ = pβ β tqβ:Q βΆ Aqβ:Q βΆ BhQ:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = qβ β t β§ tβ = qβ β tf:P βΆ Qhf_comm:pβ = qβ β f β§ pβ = qβ β frightβΒΉ:β (y : P βΆ Q), (fun t β¦ pβ = qβ β t β§ pβ = qβ β t) y β y = fg:Q βΆ Phg_comm:qβ = pβ β g β§ qβ = pβ β grightβ:β (y : Q βΆ P), (fun t β¦ qβ = pβ β t β§ qβ = pβ β t) y β y = gβ’ pβ = pβ β g β fπ:Type uinstβ:Category.{v, u} πA:πB:πP:πQ:πpβ:P βΆ Apβ:P βΆ BhP:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = pβ β t β§ tβ = pβ β tqβ:Q βΆ Aqβ:Q βΆ BhQ:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = qβ β t β§ tβ = qβ β tf:P βΆ Qhf_comm:pβ = qβ β f β§ pβ = qβ β frightβΒΉ:β (y : P βΆ Q), (fun t β¦ pβ = qβ β t β§ pβ = qβ β t) y β y = fg:Q βΆ Phg_comm:qβ = pβ β g β§ qβ = pβ β grightβ:β (y : Q βΆ P), (fun t β¦ qβ = pβ β t β§ qβ = pβ β t) y β y = gβ’ pβ = pβ β g β f
π:Type uinstβ:Category.{v, u} πA:πB:πP:πQ:πpβ:P βΆ Apβ:P βΆ BhP:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = pβ β t β§ tβ = pβ β tqβ:Q βΆ Aqβ:Q βΆ BhQ:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = qβ β t β§ tβ = qβ β tf:P βΆ Qhf_comm:pβ = qβ β f β§ pβ = qβ β frightβΒΉ:β (y : P βΆ Q), (fun t β¦ pβ = qβ β t β§ pβ = qβ β t) y β y = fg:Q βΆ Phg_comm:qβ = pβ β g β§ qβ = pβ β grightβ:β (y : Q βΆ P), (fun t β¦ qβ = pβ β t β§ qβ = pβ β t) y β y = gβ’ pβ = pβ β g β f π:Type uinstβ:Category.{v, u} πA:πB:πP:πQ:πpβ:P βΆ Apβ:P βΆ BhP:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = pβ β t β§ tβ = pβ β tqβ:Q βΆ Aqβ:Q βΆ BhQ:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = qβ β t β§ tβ = qβ β tf:P βΆ Qhf_comm:pβ = qβ β f β§ pβ = qβ β frightβΒΉ:β (y : P βΆ Q), (fun t β¦ pβ = qβ β t β§ pβ = qβ β t) y β y = fg:Q βΆ Phg_comm:qβ = pβ β g β§ qβ = pβ β grightβ:β (y : Q βΆ P), (fun t β¦ qβ = pβ β t β§ qβ = pβ β t) y β y = gβ’ pβ β g β f = pβ
calc pβ β (g β f)
_ = (pβ β g) β f := π:Type uinstβ:Category.{v, u} πA:πB:πP:πQ:πpβ:P βΆ Apβ:P βΆ BhP:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = pβ β t β§ tβ = pβ β tqβ:Q βΆ Aqβ:Q βΆ BhQ:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = qβ β t β§ tβ = qβ β tf:P βΆ Qhf_comm:pβ = qβ β f β§ pβ = qβ β frightβΒΉ:β (y : P βΆ Q), (fun t β¦ pβ = qβ β t β§ pβ = qβ β t) y β y = fg:Q βΆ Phg_comm:qβ = pβ β g β§ qβ = pβ β grightβ:β (y : Q βΆ P), (fun t β¦ qβ = pβ β t β§ qβ = pβ β t) y β y = gβ’ pβ β g β f = (pβ β g) β f All goals completed! π
_ = qβ β f := π:Type uinstβ:Category.{v, u} πA:πB:πP:πQ:πpβ:P βΆ Apβ:P βΆ BhP:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = pβ β t β§ tβ = pβ β tqβ:Q βΆ Aqβ:Q βΆ BhQ:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = qβ β t β§ tβ = qβ β tf:P βΆ Qhf_comm:pβ = qβ β f β§ pβ = qβ β frightβΒΉ:β (y : P βΆ Q), (fun t β¦ pβ = qβ β t β§ pβ = qβ β t) y β y = fg:Q βΆ Phg_comm:qβ = pβ β g β§ qβ = pβ β grightβ:β (y : Q βΆ P), (fun t β¦ qβ = pβ β t β§ qβ = pβ β t) y β y = gβ’ (pβ β g) β f = qβ β f All goals completed! π
_ = pβ := π:Type uinstβ:Category.{v, u} πA:πB:πP:πQ:πpβ:P βΆ Apβ:P βΆ BhP:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = pβ β t β§ tβ = pβ β tqβ:Q βΆ Aqβ:Q βΆ BhQ:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = qβ β t β§ tβ = qβ β tf:P βΆ Qhf_comm:pβ = qβ β f β§ pβ = qβ β frightβΒΉ:β (y : P βΆ Q), (fun t β¦ pβ = qβ β t β§ pβ = qβ β t) y β y = fg:Q βΆ Phg_comm:qβ = pβ β g β§ qβ = pβ β grightβ:β (y : Q βΆ P), (fun t β¦ qβ = pβ β t β§ qβ = pβ β t) y β y = gβ’ qβ β f = pβ All goals completed! π
π:Type uinstβ:Category.{v, u} πA:πB:πP:πQ:πpβ:P βΆ Apβ:P βΆ BhP:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = pβ β t β§ tβ = pβ β tqβ:Q βΆ Aqβ:Q βΆ BhQ:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = qβ β t β§ tβ = qβ β tf:P βΆ Qhf_comm:pβ = qβ β f β§ pβ = qβ β frightβΒΉ:β (y : P βΆ Q), (fun t β¦ pβ = qβ β t β§ pβ = qβ β t) y β y = fg:Q βΆ Phg_comm:qβ = pβ β g β§ qβ = pβ β grightβ:β (y : Q βΆ P), (fun t β¦ qβ = pβ β t β§ qβ = pβ β t) y β y = gβ’ pβ = pβ β g β f π:Type uinstβ:Category.{v, u} πA:πB:πP:πQ:πpβ:P βΆ Apβ:P βΆ BhP:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = pβ β t β§ tβ = pβ β tqβ:Q βΆ Aqβ:Q βΆ BhQ:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = qβ β t β§ tβ = qβ β tf:P βΆ Qhf_comm:pβ = qβ β f β§ pβ = qβ β frightβΒΉ:β (y : P βΆ Q), (fun t β¦ pβ = qβ β t β§ pβ = qβ β t) y β y = fg:Q βΆ Phg_comm:qβ = pβ β g β§ qβ = pβ β grightβ:β (y : Q βΆ P), (fun t β¦ qβ = pβ β t β§ qβ = pβ β t) y β y = gβ’ pβ β g β f = pβ
calc pβ β (g β f)
_ = (pβ β g) β f := π:Type uinstβ:Category.{v, u} πA:πB:πP:πQ:πpβ:P βΆ Apβ:P βΆ BhP:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = pβ β t β§ tβ = pβ β tqβ:Q βΆ Aqβ:Q βΆ BhQ:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = qβ β t β§ tβ = qβ β tf:P βΆ Qhf_comm:pβ = qβ β f β§ pβ = qβ β frightβΒΉ:β (y : P βΆ Q), (fun t β¦ pβ = qβ β t β§ pβ = qβ β t) y β y = fg:Q βΆ Phg_comm:qβ = pβ β g β§ qβ = pβ β grightβ:β (y : Q βΆ P), (fun t β¦ qβ = pβ β t β§ qβ = pβ β t) y β y = gβ’ pβ β g β f = (pβ β g) β f All goals completed! π
_ = qβ β f := π:Type uinstβ:Category.{v, u} πA:πB:πP:πQ:πpβ:P βΆ Apβ:P βΆ BhP:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = pβ β t β§ tβ = pβ β tqβ:Q βΆ Aqβ:Q βΆ BhQ:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = qβ β t β§ tβ = qβ β tf:P βΆ Qhf_comm:pβ = qβ β f β§ pβ = qβ β frightβΒΉ:β (y : P βΆ Q), (fun t β¦ pβ = qβ β t β§ pβ = qβ β t) y β y = fg:Q βΆ Phg_comm:qβ = pβ β g β§ qβ = pβ β grightβ:β (y : Q βΆ P), (fun t β¦ qβ = pβ β t β§ qβ = pβ β t) y β y = gβ’ (pβ β g) β f = qβ β f All goals completed! π
_ = pβ := π:Type uinstβ:Category.{v, u} πA:πB:πP:πQ:πpβ:P βΆ Apβ:P βΆ BhP:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = pβ β t β§ tβ = pβ β tqβ:Q βΆ Aqβ:Q βΆ BhQ:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = qβ β t β§ tβ = qβ β tf:P βΆ Qhf_comm:pβ = qβ β f β§ pβ = qβ β frightβΒΉ:β (y : P βΆ Q), (fun t β¦ pβ = qβ β t β§ pβ = qβ β t) y β y = fg:Q βΆ Phg_comm:qβ = pβ β g β§ qβ = pβ β grightβ:β (y : Q βΆ P), (fun t β¦ qβ = pβ β t β§ qβ = pβ β t) y β y = gβ’ qβ β f = pβ All goals completed! π
π:Type uinstβ:Category.{v, u} πA:πB:πP:πQ:πpβ:P βΆ Apβ:P βΆ BhP:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = pβ β t β§ tβ = pβ β tqβ:Q βΆ Aqβ:Q βΆ BhQ:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = qβ β t β§ tβ = qβ β tf:P βΆ Qhf_comm:pβ = qβ β f β§ pβ = qβ β frightβΒΉ:β (y : P βΆ Q), (fun t β¦ pβ = qβ β t β§ pβ = qβ β t) y β y = fg:Q βΆ Phg_comm:qβ = pβ β g β§ qβ = pβ β grightβ:β (y : Q βΆ P), (fun t β¦ qβ = pβ β t β§ qβ = pβ β t) y β y = gβ’ pβ = pβ β π P β§ pβ = pβ β π P π:Type uinstβ:Category.{v, u} πA:πB:πP:πQ:πpβ:P βΆ Apβ:P βΆ BhP:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = pβ β t β§ tβ = pβ β tqβ:Q βΆ Aqβ:Q βΆ BhQ:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = qβ β t β§ tβ = qβ β tf:P βΆ Qhf_comm:pβ = qβ β f β§ pβ = qβ β frightβΒΉ:β (y : P βΆ Q), (fun t β¦ pβ = qβ β t β§ pβ = qβ β t) y β y = fg:Q βΆ Phg_comm:qβ = pβ β g β§ qβ = pβ β grightβ:β (y : Q βΆ P), (fun t β¦ qβ = pβ β t β§ qβ = pβ β t) y β y = gβ’ pβ = pβ β π Pπ:Type uinstβ:Category.{v, u} πA:πB:πP:πQ:πpβ:P βΆ Apβ:P βΆ BhP:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = pβ β t β§ tβ = pβ β tqβ:Q βΆ Aqβ:Q βΆ BhQ:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = qβ β t β§ tβ = qβ β tf:P βΆ Qhf_comm:pβ = qβ β f β§ pβ = qβ β frightβΒΉ:β (y : P βΆ Q), (fun t β¦ pβ = qβ β t β§ pβ = qβ β t) y β y = fg:Q βΆ Phg_comm:qβ = pβ β g β§ qβ = pβ β grightβ:β (y : Q βΆ P), (fun t β¦ qβ = pβ β t β§ qβ = pβ β t) y β y = gβ’ pβ = pβ β π P π:Type uinstβ:Category.{v, u} πA:πB:πP:πQ:πpβ:P βΆ Apβ:P βΆ BhP:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = pβ β t β§ tβ = pβ β tqβ:Q βΆ Aqβ:Q βΆ BhQ:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = qβ β t β§ tβ = qβ β tf:P βΆ Qhf_comm:pβ = qβ β f β§ pβ = qβ β frightβΒΉ:β (y : P βΆ Q), (fun t β¦ pβ = qβ β t β§ pβ = qβ β t) y β y = fg:Q βΆ Phg_comm:qβ = pβ β g β§ qβ = pβ β grightβ:β (y : Q βΆ P), (fun t β¦ qβ = pβ β t β§ qβ = pβ β t) y β y = gβ’ pβ = pβ β π Pπ:Type uinstβ:Category.{v, u} πA:πB:πP:πQ:πpβ:P βΆ Apβ:P βΆ BhP:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = pβ β t β§ tβ = pβ β tqβ:Q βΆ Aqβ:Q βΆ BhQ:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = qβ β t β§ tβ = qβ β tf:P βΆ Qhf_comm:pβ = qβ β f β§ pβ = qβ β frightβΒΉ:β (y : P βΆ Q), (fun t β¦ pβ = qβ β t β§ pβ = qβ β t) y β y = fg:Q βΆ Phg_comm:qβ = pβ β g β§ qβ = pβ β grightβ:β (y : Q βΆ P), (fun t β¦ qβ = pβ β t β§ qβ = pβ β t) y β y = gβ’ pβ = pβ β π P All goals completed! π
have hfg : f β g = π Q := π:Type uinstβ:Category.{v, u} πA:πB:πP:πQ:πpβ:P βΆ Apβ:P βΆ BhP:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = pβ β t β§ tβ = pβ β tqβ:Q βΆ Aqβ:Q βΆ BhQ:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = qβ β t β§ tβ = qβ β tβ’ Nonempty (P β
Q)
π:Type uinstβ:Category.{v, u} πA:πB:πP:πQ:πpβ:P βΆ Apβ:P βΆ BhP:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = pβ β t β§ tβ = pβ β tqβ:Q βΆ Aqβ:Q βΆ BhQ:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = qβ β t β§ tβ = qβ β tf:P βΆ Qhf_comm:pβ = qβ β f β§ pβ = qβ β frightβΒΉ:β (y : P βΆ Q), (fun t β¦ pβ = qβ β t β§ pβ = qβ β t) y β y = fg:Q βΆ Phg_comm:qβ = pβ β g β§ qβ = pβ β grightβ:β (y : Q βΆ P), (fun t β¦ qβ = pβ β t β§ qβ = pβ β t) y β y = ghgf:g β f = π P :=
ExistsUnique.unique (hP P pβ pβ)
β¨Eq.symm
(Trans.trans
(Trans.trans
(Trans.trans rfl
(Eq.mpr (id (congrArg (fun _a β¦ _a = (pβ β g) β f) (Category.assoc f g pβ))) (Eq.refl ((pβ β g) β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a β f = qβ β f) (Eq.symm hg_comm.left))) (Eq.refl (qβ β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a = pβ) (Eq.symm hf_comm.left))) (Eq.refl pβ))),
Eq.symm
(Trans.trans
(Trans.trans
(Trans.trans rfl
(Eq.mpr (id (congrArg (fun _a β¦ _a = (pβ β g) β f) (Category.assoc f g pβ))) (Eq.refl ((pβ β g) β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a β f = qβ β f) (Eq.symm hg_comm.right))) (Eq.refl (qβ β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a = pβ) (Eq.symm hf_comm.right))) (Eq.refl pβ)))β©
β¨Eq.mpr (id (congrArg (fun _a β¦ pβ = _a) (Category.id_comp pβ))) (Eq.refl pβ),
Eq.mpr (id (congrArg (fun _a β¦ pβ = _a) (Category.id_comp pβ))) (Eq.refl pβ)β©β’ qβ = qβ β f β g β§ qβ = qβ β f β gπ:Type uinstβ:Category.{v, u} πA:πB:πP:πQ:πpβ:P βΆ Apβ:P βΆ BhP:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = pβ β t β§ tβ = pβ β tqβ:Q βΆ Aqβ:Q βΆ BhQ:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = qβ β t β§ tβ = qβ β tf:P βΆ Qhf_comm:pβ = qβ β f β§ pβ = qβ β frightβΒΉ:β (y : P βΆ Q), (fun t β¦ pβ = qβ β t β§ pβ = qβ β t) y β y = fg:Q βΆ Phg_comm:qβ = pβ β g β§ qβ = pβ β grightβ:β (y : Q βΆ P), (fun t β¦ qβ = pβ β t β§ qβ = pβ β t) y β y = ghgf:g β f = π P :=
ExistsUnique.unique (hP P pβ pβ)
β¨Eq.symm
(Trans.trans
(Trans.trans
(Trans.trans rfl
(Eq.mpr (id (congrArg (fun _a β¦ _a = (pβ β g) β f) (Category.assoc f g pβ))) (Eq.refl ((pβ β g) β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a β f = qβ β f) (Eq.symm hg_comm.left))) (Eq.refl (qβ β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a = pβ) (Eq.symm hf_comm.left))) (Eq.refl pβ))),
Eq.symm
(Trans.trans
(Trans.trans
(Trans.trans rfl
(Eq.mpr (id (congrArg (fun _a β¦ _a = (pβ β g) β f) (Category.assoc f g pβ))) (Eq.refl ((pβ β g) β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a β f = qβ β f) (Eq.symm hg_comm.right))) (Eq.refl (qβ β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a = pβ) (Eq.symm hf_comm.right))) (Eq.refl pβ)))β©
β¨Eq.mpr (id (congrArg (fun _a β¦ pβ = _a) (Category.id_comp pβ))) (Eq.refl pβ),
Eq.mpr (id (congrArg (fun _a β¦ pβ = _a) (Category.id_comp pβ))) (Eq.refl pβ)β©β’ qβ = qβ β π Q β§ qβ = qβ β π Q
π:Type uinstβ:Category.{v, u} πA:πB:πP:πQ:πpβ:P βΆ Apβ:P βΆ BhP:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = pβ β t β§ tβ = pβ β tqβ:Q βΆ Aqβ:Q βΆ BhQ:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = qβ β t β§ tβ = qβ β tf:P βΆ Qhf_comm:pβ = qβ β f β§ pβ = qβ β frightβΒΉ:β (y : P βΆ Q), (fun t β¦ pβ = qβ β t β§ pβ = qβ β t) y β y = fg:Q βΆ Phg_comm:qβ = pβ β g β§ qβ = pβ β grightβ:β (y : Q βΆ P), (fun t β¦ qβ = pβ β t β§ qβ = pβ β t) y β y = ghgf:g β f = π P :=
ExistsUnique.unique (hP P pβ pβ)
β¨Eq.symm
(Trans.trans
(Trans.trans
(Trans.trans rfl
(Eq.mpr (id (congrArg (fun _a β¦ _a = (pβ β g) β f) (Category.assoc f g pβ))) (Eq.refl ((pβ β g) β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a β f = qβ β f) (Eq.symm hg_comm.left))) (Eq.refl (qβ β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a = pβ) (Eq.symm hf_comm.left))) (Eq.refl pβ))),
Eq.symm
(Trans.trans
(Trans.trans
(Trans.trans rfl
(Eq.mpr (id (congrArg (fun _a β¦ _a = (pβ β g) β f) (Category.assoc f g pβ))) (Eq.refl ((pβ β g) β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a β f = qβ β f) (Eq.symm hg_comm.right))) (Eq.refl (qβ β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a = pβ) (Eq.symm hf_comm.right))) (Eq.refl pβ)))β©
β¨Eq.mpr (id (congrArg (fun _a β¦ pβ = _a) (Category.id_comp pβ))) (Eq.refl pβ),
Eq.mpr (id (congrArg (fun _a β¦ pβ = _a) (Category.id_comp pβ))) (Eq.refl pβ)β©β’ qβ = qβ β f β g β§ qβ = qβ β f β g π:Type uinstβ:Category.{v, u} πA:πB:πP:πQ:πpβ:P βΆ Apβ:P βΆ BhP:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = pβ β t β§ tβ = pβ β tqβ:Q βΆ Aqβ:Q βΆ BhQ:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = qβ β t β§ tβ = qβ β tf:P βΆ Qhf_comm:pβ = qβ β f β§ pβ = qβ β frightβΒΉ:β (y : P βΆ Q), (fun t β¦ pβ = qβ β t β§ pβ = qβ β t) y β y = fg:Q βΆ Phg_comm:qβ = pβ β g β§ qβ = pβ β grightβ:β (y : Q βΆ P), (fun t β¦ qβ = pβ β t β§ qβ = pβ β t) y β y = ghgf:g β f = π P :=
ExistsUnique.unique (hP P pβ pβ)
β¨Eq.symm
(Trans.trans
(Trans.trans
(Trans.trans rfl
(Eq.mpr (id (congrArg (fun _a β¦ _a = (pβ β g) β f) (Category.assoc f g pβ))) (Eq.refl ((pβ β g) β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a β f = qβ β f) (Eq.symm hg_comm.left))) (Eq.refl (qβ β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a = pβ) (Eq.symm hf_comm.left))) (Eq.refl pβ))),
Eq.symm
(Trans.trans
(Trans.trans
(Trans.trans rfl
(Eq.mpr (id (congrArg (fun _a β¦ _a = (pβ β g) β f) (Category.assoc f g pβ))) (Eq.refl ((pβ β g) β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a β f = qβ β f) (Eq.symm hg_comm.right))) (Eq.refl (qβ β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a = pβ) (Eq.symm hf_comm.right))) (Eq.refl pβ)))β©
β¨Eq.mpr (id (congrArg (fun _a β¦ pβ = _a) (Category.id_comp pβ))) (Eq.refl pβ),
Eq.mpr (id (congrArg (fun _a β¦ pβ = _a) (Category.id_comp pβ))) (Eq.refl pβ)β©β’ qβ = qβ β f β gπ:Type uinstβ:Category.{v, u} πA:πB:πP:πQ:πpβ:P βΆ Apβ:P βΆ BhP:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = pβ β t β§ tβ = pβ β tqβ:Q βΆ Aqβ:Q βΆ BhQ:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = qβ β t β§ tβ = qβ β tf:P βΆ Qhf_comm:pβ = qβ β f β§ pβ = qβ β frightβΒΉ:β (y : P βΆ Q), (fun t β¦ pβ = qβ β t β§ pβ = qβ β t) y β y = fg:Q βΆ Phg_comm:qβ = pβ β g β§ qβ = pβ β grightβ:β (y : Q βΆ P), (fun t β¦ qβ = pβ β t β§ qβ = pβ β t) y β y = ghgf:g β f = π P :=
ExistsUnique.unique (hP P pβ pβ)
β¨Eq.symm
(Trans.trans
(Trans.trans
(Trans.trans rfl
(Eq.mpr (id (congrArg (fun _a β¦ _a = (pβ β g) β f) (Category.assoc f g pβ))) (Eq.refl ((pβ β g) β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a β f = qβ β f) (Eq.symm hg_comm.left))) (Eq.refl (qβ β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a = pβ) (Eq.symm hf_comm.left))) (Eq.refl pβ))),
Eq.symm
(Trans.trans
(Trans.trans
(Trans.trans rfl
(Eq.mpr (id (congrArg (fun _a β¦ _a = (pβ β g) β f) (Category.assoc f g pβ))) (Eq.refl ((pβ β g) β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a β f = qβ β f) (Eq.symm hg_comm.right))) (Eq.refl (qβ β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a = pβ) (Eq.symm hf_comm.right))) (Eq.refl pβ)))β©
β¨Eq.mpr (id (congrArg (fun _a β¦ pβ = _a) (Category.id_comp pβ))) (Eq.refl pβ),
Eq.mpr (id (congrArg (fun _a β¦ pβ = _a) (Category.id_comp pβ))) (Eq.refl pβ)β©β’ qβ = qβ β f β g
π:Type uinstβ:Category.{v, u} πA:πB:πP:πQ:πpβ:P βΆ Apβ:P βΆ BhP:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = pβ β t β§ tβ = pβ β tqβ:Q βΆ Aqβ:Q βΆ BhQ:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = qβ β t β§ tβ = qβ β tf:P βΆ Qhf_comm:pβ = qβ β f β§ pβ = qβ β frightβΒΉ:β (y : P βΆ Q), (fun t β¦ pβ = qβ β t β§ pβ = qβ β t) y β y = fg:Q βΆ Phg_comm:qβ = pβ β g β§ qβ = pβ β grightβ:β (y : Q βΆ P), (fun t β¦ qβ = pβ β t β§ qβ = pβ β t) y β y = ghgf:g β f = π P :=
ExistsUnique.unique (hP P pβ pβ)
β¨Eq.symm
(Trans.trans
(Trans.trans
(Trans.trans rfl
(Eq.mpr (id (congrArg (fun _a β¦ _a = (pβ β g) β f) (Category.assoc f g pβ))) (Eq.refl ((pβ β g) β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a β f = qβ β f) (Eq.symm hg_comm.left))) (Eq.refl (qβ β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a = pβ) (Eq.symm hf_comm.left))) (Eq.refl pβ))),
Eq.symm
(Trans.trans
(Trans.trans
(Trans.trans rfl
(Eq.mpr (id (congrArg (fun _a β¦ _a = (pβ β g) β f) (Category.assoc f g pβ))) (Eq.refl ((pβ β g) β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a β f = qβ β f) (Eq.symm hg_comm.right))) (Eq.refl (qβ β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a = pβ) (Eq.symm hf_comm.right))) (Eq.refl pβ)))β©
β¨Eq.mpr (id (congrArg (fun _a β¦ pβ = _a) (Category.id_comp pβ))) (Eq.refl pβ),
Eq.mpr (id (congrArg (fun _a β¦ pβ = _a) (Category.id_comp pβ))) (Eq.refl pβ)β©β’ qβ = qβ β f β g π:Type uinstβ:Category.{v, u} πA:πB:πP:πQ:πpβ:P βΆ Apβ:P βΆ BhP:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = pβ β t β§ tβ = pβ β tqβ:Q βΆ Aqβ:Q βΆ BhQ:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = qβ β t β§ tβ = qβ β tf:P βΆ Qhf_comm:pβ = qβ β f β§ pβ = qβ β frightβΒΉ:β (y : P βΆ Q), (fun t β¦ pβ = qβ β t β§ pβ = qβ β t) y β y = fg:Q βΆ Phg_comm:qβ = pβ β g β§ qβ = pβ β grightβ:β (y : Q βΆ P), (fun t β¦ qβ = pβ β t β§ qβ = pβ β t) y β y = ghgf:g β f = π P :=
ExistsUnique.unique (hP P pβ pβ)
β¨Eq.symm
(Trans.trans
(Trans.trans
(Trans.trans rfl
(Eq.mpr (id (congrArg (fun _a β¦ _a = (pβ β g) β f) (Category.assoc f g pβ))) (Eq.refl ((pβ β g) β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a β f = qβ β f) (Eq.symm hg_comm.left))) (Eq.refl (qβ β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a = pβ) (Eq.symm hf_comm.left))) (Eq.refl pβ))),
Eq.symm
(Trans.trans
(Trans.trans
(Trans.trans rfl
(Eq.mpr (id (congrArg (fun _a β¦ _a = (pβ β g) β f) (Category.assoc f g pβ))) (Eq.refl ((pβ β g) β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a β f = qβ β f) (Eq.symm hg_comm.right))) (Eq.refl (qβ β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a = pβ) (Eq.symm hf_comm.right))) (Eq.refl pβ)))β©
β¨Eq.mpr (id (congrArg (fun _a β¦ pβ = _a) (Category.id_comp pβ))) (Eq.refl pβ),
Eq.mpr (id (congrArg (fun _a β¦ pβ = _a) (Category.id_comp pβ))) (Eq.refl pβ)β©β’ qβ β f β g = qβ
calc qβ β (f β g)
_ = (qβ β f) β g := π:Type uinstβ:Category.{v, u} πA:πB:πP:πQ:πpβ:P βΆ Apβ:P βΆ BhP:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = pβ β t β§ tβ = pβ β tqβ:Q βΆ Aqβ:Q βΆ BhQ:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = qβ β t β§ tβ = qβ β tf:P βΆ Qhf_comm:pβ = qβ β f β§ pβ = qβ β frightβΒΉ:β (y : P βΆ Q), (fun t β¦ pβ = qβ β t β§ pβ = qβ β t) y β y = fg:Q βΆ Phg_comm:qβ = pβ β g β§ qβ = pβ β grightβ:β (y : Q βΆ P), (fun t β¦ qβ = pβ β t β§ qβ = pβ β t) y β y = ghgf:g β f = π P :=
ExistsUnique.unique (hP P pβ pβ)
β¨Eq.symm
(Trans.trans
(Trans.trans
(Trans.trans rfl
(Eq.mpr (id (congrArg (fun _a β¦ _a = (pβ β g) β f) (Category.assoc f g pβ))) (Eq.refl ((pβ β g) β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a β f = qβ β f) (Eq.symm hg_comm.left))) (Eq.refl (qβ β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a = pβ) (Eq.symm hf_comm.left))) (Eq.refl pβ))),
Eq.symm
(Trans.trans
(Trans.trans
(Trans.trans rfl
(Eq.mpr (id (congrArg (fun _a β¦ _a = (pβ β g) β f) (Category.assoc f g pβ))) (Eq.refl ((pβ β g) β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a β f = qβ β f) (Eq.symm hg_comm.right))) (Eq.refl (qβ β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a = pβ) (Eq.symm hf_comm.right))) (Eq.refl pβ)))β©
β¨Eq.mpr (id (congrArg (fun _a β¦ pβ = _a) (Category.id_comp pβ))) (Eq.refl pβ),
Eq.mpr (id (congrArg (fun _a β¦ pβ = _a) (Category.id_comp pβ))) (Eq.refl pβ)β©β’ qβ β f β g = (qβ β f) β g All goals completed! π
_ = pβ β g := π:Type uinstβ:Category.{v, u} πA:πB:πP:πQ:πpβ:P βΆ Apβ:P βΆ BhP:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = pβ β t β§ tβ = pβ β tqβ:Q βΆ Aqβ:Q βΆ BhQ:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = qβ β t β§ tβ = qβ β tf:P βΆ Qhf_comm:pβ = qβ β f β§ pβ = qβ β frightβΒΉ:β (y : P βΆ Q), (fun t β¦ pβ = qβ β t β§ pβ = qβ β t) y β y = fg:Q βΆ Phg_comm:qβ = pβ β g β§ qβ = pβ β grightβ:β (y : Q βΆ P), (fun t β¦ qβ = pβ β t β§ qβ = pβ β t) y β y = ghgf:g β f = π P :=
ExistsUnique.unique (hP P pβ pβ)
β¨Eq.symm
(Trans.trans
(Trans.trans
(Trans.trans rfl
(Eq.mpr (id (congrArg (fun _a β¦ _a = (pβ β g) β f) (Category.assoc f g pβ))) (Eq.refl ((pβ β g) β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a β f = qβ β f) (Eq.symm hg_comm.left))) (Eq.refl (qβ β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a = pβ) (Eq.symm hf_comm.left))) (Eq.refl pβ))),
Eq.symm
(Trans.trans
(Trans.trans
(Trans.trans rfl
(Eq.mpr (id (congrArg (fun _a β¦ _a = (pβ β g) β f) (Category.assoc f g pβ))) (Eq.refl ((pβ β g) β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a β f = qβ β f) (Eq.symm hg_comm.right))) (Eq.refl (qβ β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a = pβ) (Eq.symm hf_comm.right))) (Eq.refl pβ)))β©
β¨Eq.mpr (id (congrArg (fun _a β¦ pβ = _a) (Category.id_comp pβ))) (Eq.refl pβ),
Eq.mpr (id (congrArg (fun _a β¦ pβ = _a) (Category.id_comp pβ))) (Eq.refl pβ)β©β’ (qβ β f) β g = pβ β g All goals completed! π
_ = qβ := π:Type uinstβ:Category.{v, u} πA:πB:πP:πQ:πpβ:P βΆ Apβ:P βΆ BhP:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = pβ β t β§ tβ = pβ β tqβ:Q βΆ Aqβ:Q βΆ BhQ:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = qβ β t β§ tβ = qβ β tf:P βΆ Qhf_comm:pβ = qβ β f β§ pβ = qβ β frightβΒΉ:β (y : P βΆ Q), (fun t β¦ pβ = qβ β t β§ pβ = qβ β t) y β y = fg:Q βΆ Phg_comm:qβ = pβ β g β§ qβ = pβ β grightβ:β (y : Q βΆ P), (fun t β¦ qβ = pβ β t β§ qβ = pβ β t) y β y = ghgf:g β f = π P :=
ExistsUnique.unique (hP P pβ pβ)
β¨Eq.symm
(Trans.trans
(Trans.trans
(Trans.trans rfl
(Eq.mpr (id (congrArg (fun _a β¦ _a = (pβ β g) β f) (Category.assoc f g pβ))) (Eq.refl ((pβ β g) β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a β f = qβ β f) (Eq.symm hg_comm.left))) (Eq.refl (qβ β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a = pβ) (Eq.symm hf_comm.left))) (Eq.refl pβ))),
Eq.symm
(Trans.trans
(Trans.trans
(Trans.trans rfl
(Eq.mpr (id (congrArg (fun _a β¦ _a = (pβ β g) β f) (Category.assoc f g pβ))) (Eq.refl ((pβ β g) β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a β f = qβ β f) (Eq.symm hg_comm.right))) (Eq.refl (qβ β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a = pβ) (Eq.symm hf_comm.right))) (Eq.refl pβ)))β©
β¨Eq.mpr (id (congrArg (fun _a β¦ pβ = _a) (Category.id_comp pβ))) (Eq.refl pβ),
Eq.mpr (id (congrArg (fun _a β¦ pβ = _a) (Category.id_comp pβ))) (Eq.refl pβ)β©β’ pβ β g = qβ All goals completed! π
π:Type uinstβ:Category.{v, u} πA:πB:πP:πQ:πpβ:P βΆ Apβ:P βΆ BhP:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = pβ β t β§ tβ = pβ β tqβ:Q βΆ Aqβ:Q βΆ BhQ:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = qβ β t β§ tβ = qβ β tf:P βΆ Qhf_comm:pβ = qβ β f β§ pβ = qβ β frightβΒΉ:β (y : P βΆ Q), (fun t β¦ pβ = qβ β t β§ pβ = qβ β t) y β y = fg:Q βΆ Phg_comm:qβ = pβ β g β§ qβ = pβ β grightβ:β (y : Q βΆ P), (fun t β¦ qβ = pβ β t β§ qβ = pβ β t) y β y = ghgf:g β f = π P :=
ExistsUnique.unique (hP P pβ pβ)
β¨Eq.symm
(Trans.trans
(Trans.trans
(Trans.trans rfl
(Eq.mpr (id (congrArg (fun _a β¦ _a = (pβ β g) β f) (Category.assoc f g pβ))) (Eq.refl ((pβ β g) β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a β f = qβ β f) (Eq.symm hg_comm.left))) (Eq.refl (qβ β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a = pβ) (Eq.symm hf_comm.left))) (Eq.refl pβ))),
Eq.symm
(Trans.trans
(Trans.trans
(Trans.trans rfl
(Eq.mpr (id (congrArg (fun _a β¦ _a = (pβ β g) β f) (Category.assoc f g pβ))) (Eq.refl ((pβ β g) β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a β f = qβ β f) (Eq.symm hg_comm.right))) (Eq.refl (qβ β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a = pβ) (Eq.symm hf_comm.right))) (Eq.refl pβ)))β©
β¨Eq.mpr (id (congrArg (fun _a β¦ pβ = _a) (Category.id_comp pβ))) (Eq.refl pβ),
Eq.mpr (id (congrArg (fun _a β¦ pβ = _a) (Category.id_comp pβ))) (Eq.refl pβ)β©β’ qβ = qβ β f β g π:Type uinstβ:Category.{v, u} πA:πB:πP:πQ:πpβ:P βΆ Apβ:P βΆ BhP:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = pβ β t β§ tβ = pβ β tqβ:Q βΆ Aqβ:Q βΆ BhQ:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = qβ β t β§ tβ = qβ β tf:P βΆ Qhf_comm:pβ = qβ β f β§ pβ = qβ β frightβΒΉ:β (y : P βΆ Q), (fun t β¦ pβ = qβ β t β§ pβ = qβ β t) y β y = fg:Q βΆ Phg_comm:qβ = pβ β g β§ qβ = pβ β grightβ:β (y : Q βΆ P), (fun t β¦ qβ = pβ β t β§ qβ = pβ β t) y β y = ghgf:g β f = π P :=
ExistsUnique.unique (hP P pβ pβ)
β¨Eq.symm
(Trans.trans
(Trans.trans
(Trans.trans rfl
(Eq.mpr (id (congrArg (fun _a β¦ _a = (pβ β g) β f) (Category.assoc f g pβ))) (Eq.refl ((pβ β g) β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a β f = qβ β f) (Eq.symm hg_comm.left))) (Eq.refl (qβ β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a = pβ) (Eq.symm hf_comm.left))) (Eq.refl pβ))),
Eq.symm
(Trans.trans
(Trans.trans
(Trans.trans rfl
(Eq.mpr (id (congrArg (fun _a β¦ _a = (pβ β g) β f) (Category.assoc f g pβ))) (Eq.refl ((pβ β g) β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a β f = qβ β f) (Eq.symm hg_comm.right))) (Eq.refl (qβ β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a = pβ) (Eq.symm hf_comm.right))) (Eq.refl pβ)))β©
β¨Eq.mpr (id (congrArg (fun _a β¦ pβ = _a) (Category.id_comp pβ))) (Eq.refl pβ),
Eq.mpr (id (congrArg (fun _a β¦ pβ = _a) (Category.id_comp pβ))) (Eq.refl pβ)β©β’ qβ β f β g = qβ
calc qβ β (f β g)
_ = (qβ β f) β g := π:Type uinstβ:Category.{v, u} πA:πB:πP:πQ:πpβ:P βΆ Apβ:P βΆ BhP:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = pβ β t β§ tβ = pβ β tqβ:Q βΆ Aqβ:Q βΆ BhQ:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = qβ β t β§ tβ = qβ β tf:P βΆ Qhf_comm:pβ = qβ β f β§ pβ = qβ β frightβΒΉ:β (y : P βΆ Q), (fun t β¦ pβ = qβ β t β§ pβ = qβ β t) y β y = fg:Q βΆ Phg_comm:qβ = pβ β g β§ qβ = pβ β grightβ:β (y : Q βΆ P), (fun t β¦ qβ = pβ β t β§ qβ = pβ β t) y β y = ghgf:g β f = π P :=
ExistsUnique.unique (hP P pβ pβ)
β¨Eq.symm
(Trans.trans
(Trans.trans
(Trans.trans rfl
(Eq.mpr (id (congrArg (fun _a β¦ _a = (pβ β g) β f) (Category.assoc f g pβ))) (Eq.refl ((pβ β g) β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a β f = qβ β f) (Eq.symm hg_comm.left))) (Eq.refl (qβ β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a = pβ) (Eq.symm hf_comm.left))) (Eq.refl pβ))),
Eq.symm
(Trans.trans
(Trans.trans
(Trans.trans rfl
(Eq.mpr (id (congrArg (fun _a β¦ _a = (pβ β g) β f) (Category.assoc f g pβ))) (Eq.refl ((pβ β g) β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a β f = qβ β f) (Eq.symm hg_comm.right))) (Eq.refl (qβ β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a = pβ) (Eq.symm hf_comm.right))) (Eq.refl pβ)))β©
β¨Eq.mpr (id (congrArg (fun _a β¦ pβ = _a) (Category.id_comp pβ))) (Eq.refl pβ),
Eq.mpr (id (congrArg (fun _a β¦ pβ = _a) (Category.id_comp pβ))) (Eq.refl pβ)β©β’ qβ β f β g = (qβ β f) β g All goals completed! π
_ = pβ β g := π:Type uinstβ:Category.{v, u} πA:πB:πP:πQ:πpβ:P βΆ Apβ:P βΆ BhP:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = pβ β t β§ tβ = pβ β tqβ:Q βΆ Aqβ:Q βΆ BhQ:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = qβ β t β§ tβ = qβ β tf:P βΆ Qhf_comm:pβ = qβ β f β§ pβ = qβ β frightβΒΉ:β (y : P βΆ Q), (fun t β¦ pβ = qβ β t β§ pβ = qβ β t) y β y = fg:Q βΆ Phg_comm:qβ = pβ β g β§ qβ = pβ β grightβ:β (y : Q βΆ P), (fun t β¦ qβ = pβ β t β§ qβ = pβ β t) y β y = ghgf:g β f = π P :=
ExistsUnique.unique (hP P pβ pβ)
β¨Eq.symm
(Trans.trans
(Trans.trans
(Trans.trans rfl
(Eq.mpr (id (congrArg (fun _a β¦ _a = (pβ β g) β f) (Category.assoc f g pβ))) (Eq.refl ((pβ β g) β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a β f = qβ β f) (Eq.symm hg_comm.left))) (Eq.refl (qβ β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a = pβ) (Eq.symm hf_comm.left))) (Eq.refl pβ))),
Eq.symm
(Trans.trans
(Trans.trans
(Trans.trans rfl
(Eq.mpr (id (congrArg (fun _a β¦ _a = (pβ β g) β f) (Category.assoc f g pβ))) (Eq.refl ((pβ β g) β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a β f = qβ β f) (Eq.symm hg_comm.right))) (Eq.refl (qβ β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a = pβ) (Eq.symm hf_comm.right))) (Eq.refl pβ)))β©
β¨Eq.mpr (id (congrArg (fun _a β¦ pβ = _a) (Category.id_comp pβ))) (Eq.refl pβ),
Eq.mpr (id (congrArg (fun _a β¦ pβ = _a) (Category.id_comp pβ))) (Eq.refl pβ)β©β’ (qβ β f) β g = pβ β g All goals completed! π
_ = qβ := π:Type uinstβ:Category.{v, u} πA:πB:πP:πQ:πpβ:P βΆ Apβ:P βΆ BhP:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = pβ β t β§ tβ = pβ β tqβ:Q βΆ Aqβ:Q βΆ BhQ:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = qβ β t β§ tβ = qβ β tf:P βΆ Qhf_comm:pβ = qβ β f β§ pβ = qβ β frightβΒΉ:β (y : P βΆ Q), (fun t β¦ pβ = qβ β t β§ pβ = qβ β t) y β y = fg:Q βΆ Phg_comm:qβ = pβ β g β§ qβ = pβ β grightβ:β (y : Q βΆ P), (fun t β¦ qβ = pβ β t β§ qβ = pβ β t) y β y = ghgf:g β f = π P :=
ExistsUnique.unique (hP P pβ pβ)
β¨Eq.symm
(Trans.trans
(Trans.trans
(Trans.trans rfl
(Eq.mpr (id (congrArg (fun _a β¦ _a = (pβ β g) β f) (Category.assoc f g pβ))) (Eq.refl ((pβ β g) β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a β f = qβ β f) (Eq.symm hg_comm.left))) (Eq.refl (qβ β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a = pβ) (Eq.symm hf_comm.left))) (Eq.refl pβ))),
Eq.symm
(Trans.trans
(Trans.trans
(Trans.trans rfl
(Eq.mpr (id (congrArg (fun _a β¦ _a = (pβ β g) β f) (Category.assoc f g pβ))) (Eq.refl ((pβ β g) β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a β f = qβ β f) (Eq.symm hg_comm.right))) (Eq.refl (qβ β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a = pβ) (Eq.symm hf_comm.right))) (Eq.refl pβ)))β©
β¨Eq.mpr (id (congrArg (fun _a β¦ pβ = _a) (Category.id_comp pβ))) (Eq.refl pβ),
Eq.mpr (id (congrArg (fun _a β¦ pβ = _a) (Category.id_comp pβ))) (Eq.refl pβ)β©β’ pβ β g = qβ All goals completed! π
π:Type uinstβ:Category.{v, u} πA:πB:πP:πQ:πpβ:P βΆ Apβ:P βΆ BhP:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = pβ β t β§ tβ = pβ β tqβ:Q βΆ Aqβ:Q βΆ BhQ:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = qβ β t β§ tβ = qβ β tf:P βΆ Qhf_comm:pβ = qβ β f β§ pβ = qβ β frightβΒΉ:β (y : P βΆ Q), (fun t β¦ pβ = qβ β t β§ pβ = qβ β t) y β y = fg:Q βΆ Phg_comm:qβ = pβ β g β§ qβ = pβ β grightβ:β (y : Q βΆ P), (fun t β¦ qβ = pβ β t β§ qβ = pβ β t) y β y = ghgf:g β f = π P :=
ExistsUnique.unique (hP P pβ pβ)
β¨Eq.symm
(Trans.trans
(Trans.trans
(Trans.trans rfl
(Eq.mpr (id (congrArg (fun _a β¦ _a = (pβ β g) β f) (Category.assoc f g pβ))) (Eq.refl ((pβ β g) β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a β f = qβ β f) (Eq.symm hg_comm.left))) (Eq.refl (qβ β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a = pβ) (Eq.symm hf_comm.left))) (Eq.refl pβ))),
Eq.symm
(Trans.trans
(Trans.trans
(Trans.trans rfl
(Eq.mpr (id (congrArg (fun _a β¦ _a = (pβ β g) β f) (Category.assoc f g pβ))) (Eq.refl ((pβ β g) β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a β f = qβ β f) (Eq.symm hg_comm.right))) (Eq.refl (qβ β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a = pβ) (Eq.symm hf_comm.right))) (Eq.refl pβ)))β©
β¨Eq.mpr (id (congrArg (fun _a β¦ pβ = _a) (Category.id_comp pβ))) (Eq.refl pβ),
Eq.mpr (id (congrArg (fun _a β¦ pβ = _a) (Category.id_comp pβ))) (Eq.refl pβ)β©β’ qβ = qβ β π Q β§ qβ = qβ β π Q π:Type uinstβ:Category.{v, u} πA:πB:πP:πQ:πpβ:P βΆ Apβ:P βΆ BhP:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = pβ β t β§ tβ = pβ β tqβ:Q βΆ Aqβ:Q βΆ BhQ:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = qβ β t β§ tβ = qβ β tf:P βΆ Qhf_comm:pβ = qβ β f β§ pβ = qβ β frightβΒΉ:β (y : P βΆ Q), (fun t β¦ pβ = qβ β t β§ pβ = qβ β t) y β y = fg:Q βΆ Phg_comm:qβ = pβ β g β§ qβ = pβ β grightβ:β (y : Q βΆ P), (fun t β¦ qβ = pβ β t β§ qβ = pβ β t) y β y = ghgf:g β f = π P :=
ExistsUnique.unique (hP P pβ pβ)
β¨Eq.symm
(Trans.trans
(Trans.trans
(Trans.trans rfl
(Eq.mpr (id (congrArg (fun _a β¦ _a = (pβ β g) β f) (Category.assoc f g pβ))) (Eq.refl ((pβ β g) β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a β f = qβ β f) (Eq.symm hg_comm.left))) (Eq.refl (qβ β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a = pβ) (Eq.symm hf_comm.left))) (Eq.refl pβ))),
Eq.symm
(Trans.trans
(Trans.trans
(Trans.trans rfl
(Eq.mpr (id (congrArg (fun _a β¦ _a = (pβ β g) β f) (Category.assoc f g pβ))) (Eq.refl ((pβ β g) β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a β f = qβ β f) (Eq.symm hg_comm.right))) (Eq.refl (qβ β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a = pβ) (Eq.symm hf_comm.right))) (Eq.refl pβ)))β©
β¨Eq.mpr (id (congrArg (fun _a β¦ pβ = _a) (Category.id_comp pβ))) (Eq.refl pβ),
Eq.mpr (id (congrArg (fun _a β¦ pβ = _a) (Category.id_comp pβ))) (Eq.refl pβ)β©β’ qβ = qβ β π Qπ:Type uinstβ:Category.{v, u} πA:πB:πP:πQ:πpβ:P βΆ Apβ:P βΆ BhP:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = pβ β t β§ tβ = pβ β tqβ:Q βΆ Aqβ:Q βΆ BhQ:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = qβ β t β§ tβ = qβ β tf:P βΆ Qhf_comm:pβ = qβ β f β§ pβ = qβ β frightβΒΉ:β (y : P βΆ Q), (fun t β¦ pβ = qβ β t β§ pβ = qβ β t) y β y = fg:Q βΆ Phg_comm:qβ = pβ β g β§ qβ = pβ β grightβ:β (y : Q βΆ P), (fun t β¦ qβ = pβ β t β§ qβ = pβ β t) y β y = ghgf:g β f = π P :=
ExistsUnique.unique (hP P pβ pβ)
β¨Eq.symm
(Trans.trans
(Trans.trans
(Trans.trans rfl
(Eq.mpr (id (congrArg (fun _a β¦ _a = (pβ β g) β f) (Category.assoc f g pβ))) (Eq.refl ((pβ β g) β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a β f = qβ β f) (Eq.symm hg_comm.left))) (Eq.refl (qβ β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a = pβ) (Eq.symm hf_comm.left))) (Eq.refl pβ))),
Eq.symm
(Trans.trans
(Trans.trans
(Trans.trans rfl
(Eq.mpr (id (congrArg (fun _a β¦ _a = (pβ β g) β f) (Category.assoc f g pβ))) (Eq.refl ((pβ β g) β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a β f = qβ β f) (Eq.symm hg_comm.right))) (Eq.refl (qβ β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a = pβ) (Eq.symm hf_comm.right))) (Eq.refl pβ)))β©
β¨Eq.mpr (id (congrArg (fun _a β¦ pβ = _a) (Category.id_comp pβ))) (Eq.refl pβ),
Eq.mpr (id (congrArg (fun _a β¦ pβ = _a) (Category.id_comp pβ))) (Eq.refl pβ)β©β’ qβ = qβ β π Q π:Type uinstβ:Category.{v, u} πA:πB:πP:πQ:πpβ:P βΆ Apβ:P βΆ BhP:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = pβ β t β§ tβ = pβ β tqβ:Q βΆ Aqβ:Q βΆ BhQ:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = qβ β t β§ tβ = qβ β tf:P βΆ Qhf_comm:pβ = qβ β f β§ pβ = qβ β frightβΒΉ:β (y : P βΆ Q), (fun t β¦ pβ = qβ β t β§ pβ = qβ β t) y β y = fg:Q βΆ Phg_comm:qβ = pβ β g β§ qβ = pβ β grightβ:β (y : Q βΆ P), (fun t β¦ qβ = pβ β t β§ qβ = pβ β t) y β y = ghgf:g β f = π P :=
ExistsUnique.unique (hP P pβ pβ)
β¨Eq.symm
(Trans.trans
(Trans.trans
(Trans.trans rfl
(Eq.mpr (id (congrArg (fun _a β¦ _a = (pβ β g) β f) (Category.assoc f g pβ))) (Eq.refl ((pβ β g) β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a β f = qβ β f) (Eq.symm hg_comm.left))) (Eq.refl (qβ β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a = pβ) (Eq.symm hf_comm.left))) (Eq.refl pβ))),
Eq.symm
(Trans.trans
(Trans.trans
(Trans.trans rfl
(Eq.mpr (id (congrArg (fun _a β¦ _a = (pβ β g) β f) (Category.assoc f g pβ))) (Eq.refl ((pβ β g) β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a β f = qβ β f) (Eq.symm hg_comm.right))) (Eq.refl (qβ β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a = pβ) (Eq.symm hf_comm.right))) (Eq.refl pβ)))β©
β¨Eq.mpr (id (congrArg (fun _a β¦ pβ = _a) (Category.id_comp pβ))) (Eq.refl pβ),
Eq.mpr (id (congrArg (fun _a β¦ pβ = _a) (Category.id_comp pβ))) (Eq.refl pβ)β©β’ qβ = qβ β π Qπ:Type uinstβ:Category.{v, u} πA:πB:πP:πQ:πpβ:P βΆ Apβ:P βΆ BhP:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = pβ β t β§ tβ = pβ β tqβ:Q βΆ Aqβ:Q βΆ BhQ:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = qβ β t β§ tβ = qβ β tf:P βΆ Qhf_comm:pβ = qβ β f β§ pβ = qβ β frightβΒΉ:β (y : P βΆ Q), (fun t β¦ pβ = qβ β t β§ pβ = qβ β t) y β y = fg:Q βΆ Phg_comm:qβ = pβ β g β§ qβ = pβ β grightβ:β (y : Q βΆ P), (fun t β¦ qβ = pβ β t β§ qβ = pβ β t) y β y = ghgf:g β f = π P :=
ExistsUnique.unique (hP P pβ pβ)
β¨Eq.symm
(Trans.trans
(Trans.trans
(Trans.trans rfl
(Eq.mpr (id (congrArg (fun _a β¦ _a = (pβ β g) β f) (Category.assoc f g pβ))) (Eq.refl ((pβ β g) β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a β f = qβ β f) (Eq.symm hg_comm.left))) (Eq.refl (qβ β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a = pβ) (Eq.symm hf_comm.left))) (Eq.refl pβ))),
Eq.symm
(Trans.trans
(Trans.trans
(Trans.trans rfl
(Eq.mpr (id (congrArg (fun _a β¦ _a = (pβ β g) β f) (Category.assoc f g pβ))) (Eq.refl ((pβ β g) β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a β f = qβ β f) (Eq.symm hg_comm.right))) (Eq.refl (qβ β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a = pβ) (Eq.symm hf_comm.right))) (Eq.refl pβ)))β©
β¨Eq.mpr (id (congrArg (fun _a β¦ pβ = _a) (Category.id_comp pβ))) (Eq.refl pβ),
Eq.mpr (id (congrArg (fun _a β¦ pβ = _a) (Category.id_comp pβ))) (Eq.refl pβ)β©β’ qβ = qβ β π Q All goals completed! π
π:Type uinstβ:Category.{v, u} πA:πB:πP:πQ:πpβ:P βΆ Apβ:P βΆ BhP:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = pβ β t β§ tβ = pβ β tqβ:Q βΆ Aqβ:Q βΆ BhQ:β (T : π) (tβ : T βΆ A) (tβ : T βΆ B), β! t, tβ = qβ β t β§ tβ = qβ β tf:P βΆ Qhf_comm:pβ = qβ β f β§ pβ = qβ β frightβΒΉ:β (y : P βΆ Q), (fun t β¦ pβ = qβ β t β§ pβ = qβ β t) y β y = fg:Q βΆ Phg_comm:qβ = pβ β g β§ qβ = pβ β grightβ:β (y : Q βΆ P), (fun t β¦ qβ = pβ β t β§ qβ = pβ β t) y β y = ghgf:g β f = π P :=
ExistsUnique.unique (hP P pβ pβ)
β¨Eq.symm
(Trans.trans
(Trans.trans
(Trans.trans rfl
(Eq.mpr (id (congrArg (fun _a β¦ _a = (pβ β g) β f) (Category.assoc f g pβ))) (Eq.refl ((pβ β g) β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a β f = qβ β f) (Eq.symm hg_comm.left))) (Eq.refl (qβ β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a = pβ) (Eq.symm hf_comm.left))) (Eq.refl pβ))),
Eq.symm
(Trans.trans
(Trans.trans
(Trans.trans rfl
(Eq.mpr (id (congrArg (fun _a β¦ _a = (pβ β g) β f) (Category.assoc f g pβ))) (Eq.refl ((pβ β g) β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a β f = qβ β f) (Eq.symm hg_comm.right))) (Eq.refl (qβ β f))))
(Eq.mpr (id (congrArg (fun _a β¦ _a = pβ) (Eq.symm hf_comm.right))) (Eq.refl pβ)))β©
β¨Eq.mpr (id (congrArg (fun _a β¦ pβ = _a) (Category.id_comp pβ))) (Eq.refl pβ),
Eq.mpr (id (congrArg (fun _a β¦ pβ = _a) (Category.id_comp pβ))) (Eq.refl pβ)β©hfg:f β g = π Q :=
ExistsUnique.unique (hQ Q qβ qβ)
β¨Eq.symm
(Trans.trans
(Trans.trans
(Trans.trans rfl
(Eq.mpr (id (congrArg (fun _a β¦ _a = (qβ β f) β g) (Category.assoc g f qβ))) (Eq.refl ((qβ β f) β g))))
(Eq.mpr (id (congrArg (fun _a β¦ _a β g = pβ β g) (Eq.symm hf_comm.left))) (Eq.refl (pβ β g))))
(Eq.mpr (id (congrArg (fun _a β¦ _a = qβ) (Eq.symm hg_comm.left))) (Eq.refl qβ))),
Eq.symm
(Trans.trans
(Trans.trans
(Trans.trans rfl
(Eq.mpr (id (congrArg (fun _a β¦ _a = (qβ β f) β g) (Category.assoc g f qβ))) (Eq.refl ((qβ β f) β g))))
(Eq.mpr (id (congrArg (fun _a β¦ _a β g = pβ β g) (Eq.symm hf_comm.right))) (Eq.refl (pβ β g))))
(Eq.mpr (id (congrArg (fun _a β¦ _a = qβ) (Eq.symm hg_comm.right))) (Eq.refl qβ)))β©
β¨Eq.mpr (id (congrArg (fun _a β¦ qβ = _a) (Category.id_comp qβ))) (Eq.refl qβ),
Eq.mpr (id (congrArg (fun _a β¦ qβ = _a) (Category.id_comp qβ))) (Eq.refl qβ)β©β’ P β
Q
All goals completed! π
Exercise 1 (p. 241)
Is there a map in πΊβ» from the 'day clock'
abbrev dayClock : SetWithEndomap := {
carrier := Fin 24
toEnd := (Β· + 1)
}
to some X^{β»\alpha} which together with the ['shift clock' and map]
abbrev shiftClock : SetWithEndomap := {
carrier := Fin 8
toEnd := (Β· + 1)
}
def pβ : dayClock βΆ shiftClock := β¨
fun n β¦ Fin.ofNat 8 n,
β’ (fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd = shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn
x:dayClock.carrierβ’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) x = (shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) x
β’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) ((fun i β¦ i) β¨0, β―β©) =
(shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) ((fun i β¦ i) β¨0, β―β©)β’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) ((fun i β¦ i) β¨1, β―β©) =
(shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) ((fun i β¦ i) β¨1, β―β©)β’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) ((fun i β¦ i) β¨2, β―β©) =
(shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) ((fun i β¦ i) β¨2, β―β©)β’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) ((fun i β¦ i) β¨3, β―β©) =
(shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) ((fun i β¦ i) β¨3, β―β©)β’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) ((fun i β¦ i) β¨4, β―β©) =
(shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) ((fun i β¦ i) β¨4, β―β©)β’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) ((fun i β¦ i) β¨5, β―β©) =
(shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) ((fun i β¦ i) β¨5, β―β©)β’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) ((fun i β¦ i) β¨6, β―β©) =
(shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) ((fun i β¦ i) β¨6, β―β©)β’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) ((fun i β¦ i) β¨7, β―β©) =
(shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) ((fun i β¦ i) β¨7, β―β©)β’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) ((fun i β¦ i) β¨8, β―β©) =
(shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) ((fun i β¦ i) β¨8, β―β©)β’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) ((fun i β¦ i) β¨9, β―β©) =
(shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) ((fun i β¦ i) β¨9, β―β©)β’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) ((fun i β¦ i) β¨10, β―β©) =
(shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) ((fun i β¦ i) β¨10, β―β©)β’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) ((fun i β¦ i) β¨11, β―β©) =
(shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) ((fun i β¦ i) β¨11, β―β©)β’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) ((fun i β¦ i) β¨12, β―β©) =
(shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) ((fun i β¦ i) β¨12, β―β©)β’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) ((fun i β¦ i) β¨13, β―β©) =
(shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) ((fun i β¦ i) β¨13, β―β©)β’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) ((fun i β¦ i) β¨14, β―β©) =
(shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) ((fun i β¦ i) β¨14, β―β©)β’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) ((fun i β¦ i) β¨15, β―β©) =
(shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) ((fun i β¦ i) β¨15, β―β©)β’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) ((fun i β¦ i) β¨16, β―β©) =
(shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) ((fun i β¦ i) β¨16, β―β©)β’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) ((fun i β¦ i) β¨17, β―β©) =
(shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) ((fun i β¦ i) β¨17, β―β©)β’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) ((fun i β¦ i) β¨18, β―β©) =
(shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) ((fun i β¦ i) β¨18, β―β©)β’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) ((fun i β¦ i) β¨19, β―β©) =
(shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) ((fun i β¦ i) β¨19, β―β©)β’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) ((fun i β¦ i) β¨20, β―β©) =
(shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) ((fun i β¦ i) β¨20, β―β©)β’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) ((fun i β¦ i) β¨21, β―β©) =
(shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) ((fun i β¦ i) β¨21, β―β©)β’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) ((fun i β¦ i) β¨22, β―β©) =
(shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) ((fun i β¦ i) β¨22, β―β©)β’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) ((fun i β¦ i) β¨23, β―β©) =
(shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) ((fun i β¦ i) β¨23, β―β©) β’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) ((fun i β¦ i) β¨0, β―β©) =
(shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) ((fun i β¦ i) β¨0, β―β©)β’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) ((fun i β¦ i) β¨1, β―β©) =
(shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) ((fun i β¦ i) β¨1, β―β©)β’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) ((fun i β¦ i) β¨2, β―β©) =
(shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) ((fun i β¦ i) β¨2, β―β©)β’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) ((fun i β¦ i) β¨3, β―β©) =
(shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) ((fun i β¦ i) β¨3, β―β©)β’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) ((fun i β¦ i) β¨4, β―β©) =
(shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) ((fun i β¦ i) β¨4, β―β©)β’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) ((fun i β¦ i) β¨5, β―β©) =
(shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) ((fun i β¦ i) β¨5, β―β©)β’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) ((fun i β¦ i) β¨6, β―β©) =
(shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) ((fun i β¦ i) β¨6, β―β©)β’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) ((fun i β¦ i) β¨7, β―β©) =
(shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) ((fun i β¦ i) β¨7, β―β©)β’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) ((fun i β¦ i) β¨8, β―β©) =
(shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) ((fun i β¦ i) β¨8, β―β©)β’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) ((fun i β¦ i) β¨9, β―β©) =
(shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) ((fun i β¦ i) β¨9, β―β©)β’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) ((fun i β¦ i) β¨10, β―β©) =
(shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) ((fun i β¦ i) β¨10, β―β©)β’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) ((fun i β¦ i) β¨11, β―β©) =
(shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) ((fun i β¦ i) β¨11, β―β©)β’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) ((fun i β¦ i) β¨12, β―β©) =
(shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) ((fun i β¦ i) β¨12, β―β©)β’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) ((fun i β¦ i) β¨13, β―β©) =
(shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) ((fun i β¦ i) β¨13, β―β©)β’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) ((fun i β¦ i) β¨14, β―β©) =
(shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) ((fun i β¦ i) β¨14, β―β©)β’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) ((fun i β¦ i) β¨15, β―β©) =
(shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) ((fun i β¦ i) β¨15, β―β©)β’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) ((fun i β¦ i) β¨16, β―β©) =
(shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) ((fun i β¦ i) β¨16, β―β©)β’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) ((fun i β¦ i) β¨17, β―β©) =
(shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) ((fun i β¦ i) β¨17, β―β©)β’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) ((fun i β¦ i) β¨18, β―β©) =
(shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) ((fun i β¦ i) β¨18, β―β©)β’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) ((fun i β¦ i) β¨19, β―β©) =
(shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) ((fun i β¦ i) β¨19, β―β©)β’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) ((fun i β¦ i) β¨20, β―β©) =
(shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) ((fun i β¦ i) β¨20, β―β©)β’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) ((fun i β¦ i) β¨21, β―β©) =
(shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) ((fun i β¦ i) β¨21, β―β©)β’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) ((fun i β¦ i) β¨22, β―β©) =
(shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) ((fun i β¦ i) β¨22, β―β©)β’ ((fun n β¦ Fin.ofNat 8 βn) β dayClock.toEnd) ((fun i β¦ i) β¨23, β―β©) =
(shiftClock.toEnd β fun n β¦ Fin.ofNat 8 βn) ((fun i β¦ i) β¨23, β―β©) All goals completed! π
β©
makes the 'day clock' into the product of X^{β»\alpha} and the 'shift clock'?
Solution: Exercise 1
We can use a '3-hour clock' as the object X^{β»\alpha}, with the required map {\mathrm{dayClock} \rightarrow X^{β»\alpha}} given by {n \mapsto n \mod 3}.
abbrev XΞ± : SetWithEndomap := {
carrier := Fin 3
toEnd := (Β· + 1)
}
def pβ : dayClock βΆ XΞ± := β¨
fun n β¦ Fin.ofNat 3 n,
β’ (fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd = XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn
x:dayClock.carrierβ’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) x = (XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) x
β’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) ((fun i β¦ i) β¨0, β―β©) =
(XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) ((fun i β¦ i) β¨0, β―β©)β’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) ((fun i β¦ i) β¨1, β―β©) =
(XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) ((fun i β¦ i) β¨1, β―β©)β’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) ((fun i β¦ i) β¨2, β―β©) =
(XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) ((fun i β¦ i) β¨2, β―β©)β’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) ((fun i β¦ i) β¨3, β―β©) =
(XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) ((fun i β¦ i) β¨3, β―β©)β’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) ((fun i β¦ i) β¨4, β―β©) =
(XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) ((fun i β¦ i) β¨4, β―β©)β’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) ((fun i β¦ i) β¨5, β―β©) =
(XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) ((fun i β¦ i) β¨5, β―β©)β’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) ((fun i β¦ i) β¨6, β―β©) =
(XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) ((fun i β¦ i) β¨6, β―β©)β’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) ((fun i β¦ i) β¨7, β―β©) =
(XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) ((fun i β¦ i) β¨7, β―β©)β’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) ((fun i β¦ i) β¨8, β―β©) =
(XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) ((fun i β¦ i) β¨8, β―β©)β’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) ((fun i β¦ i) β¨9, β―β©) =
(XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) ((fun i β¦ i) β¨9, β―β©)β’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) ((fun i β¦ i) β¨10, β―β©) =
(XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) ((fun i β¦ i) β¨10, β―β©)β’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) ((fun i β¦ i) β¨11, β―β©) =
(XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) ((fun i β¦ i) β¨11, β―β©)β’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) ((fun i β¦ i) β¨12, β―β©) =
(XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) ((fun i β¦ i) β¨12, β―β©)β’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) ((fun i β¦ i) β¨13, β―β©) =
(XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) ((fun i β¦ i) β¨13, β―β©)β’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) ((fun i β¦ i) β¨14, β―β©) =
(XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) ((fun i β¦ i) β¨14, β―β©)β’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) ((fun i β¦ i) β¨15, β―β©) =
(XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) ((fun i β¦ i) β¨15, β―β©)β’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) ((fun i β¦ i) β¨16, β―β©) =
(XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) ((fun i β¦ i) β¨16, β―β©)β’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) ((fun i β¦ i) β¨17, β―β©) =
(XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) ((fun i β¦ i) β¨17, β―β©)β’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) ((fun i β¦ i) β¨18, β―β©) =
(XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) ((fun i β¦ i) β¨18, β―β©)β’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) ((fun i β¦ i) β¨19, β―β©) =
(XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) ((fun i β¦ i) β¨19, β―β©)β’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) ((fun i β¦ i) β¨20, β―β©) =
(XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) ((fun i β¦ i) β¨20, β―β©)β’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) ((fun i β¦ i) β¨21, β―β©) =
(XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) ((fun i β¦ i) β¨21, β―β©)β’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) ((fun i β¦ i) β¨22, β―β©) =
(XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) ((fun i β¦ i) β¨22, β―β©)β’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) ((fun i β¦ i) β¨23, β―β©) =
(XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) ((fun i β¦ i) β¨23, β―β©) β’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) ((fun i β¦ i) β¨0, β―β©) =
(XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) ((fun i β¦ i) β¨0, β―β©)β’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) ((fun i β¦ i) β¨1, β―β©) =
(XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) ((fun i β¦ i) β¨1, β―β©)β’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) ((fun i β¦ i) β¨2, β―β©) =
(XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) ((fun i β¦ i) β¨2, β―β©)β’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) ((fun i β¦ i) β¨3, β―β©) =
(XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) ((fun i β¦ i) β¨3, β―β©)β’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) ((fun i β¦ i) β¨4, β―β©) =
(XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) ((fun i β¦ i) β¨4, β―β©)β’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) ((fun i β¦ i) β¨5, β―β©) =
(XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) ((fun i β¦ i) β¨5, β―β©)β’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) ((fun i β¦ i) β¨6, β―β©) =
(XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) ((fun i β¦ i) β¨6, β―β©)β’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) ((fun i β¦ i) β¨7, β―β©) =
(XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) ((fun i β¦ i) β¨7, β―β©)β’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) ((fun i β¦ i) β¨8, β―β©) =
(XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) ((fun i β¦ i) β¨8, β―β©)β’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) ((fun i β¦ i) β¨9, β―β©) =
(XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) ((fun i β¦ i) β¨9, β―β©)β’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) ((fun i β¦ i) β¨10, β―β©) =
(XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) ((fun i β¦ i) β¨10, β―β©)β’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) ((fun i β¦ i) β¨11, β―β©) =
(XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) ((fun i β¦ i) β¨11, β―β©)β’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) ((fun i β¦ i) β¨12, β―β©) =
(XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) ((fun i β¦ i) β¨12, β―β©)β’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) ((fun i β¦ i) β¨13, β―β©) =
(XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) ((fun i β¦ i) β¨13, β―β©)β’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) ((fun i β¦ i) β¨14, β―β©) =
(XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) ((fun i β¦ i) β¨14, β―β©)β’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) ((fun i β¦ i) β¨15, β―β©) =
(XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) ((fun i β¦ i) β¨15, β―β©)β’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) ((fun i β¦ i) β¨16, β―β©) =
(XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) ((fun i β¦ i) β¨16, β―β©)β’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) ((fun i β¦ i) β¨17, β―β©) =
(XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) ((fun i β¦ i) β¨17, β―β©)β’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) ((fun i β¦ i) β¨18, β―β©) =
(XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) ((fun i β¦ i) β¨18, β―β©)β’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) ((fun i β¦ i) β¨19, β―β©) =
(XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) ((fun i β¦ i) β¨19, β―β©)β’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) ((fun i β¦ i) β¨20, β―β©) =
(XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) ((fun i β¦ i) β¨20, β―β©)β’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) ((fun i β¦ i) β¨21, β―β©) =
(XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) ((fun i β¦ i) β¨21, β―β©)β’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) ((fun i β¦ i) β¨22, β―β©) =
(XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) ((fun i β¦ i) β¨22, β―β©)β’ ((fun n β¦ Fin.ofNat 3 βn) β dayClock.toEnd) ((fun i β¦ i) β¨23, β―β©) =
(XΞ±.toEnd β fun n β¦ Fin.ofNat 3 βn) ((fun i β¦ i) β¨23, β―β©) All goals completed! π
β©
The proof is a direct application of the Chinese Remainder Theorem (CRT), and we begin by defining some helpers:
[Isomorphism] Construct Fin 24 from Fin 8 and Fin 3 via CRT.
def crt (a : Fin 8) (b : Fin 3) : Fin 24 :=
Fin.ofNat 24 (9 * a.val + 16 * b.val)
[Homomorphism] Show that crt preserves (Β· + 1) structure.
lemma h_crt_comm (a : Fin 8) (b : Fin 3) :
crt (a + 1) (b + 1) = crt a b + 1 := a:Fin 8b:Fin 3β’ crt (a + 1) (b + 1) = crt a b + 1
b:Fin 3β’ crt ((fun i β¦ i) β¨0, β―β© + 1) (b + 1) = crt ((fun i β¦ i) β¨0, β―β©) b + 1b:Fin 3β’ crt ((fun i β¦ i) β¨1, β―β© + 1) (b + 1) = crt ((fun i β¦ i) β¨1, β―β©) b + 1b:Fin 3β’ crt ((fun i β¦ i) β¨2, β―β© + 1) (b + 1) = crt ((fun i β¦ i) β¨2, β―β©) b + 1b:Fin 3β’ crt ((fun i β¦ i) β¨3, β―β© + 1) (b + 1) = crt ((fun i β¦ i) β¨3, β―β©) b + 1b:Fin 3β’ crt ((fun i β¦ i) β¨4, β―β© + 1) (b + 1) = crt ((fun i β¦ i) β¨4, β―β©) b + 1b:Fin 3β’ crt ((fun i β¦ i) β¨5, β―β© + 1) (b + 1) = crt ((fun i β¦ i) β¨5, β―β©) b + 1b:Fin 3β’ crt ((fun i β¦ i) β¨6, β―β© + 1) (b + 1) = crt ((fun i β¦ i) β¨6, β―β©) b + 1b:Fin 3β’ crt ((fun i β¦ i) β¨7, β―β© + 1) (b + 1) = crt ((fun i β¦ i) β¨7, β―β©) b + 1 b:Fin 3β’ crt ((fun i β¦ i) β¨0, β―β© + 1) (b + 1) = crt ((fun i β¦ i) β¨0, β―β©) b + 1b:Fin 3β’ crt ((fun i β¦ i) β¨1, β―β© + 1) (b + 1) = crt ((fun i β¦ i) β¨1, β―β©) b + 1b:Fin 3β’ crt ((fun i β¦ i) β¨2, β―β© + 1) (b + 1) = crt ((fun i β¦ i) β¨2, β―β©) b + 1b:Fin 3β’ crt ((fun i β¦ i) β¨3, β―β© + 1) (b + 1) = crt ((fun i β¦ i) β¨3, β―β©) b + 1b:Fin 3β’ crt ((fun i β¦ i) β¨4, β―β© + 1) (b + 1) = crt ((fun i β¦ i) β¨4, β―β©) b + 1b:Fin 3β’ crt ((fun i β¦ i) β¨5, β―β© + 1) (b + 1) = crt ((fun i β¦ i) β¨5, β―β©) b + 1b:Fin 3β’ crt ((fun i β¦ i) β¨6, β―β© + 1) (b + 1) = crt ((fun i β¦ i) β¨6, β―β©) b + 1b:Fin 3β’ crt ((fun i β¦ i) β¨7, β―β© + 1) (b + 1) = crt ((fun i β¦ i) β¨7, β―β©) b + 1 β’ crt ((fun i β¦ i) β¨7, β―β© + 1) ((fun i β¦ i) β¨0, β―β© + 1) = crt ((fun i β¦ i) β¨7, β―β©) ((fun i β¦ i) β¨0, β―β©) + 1β’ crt ((fun i β¦ i) β¨7, β―β© + 1) ((fun i β¦ i) β¨1, β―β© + 1) = crt ((fun i β¦ i) β¨7, β―β©) ((fun i β¦ i) β¨1, β―β©) + 1β’ crt ((fun i β¦ i) β¨7, β―β© + 1) ((fun i β¦ i) β¨2, β―β© + 1) = crt ((fun i β¦ i) β¨7, β―β©) ((fun i β¦ i) β¨2, β―β©) + 1 β’ crt ((fun i β¦ i) β¨0, β―β© + 1) ((fun i β¦ i) β¨0, β―β© + 1) = crt ((fun i β¦ i) β¨0, β―β©) ((fun i β¦ i) β¨0, β―β©) + 1β’ crt ((fun i β¦ i) β¨0, β―β© + 1) ((fun i β¦ i) β¨1, β―β© + 1) = crt ((fun i β¦ i) β¨0, β―β©) ((fun i β¦ i) β¨1, β―β©) + 1β’ crt ((fun i β¦ i) β¨0, β―β© + 1) ((fun i β¦ i) β¨2, β―β© + 1) = crt ((fun i β¦ i) β¨0, β―β©) ((fun i β¦ i) β¨2, β―β©) + 1β’ crt ((fun i β¦ i) β¨1, β―β© + 1) ((fun i β¦ i) β¨0, β―β© + 1) = crt ((fun i β¦ i) β¨1, β―β©) ((fun i β¦ i) β¨0, β―β©) + 1β’ crt ((fun i β¦ i) β¨1, β―β© + 1) ((fun i β¦ i) β¨1, β―β© + 1) = crt ((fun i β¦ i) β¨1, β―β©) ((fun i β¦ i) β¨1, β―β©) + 1β’ crt ((fun i β¦ i) β¨1, β―β© + 1) ((fun i β¦ i) β¨2, β―β© + 1) = crt ((fun i β¦ i) β¨1, β―β©) ((fun i β¦ i) β¨2, β―β©) + 1β’ crt ((fun i β¦ i) β¨2, β―β© + 1) ((fun i β¦ i) β¨0, β―β© + 1) = crt ((fun i β¦ i) β¨2, β―β©) ((fun i β¦ i) β¨0, β―β©) + 1β’ crt ((fun i β¦ i) β¨2, β―β© + 1) ((fun i β¦ i) β¨1, β―β© + 1) = crt ((fun i β¦ i) β¨2, β―β©) ((fun i β¦ i) β¨1, β―β©) + 1β’ crt ((fun i β¦ i) β¨2, β―β© + 1) ((fun i β¦ i) β¨2, β―β© + 1) = crt ((fun i β¦ i) β¨2, β―β©) ((fun i β¦ i) β¨2, β―β©) + 1β’ crt ((fun i β¦ i) β¨3, β―β© + 1) ((fun i β¦ i) β¨0, β―β© + 1) = crt ((fun i β¦ i) β¨3, β―β©) ((fun i β¦ i) β¨0, β―β©) + 1β’ crt ((fun i β¦ i) β¨3, β―β© + 1) ((fun i β¦ i) β¨1, β―β© + 1) = crt ((fun i β¦ i) β¨3, β―β©) ((fun i β¦ i) β¨1, β―β©) + 1β’ crt ((fun i β¦ i) β¨3, β―β© + 1) ((fun i β¦ i) β¨2, β―β© + 1) = crt ((fun i β¦ i) β¨3, β―β©) ((fun i β¦ i) β¨2, β―β©) + 1β’ crt ((fun i β¦ i) β¨4, β―β© + 1) ((fun i β¦ i) β¨0, β―β© + 1) = crt ((fun i β¦ i) β¨4, β―β©) ((fun i β¦ i) β¨0, β―β©) + 1β’ crt ((fun i β¦ i) β¨4, β―β© + 1) ((fun i β¦ i) β¨1, β―β© + 1) = crt ((fun i β¦ i) β¨4, β―β©) ((fun i β¦ i) β¨1, β―β©) + 1β’ crt ((fun i β¦ i) β¨4, β―β© + 1) ((fun i β¦ i) β¨2, β―β© + 1) = crt ((fun i β¦ i) β¨4, β―β©) ((fun i β¦ i) β¨2, β―β©) + 1β’ crt ((fun i β¦ i) β¨5, β―β© + 1) ((fun i β¦ i) β¨0, β―β© + 1) = crt ((fun i β¦ i) β¨5, β―β©) ((fun i β¦ i) β¨0, β―β©) + 1β’ crt ((fun i β¦ i) β¨5, β―β© + 1) ((fun i β¦ i) β¨1, β―β© + 1) = crt ((fun i β¦ i) β¨5, β―β©) ((fun i β¦ i) β¨1, β―β©) + 1β’ crt ((fun i β¦ i) β¨5, β―β© + 1) ((fun i β¦ i) β¨2, β―β© + 1) = crt ((fun i β¦ i) β¨5, β―β©) ((fun i β¦ i) β¨2, β―β©) + 1β’ crt ((fun i β¦ i) β¨6, β―β© + 1) ((fun i β¦ i) β¨0, β―β© + 1) = crt ((fun i β¦ i) β¨6, β―β©) ((fun i β¦ i) β¨0, β―β©) + 1β’ crt ((fun i β¦ i) β¨6, β―β© + 1) ((fun i β¦ i) β¨1, β―β© + 1) = crt ((fun i β¦ i) β¨6, β―β©) ((fun i β¦ i) β¨1, β―β©) + 1β’ crt ((fun i β¦ i) β¨6, β―β© + 1) ((fun i β¦ i) β¨2, β―β© + 1) = crt ((fun i β¦ i) β¨6, β―β©) ((fun i β¦ i) β¨2, β―β©) + 1β’ crt ((fun i β¦ i) β¨7, β―β© + 1) ((fun i β¦ i) β¨0, β―β© + 1) = crt ((fun i β¦ i) β¨7, β―β©) ((fun i β¦ i) β¨0, β―β©) + 1β’ crt ((fun i β¦ i) β¨7, β―β© + 1) ((fun i β¦ i) β¨1, β―β© + 1) = crt ((fun i β¦ i) β¨7, β―β©) ((fun i β¦ i) β¨1, β―β©) + 1β’ crt ((fun i β¦ i) β¨7, β―β© + 1) ((fun i β¦ i) β¨2, β―β© + 1) = crt ((fun i β¦ i) β¨7, β―β©) ((fun i β¦ i) β¨2, β―β©) + 1 All goals completed! π
[Commutativity] Show that pβ β crt and pβ β crt recover components.
lemma h_pβ_crt (a : Fin 8) (b : Fin 3) : pβ.val (crt a b) = a := a:Fin 8b:Fin 3β’ βpβ (crt a b) = a
b:Fin 3β’ βpβ (crt ((fun i β¦ i) β¨0, β―β©) b) = (fun i β¦ i) β¨0, β―β©b:Fin 3β’ βpβ (crt ((fun i β¦ i) β¨1, β―β©) b) = (fun i β¦ i) β¨1, β―β©b:Fin 3β’ βpβ (crt ((fun i β¦ i) β¨2, β―β©) b) = (fun i β¦ i) β¨2, β―β©b:Fin 3β’ βpβ (crt ((fun i β¦ i) β¨3, β―β©) b) = (fun i β¦ i) β¨3, β―β©b:Fin 3β’ βpβ (crt ((fun i β¦ i) β¨4, β―β©) b) = (fun i β¦ i) β¨4, β―β©b:Fin 3β’ βpβ (crt ((fun i β¦ i) β¨5, β―β©) b) = (fun i β¦ i) β¨5, β―β©b:Fin 3β’ βpβ (crt ((fun i β¦ i) β¨6, β―β©) b) = (fun i β¦ i) β¨6, β―β©b:Fin 3β’ βpβ (crt ((fun i β¦ i) β¨7, β―β©) b) = (fun i β¦ i) β¨7, β―β© b:Fin 3β’ βpβ (crt ((fun i β¦ i) β¨0, β―β©) b) = (fun i β¦ i) β¨0, β―β©b:Fin 3β’ βpβ (crt ((fun i β¦ i) β¨1, β―β©) b) = (fun i β¦ i) β¨1, β―β©b:Fin 3β’ βpβ (crt ((fun i β¦ i) β¨2, β―β©) b) = (fun i β¦ i) β¨2, β―β©b:Fin 3β’ βpβ (crt ((fun i β¦ i) β¨3, β―β©) b) = (fun i β¦ i) β¨3, β―β©b:Fin 3β’ βpβ (crt ((fun i β¦ i) β¨4, β―β©) b) = (fun i β¦ i) β¨4, β―β©b:Fin 3β’ βpβ (crt ((fun i β¦ i) β¨5, β―β©) b) = (fun i β¦ i) β¨5, β―β©b:Fin 3β’ βpβ (crt ((fun i β¦ i) β¨6, β―β©) b) = (fun i β¦ i) β¨6, β―β©b:Fin 3β’ βpβ (crt ((fun i β¦ i) β¨7, β―β©) b) = (fun i β¦ i) β¨7, β―β© β’ βpβ (crt ((fun i β¦ i) β¨7, β―β©) ((fun i β¦ i) β¨0, β―β©)) = (fun i β¦ i) β¨7, β―β©β’ βpβ (crt ((fun i β¦ i) β¨7, β―β©) ((fun i β¦ i) β¨1, β―β©)) = (fun i β¦ i) β¨7, β―β©β’ βpβ (crt ((fun i β¦ i) β¨7, β―β©) ((fun i β¦ i) β¨2, β―β©)) = (fun i β¦ i) β¨7, β―β© β’ βpβ (crt ((fun i β¦ i) β¨0, β―β©) ((fun i β¦ i) β¨0, β―β©)) = (fun i β¦ i) β¨0, β―β©β’ βpβ (crt ((fun i β¦ i) β¨0, β―β©) ((fun i β¦ i) β¨1, β―β©)) = (fun i β¦ i) β¨0, β―β©β’ βpβ (crt ((fun i β¦ i) β¨0, β―β©) ((fun i β¦ i) β¨2, β―β©)) = (fun i β¦ i) β¨0, β―β©β’ βpβ (crt ((fun i β¦ i) β¨1, β―β©) ((fun i β¦ i) β¨0, β―β©)) = (fun i β¦ i) β¨1, β―β©β’ βpβ (crt ((fun i β¦ i) β¨1, β―β©) ((fun i β¦ i) β¨1, β―β©)) = (fun i β¦ i) β¨1, β―β©β’ βpβ (crt ((fun i β¦ i) β¨1, β―β©) ((fun i β¦ i) β¨2, β―β©)) = (fun i β¦ i) β¨1, β―β©β’ βpβ (crt ((fun i β¦ i) β¨2, β―β©) ((fun i β¦ i) β¨0, β―β©)) = (fun i β¦ i) β¨2, β―β©β’ βpβ (crt ((fun i β¦ i) β¨2, β―β©) ((fun i β¦ i) β¨1, β―β©)) = (fun i β¦ i) β¨2, β―β©β’ βpβ (crt ((fun i β¦ i) β¨2, β―β©) ((fun i β¦ i) β¨2, β―β©)) = (fun i β¦ i) β¨2, β―β©β’ βpβ (crt ((fun i β¦ i) β¨3, β―β©) ((fun i β¦ i) β¨0, β―β©)) = (fun i β¦ i) β¨3, β―β©β’ βpβ (crt ((fun i β¦ i) β¨3, β―β©) ((fun i β¦ i) β¨1, β―β©)) = (fun i β¦ i) β¨3, β―β©β’ βpβ (crt ((fun i β¦ i) β¨3, β―β©) ((fun i β¦ i) β¨2, β―β©)) = (fun i β¦ i) β¨3, β―β©β’ βpβ (crt ((fun i β¦ i) β¨4, β―β©) ((fun i β¦ i) β¨0, β―β©)) = (fun i β¦ i) β¨4, β―β©β’ βpβ (crt ((fun i β¦ i) β¨4, β―β©) ((fun i β¦ i) β¨1, β―β©)) = (fun i β¦ i) β¨4, β―β©β’ βpβ (crt ((fun i β¦ i) β¨4, β―β©) ((fun i β¦ i) β¨2, β―β©)) = (fun i β¦ i) β¨4, β―β©β’ βpβ (crt ((fun i β¦ i) β¨5, β―β©) ((fun i β¦ i) β¨0, β―β©)) = (fun i β¦ i) β¨5, β―β©β’ βpβ (crt ((fun i β¦ i) β¨5, β―β©) ((fun i β¦ i) β¨1, β―β©)) = (fun i β¦ i) β¨5, β―β©β’ βpβ (crt ((fun i β¦ i) β¨5, β―β©) ((fun i β¦ i) β¨2, β―β©)) = (fun i β¦ i) β¨5, β―β©β’ βpβ (crt ((fun i β¦ i) β¨6, β―β©) ((fun i β¦ i) β¨0, β―β©)) = (fun i β¦ i) β¨6, β―β©β’ βpβ (crt ((fun i β¦ i) β¨6, β―β©) ((fun i β¦ i) β¨1, β―β©)) = (fun i β¦ i) β¨6, β―β©β’ βpβ (crt ((fun i β¦ i) β¨6, β―β©) ((fun i β¦ i) β¨2, β―β©)) = (fun i β¦ i) β¨6, β―β©β’ βpβ (crt ((fun i β¦ i) β¨7, β―β©) ((fun i β¦ i) β¨0, β―β©)) = (fun i β¦ i) β¨7, β―β©β’ βpβ (crt ((fun i β¦ i) β¨7, β―β©) ((fun i β¦ i) β¨1, β―β©)) = (fun i β¦ i) β¨7, β―β©β’ βpβ (crt ((fun i β¦ i) β¨7, β―β©) ((fun i β¦ i) β¨2, β―β©)) = (fun i β¦ i) β¨7, β―β© All goals completed! π
lemma h_pβ_crt (a : Fin 8) (b : Fin 3) : pβ.val (crt a b) = b := a:Fin 8b:Fin 3β’ βpβ (crt a b) = b
b:Fin 3β’ βpβ (crt ((fun i β¦ i) β¨0, β―β©) b) = bb:Fin 3β’ βpβ (crt ((fun i β¦ i) β¨1, β―β©) b) = bb:Fin 3β’ βpβ (crt ((fun i β¦ i) β¨2, β―β©) b) = bb:Fin 3β’ βpβ (crt ((fun i β¦ i) β¨3, β―β©) b) = bb:Fin 3β’ βpβ (crt ((fun i β¦ i) β¨4, β―β©) b) = bb:Fin 3β’ βpβ (crt ((fun i β¦ i) β¨5, β―β©) b) = bb:Fin 3β’ βpβ (crt ((fun i β¦ i) β¨6, β―β©) b) = bb:Fin 3β’ βpβ (crt ((fun i β¦ i) β¨7, β―β©) b) = b b:Fin 3β’ βpβ (crt ((fun i β¦ i) β¨0, β―β©) b) = bb:Fin 3β’ βpβ (crt ((fun i β¦ i) β¨1, β―β©) b) = bb:Fin 3β’ βpβ (crt ((fun i β¦ i) β¨2, β―β©) b) = bb:Fin 3β’ βpβ (crt ((fun i β¦ i) β¨3, β―β©) b) = bb:Fin 3β’ βpβ (crt ((fun i β¦ i) β¨4, β―β©) b) = bb:Fin 3β’ βpβ (crt ((fun i β¦ i) β¨5, β―β©) b) = bb:Fin 3β’ βpβ (crt ((fun i β¦ i) β¨6, β―β©) b) = bb:Fin 3β’ βpβ (crt ((fun i β¦ i) β¨7, β―β©) b) = b β’ βpβ (crt ((fun i β¦ i) β¨7, β―β©) ((fun i β¦ i) β¨0, β―β©)) = (fun i β¦ i) β¨0, β―β©β’ βpβ (crt ((fun i β¦ i) β¨7, β―β©) ((fun i β¦ i) β¨1, β―β©)) = (fun i β¦ i) β¨1, β―β©β’ βpβ (crt ((fun i β¦ i) β¨7, β―β©) ((fun i β¦ i) β¨2, β―β©)) = (fun i β¦ i) β¨2, β―β© β’ βpβ (crt ((fun i β¦ i) β¨0, β―β©) ((fun i β¦ i) β¨0, β―β©)) = (fun i β¦ i) β¨0, β―β©β’ βpβ (crt ((fun i β¦ i) β¨0, β―β©) ((fun i β¦ i) β¨1, β―β©)) = (fun i β¦ i) β¨1, β―β©β’ βpβ (crt ((fun i β¦ i) β¨0, β―β©) ((fun i β¦ i) β¨2, β―β©)) = (fun i β¦ i) β¨2, β―β©β’ βpβ (crt ((fun i β¦ i) β¨1, β―β©) ((fun i β¦ i) β¨0, β―β©)) = (fun i β¦ i) β¨0, β―β©β’ βpβ (crt ((fun i β¦ i) β¨1, β―β©) ((fun i β¦ i) β¨1, β―β©)) = (fun i β¦ i) β¨1, β―β©β’ βpβ (crt ((fun i β¦ i) β¨1, β―β©) ((fun i β¦ i) β¨2, β―β©)) = (fun i β¦ i) β¨2, β―β©β’ βpβ (crt ((fun i β¦ i) β¨2, β―β©) ((fun i β¦ i) β¨0, β―β©)) = (fun i β¦ i) β¨0, β―β©β’ βpβ (crt ((fun i β¦ i) β¨2, β―β©) ((fun i β¦ i) β¨1, β―β©)) = (fun i β¦ i) β¨1, β―β©β’ βpβ (crt ((fun i β¦ i) β¨2, β―β©) ((fun i β¦ i) β¨2, β―β©)) = (fun i β¦ i) β¨2, β―β©β’ βpβ (crt ((fun i β¦ i) β¨3, β―β©) ((fun i β¦ i) β¨0, β―β©)) = (fun i β¦ i) β¨0, β―β©β’ βpβ (crt ((fun i β¦ i) β¨3, β―β©) ((fun i β¦ i) β¨1, β―β©)) = (fun i β¦ i) β¨1, β―β©β’ βpβ (crt ((fun i β¦ i) β¨3, β―β©) ((fun i β¦ i) β¨2, β―β©)) = (fun i β¦ i) β¨2, β―β©β’ βpβ (crt ((fun i β¦ i) β¨4, β―β©) ((fun i β¦ i) β¨0, β―β©)) = (fun i β¦ i) β¨0, β―β©β’ βpβ (crt ((fun i β¦ i) β¨4, β―β©) ((fun i β¦ i) β¨1, β―β©)) = (fun i β¦ i) β¨1, β―β©β’ βpβ (crt ((fun i β¦ i) β¨4, β―β©) ((fun i β¦ i) β¨2, β―β©)) = (fun i β¦ i) β¨2, β―β©β’ βpβ (crt ((fun i β¦ i) β¨5, β―β©) ((fun i β¦ i) β¨0, β―β©)) = (fun i β¦ i) β¨0, β―β©β’ βpβ (crt ((fun i β¦ i) β¨5, β―β©) ((fun i β¦ i) β¨1, β―β©)) = (fun i β¦ i) β¨1, β―β©β’ βpβ (crt ((fun i β¦ i) β¨5, β―β©) ((fun i β¦ i) β¨2, β―β©)) = (fun i β¦ i) β¨2, β―β©β’ βpβ (crt ((fun i β¦ i) β¨6, β―β©) ((fun i β¦ i) β¨0, β―β©)) = (fun i β¦ i) β¨0, β―β©β’ βpβ (crt ((fun i β¦ i) β¨6, β―β©) ((fun i β¦ i) β¨1, β―β©)) = (fun i β¦ i) β¨1, β―β©β’ βpβ (crt ((fun i β¦ i) β¨6, β―β©) ((fun i β¦ i) β¨2, β―β©)) = (fun i β¦ i) β¨2, β―β©β’ βpβ (crt ((fun i β¦ i) β¨7, β―β©) ((fun i β¦ i) β¨0, β―β©)) = (fun i β¦ i) β¨0, β―β©β’ βpβ (crt ((fun i β¦ i) β¨7, β―β©) ((fun i β¦ i) β¨1, β―β©)) = (fun i β¦ i) β¨1, β―β©β’ βpβ (crt ((fun i β¦ i) β¨7, β―β©) ((fun i β¦ i) β¨2, β―β©)) = (fun i β¦ i) β¨2, β―β© All goals completed! π
[Uniqueness] Show that any Fin 24 decomposes into projections.
lemma h_crt_uniq (x : dayClock.carrier) :
crt (pβ.val x) (pβ.val x) = x := x:dayClock.carrierβ’ crt (βpβ x) (βpβ x) = x
β’ crt (βpβ ((fun i β¦ i) β¨0, β―β©)) (βpβ ((fun i β¦ i) β¨0, β―β©)) = (fun i β¦ i) β¨0, β―β©β’ crt (βpβ ((fun i β¦ i) β¨1, β―β©)) (βpβ ((fun i β¦ i) β¨1, β―β©)) = (fun i β¦ i) β¨1, β―β©β’ crt (βpβ ((fun i β¦ i) β¨2, β―β©)) (βpβ ((fun i β¦ i) β¨2, β―β©)) = (fun i β¦ i) β¨2, β―β©β’ crt (βpβ ((fun i β¦ i) β¨3, β―β©)) (βpβ ((fun i β¦ i) β¨3, β―β©)) = (fun i β¦ i) β¨3, β―β©β’ crt (βpβ ((fun i β¦ i) β¨4, β―β©)) (βpβ ((fun i β¦ i) β¨4, β―β©)) = (fun i β¦ i) β¨4, β―β©β’ crt (βpβ ((fun i β¦ i) β¨5, β―β©)) (βpβ ((fun i β¦ i) β¨5, β―β©)) = (fun i β¦ i) β¨5, β―β©β’ crt (βpβ ((fun i β¦ i) β¨6, β―β©)) (βpβ ((fun i β¦ i) β¨6, β―β©)) = (fun i β¦ i) β¨6, β―β©β’ crt (βpβ ((fun i β¦ i) β¨7, β―β©)) (βpβ ((fun i β¦ i) β¨7, β―β©)) = (fun i β¦ i) β¨7, β―β©β’ crt (βpβ ((fun i β¦ i) β¨8, β―β©)) (βpβ ((fun i β¦ i) β¨8, β―β©)) = (fun i β¦ i) β¨8, β―β©β’ crt (βpβ ((fun i β¦ i) β¨9, β―β©)) (βpβ ((fun i β¦ i) β¨9, β―β©)) = (fun i β¦ i) β¨9, β―β©β’ crt (βpβ ((fun i β¦ i) β¨10, β―β©)) (βpβ ((fun i β¦ i) β¨10, β―β©)) = (fun i β¦ i) β¨10, β―β©β’ crt (βpβ ((fun i β¦ i) β¨11, β―β©)) (βpβ ((fun i β¦ i) β¨11, β―β©)) = (fun i β¦ i) β¨11, β―β©β’ crt (βpβ ((fun i β¦ i) β¨12, β―β©)) (βpβ ((fun i β¦ i) β¨12, β―β©)) = (fun i β¦ i) β¨12, β―β©β’ crt (βpβ ((fun i β¦ i) β¨13, β―β©)) (βpβ ((fun i β¦ i) β¨13, β―β©)) = (fun i β¦ i) β¨13, β―β©β’ crt (βpβ ((fun i β¦ i) β¨14, β―β©)) (βpβ ((fun i β¦ i) β¨14, β―β©)) = (fun i β¦ i) β¨14, β―β©β’ crt (βpβ ((fun i β¦ i) β¨15, β―β©)) (βpβ ((fun i β¦ i) β¨15, β―β©)) = (fun i β¦ i) β¨15, β―β©β’ crt (βpβ ((fun i β¦ i) β¨16, β―β©)) (βpβ ((fun i β¦ i) β¨16, β―β©)) = (fun i β¦ i) β¨16, β―β©β’ crt (βpβ ((fun i β¦ i) β¨17, β―β©)) (βpβ ((fun i β¦ i) β¨17, β―β©)) = (fun i β¦ i) β¨17, β―β©β’ crt (βpβ ((fun i β¦ i) β¨18, β―β©)) (βpβ ((fun i β¦ i) β¨18, β―β©)) = (fun i β¦ i) β¨18, β―β©β’ crt (βpβ ((fun i β¦ i) β¨19, β―β©)) (βpβ ((fun i β¦ i) β¨19, β―β©)) = (fun i β¦ i) β¨19, β―β©β’ crt (βpβ ((fun i β¦ i) β¨20, β―β©)) (βpβ ((fun i β¦ i) β¨20, β―β©)) = (fun i β¦ i) β¨20, β―β©β’ crt (βpβ ((fun i β¦ i) β¨21, β―β©)) (βpβ ((fun i β¦ i) β¨21, β―β©)) = (fun i β¦ i) β¨21, β―β©β’ crt (βpβ ((fun i β¦ i) β¨22, β―β©)) (βpβ ((fun i β¦ i) β¨22, β―β©)) = (fun i β¦ i) β¨22, β―β©β’ crt (βpβ ((fun i β¦ i) β¨23, β―β©)) (βpβ ((fun i β¦ i) β¨23, β―β©)) = (fun i β¦ i) β¨23, β―β© β’ crt (βpβ ((fun i β¦ i) β¨0, β―β©)) (βpβ ((fun i β¦ i) β¨0, β―β©)) = (fun i β¦ i) β¨0, β―β©β’ crt (βpβ ((fun i β¦ i) β¨1, β―β©)) (βpβ ((fun i β¦ i) β¨1, β―β©)) = (fun i β¦ i) β¨1, β―β©β’ crt (βpβ ((fun i β¦ i) β¨2, β―β©)) (βpβ ((fun i β¦ i) β¨2, β―β©)) = (fun i β¦ i) β¨2, β―β©β’ crt (βpβ ((fun i β¦ i) β¨3, β―β©)) (βpβ ((fun i β¦ i) β¨3, β―β©)) = (fun i β¦ i) β¨3, β―β©β’ crt (βpβ ((fun i β¦ i) β¨4, β―β©)) (βpβ ((fun i β¦ i) β¨4, β―β©)) = (fun i β¦ i) β¨4, β―β©β’ crt (βpβ ((fun i β¦ i) β¨5, β―β©)) (βpβ ((fun i β¦ i) β¨5, β―β©)) = (fun i β¦ i) β¨5, β―β©β’ crt (βpβ ((fun i β¦ i) β¨6, β―β©)) (βpβ ((fun i β¦ i) β¨6, β―β©)) = (fun i β¦ i) β¨6, β―β©β’ crt (βpβ ((fun i β¦ i) β¨7, β―β©)) (βpβ ((fun i β¦ i) β¨7, β―β©)) = (fun i β¦ i) β¨7, β―β©β’ crt (βpβ ((fun i β¦ i) β¨8, β―β©)) (βpβ ((fun i β¦ i) β¨8, β―β©)) = (fun i β¦ i) β¨8, β―β©β’ crt (βpβ ((fun i β¦ i) β¨9, β―β©)) (βpβ ((fun i β¦ i) β¨9, β―β©)) = (fun i β¦ i) β¨9, β―β©β’ crt (βpβ ((fun i β¦ i) β¨10, β―β©)) (βpβ ((fun i β¦ i) β¨10, β―β©)) = (fun i β¦ i) β¨10, β―β©β’ crt (βpβ ((fun i β¦ i) β¨11, β―β©)) (βpβ ((fun i β¦ i) β¨11, β―β©)) = (fun i β¦ i) β¨11, β―β©β’ crt (βpβ ((fun i β¦ i) β¨12, β―β©)) (βpβ ((fun i β¦ i) β¨12, β―β©)) = (fun i β¦ i) β¨12, β―β©β’ crt (βpβ ((fun i β¦ i) β¨13, β―β©)) (βpβ ((fun i β¦ i) β¨13, β―β©)) = (fun i β¦ i) β¨13, β―β©β’ crt (βpβ ((fun i β¦ i) β¨14, β―β©)) (βpβ ((fun i β¦ i) β¨14, β―β©)) = (fun i β¦ i) β¨14, β―β©β’ crt (βpβ ((fun i β¦ i) β¨15, β―β©)) (βpβ ((fun i β¦ i) β¨15, β―β©)) = (fun i β¦ i) β¨15, β―β©β’ crt (βpβ ((fun i β¦ i) β¨16, β―β©)) (βpβ ((fun i β¦ i) β¨16, β―β©)) = (fun i β¦ i) β¨16, β―β©β’ crt (βpβ ((fun i β¦ i) β¨17, β―β©)) (βpβ ((fun i β¦ i) β¨17, β―β©)) = (fun i β¦ i) β¨17, β―β©β’ crt (βpβ ((fun i β¦ i) β¨18, β―β©)) (βpβ ((fun i β¦ i) β¨18, β―β©)) = (fun i β¦ i) β¨18, β―β©β’ crt (βpβ ((fun i β¦ i) β¨19, β―β©)) (βpβ ((fun i β¦ i) β¨19, β―β©)) = (fun i β¦ i) β¨19, β―β©β’ crt (βpβ ((fun i β¦ i) β¨20, β―β©)) (βpβ ((fun i β¦ i) β¨20, β―β©)) = (fun i β¦ i) β¨20, β―β©β’ crt (βpβ ((fun i β¦ i) β¨21, β―β©)) (βpβ ((fun i β¦ i) β¨21, β―β©)) = (fun i β¦ i) β¨21, β―β©β’ crt (βpβ ((fun i β¦ i) β¨22, β―β©)) (βpβ ((fun i β¦ i) β¨22, β―β©)) = (fun i β¦ i) β¨22, β―β©β’ crt (βpβ ((fun i β¦ i) β¨23, β―β©)) (βpβ ((fun i β¦ i) β¨23, β―β©)) = (fun i β¦ i) β¨23, β―β© All goals completed! π
We are now ready to prove that the 'day clock' with the given projections is the product of the 'shift clock' and our '3-hour clock' X^{β»\alpha}.
example : IsLimit (BinaryFan.mk pβ pβ) := {
-- Construct morphism f from cone point s.pt to product
lift s := β¨
fun x β¦ crt ((BinaryFan.fst s).val x)
((BinaryFan.snd s).val x),
s:Cone (pair shiftClock XΞ±)β’ (fun x β¦ crt (β(BinaryFan.fst s) x) (β(BinaryFan.snd s) x)) β s.pt.toEnd =
(BinaryFan.mk pβ pβ).pt.toEnd β fun x β¦ crt (β(BinaryFan.fst s) x) (β(BinaryFan.snd s) x)
s:Cone (pair shiftClock XΞ±)x:s.pt.carrierβ’ ((fun x β¦ crt (β(BinaryFan.fst s) x) (β(BinaryFan.snd s) x)) β s.pt.toEnd) x =
((BinaryFan.mk pβ pβ).pt.toEnd β fun x β¦ crt (β(BinaryFan.fst s) x) (β(BinaryFan.snd s) x)) x
s:Cone (pair shiftClock XΞ±)x:s.pt.carrierhfβ_comm:(β(BinaryFan.fst s) β (((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left }).toEnd) x =
(((pair shiftClock XΞ±).obj { as := WalkingPair.left }).toEnd β β(BinaryFan.fst s)) x :=
congr_fun (BinaryFan.fst s).property xβ’ ((fun x β¦ crt (β(BinaryFan.fst s) x) (β(BinaryFan.snd s) x)) β s.pt.toEnd) x =
((BinaryFan.mk pβ pβ).pt.toEnd β fun x β¦ crt (β(BinaryFan.fst s) x) (β(BinaryFan.snd s) x)) x
s:Cone (pair shiftClock XΞ±)x:s.pt.carrierhfβ_comm:(β(BinaryFan.fst s) β (((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left }).toEnd) x =
(((pair shiftClock XΞ±).obj { as := WalkingPair.left }).toEnd β β(BinaryFan.fst s)) x :=
congr_fun (BinaryFan.fst s).property xhfβ_comm:(β(BinaryFan.snd s) β (((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.right }).toEnd) x =
(((pair shiftClock XΞ±).obj { as := WalkingPair.right }).toEnd β β(BinaryFan.snd s)) x :=
congr_fun (BinaryFan.snd s).property xβ’ ((fun x β¦ crt (β(BinaryFan.fst s) x) (β(BinaryFan.snd s) x)) β s.pt.toEnd) x =
((BinaryFan.mk pβ pβ).pt.toEnd β fun x β¦ crt (β(BinaryFan.fst s) x) (β(BinaryFan.snd s) x)) x
s:Cone (pair shiftClock XΞ±)x:s.pt.carrierhfβ_comm:β(BinaryFan.fst s) (s.pt.toEnd x) = β(BinaryFan.fst s) x + 1 := congr_fun (BinaryFan.fst s).property xhfβ_comm:β(BinaryFan.snd s) (s.pt.toEnd x) = β(BinaryFan.snd s) x + 1 := congr_fun (BinaryFan.snd s).property xβ’ crt (β(BinaryFan.fst s) (s.pt.toEnd x)) (β(BinaryFan.snd s) (s.pt.toEnd x)) =
crt (β(BinaryFan.fst s) x) (β(BinaryFan.snd s) x) + 1
All goals completed! π
β©
-- Verify triangle diagrams commute for both legs of cone s
fac s j := s:Cone (pair shiftClock XΞ±)j:Discrete WalkingPairβ’ (BinaryFan.mk pβ pβ).Ο.app j β β¨fun x β¦ crt (β(BinaryFan.fst s) x) (β(BinaryFan.snd s) x), β―β© = s.Ο.app j
s:Cone (pair shiftClock XΞ±)β’ (BinaryFan.mk pβ pβ).Ο.app { as := WalkingPair.left } β β¨fun x β¦ crt (β(BinaryFan.fst s) x) (β(BinaryFan.snd s) x), β―β© =
s.Ο.app { as := WalkingPair.left }s:Cone (pair shiftClock XΞ±)β’ (BinaryFan.mk pβ pβ).Ο.app { as := WalkingPair.right } β
β¨fun x β¦ crt (β(BinaryFan.fst s) x) (β(BinaryFan.snd s) x), β―β© =
s.Ο.app { as := WalkingPair.right }
all_goals
s:Cone (pair shiftClock XΞ±)β’ β((BinaryFan.mk pβ pβ).Ο.app { as := WalkingPair.right } β
β¨fun x β¦ crt (β(BinaryFan.fst s) x) (β(BinaryFan.snd s) x), β―β©) =
β(s.Ο.app { as := WalkingPair.right })
s:Cone (pair shiftClock XΞ±)x:s.pt.carrierβ’ β((BinaryFan.mk pβ pβ).Ο.app { as := WalkingPair.right } β
β¨fun x β¦ crt (β(BinaryFan.fst s) x) (β(BinaryFan.snd s) x), β―β©)
x =
β(s.Ο.app { as := WalkingPair.right }) x
first | s:Cone (pair shiftClock XΞ±)x:s.pt.carrierβ’ β((BinaryFan.mk pβ pβ).Ο.app { as := WalkingPair.right } β
β¨fun x β¦ crt (β(BinaryFan.fst s) x) (β(BinaryFan.snd s) x), β―β©)
x =
β(s.Ο.app { as := WalkingPair.right }) x | All goals completed! π
-- Show morphism f is unique by decomposing it into projections
uniq s f hf := s:Cone (pair shiftClock XΞ±)f:s.pt βΆ (BinaryFan.mk pβ pβ).pthf:β (j : Discrete WalkingPair), (BinaryFan.mk pβ pβ).Ο.app j β f = s.Ο.app jβ’ f = β¨fun x β¦ crt (β(BinaryFan.fst s) x) (β(BinaryFan.snd s) x), β―β©
s:Cone (pair shiftClock XΞ±)f:s.pt βΆ (BinaryFan.mk pβ pβ).pthf:β (j : Discrete WalkingPair), (BinaryFan.mk pβ pβ).Ο.app j β f = s.Ο.app jβ’ βf = ββ¨fun x β¦ crt (β(BinaryFan.fst s) x) (β(BinaryFan.snd s) x), β―β©
s:Cone (pair shiftClock XΞ±)f:s.pt βΆ (BinaryFan.mk pβ pβ).pthf:β (j : Discrete WalkingPair), (BinaryFan.mk pβ pβ).Ο.app j β f = s.Ο.app jx:s.pt.carrierβ’ βf x = ββ¨fun x β¦ crt (β(BinaryFan.fst s) x) (β(BinaryFan.snd s) x), β―β© x
s:Cone (pair shiftClock XΞ±)f:s.pt βΆ (BinaryFan.mk pβ pβ).pthf:β (j : Discrete WalkingPair), (BinaryFan.mk pβ pβ).Ο.app j β f = s.Ο.app jx:s.pt.carrierβ’ βf x = crt (β(s.Ο.app { as := WalkingPair.left }) x) (β(s.Ο.app { as := WalkingPair.right }) x)
s:Cone (pair shiftClock XΞ±)f:s.pt βΆ (BinaryFan.mk pβ pβ).pthf:β (j : Discrete WalkingPair), (BinaryFan.mk pβ pβ).Ο.app j β f = s.Ο.app jx:s.pt.carrierβ’ crt (βpβ (βf x)) (βpβ (βf x)) =
crt (β((BinaryFan.mk pβ pβ).Ο.app { as := WalkingPair.left } β f) x)
(β((BinaryFan.mk pβ pβ).Ο.app { as := WalkingPair.right } β f) x)
All goals completed! π
}
Exercise 2 (p. 244)
What is the product {C_m \times C_n} of an m-cycle and an n-cycle? For example, what is the product {C_{12} \times C_{8}}? Hint: Start by investigating products of cycles of smaller sizes.
Solution: Exercise 2
TODO Exercise 21.2
Exercise 3 (p. 244)
Return to Exercise 3 of Session 12. Show that the object which was called {\mathbf{G} \times \mathbf{C}}, when provided with appropriate projection maps, really is the product in the category πΊβ»β».
Solution: Exercise 3
See Exercise 3 of Session 12 for the relevant definitions.
We begin by defining appropriate projection maps.
def pβ : GC βΆ G := β¨
fun (g, _) β¦ g,
β’ ((fun x β¦
match x with
| (g, snd) => g) β
GC.toEnd =
G.toEnd β fun x β¦
match x with
| (g, snd) => g) β§
(fun x β¦
match x with
| (g, snd) => g) β
GC.toEnd2 =
G.toEnd2 β fun x β¦
match x with
| (g, snd) => g
β’ (fun x β¦
match x with
| (g, snd) => g) β
GC.toEnd =
G.toEnd β fun x β¦
match x with
| (g, snd) => gβ’ (fun x β¦
match x with
| (g, snd) => g) β
GC.toEnd2 =
G.toEnd2 β fun x β¦
match x with
| (g, snd) => g
β’ (fun x β¦
match x with
| (g, snd) => g) β
GC.toEnd =
G.toEnd β fun x β¦
match x with
| (g, snd) => g x:GC.carrierβ’ ((fun x β¦
match x with
| (g, snd) => g) β
GC.toEnd)
x =
(G.toEnd β fun x β¦
match x with
| (g, snd) => g)
x
All goals completed! π
β’ (fun x β¦
match x with
| (g, snd) => g) β
GC.toEnd2 =
G.toEnd2 β fun x β¦
match x with
| (g, snd) => g xβ:Genderxβ:Clanβ’ ((fun x β¦
match x with
| (g, snd) => g) β
GC.toEnd2)
(xβ, xβ) =
(G.toEnd2 β fun x β¦
match x with
| (g, snd) => g)
(xβ, xβ)
xβ:Clanβ’ ((fun x β¦
match x with
| (g, snd) => g) β
GC.toEnd2)
(Gender.female, xβ) =
(G.toEnd2 β fun x β¦
match x with
| (g, snd) => g)
(Gender.female, xβ)xβ:Clanβ’ ((fun x β¦
match x with
| (g, snd) => g) β
GC.toEnd2)
(Gender.male, xβ) =
(G.toEnd2 β fun x β¦
match x with
| (g, snd) => g)
(Gender.male, xβ) xβ:Clanβ’ ((fun x β¦
match x with
| (g, snd) => g) β
GC.toEnd2)
(Gender.female, xβ) =
(G.toEnd2 β fun x β¦
match x with
| (g, snd) => g)
(Gender.female, xβ)xβ:Clanβ’ ((fun x β¦
match x with
| (g, snd) => g) β
GC.toEnd2)
(Gender.male, xβ) =
(G.toEnd2 β fun x β¦
match x with
| (g, snd) => g)
(Gender.male, xβ) β’ ((fun x β¦
match x with
| (g, snd) => g) β
GC.toEnd2)
(Gender.male, Clan.wolf) =
(G.toEnd2 β fun x β¦
match x with
| (g, snd) => g)
(Gender.male, Clan.wolf)β’ ((fun x β¦
match x with
| (g, snd) => g) β
GC.toEnd2)
(Gender.male, Clan.bear) =
(G.toEnd2 β fun x β¦
match x with
| (g, snd) => g)
(Gender.male, Clan.bear) β’ ((fun x β¦
match x with
| (g, snd) => g) β
GC.toEnd2)
(Gender.female, Clan.wolf) =
(G.toEnd2 β fun x β¦
match x with
| (g, snd) => g)
(Gender.female, Clan.wolf)β’ ((fun x β¦
match x with
| (g, snd) => g) β
GC.toEnd2)
(Gender.female, Clan.bear) =
(G.toEnd2 β fun x β¦
match x with
| (g, snd) => g)
(Gender.female, Clan.bear)β’ ((fun x β¦
match x with
| (g, snd) => g) β
GC.toEnd2)
(Gender.male, Clan.wolf) =
(G.toEnd2 β fun x β¦
match x with
| (g, snd) => g)
(Gender.male, Clan.wolf)β’ ((fun x β¦
match x with
| (g, snd) => g) β
GC.toEnd2)
(Gender.male, Clan.bear) =
(G.toEnd2 β fun x β¦
match x with
| (g, snd) => g)
(Gender.male, Clan.bear) All goals completed! π
β©
def pβ : GC βΆ C := β¨
fun (_, c) β¦ c,
β’ ((fun x β¦
match x with
| (fst, c) => c) β
GC.toEnd =
C.toEnd β fun x β¦
match x with
| (fst, c) => c) β§
(fun x β¦
match x with
| (fst, c) => c) β
GC.toEnd2 =
C.toEnd2 β fun x β¦
match x with
| (fst, c) => c
β’ (fun x β¦
match x with
| (fst, c) => c) β
GC.toEnd =
C.toEnd β fun x β¦
match x with
| (fst, c) => cβ’ (fun x β¦
match x with
| (fst, c) => c) β
GC.toEnd2 =
C.toEnd2 β fun x β¦
match x with
| (fst, c) => c
β’ (fun x β¦
match x with
| (fst, c) => c) β
GC.toEnd =
C.toEnd β fun x β¦
match x with
| (fst, c) => c x:GC.carrierβ’ ((fun x β¦
match x with
| (fst, c) => c) β
GC.toEnd)
x =
(C.toEnd β fun x β¦
match x with
| (fst, c) => c)
x
All goals completed! π
β’ (fun x β¦
match x with
| (fst, c) => c) β
GC.toEnd2 =
C.toEnd2 β fun x β¦
match x with
| (fst, c) => c xβ:Genderxβ:Clanβ’ ((fun x β¦
match x with
| (fst, c) => c) β
GC.toEnd2)
(xβ, xβ) =
(C.toEnd2 β fun x β¦
match x with
| (fst, c) => c)
(xβ, xβ)
xβ:Clanβ’ ((fun x β¦
match x with
| (fst, c) => c) β
GC.toEnd2)
(Gender.female, xβ) =
(C.toEnd2 β fun x β¦
match x with
| (fst, c) => c)
(Gender.female, xβ)xβ:Clanβ’ ((fun x β¦
match x with
| (fst, c) => c) β
GC.toEnd2)
(Gender.male, xβ) =
(C.toEnd2 β fun x β¦
match x with
| (fst, c) => c)
(Gender.male, xβ) xβ:Clanβ’ ((fun x β¦
match x with
| (fst, c) => c) β
GC.toEnd2)
(Gender.female, xβ) =
(C.toEnd2 β fun x β¦
match x with
| (fst, c) => c)
(Gender.female, xβ)xβ:Clanβ’ ((fun x β¦
match x with
| (fst, c) => c) β
GC.toEnd2)
(Gender.male, xβ) =
(C.toEnd2 β fun x β¦
match x with
| (fst, c) => c)
(Gender.male, xβ) β’ ((fun x β¦
match x with
| (fst, c) => c) β
GC.toEnd2)
(Gender.male, Clan.wolf) =
(C.toEnd2 β fun x β¦
match x with
| (fst, c) => c)
(Gender.male, Clan.wolf)β’ ((fun x β¦
match x with
| (fst, c) => c) β
GC.toEnd2)
(Gender.male, Clan.bear) =
(C.toEnd2 β fun x β¦
match x with
| (fst, c) => c)
(Gender.male, Clan.bear) β’ ((fun x β¦
match x with
| (fst, c) => c) β
GC.toEnd2)
(Gender.female, Clan.wolf) =
(C.toEnd2 β fun x β¦
match x with
| (fst, c) => c)
(Gender.female, Clan.wolf)β’ ((fun x β¦
match x with
| (fst, c) => c) β
GC.toEnd2)
(Gender.female, Clan.bear) =
(C.toEnd2 β fun x β¦
match x with
| (fst, c) => c)
(Gender.female, Clan.bear)β’ ((fun x β¦
match x with
| (fst, c) => c) β
GC.toEnd2)
(Gender.male, Clan.wolf) =
(C.toEnd2 β fun x β¦
match x with
| (fst, c) => c)
(Gender.male, Clan.wolf)β’ ((fun x β¦
match x with
| (fst, c) => c) β
GC.toEnd2)
(Gender.male, Clan.bear) =
(C.toEnd2 β fun x β¦
match x with
| (fst, c) => c)
(Gender.male, Clan.bear) All goals completed! π
β©
We use mathlib's API for binary products in the proof that follows.
example : IsLimit (BinaryFan.mk pβ pβ) := {
lift s := β¨
fun x β¦ ((BinaryFan.fst s).val x, (BinaryFan.snd s).val x),
s:Cone (pair G C)β’ ((fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)) β s.pt.toEnd =
(BinaryFan.mk pβ pβ).pt.toEnd β fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)) β§
(fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)) β s.pt.toEnd2 =
(BinaryFan.mk pβ pβ).pt.toEnd2 β fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)
s:Cone (pair G C)h_fst_m:β(BinaryFan.fst s) β (((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left }).toEnd =
((pair G C).obj { as := WalkingPair.left }).toEnd β β(BinaryFan.fst s)h_fst_f:β(BinaryFan.fst s) β (((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left }).toEnd2 =
((pair G C).obj { as := WalkingPair.left }).toEnd2 β β(BinaryFan.fst s)β’ ((fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)) β s.pt.toEnd =
(BinaryFan.mk pβ pβ).pt.toEnd β fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)) β§
(fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)) β s.pt.toEnd2 =
(BinaryFan.mk pβ pβ).pt.toEnd2 β fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)
s:Cone (pair G C)h_fst_m:β(BinaryFan.fst s) β (((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left }).toEnd =
((pair G C).obj { as := WalkingPair.left }).toEnd β β(BinaryFan.fst s)h_fst_f:β(BinaryFan.fst s) β (((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left }).toEnd2 =
((pair G C).obj { as := WalkingPair.left }).toEnd2 β β(BinaryFan.fst s)h_snd_m:β(BinaryFan.snd s) β (((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.right }).toEnd =
((pair G C).obj { as := WalkingPair.right }).toEnd β β(BinaryFan.snd s)h_snd_f:β(BinaryFan.snd s) β (((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.right }).toEnd2 =
((pair G C).obj { as := WalkingPair.right }).toEnd2 β β(BinaryFan.snd s)β’ ((fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)) β s.pt.toEnd =
(BinaryFan.mk pβ pβ).pt.toEnd β fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)) β§
(fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)) β s.pt.toEnd2 =
(BinaryFan.mk pβ pβ).pt.toEnd2 β fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)
s:Cone (pair G C)h_fst_m:β(BinaryFan.fst s) β s.pt.toEnd = G.toEnd β β(BinaryFan.fst s)h_fst_f:β(BinaryFan.fst s) β s.pt.toEnd2 = G.toEnd2 β β(BinaryFan.fst s)h_snd_m:β(BinaryFan.snd s) β s.pt.toEnd = C.toEnd β β(BinaryFan.snd s)h_snd_f:β(BinaryFan.snd s) β s.pt.toEnd2 = C.toEnd2 β β(BinaryFan.snd s)β’ ((fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)) β s.pt.toEnd =
GC.toEnd β fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)) β§
(fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)) β s.pt.toEnd2 =
GC.toEnd2 β fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)
s:Cone (pair G C)h_fst_m:β(BinaryFan.fst s) β s.pt.toEnd = G.toEnd β β(BinaryFan.fst s)h_fst_f:β(BinaryFan.fst s) β s.pt.toEnd2 = G.toEnd2 β β(BinaryFan.fst s)h_snd_m:β(BinaryFan.snd s) β s.pt.toEnd = C.toEnd β β(BinaryFan.snd s)h_snd_f:β(BinaryFan.snd s) β s.pt.toEnd2 = C.toEnd2 β β(BinaryFan.snd s)β’ (fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)) β s.pt.toEnd =
GC.toEnd β fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)s:Cone (pair G C)h_fst_m:β(BinaryFan.fst s) β s.pt.toEnd = G.toEnd β β(BinaryFan.fst s)h_fst_f:β(BinaryFan.fst s) β s.pt.toEnd2 = G.toEnd2 β β(BinaryFan.fst s)h_snd_m:β(BinaryFan.snd s) β s.pt.toEnd = C.toEnd β β(BinaryFan.snd s)h_snd_f:β(BinaryFan.snd s) β s.pt.toEnd2 = C.toEnd2 β β(BinaryFan.snd s)β’ (fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)) β s.pt.toEnd2 =
GC.toEnd2 β fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)
s:Cone (pair G C)h_fst_m:β(BinaryFan.fst s) β s.pt.toEnd = G.toEnd β β(BinaryFan.fst s)h_fst_f:β(BinaryFan.fst s) β s.pt.toEnd2 = G.toEnd2 β β(BinaryFan.fst s)h_snd_m:β(BinaryFan.snd s) β s.pt.toEnd = C.toEnd β β(BinaryFan.snd s)h_snd_f:β(BinaryFan.snd s) β s.pt.toEnd2 = C.toEnd2 β β(BinaryFan.snd s)β’ (fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)) β s.pt.toEnd =
GC.toEnd β fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x) s:Cone (pair G C)h_fst_m:β(BinaryFan.fst s) β s.pt.toEnd = G.toEnd β β(BinaryFan.fst s)h_fst_f:β(BinaryFan.fst s) β s.pt.toEnd2 = G.toEnd2 β β(BinaryFan.fst s)h_snd_m:β(BinaryFan.snd s) β s.pt.toEnd = C.toEnd β β(BinaryFan.snd s)h_snd_f:β(BinaryFan.snd s) β s.pt.toEnd2 = C.toEnd2 β β(BinaryFan.snd s)x:s.pt.carrierβ’ ((fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)) β s.pt.toEnd) x =
(GC.toEnd β fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)) x
s:Cone (pair G C)h_fst_m:β(BinaryFan.fst s) β s.pt.toEnd = G.toEnd β β(BinaryFan.fst s)h_fst_f:β(BinaryFan.fst s) β s.pt.toEnd2 = G.toEnd2 β β(BinaryFan.fst s)h_snd_m:β(BinaryFan.snd s) β s.pt.toEnd = C.toEnd β β(BinaryFan.snd s)h_snd_f:β(BinaryFan.snd s) β s.pt.toEnd2 = C.toEnd2 β β(BinaryFan.snd s)x:s.pt.carrierβ’ (((fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)) β s.pt.toEnd) x).1 =
((GC.toEnd β fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)) x).1s:Cone (pair G C)h_fst_m:β(BinaryFan.fst s) β s.pt.toEnd = G.toEnd β β(BinaryFan.fst s)h_fst_f:β(BinaryFan.fst s) β s.pt.toEnd2 = G.toEnd2 β β(BinaryFan.fst s)h_snd_m:β(BinaryFan.snd s) β s.pt.toEnd = C.toEnd β β(BinaryFan.snd s)h_snd_f:β(BinaryFan.snd s) β s.pt.toEnd2 = C.toEnd2 β β(BinaryFan.snd s)x:s.pt.carrierβ’ (((fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)) β s.pt.toEnd) x).2 =
((GC.toEnd β fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)) x).2
s:Cone (pair G C)h_fst_m:β(BinaryFan.fst s) β s.pt.toEnd = G.toEnd β β(BinaryFan.fst s)h_fst_f:β(BinaryFan.fst s) β s.pt.toEnd2 = G.toEnd2 β β(BinaryFan.fst s)h_snd_m:β(BinaryFan.snd s) β s.pt.toEnd = C.toEnd β β(BinaryFan.snd s)h_snd_f:β(BinaryFan.snd s) β s.pt.toEnd2 = C.toEnd2 β β(BinaryFan.snd s)x:s.pt.carrierβ’ (((fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)) β s.pt.toEnd) x).1 =
((GC.toEnd β fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)) x).1 s:Cone (pair G C)h_fst_m:β(BinaryFan.fst s) β s.pt.toEnd = G.toEnd β β(BinaryFan.fst s)h_fst_f:β(BinaryFan.fst s) β s.pt.toEnd2 = G.toEnd2 β β(BinaryFan.fst s)h_snd_m:β(BinaryFan.snd s) β s.pt.toEnd = C.toEnd β β(BinaryFan.snd s)h_snd_f:β(BinaryFan.snd s) β s.pt.toEnd2 = C.toEnd2 β β(BinaryFan.snd s)x:s.pt.carrierβ’ (β(BinaryFan.fst s) β s.pt.toEnd) x = ((GC.toEnd β fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)) x).1
s:Cone (pair G C)h_fst_m:β(BinaryFan.fst s) β s.pt.toEnd = G.toEnd β β(BinaryFan.fst s)h_fst_f:β(BinaryFan.fst s) β s.pt.toEnd2 = G.toEnd2 β β(BinaryFan.fst s)h_snd_m:β(BinaryFan.snd s) β s.pt.toEnd = C.toEnd β β(BinaryFan.snd s)h_snd_f:β(BinaryFan.snd s) β s.pt.toEnd2 = C.toEnd2 β β(BinaryFan.snd s)x:s.pt.carrierβ’ (G.toEnd β β(BinaryFan.fst s)) x = ((GC.toEnd β fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)) x).1; All goals completed! π
s:Cone (pair G C)h_fst_m:β(BinaryFan.fst s) β s.pt.toEnd = G.toEnd β β(BinaryFan.fst s)h_fst_f:β(BinaryFan.fst s) β s.pt.toEnd2 = G.toEnd2 β β(BinaryFan.fst s)h_snd_m:β(BinaryFan.snd s) β s.pt.toEnd = C.toEnd β β(BinaryFan.snd s)h_snd_f:β(BinaryFan.snd s) β s.pt.toEnd2 = C.toEnd2 β β(BinaryFan.snd s)x:s.pt.carrierβ’ (((fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)) β s.pt.toEnd) x).2 =
((GC.toEnd β fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)) x).2 s:Cone (pair G C)h_fst_m:β(BinaryFan.fst s) β s.pt.toEnd = G.toEnd β β(BinaryFan.fst s)h_fst_f:β(BinaryFan.fst s) β s.pt.toEnd2 = G.toEnd2 β β(BinaryFan.fst s)h_snd_m:β(BinaryFan.snd s) β s.pt.toEnd = C.toEnd β β(BinaryFan.snd s)h_snd_f:β(BinaryFan.snd s) β s.pt.toEnd2 = C.toEnd2 β β(BinaryFan.snd s)x:s.pt.carrierβ’ (β(BinaryFan.snd s) β s.pt.toEnd) x = ((GC.toEnd β fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)) x).2
s:Cone (pair G C)h_fst_m:β(BinaryFan.fst s) β s.pt.toEnd = G.toEnd β β(BinaryFan.fst s)h_fst_f:β(BinaryFan.fst s) β s.pt.toEnd2 = G.toEnd2 β β(BinaryFan.fst s)h_snd_m:β(BinaryFan.snd s) β s.pt.toEnd = C.toEnd β β(BinaryFan.snd s)h_snd_f:β(BinaryFan.snd s) β s.pt.toEnd2 = C.toEnd2 β β(BinaryFan.snd s)x:s.pt.carrierβ’ (C.toEnd β β(BinaryFan.snd s)) x = ((GC.toEnd β fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)) x).2; All goals completed! π
s:Cone (pair G C)h_fst_m:β(BinaryFan.fst s) β s.pt.toEnd = G.toEnd β β(BinaryFan.fst s)h_fst_f:β(BinaryFan.fst s) β s.pt.toEnd2 = G.toEnd2 β β(BinaryFan.fst s)h_snd_m:β(BinaryFan.snd s) β s.pt.toEnd = C.toEnd β β(BinaryFan.snd s)h_snd_f:β(BinaryFan.snd s) β s.pt.toEnd2 = C.toEnd2 β β(BinaryFan.snd s)β’ (fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)) β s.pt.toEnd2 =
GC.toEnd2 β fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x) s:Cone (pair G C)h_fst_m:β(BinaryFan.fst s) β s.pt.toEnd = G.toEnd β β(BinaryFan.fst s)h_fst_f:β(BinaryFan.fst s) β s.pt.toEnd2 = G.toEnd2 β β(BinaryFan.fst s)h_snd_m:β(BinaryFan.snd s) β s.pt.toEnd = C.toEnd β β(BinaryFan.snd s)h_snd_f:β(BinaryFan.snd s) β s.pt.toEnd2 = C.toEnd2 β β(BinaryFan.snd s)x:s.pt.carrierβ’ ((fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)) β s.pt.toEnd2) x =
(GC.toEnd2 β fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)) x
s:Cone (pair G C)h_fst_m:β(BinaryFan.fst s) β s.pt.toEnd = G.toEnd β β(BinaryFan.fst s)h_fst_f:β(BinaryFan.fst s) β s.pt.toEnd2 = G.toEnd2 β β(BinaryFan.fst s)h_snd_m:β(BinaryFan.snd s) β s.pt.toEnd = C.toEnd β β(BinaryFan.snd s)h_snd_f:β(BinaryFan.snd s) β s.pt.toEnd2 = C.toEnd2 β β(BinaryFan.snd s)x:s.pt.carrierβ’ (((fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)) β s.pt.toEnd2) x).1 =
((GC.toEnd2 β fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)) x).1s:Cone (pair G C)h_fst_m:β(BinaryFan.fst s) β s.pt.toEnd = G.toEnd β β(BinaryFan.fst s)h_fst_f:β(BinaryFan.fst s) β s.pt.toEnd2 = G.toEnd2 β β(BinaryFan.fst s)h_snd_m:β(BinaryFan.snd s) β s.pt.toEnd = C.toEnd β β(BinaryFan.snd s)h_snd_f:β(BinaryFan.snd s) β s.pt.toEnd2 = C.toEnd2 β β(BinaryFan.snd s)x:s.pt.carrierβ’ (((fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)) β s.pt.toEnd2) x).2 =
((GC.toEnd2 β fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)) x).2
s:Cone (pair G C)h_fst_m:β(BinaryFan.fst s) β s.pt.toEnd = G.toEnd β β(BinaryFan.fst s)h_fst_f:β(BinaryFan.fst s) β s.pt.toEnd2 = G.toEnd2 β β(BinaryFan.fst s)h_snd_m:β(BinaryFan.snd s) β s.pt.toEnd = C.toEnd β β(BinaryFan.snd s)h_snd_f:β(BinaryFan.snd s) β s.pt.toEnd2 = C.toEnd2 β β(BinaryFan.snd s)x:s.pt.carrierβ’ (((fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)) β s.pt.toEnd2) x).1 =
((GC.toEnd2 β fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)) x).1 s:Cone (pair G C)h_fst_m:β(BinaryFan.fst s) β s.pt.toEnd = G.toEnd β β(BinaryFan.fst s)h_fst_f:β(BinaryFan.fst s) β s.pt.toEnd2 = G.toEnd2 β β(BinaryFan.fst s)h_snd_m:β(BinaryFan.snd s) β s.pt.toEnd = C.toEnd β β(BinaryFan.snd s)h_snd_f:β(BinaryFan.snd s) β s.pt.toEnd2 = C.toEnd2 β β(BinaryFan.snd s)x:s.pt.carrierβ’ (β(BinaryFan.fst s) β s.pt.toEnd2) x = ((GC.toEnd2 β fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)) x).1
s:Cone (pair G C)h_fst_m:β(BinaryFan.fst s) β s.pt.toEnd = G.toEnd β β(BinaryFan.fst s)h_fst_f:β(BinaryFan.fst s) β s.pt.toEnd2 = G.toEnd2 β β(BinaryFan.fst s)h_snd_m:β(BinaryFan.snd s) β s.pt.toEnd = C.toEnd β β(BinaryFan.snd s)h_snd_f:β(BinaryFan.snd s) β s.pt.toEnd2 = C.toEnd2 β β(BinaryFan.snd s)x:s.pt.carrierβ’ (G.toEnd2 β β(BinaryFan.fst s)) x = ((GC.toEnd2 β fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)) x).1
s:Cone (pair G C)h_fst_m:β(BinaryFan.fst s) β s.pt.toEnd = G.toEnd β β(BinaryFan.fst s)h_fst_f:β(BinaryFan.fst s) β s.pt.toEnd2 = G.toEnd2 β β(BinaryFan.fst s)h_snd_m:β(BinaryFan.snd s) β s.pt.toEnd = C.toEnd β β(BinaryFan.snd s)h_snd_f:β(BinaryFan.snd s) β s.pt.toEnd2 = C.toEnd2 β β(BinaryFan.snd s)x:s.pt.carrierβ’ G.toEnd2 (β(BinaryFan.fst s) x) = (GC.toEnd2 (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)).1
s:Cone (pair G C)h_fst_m:β(BinaryFan.fst s) β s.pt.toEnd = G.toEnd β β(BinaryFan.fst s)h_fst_f:β(BinaryFan.fst s) β s.pt.toEnd2 = G.toEnd2 β β(BinaryFan.fst s)h_snd_m:β(BinaryFan.snd s) β s.pt.toEnd = C.toEnd β β(BinaryFan.snd s)h_snd_f:β(BinaryFan.snd s) β s.pt.toEnd2 = C.toEnd2 β β(BinaryFan.snd s)x:s.pt.carrierc:((pair G C).obj { as := WalkingPair.right }).carrierβ’ G.toEnd2 (β(BinaryFan.fst s) x) = (GC.toEnd2 (β(BinaryFan.fst s) x, c)).1
s:Cone (pair G C)h_fst_m:β(BinaryFan.fst s) β s.pt.toEnd = G.toEnd β β(BinaryFan.fst s)h_fst_f:β(BinaryFan.fst s) β s.pt.toEnd2 = G.toEnd2 β β(BinaryFan.fst s)h_snd_m:β(BinaryFan.snd s) β s.pt.toEnd = C.toEnd β β(BinaryFan.snd s)h_snd_f:β(BinaryFan.snd s) β s.pt.toEnd2 = C.toEnd2 β β(BinaryFan.snd s)x:s.pt.carrierβ’ G.toEnd2 (β(BinaryFan.fst s) x) = (GC.toEnd2 (β(BinaryFan.fst s) x, Clan.wolf)).1s:Cone (pair G C)h_fst_m:β(BinaryFan.fst s) β s.pt.toEnd = G.toEnd β β(BinaryFan.fst s)h_fst_f:β(BinaryFan.fst s) β s.pt.toEnd2 = G.toEnd2 β β(BinaryFan.fst s)h_snd_m:β(BinaryFan.snd s) β s.pt.toEnd = C.toEnd β β(BinaryFan.snd s)h_snd_f:β(BinaryFan.snd s) β s.pt.toEnd2 = C.toEnd2 β β(BinaryFan.snd s)x:s.pt.carrierβ’ G.toEnd2 (β(BinaryFan.fst s) x) = (GC.toEnd2 (β(BinaryFan.fst s) x, Clan.bear)).1 s:Cone (pair G C)h_fst_m:β(BinaryFan.fst s) β s.pt.toEnd = G.toEnd β β(BinaryFan.fst s)h_fst_f:β(BinaryFan.fst s) β s.pt.toEnd2 = G.toEnd2 β β(BinaryFan.fst s)h_snd_m:β(BinaryFan.snd s) β s.pt.toEnd = C.toEnd β β(BinaryFan.snd s)h_snd_f:β(BinaryFan.snd s) β s.pt.toEnd2 = C.toEnd2 β β(BinaryFan.snd s)x:s.pt.carrierβ’ G.toEnd2 (β(BinaryFan.fst s) x) = (GC.toEnd2 (β(BinaryFan.fst s) x, Clan.wolf)).1s:Cone (pair G C)h_fst_m:β(BinaryFan.fst s) β s.pt.toEnd = G.toEnd β β(BinaryFan.fst s)h_fst_f:β(BinaryFan.fst s) β s.pt.toEnd2 = G.toEnd2 β β(BinaryFan.fst s)h_snd_m:β(BinaryFan.snd s) β s.pt.toEnd = C.toEnd β β(BinaryFan.snd s)h_snd_f:β(BinaryFan.snd s) β s.pt.toEnd2 = C.toEnd2 β β(BinaryFan.snd s)x:s.pt.carrierβ’ G.toEnd2 (β(BinaryFan.fst s) x) = (GC.toEnd2 (β(BinaryFan.fst s) x, Clan.bear)).1 All goals completed! π
s:Cone (pair G C)h_fst_m:β(BinaryFan.fst s) β s.pt.toEnd = G.toEnd β β(BinaryFan.fst s)h_fst_f:β(BinaryFan.fst s) β s.pt.toEnd2 = G.toEnd2 β β(BinaryFan.fst s)h_snd_m:β(BinaryFan.snd s) β s.pt.toEnd = C.toEnd β β(BinaryFan.snd s)h_snd_f:β(BinaryFan.snd s) β s.pt.toEnd2 = C.toEnd2 β β(BinaryFan.snd s)x:s.pt.carrierβ’ (((fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)) β s.pt.toEnd2) x).2 =
((GC.toEnd2 β fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)) x).2 s:Cone (pair G C)h_fst_m:β(BinaryFan.fst s) β s.pt.toEnd = G.toEnd β β(BinaryFan.fst s)h_fst_f:β(BinaryFan.fst s) β s.pt.toEnd2 = G.toEnd2 β β(BinaryFan.fst s)h_snd_m:β(BinaryFan.snd s) β s.pt.toEnd = C.toEnd β β(BinaryFan.snd s)h_snd_f:β(BinaryFan.snd s) β s.pt.toEnd2 = C.toEnd2 β β(BinaryFan.snd s)x:s.pt.carrierβ’ (β(BinaryFan.snd s) β s.pt.toEnd2) x = ((GC.toEnd2 β fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)) x).2
s:Cone (pair G C)h_fst_m:β(BinaryFan.fst s) β s.pt.toEnd = G.toEnd β β(BinaryFan.fst s)h_fst_f:β(BinaryFan.fst s) β s.pt.toEnd2 = G.toEnd2 β β(BinaryFan.fst s)h_snd_m:β(BinaryFan.snd s) β s.pt.toEnd = C.toEnd β β(BinaryFan.snd s)h_snd_f:β(BinaryFan.snd s) β s.pt.toEnd2 = C.toEnd2 β β(BinaryFan.snd s)x:s.pt.carrierβ’ (C.toEnd2 β β(BinaryFan.snd s)) x = ((GC.toEnd2 β fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)) x).2
s:Cone (pair G C)h_fst_m:β(BinaryFan.fst s) β s.pt.toEnd = G.toEnd β β(BinaryFan.fst s)h_fst_f:β(BinaryFan.fst s) β s.pt.toEnd2 = G.toEnd2 β β(BinaryFan.fst s)h_snd_m:β(BinaryFan.snd s) β s.pt.toEnd = C.toEnd β β(BinaryFan.snd s)h_snd_f:β(BinaryFan.snd s) β s.pt.toEnd2 = C.toEnd2 β β(BinaryFan.snd s)x:s.pt.carrierβ’ C.toEnd2 (β(BinaryFan.snd s) x) = (GC.toEnd2 (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x)).2
s:Cone (pair G C)h_fst_m:β(BinaryFan.fst s) β s.pt.toEnd = G.toEnd β β(BinaryFan.fst s)h_fst_f:β(BinaryFan.fst s) β s.pt.toEnd2 = G.toEnd2 β β(BinaryFan.fst s)h_snd_m:β(BinaryFan.snd s) β s.pt.toEnd = C.toEnd β β(BinaryFan.snd s)h_snd_f:β(BinaryFan.snd s) β s.pt.toEnd2 = C.toEnd2 β β(BinaryFan.snd s)x:s.pt.carrierc:((pair G C).obj { as := WalkingPair.right }).carrierβ’ C.toEnd2 c = (GC.toEnd2 (β(BinaryFan.fst s) x, c)).2
s:Cone (pair G C)h_fst_m:β(BinaryFan.fst s) β s.pt.toEnd = G.toEnd β β(BinaryFan.fst s)h_fst_f:β(BinaryFan.fst s) β s.pt.toEnd2 = G.toEnd2 β β(BinaryFan.fst s)h_snd_m:β(BinaryFan.snd s) β s.pt.toEnd = C.toEnd β β(BinaryFan.snd s)h_snd_f:β(BinaryFan.snd s) β s.pt.toEnd2 = C.toEnd2 β β(BinaryFan.snd s)x:s.pt.carrierβ’ C.toEnd2 Clan.wolf = (GC.toEnd2 (β(BinaryFan.fst s) x, Clan.wolf)).2s:Cone (pair G C)h_fst_m:β(BinaryFan.fst s) β s.pt.toEnd = G.toEnd β β(BinaryFan.fst s)h_fst_f:β(BinaryFan.fst s) β s.pt.toEnd2 = G.toEnd2 β β(BinaryFan.fst s)h_snd_m:β(BinaryFan.snd s) β s.pt.toEnd = C.toEnd β β(BinaryFan.snd s)h_snd_f:β(BinaryFan.snd s) β s.pt.toEnd2 = C.toEnd2 β β(BinaryFan.snd s)x:s.pt.carrierβ’ C.toEnd2 Clan.bear = (GC.toEnd2 (β(BinaryFan.fst s) x, Clan.bear)).2 s:Cone (pair G C)h_fst_m:β(BinaryFan.fst s) β s.pt.toEnd = G.toEnd β β(BinaryFan.fst s)h_fst_f:β(BinaryFan.fst s) β s.pt.toEnd2 = G.toEnd2 β β(BinaryFan.fst s)h_snd_m:β(BinaryFan.snd s) β s.pt.toEnd = C.toEnd β β(BinaryFan.snd s)h_snd_f:β(BinaryFan.snd s) β s.pt.toEnd2 = C.toEnd2 β β(BinaryFan.snd s)x:s.pt.carrierβ’ C.toEnd2 Clan.wolf = (GC.toEnd2 (β(BinaryFan.fst s) x, Clan.wolf)).2s:Cone (pair G C)h_fst_m:β(BinaryFan.fst s) β s.pt.toEnd = G.toEnd β β(BinaryFan.fst s)h_fst_f:β(BinaryFan.fst s) β s.pt.toEnd2 = G.toEnd2 β β(BinaryFan.fst s)h_snd_m:β(BinaryFan.snd s) β s.pt.toEnd = C.toEnd β β(BinaryFan.snd s)h_snd_f:β(BinaryFan.snd s) β s.pt.toEnd2 = C.toEnd2 β β(BinaryFan.snd s)x:s.pt.carrierβ’ C.toEnd2 Clan.bear = (GC.toEnd2 (β(BinaryFan.fst s) x, Clan.bear)).2 All goals completed! π
β©
fac s j := s:Cone (pair G C)j:Discrete WalkingPairβ’ (BinaryFan.mk pβ pβ).Ο.app j β β¨fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x), β―β© = s.Ο.app j
s:Cone (pair G C)j:Discrete WalkingPairβ’ β((BinaryFan.mk pβ pβ).Ο.app j β β¨fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x), β―β©) = β(s.Ο.app j)
s:Cone (pair G C)j:Discrete WalkingPairx:s.pt.carrierβ’ β((BinaryFan.mk pβ pβ).Ο.app j β β¨fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x), β―β©) x = β(s.Ο.app j) x
s:Cone (pair G C)x:s.pt.carrierβ’ β((BinaryFan.mk pβ pβ).Ο.app { as := WalkingPair.left } β β¨fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x), β―β©) x =
β(s.Ο.app { as := WalkingPair.left }) xs:Cone (pair G C)x:s.pt.carrierβ’ β((BinaryFan.mk pβ pβ).Ο.app { as := WalkingPair.right } β β¨fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x), β―β©)
x =
β(s.Ο.app { as := WalkingPair.right }) x s:Cone (pair G C)x:s.pt.carrierβ’ β((BinaryFan.mk pβ pβ).Ο.app { as := WalkingPair.left } β β¨fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x), β―β©) x =
β(s.Ο.app { as := WalkingPair.left }) xs:Cone (pair G C)x:s.pt.carrierβ’ β((BinaryFan.mk pβ pβ).Ο.app { as := WalkingPair.right } β β¨fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x), β―β©)
x =
β(s.Ο.app { as := WalkingPair.right }) x All goals completed! π
uniq s m hm := s:Cone (pair G C)m:s.pt βΆ (BinaryFan.mk pβ pβ).pthm:β (j : Discrete WalkingPair), (BinaryFan.mk pβ pβ).Ο.app j β m = s.Ο.app jβ’ m = β¨fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x), β―β©
s:Cone (pair G C)m:s.pt βΆ (BinaryFan.mk pβ pβ).pthm:β (j : Discrete WalkingPair), (BinaryFan.mk pβ pβ).Ο.app j β m = s.Ο.app jβ’ βm = ββ¨fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x), β―β©
s:Cone (pair G C)m:s.pt βΆ (BinaryFan.mk pβ pβ).pthm:β (j : Discrete WalkingPair), (BinaryFan.mk pβ pβ).Ο.app j β m = s.Ο.app jx:s.pt.carrierβ’ βm x = ββ¨fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x), β―β© x
s:Cone (pair G C)m:s.pt βΆ (BinaryFan.mk pβ pβ).pthm:β (j : Discrete WalkingPair), (BinaryFan.mk pβ pβ).Ο.app j β m = s.Ο.app jx:s.pt.carrierβ’ (βm x).1 = (ββ¨fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x), β―β© x).1s:Cone (pair G C)m:s.pt βΆ (BinaryFan.mk pβ pβ).pthm:β (j : Discrete WalkingPair), (BinaryFan.mk pβ pβ).Ο.app j β m = s.Ο.app jx:s.pt.carrierβ’ (βm x).2 = (ββ¨fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x), β―β© x).2
s:Cone (pair G C)m:s.pt βΆ (BinaryFan.mk pβ pβ).pthm:β (j : Discrete WalkingPair), (BinaryFan.mk pβ pβ).Ο.app j β m = s.Ο.app jx:s.pt.carrierβ’ (βm x).1 = (ββ¨fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x), β―β© x).1 All goals completed! π
s:Cone (pair G C)m:s.pt βΆ (BinaryFan.mk pβ pβ).pthm:β (j : Discrete WalkingPair), (BinaryFan.mk pβ pβ).Ο.app j β m = s.Ο.app jx:s.pt.carrierβ’ (βm x).2 = (ββ¨fun x β¦ (β(BinaryFan.fst s) x, β(BinaryFan.snd s) x), β―β© x).2 All goals completed! π
}