A Lean Companion to Conceptual Mathematics

Session 22: Universal mapping properties; Incidence relations🔗

4. Basic figure-types, singular figures, and incidence, in the category of graphs🔗

Exercise 1 (p. 250)

Consider the diagram of graphs B_1 \leftarrow P \rightarrow B_2 Suppose it satisfies the fragment of the definition of product in which we test against only the two figure-types {X = A} and {X = D}. Prove that the diagram actually is a product, i.e. that the product property holds for all graphs X.

Solution: Exercise 1

We begin by creating helpers for two key equivalences.

open IrreflexiveGraph in -- Establish equivalence between Hom(A, X) and arrows of X def homAEquiv (X : IrreflexiveGraph) : (A X) X.carrierA where toFun fAX := fAX.val.1 () invFun xA := (fun _ xA, (fun | 0 => X.toSrc xA | 1 => X.toTgt xA : Fin 2 X.carrierD)), X:IrreflexiveGraphxA:X.carrierA(fun x xA, fun x match x with | 0 => X.toSrc xA | 1 => X.toTgt xA).2 A.toSrc = X.toSrc (fun x xA, fun x match x with | 0 => X.toSrc xA | 1 => X.toTgt xA).1 (fun x xA, fun x match x with | 0 => X.toSrc xA | 1 => X.toTgt xA).2 A.toTgt = X.toTgt (fun x xA, fun x match x with | 0 => X.toSrc xA | 1 => X.toTgt xA).1 X:IrreflexiveGraphxA:X.carrierA(fun x xA, fun x match x with | 0 => X.toSrc xA | 1 => X.toTgt xA).2 A.toSrc = X.toSrc (fun x xA, fun x match x with | 0 => X.toSrc xA | 1 => X.toTgt xA).1X:IrreflexiveGraphxA:X.carrierA(fun x xA, fun x match x with | 0 => X.toSrc xA | 1 => X.toTgt xA).2 A.toTgt = X.toTgt (fun x xA, fun x match x with | 0 => X.toSrc xA | 1 => X.toTgt xA).1 X:IrreflexiveGraphxA:X.carrierA(fun x xA, fun x match x with | 0 => X.toSrc xA | 1 => X.toTgt xA).2 A.toSrc = X.toSrc (fun x xA, fun x match x with | 0 => X.toSrc xA | 1 => X.toTgt xA).1X:IrreflexiveGraphxA:X.carrierA(fun x xA, fun x match x with | 0 => X.toSrc xA | 1 => X.toTgt xA).2 A.toTgt = X.toTgt (fun x xA, fun x match x with | 0 => X.toSrc xA | 1 => X.toTgt xA).1 (X:IrreflexiveGraphxA:X.carrierAx✝:A.carrierA((fun x xA, fun x match x with | 0 => X.toSrc xA | 1 => X.toTgt xA).2 A.toTgt) x✝ = (X.toTgt (fun x xA, fun x match x with | 0 => X.toSrc xA | 1 => X.toTgt xA).1) x✝; All goals completed! 🐙) left_inv fAX := X:IrreflexiveGraphfAX:A X(fun xA (fun x xA, fun x match x with | 0 => X.toSrc xA | 1 => X.toTgt xA), ) ((fun fAX (↑fAX).1 ()) fAX) = fAX X:IrreflexiveGraphfAX:A X(↑((fun xA (fun x xA, fun x match x with | 0 => X.toSrc xA | 1 => X.toTgt xA), ) ((fun fAX (↑fAX).1 ()) fAX))).1 = (↑fAX).1X:IrreflexiveGraphfAX:A X(↑((fun xA (fun x xA, fun x match x with | 0 => X.toSrc xA | 1 => X.toTgt xA), ) ((fun fAX (↑fAX).1 ()) fAX))).2 = (↑fAX).2 X:IrreflexiveGraphfAX:A X(↑((fun xA (fun x xA, fun x match x with | 0 => X.toSrc xA | 1 => X.toTgt xA), ) ((fun fAX (↑fAX).1 ()) fAX))).1 = (↑fAX).1 X:IrreflexiveGraphfAX:A Xx✝:A.carrierA(↑((fun xA (fun x xA, fun x match x with | 0 => X.toSrc xA | 1 => X.toTgt xA), ) ((fun fAX (↑fAX).1 ()) fAX))).1 x✝ = (↑fAX).1 x✝; All goals completed! 🐙 X:IrreflexiveGraphfAX:A X(↑((fun xA (fun x xA, fun x match x with | 0 => X.toSrc xA | 1 => X.toTgt xA), ) ((fun fAX (↑fAX).1 ()) fAX))).2 = (↑fAX).2 X:IrreflexiveGraphfAX:A Xi:A.carrierD(↑((fun xA (fun x xA, fun x match x with | 0 => X.toSrc xA | 1 => X.toTgt xA), ) ((fun fAX (↑fAX).1 ()) fAX))).2 i = (↑fAX).2 i X:IrreflexiveGraphfAX:A Xi:Fin 2(↑((fun xA (fun x xA, fun x match x with | 0 => X.toSrc xA | 1 => X.toTgt xA), ) ((fun fAX (↑fAX).1 ()) fAX))).2 i = (↑fAX).2 i X:IrreflexiveGraphfAX:A X(↑((fun xA (fun x xA, fun x match x with | 0 => X.toSrc xA | 1 => X.toTgt xA), ) ((fun fAX (↑fAX).1 ()) fAX))).2 ((fun i i) 0, ) = (↑fAX).2 ((fun i i) 0, )X:IrreflexiveGraphfAX:A X(↑((fun xA (fun x xA, fun x match x with | 0 => X.toSrc xA | 1 => X.toTgt xA), ) ((fun fAX (↑fAX).1 ()) fAX))).2 ((fun i i) 1, ) = (↑fAX).2 ((fun i i) 1, ) X:IrreflexiveGraphfAX:A X(↑((fun xA (fun x xA, fun x match x with | 0 => X.toSrc xA | 1 => X.toTgt xA), ) ((fun fAX (↑fAX).1 ()) fAX))).2 ((fun i i) 0, ) = (↑fAX).2 ((fun i i) 0, ) All goals completed! 🐙 X:IrreflexiveGraphfAX:A X(↑((fun xA (fun x xA, fun x match x with | 0 => X.toSrc xA | 1 => X.toTgt xA), ) ((fun fAX (↑fAX).1 ()) fAX))).2 ((fun i i) 1, ) = (↑fAX).2 ((fun i i) 1, ) All goals completed! 🐙 right_inv xA := rfl open IrreflexiveGraph in -- Establish equivalence between Hom(D, X) and dots of X def homDEquiv (X : IrreflexiveGraph) : (D X) X.carrierD where toFun fDX := fDX.val.2 () invFun xD := (Empty.elim, fun _ xD), X:IrreflexiveGraphxD:X.carrierD(Empty.elim, fun x xD).2 D.toSrc = X.toSrc (Empty.elim, fun x xD).1 (Empty.elim, fun x xD).2 D.toTgt = X.toTgt (Empty.elim, fun x xD).1 X:IrreflexiveGraphxD:X.carrierD(Empty.elim, fun x xD).2 D.toSrc = X.toSrc (Empty.elim, fun x xD).1X:IrreflexiveGraphxD:X.carrierD(Empty.elim, fun x xD).2 D.toTgt = X.toTgt (Empty.elim, fun x xD).1 X:IrreflexiveGraphxD:X.carrierD(Empty.elim, fun x xD).2 D.toSrc = X.toSrc (Empty.elim, fun x xD).1X:IrreflexiveGraphxD:X.carrierD(Empty.elim, fun x xD).2 D.toTgt = X.toTgt (Empty.elim, fun x xD).1 (X:IrreflexiveGraphxD:X.carrierDe:D.carrierA((Empty.elim, fun x xD).2 D.toTgt) e = (X.toTgt (Empty.elim, fun x xD).1) e; All goals completed! 🐙) left_inv fDX := X:IrreflexiveGraphfDX:D X(fun xD (Empty.elim, fun x xD), ) ((fun fDX (↑fDX).2 ()) fDX) = fDX X:IrreflexiveGraphfDX:D X(↑((fun xD (Empty.elim, fun x xD), ) ((fun fDX (↑fDX).2 ()) fDX))).1 = (↑fDX).1X:IrreflexiveGraphfDX:D X(↑((fun xD (Empty.elim, fun x xD), ) ((fun fDX (↑fDX).2 ()) fDX))).2 = (↑fDX).2 X:IrreflexiveGraphfDX:D X(↑((fun xD (Empty.elim, fun x xD), ) ((fun fDX (↑fDX).2 ()) fDX))).1 = (↑fDX).1 X:IrreflexiveGraphfDX:D Xe:D.carrierA(↑((fun xD (Empty.elim, fun x xD), ) ((fun fDX (↑fDX).2 ()) fDX))).1 e = (↑fDX).1 e; All goals completed! 🐙 X:IrreflexiveGraphfDX:D X(↑((fun xD (Empty.elim, fun x xD), ) ((fun fDX (↑fDX).2 ()) fDX))).2 = (↑fDX).2 X:IrreflexiveGraphfDX:D Xx✝:D.carrierD(↑((fun xD (Empty.elim, fun x xD), ) ((fun fDX (↑fDX).2 ()) fDX))).2 x✝ = (↑fDX).2 x✝; All goals completed! 🐙 right_inv xD := rfl

Our proof then follows.

open IrreflexiveGraph in example (P B₁ B₂ : IrreflexiveGraph) (p₁ : P B₁) (p₂ : P B₂) -- Satisfies fragment of definition of product for X = A (hA : (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP : A P, p₁ fAP = fAP₁ p₂ fAP = fAP₂) -- Satisfies fragment of definition of product for X = D (hD : (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP : D P, p₁ fDP = fDP₁ p₂ fDP = fDP₂) : (X : IrreflexiveGraph) (f₁ : X B₁) (f₂ : X B₂), ∃! f : X P, p₁ f = f₁ p₂ f = f₂ := P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂ (X : IrreflexiveGraph) (f₁ : X B₁) (f₂ : X B₂), ∃! f, p₁ f = f₁ p₂ f = f₂ intro X P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁ (f₂ : X B₂), ∃! f, p₁ f = f₁ p₂ f = f₂ P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂∃! f, p₁ f = f₁ p₂ f = f₂ -- For each arrow in X, get equivalent morphism fAX : A ⟶ X P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xA∃! f, p₁ f = f₁ p₂ f = f₂ -- For each dot in X, get equivalent morphism fDX : D ⟶ X P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xD∃! f, p₁ f = f₁ p₂ f = f₂ -- Construct fA : X.carrierA ⟶ P.carrierA P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)∃! f, p₁ f = f₁ p₂ f = f₂ -- Construct fD : X.carrierD ⟶ P.carrierD (cf. fA) P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)∃! f, p₁ f = f₁ p₂ f = f₂ -- For each arrow in P, get morphism fAP : A ⟶ P P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pA∃! f, p₁ f = f₁ p₂ f = f₂ -- For each dot in P, get morphism fDP : D ⟶ P P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pD∃! f, p₁ f = f₁ p₂ f = f₂ -- Show that p₁ ⊚ fAP = f₁ ⊚ fAX ∧ p₂ ⊚ fAP = f₂ ⊚ fAX have hA_proj : xA : X.carrierA, p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xA := P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂ (X : IrreflexiveGraph) (f₁ : X B₁) (f₂ : X B₂), ∃! f, p₁ f = f₁ p₂ f = f₂ P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDxA:X.carrierAp₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xA P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDxA:X.carrierAp₁ (homAEquiv P).symm (fA xA) = f₁ (homAEquiv X).symm xA p₂ (homAEquiv P).symm (fA xA) = f₂ (homAEquiv X).symm xA P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDxA:X.carrierAp₁ Classical.choose = f₁ (homAEquiv X).symm xA p₂ Classical.choose = f₂ (homAEquiv X).symm xA All goals completed! 🐙 -- Show that p₁ ⊚ fDP = f₁ ⊚ fDX ∧ p₂ ⊚ fDP = f₂ ⊚ fDX have hD_proj : xD : X.carrierD, p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xD := P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂ (X : IrreflexiveGraph) (f₁ : X B₁) (f₂ : X B₂), ∃! f, p₁ f = f₁ p₂ f = f₂ P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAxD:X.carrierDp₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xD P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAxD:X.carrierDp₁ (homDEquiv P).symm (fD xD) = f₁ (homDEquiv X).symm xD p₂ (homDEquiv P).symm (fD xD) = f₂ (homDEquiv X).symm xD P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAxD:X.carrierDp₁ Classical.choose = f₁ (homDEquiv X).symm xD p₂ Classical.choose = f₂ (homDEquiv X).symm xD All goals completed! 🐙 -- Show that P.toSrc ⊚ fA = fD ⊚ X.toSrc have hSrc_comm : xA : X.carrierA, P.toSrc (fA xA) = fD (X.toSrc xA) := P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂ (X : IrreflexiveGraph) (f₁ : X B₁) (f₂ : X B₂), ∃! f, p₁ f = f₁ p₂ f = f₂ P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDxA:X.carrierAP.toSrc (fA xA) = fD (X.toSrc xA) -- Show that p₁ ⊚ fDP = f₁ ⊚ fDX have hp₁ : p₁ fDP (P.toSrc (fA xA)) = f₁ fDX (X.toSrc xA) := P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂ (X : IrreflexiveGraph) (f₁ : X B₁) (f₂ : X B₂), ∃! f, p₁ f = f₁ p₂ f = f₂ -- Transform goal from map equality to dot equality P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDxA:X.carrierA(homDEquiv B₁) (p₁ fDP (P.toSrc (fA xA))) = (homDEquiv B₁) (f₁ fDX (X.toSrc xA)) calc (p₁.val.2 P.toSrc) (fA xA) _ = (B₁.toSrc p₁.val.1) (fA xA) := P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDxA:X.carrierA((↑p₁).2 P.toSrc) (fA xA) = (B₁.toSrc (↑p₁).1) (fA xA) All goals completed! 🐙 _ = B₁.toSrc ((p₁ fAP (fA xA)).val.1 ()) := rfl _ = B₁.toSrc ((f₁ fAX xA).val.1 ()) := P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDxA:X.carrierAB₁.toSrc ((↑(p₁ fAP (fA xA))).1 ()) = B₁.toSrc ((↑(f₁ fAX xA)).1 ()) All goals completed! 🐙 _ = (B₁.toSrc f₁.val.1) xA := rfl _ = (f₁.val.2 X.toSrc) xA := P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDxA:X.carrierA(B₁.toSrc (↑f₁).1) xA = ((↑f₁).2 X.toSrc) xA All goals completed! 🐙 -- Show that p₂ ⊚ fDP = f₂ ⊚ fDX have hp₂ : p₂ fDP (P.toSrc (fA xA)) = f₂ fDX (X.toSrc xA) := P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂ (X : IrreflexiveGraph) (f₁ : X B₁) (f₂ : X B₂), ∃! f, p₁ f = f₁ p₂ f = f₂ -- Transform goal from map equality to dot equality P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDxA:X.carrierAhp₁:p₁ fDP (P.toSrc (fA xA)) = f₁ fDX (X.toSrc xA)(homDEquiv B₂) (p₂ fDP (P.toSrc (fA xA))) = (homDEquiv B₂) (f₂ fDX (X.toSrc xA)) calc (p₂.val.2 P.toSrc) (fA xA) _ = (B₂.toSrc p₂.val.1) (fA xA) := P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDxA:X.carrierAhp₁:p₁ fDP (P.toSrc (fA xA)) = f₁ fDX (X.toSrc xA)((↑p₂).2 P.toSrc) (fA xA) = (B₂.toSrc (↑p₂).1) (fA xA) All goals completed! 🐙 _ = B₂.toSrc ((p₂ fAP (fA xA)).val.1 ()) := rfl _ = B₂.toSrc ((f₂ fAX xA).val.1 ()) := P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDxA:X.carrierAhp₁:p₁ fDP (P.toSrc (fA xA)) = f₁ fDX (X.toSrc xA)B₂.toSrc ((↑(p₂ fAP (fA xA))).1 ()) = B₂.toSrc ((↑(f₂ fAX xA)).1 ()) All goals completed! 🐙 _ = (B₂.toSrc f₂.val.1) xA := rfl _ = (f₂.val.2 X.toSrc) xA := P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDxA:X.carrierAhp₁:p₁ fDP (P.toSrc (fA xA)) = f₁ fDX (X.toSrc xA)(B₂.toSrc (↑f₂).1) xA = ((↑f₂).2 X.toSrc) xA All goals completed! 🐙 -- Transform goal from dot equality to map equality P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDxA:X.carrierAhp₁:p₁ fDP (P.toSrc (fA xA)) = f₁ fDX (X.toSrc xA)hp₂:p₂ fDP (P.toSrc (fA xA)) = f₂ fDX (X.toSrc xA)(homDEquiv P).symm (P.toSrc (fA xA)) = (homDEquiv P).symm (fD (X.toSrc xA)) P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDxA:X.carrierAhp₁:p₁ fDP (P.toSrc (fA xA)) = f₁ fDX (X.toSrc xA)hp₂:p₂ fDP (P.toSrc (fA xA)) = f₂ fDX (X.toSrc xA)fDP (P.toSrc (fA xA)) = fDP (fD (X.toSrc xA)) -- Get unique witness for D ⟶ P P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDxA:X.carrierAhp₁:p₁ fDP (P.toSrc (fA xA)) = f₁ fDX (X.toSrc xA)hp₂:p₂ fDP (P.toSrc (fA xA)) = f₂ fDX (X.toSrc xA)h_uniq: (y : D P), (fun fDP p₁ fDP = f₁ fDX (X.toSrc xA) p₂ fDP = f₂ fDX (X.toSrc xA)) y y = Classical.choose fDP (P.toSrc (fA xA)) = fDP (fD (X.toSrc xA)) -- Show that lhs and rhs both equal unique witness P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDxA:X.carrierAhp₁:p₁ fDP (P.toSrc (fA xA)) = f₁ fDX (X.toSrc xA)hp₂:p₂ fDP (P.toSrc (fA xA)) = f₂ fDX (X.toSrc xA)h_uniq: (y : D P), (fun fDP p₁ fDP = f₁ fDX (X.toSrc xA) p₂ fDP = f₂ fDX (X.toSrc xA)) y y = Classical.choose h_left:fDP (P.toSrc (fA xA)) = Classical.choose fDP (P.toSrc (fA xA)) = fDP (fD (X.toSrc xA)) P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDxA:X.carrierAhp₁:p₁ fDP (P.toSrc (fA xA)) = f₁ fDX (X.toSrc xA)hp₂:p₂ fDP (P.toSrc (fA xA)) = f₂ fDX (X.toSrc xA)h_uniq: (y : D P), (fun fDP p₁ fDP = f₁ fDX (X.toSrc xA) p₂ fDP = f₂ fDX (X.toSrc xA)) y y = Classical.choose h_left:fDP (P.toSrc (fA xA)) = Classical.choose h_right:fDP (fD (X.toSrc xA)) = Classical.choose fDP (P.toSrc (fA xA)) = fDP (fD (X.toSrc xA)) All goals completed! 🐙 -- Show that P.toTgt ⊚ fA = fD ⊚ X.toTgt (cf. hSrc_comm) have hTgt_comm : xA : X.carrierA, P.toTgt (fA xA) = fD (X.toTgt xA) := P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂ (X : IrreflexiveGraph) (f₁ : X B₁) (f₂ : X B₂), ∃! f, p₁ f = f₁ p₂ f = f₂ P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)xA:X.carrierAP.toTgt (fA xA) = fD (X.toTgt xA) have hp₁ : p₁ fDP (P.toTgt (fA xA)) = f₁ fDX (X.toTgt xA) := P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂ (X : IrreflexiveGraph) (f₁ : X B₁) (f₂ : X B₂), ∃! f, p₁ f = f₁ p₂ f = f₂ P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)xA:X.carrierA(homDEquiv B₁) (p₁ fDP (P.toTgt (fA xA))) = (homDEquiv B₁) (f₁ fDX (X.toTgt xA)) calc (p₁.val.2 P.toTgt) (fA xA) _ = (B₁.toTgt p₁.val.1) (fA xA) := P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)xA:X.carrierA((↑p₁).2 P.toTgt) (fA xA) = (B₁.toTgt (↑p₁).1) (fA xA) All goals completed! 🐙 _ = B₁.toTgt ((p₁ fAP (fA xA)).val.1 ()) := rfl _ = B₁.toTgt ((f₁ fAX xA).val.1 ()) := P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)xA:X.carrierAB₁.toTgt ((↑(p₁ fAP (fA xA))).1 ()) = B₁.toTgt ((↑(f₁ fAX xA)).1 ()) All goals completed! 🐙 _ = (B₁.toTgt f₁.val.1) xA := rfl _ = (f₁.val.2 X.toTgt) xA := P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)xA:X.carrierA(B₁.toTgt (↑f₁).1) xA = ((↑f₁).2 X.toTgt) xA All goals completed! 🐙 have hp₂ : p₂ fDP (P.toTgt (fA xA)) = f₂ fDX (X.toTgt xA) := P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂ (X : IrreflexiveGraph) (f₁ : X B₁) (f₂ : X B₂), ∃! f, p₁ f = f₁ p₂ f = f₂ P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)xA:X.carrierAhp₁:p₁ fDP (P.toTgt (fA xA)) = f₁ fDX (X.toTgt xA)(homDEquiv B₂) (p₂ fDP (P.toTgt (fA xA))) = (homDEquiv B₂) (f₂ fDX (X.toTgt xA)) calc (p₂.val.2 P.toTgt) (fA xA) _ = (B₂.toTgt p₂.val.1) (fA xA) := P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)xA:X.carrierAhp₁:p₁ fDP (P.toTgt (fA xA)) = f₁ fDX (X.toTgt xA)((↑p₂).2 P.toTgt) (fA xA) = (B₂.toTgt (↑p₂).1) (fA xA) All goals completed! 🐙 _ = B₂.toTgt ((p₂ fAP (fA xA)).val.1 ()) := rfl _ = B₂.toTgt ((f₂ fAX xA).val.1 ()) := P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)xA:X.carrierAhp₁:p₁ fDP (P.toTgt (fA xA)) = f₁ fDX (X.toTgt xA)B₂.toTgt ((↑(p₂ fAP (fA xA))).1 ()) = B₂.toTgt ((↑(f₂ fAX xA)).1 ()) All goals completed! 🐙 _ = (B₂.toTgt f₂.val.1) xA := rfl _ = (f₂.val.2 X.toTgt) xA := P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)xA:X.carrierAhp₁:p₁ fDP (P.toTgt (fA xA)) = f₁ fDX (X.toTgt xA)(B₂.toTgt (↑f₂).1) xA = ((↑f₂).2 X.toTgt) xA All goals completed! 🐙 P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)xA:X.carrierAhp₁:p₁ fDP (P.toTgt (fA xA)) = f₁ fDX (X.toTgt xA)hp₂:p₂ fDP (P.toTgt (fA xA)) = f₂ fDX (X.toTgt xA)(homDEquiv P).symm (P.toTgt (fA xA)) = (homDEquiv P).symm (fD (X.toTgt xA)) P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)xA:X.carrierAhp₁:p₁ fDP (P.toTgt (fA xA)) = f₁ fDX (X.toTgt xA)hp₂:p₂ fDP (P.toTgt (fA xA)) = f₂ fDX (X.toTgt xA)fDP (P.toTgt (fA xA)) = fDP (fD (X.toTgt xA)) P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)xA:X.carrierAhp₁:p₁ fDP (P.toTgt (fA xA)) = f₁ fDX (X.toTgt xA)hp₂:p₂ fDP (P.toTgt (fA xA)) = f₂ fDX (X.toTgt xA)h_uniq: (y : D P), (fun fDP p₁ fDP = f₁ fDX (X.toTgt xA) p₂ fDP = f₂ fDX (X.toTgt xA)) y y = Classical.choose fDP (P.toTgt (fA xA)) = fDP (fD (X.toTgt xA)) P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)xA:X.carrierAhp₁:p₁ fDP (P.toTgt (fA xA)) = f₁ fDX (X.toTgt xA)hp₂:p₂ fDP (P.toTgt (fA xA)) = f₂ fDX (X.toTgt xA)h_uniq: (y : D P), (fun fDP p₁ fDP = f₁ fDX (X.toTgt xA) p₂ fDP = f₂ fDX (X.toTgt xA)) y y = Classical.choose h_left:fDP (P.toTgt (fA xA)) = Classical.choose fDP (P.toTgt (fA xA)) = fDP (fD (X.toTgt xA)) P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)xA:X.carrierAhp₁:p₁ fDP (P.toTgt (fA xA)) = f₁ fDX (X.toTgt xA)hp₂:p₂ fDP (P.toTgt (fA xA)) = f₂ fDX (X.toTgt xA)h_uniq: (y : D P), (fun fDP p₁ fDP = f₁ fDX (X.toTgt xA) p₂ fDP = f₂ fDX (X.toTgt xA)) y y = Classical.choose h_left:fDP (P.toTgt (fA xA)) = Classical.choose h_right:fDP (fD (X.toTgt xA)) = Classical.choose fDP (P.toTgt (fA xA)) = fDP (fD (X.toTgt xA)) All goals completed! 🐙 -- Bundle fA and fD into morphism f : X ⟶ P let f : X P := (fA, fD), P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)(fA, fD).2 X.toSrc = P.toSrc (fA, fD).1 (fA, fD).2 X.toTgt = P.toTgt (fA, fD).1 P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)(fA, fD).2 X.toSrc = P.toSrc (fA, fD).1P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)(fA, fD).2 X.toTgt = P.toTgt (fA, fD).1 P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)(fA, fD).2 X.toSrc = P.toSrc (fA, fD).1P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)(fA, fD).2 X.toTgt = P.toTgt (fA, fD).1 P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)x:X.carrierA((fA, fD).2 X.toTgt) x = (P.toTgt (fA, fD).1) x P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)x:X.carrierA((fA, fD).2 X.toSrc) x = (P.toSrc (fA, fD).1) x All goals completed! 🐙 P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)x:X.carrierA((fA, fD).2 X.toTgt) x = (P.toTgt (fA, fD).1) x All goals completed! 🐙 -- Show that f satisfies commutativity and uniqueness conditions P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), (fun f p₁ f = f₁ p₂ f = f₂) f (y : X P), (fun f p₁ f = f₁ p₂ f = f₂) y y = f P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), (fun f p₁ f = f₁ p₂ f = f₂) fP:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), (y : X P), (fun f p₁ f = f₁ p₂ f = f₂) y y = f P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), (fun f p₁ f = f₁ p₂ f = f₂) fP:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), (y : X P), (fun f p₁ f = f₁ p₂ f = f₂) y y = f P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), (y : X P), p₁ y = f₁ p₂ y = f₂ y = f -- Show that the triangles commute P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), p₁ f = f₁ p₂ f = f₂ P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), p₁ f = f₁P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), p₂ f = f₂ -- Show that p₁ ⊚ f = f₁ P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), p₁ f = f₁ P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), (↑(p₁ f)).1 = (↑f₁).1P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), (↑(p₁ f)).2 = (↑f₁).2 P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), (↑(p₁ f)).1 = (↑f₁).1 P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), xA:X.carrierA(↑(p₁ f)).1 xA = (↑f₁).1 xA P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), xA:X.carrierAh:p₁ fAP (fA xA) = f₁ fAX xA(↑(p₁ f)).1 xA = (↑f₁).1 xA P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), xA:X.carrierAh:(↑(p₁ fAP (fA xA))).1 () = (↑(f₁ fAX xA)).1 ()(↑(p₁ f)).1 xA = (↑f₁).1 xA All goals completed! 🐙 P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), (↑(p₁ f)).2 = (↑f₁).2 P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), xD:X.carrierD(↑(p₁ f)).2 xD = (↑f₁).2 xD P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), xD:X.carrierDh:p₁ fDP (fD xD) = f₁ fDX xD(↑(p₁ f)).2 xD = (↑f₁).2 xD P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), xD:X.carrierDh:(↑(p₁ fDP (fD xD))).2 () = (↑(f₁ fDX xD)).2 ()(↑(p₁ f)).2 xD = (↑f₁).2 xD All goals completed! 🐙 -- Show that p₂ ⊚ f = f₂ P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), p₂ f = f₂ P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), (↑(p₂ f)).1 = (↑f₂).1P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), (↑(p₂ f)).2 = (↑f₂).2 P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), (↑(p₂ f)).1 = (↑f₂).1 P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), xA:X.carrierA(↑(p₂ f)).1 xA = (↑f₂).1 xA P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), xA:X.carrierAh:p₂ fAP (fA xA) = f₂ fAX xA(↑(p₂ f)).1 xA = (↑f₂).1 xA P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), xA:X.carrierAh:(↑(p₂ fAP (fA xA))).1 () = (↑(f₂ fAX xA)).1 ()(↑(p₂ f)).1 xA = (↑f₂).1 xA All goals completed! 🐙 P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), (↑(p₂ f)).2 = (↑f₂).2 P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), xD:X.carrierD(↑(p₂ f)).2 xD = (↑f₂).2 xD P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), xD:X.carrierDh:p₂ fDP (fD xD) = f₂ fDX xD(↑(p₂ f)).2 xD = (↑f₂).2 xD P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), xD:X.carrierDh:(↑(p₂ fDP (fD xD))).2 () = (↑(f₂ fDX xD)).2 ()(↑(p₂ f)).2 xD = (↑f₂).2 xD All goals completed! 🐙 -- Prove uniqueness of f P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), (y : X P), p₁ y = f₁ p₂ y = f₂ y = f intro f' P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), f':X Phf'₁:p₁ f' = f₁hf'₂:p₂ f' = f₂f' = f P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), f':X Phf'₁:p₁ f' = f₁hf'₂:p₂ f' = f₂(↑f').1 = (↑f).1P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), f':X Phf'₁:p₁ f' = f₁hf'₂:p₂ f' = f₂(↑f').2 = (↑f).2 -- Show that arrow maps are equal P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), f':X Phf'₁:p₁ f' = f₁hf'₂:p₂ f' = f₂(↑f').1 = (↑f).1 P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), f':X Phf'₁:p₁ f' = f₁hf'₂:p₂ f' = f₂xA:X.carrierA(↑f').1 xA = (↑f).1 xA have hp₁ : p₁ fAP (f'.val.1 xA) = f₁ fAX xA := P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂ (X : IrreflexiveGraph) (f₁ : X B₁) (f₂ : X B₂), ∃! f, p₁ f = f₁ p₂ f = f₂ P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), f':X Phf'₁:p₁ f' = f₁hf'₂:p₂ f' = f₂xA:X.carrierA(homAEquiv B₁) (p₁ fAP ((↑f').1 xA)) = (homAEquiv B₁) (f₁ fAX xA) P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), f':X Phf'₂:p₂ f' = f₂xA:X.carrierAhf'₁:(↑(p₁ f')).1 xA = (↑f₁).1 xA(homAEquiv B₁) (p₁ fAP ((↑f').1 xA)) = (homAEquiv B₁) (f₁ fAX xA) All goals completed! 🐙 have hp₂ : p₂ fAP (f'.val.1 xA) = f₂ fAX xA := P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂ (X : IrreflexiveGraph) (f₁ : X B₁) (f₂ : X B₂), ∃! f, p₁ f = f₁ p₂ f = f₂ P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), f':X Phf'₁:p₁ f' = f₁hf'₂:p₂ f' = f₂xA:X.carrierAhp₁:p₁ fAP ((↑f').1 xA) = f₁ fAX xA(homAEquiv B₂) (p₂ fAP ((↑f').1 xA)) = (homAEquiv B₂) (f₂ fAX xA) P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), f':X Phf'₁:p₁ f' = f₁xA:X.carrierAhp₁:p₁ fAP ((↑f').1 xA) = f₁ fAX xAhf'₂:(↑(p₂ f')).1 xA = (↑f₂).1 xA(homAEquiv B₂) (p₂ fAP ((↑f').1 xA)) = (homAEquiv B₂) (f₂ fAX xA) All goals completed! 🐙 P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), f':X Phf'₁:p₁ f' = f₁hf'₂:p₂ f' = f₂xA:X.carrierAhp₁:p₁ fAP ((↑f').1 xA) = f₁ fAX xAhp₂:p₂ fAP ((↑f').1 xA) = f₂ fAX xA(homAEquiv P).symm ((↑f').1 xA) = (homAEquiv P).symm ((↑f).1 xA) P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), f':X Phf'₁:p₁ f' = f₁hf'₂:p₂ f' = f₂xA:X.carrierAhp₁:p₁ fAP ((↑f').1 xA) = f₁ fAX xAhp₂:p₂ fAP ((↑f').1 xA) = f₂ fAX xAfAP ((↑f').1 xA) = fAP (fA xA) P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), f':X Phf'₁:p₁ f' = f₁hf'₂:p₂ f' = f₂xA:X.carrierAhp₁:p₁ fAP ((↑f').1 xA) = f₁ fAX xAhp₂:p₂ fAP ((↑f').1 xA) = f₂ fAX xAh_uniq: (y : A P), (fun fAP p₁ fAP = f₁ fAX xA p₂ fAP = f₂ fAX xA) y y = Classical.choose fAP ((↑f').1 xA) = fAP (fA xA) P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), f':X Phf'₁:p₁ f' = f₁hf'₂:p₂ f' = f₂xA:X.carrierAhp₁:p₁ fAP ((↑f').1 xA) = f₁ fAX xAhp₂:p₂ fAP ((↑f').1 xA) = f₂ fAX xAh_uniq: (y : A P), (fun fAP p₁ fAP = f₁ fAX xA p₂ fAP = f₂ fAX xA) y y = Classical.choose h_left:fAP ((↑f').1 xA) = Classical.choose fAP ((↑f').1 xA) = fAP (fA xA) P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), f':X Phf'₁:p₁ f' = f₁hf'₂:p₂ f' = f₂xA:X.carrierAhp₁:p₁ fAP ((↑f').1 xA) = f₁ fAX xAhp₂:p₂ fAP ((↑f').1 xA) = f₂ fAX xAh_uniq: (y : A P), (fun fAP p₁ fAP = f₁ fAX xA p₂ fAP = f₂ fAX xA) y y = Classical.choose h_left:fAP ((↑f').1 xA) = Classical.choose h_right:fAP (fA xA) = Classical.choose fAP ((↑f').1 xA) = fAP (fA xA) All goals completed! 🐙 -- Show dot maps are equal P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), f':X Phf'₁:p₁ f' = f₁hf'₂:p₂ f' = f₂(↑f').2 = (↑f).2 P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), f':X Phf'₁:p₁ f' = f₁hf'₂:p₂ f' = f₂xD:X.carrierD(↑f').2 xD = (↑f).2 xD have hp₁ : p₁ fDP (f'.val.2 xD) = f₁ fDX xD := P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂ (X : IrreflexiveGraph) (f₁ : X B₁) (f₂ : X B₂), ∃! f, p₁ f = f₁ p₂ f = f₂ P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), f':X Phf'₁:p₁ f' = f₁hf'₂:p₂ f' = f₂xD:X.carrierD(homDEquiv B₁) (p₁ fDP ((↑f').2 xD)) = (homDEquiv B₁) (f₁ fDX xD) P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), f':X Phf'₂:p₂ f' = f₂xD:X.carrierDhf'₁:(↑(p₁ f')).2 xD = (↑f₁).2 xD(homDEquiv B₁) (p₁ fDP ((↑f').2 xD)) = (homDEquiv B₁) (f₁ fDX xD) All goals completed! 🐙 have hp₂ : p₂ fDP (f'.val.2 xD) = f₂ fDX xD := P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂ (X : IrreflexiveGraph) (f₁ : X B₁) (f₂ : X B₂), ∃! f, p₁ f = f₁ p₂ f = f₂ P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), f':X Phf'₁:p₁ f' = f₁hf'₂:p₂ f' = f₂xD:X.carrierDhp₁:p₁ fDP ((↑f').2 xD) = f₁ fDX xD(homDEquiv B₂) (p₂ fDP ((↑f').2 xD)) = (homDEquiv B₂) (f₂ fDX xD) P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), f':X Phf'₁:p₁ f' = f₁xD:X.carrierDhp₁:p₁ fDP ((↑f').2 xD) = f₁ fDX xDhf'₂:(↑(p₂ f')).2 xD = (↑f₂).2 xD(homDEquiv B₂) (p₂ fDP ((↑f').2 xD)) = (homDEquiv B₂) (f₂ fDX xD) All goals completed! 🐙 P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), f':X Phf'₁:p₁ f' = f₁hf'₂:p₂ f' = f₂xD:X.carrierDhp₁:p₁ fDP ((↑f').2 xD) = f₁ fDX xDhp₂:p₂ fDP ((↑f').2 xD) = f₂ fDX xD(homDEquiv P).symm ((↑f').2 xD) = (homDEquiv P).symm ((↑f).2 xD) P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), f':X Phf'₁:p₁ f' = f₁hf'₂:p₂ f' = f₂xD:X.carrierDhp₁:p₁ fDP ((↑f').2 xD) = f₁ fDX xDhp₂:p₂ fDP ((↑f').2 xD) = f₂ fDX xDfDP ((↑f').2 xD) = fDP (fD xD) P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), f':X Phf'₁:p₁ f' = f₁hf'₂:p₂ f' = f₂xD:X.carrierDhp₁:p₁ fDP ((↑f').2 xD) = f₁ fDX xDhp₂:p₂ fDP ((↑f').2 xD) = f₂ fDX xDh_uniq: (y : D P), (fun fDP p₁ fDP = f₁ fDX xD p₂ fDP = f₂ fDX xD) y y = Classical.choose fDP ((↑f').2 xD) = fDP (fD xD) P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), f':X Phf'₁:p₁ f' = f₁hf'₂:p₂ f' = f₂xD:X.carrierDhp₁:p₁ fDP ((↑f').2 xD) = f₁ fDX xDhp₂:p₂ fDP ((↑f').2 xD) = f₂ fDX xDh_uniq: (y : D P), (fun fDP p₁ fDP = f₁ fDX xD p₂ fDP = f₂ fDX xD) y y = Classical.choose h_left:fDP ((↑f').2 xD) = Classical.choose fDP ((↑f').2 xD) = fDP (fD xD) P:IrreflexiveGraphB₁:IrreflexiveGraphB₂:IrreflexiveGraphp₁:P B₁p₂:P B₂hA: (fAP₁ : A B₁) (fAP₂ : A B₂), ∃! fAP, p₁ fAP = fAP₁ p₂ fAP = fAP₂hD: (fDP₁ : D B₁) (fDP₂ : D B₂), ∃! fDP, p₁ fDP = fDP₁ p₂ fDP = fDP₂X:IrreflexiveGraphf₁:X B₁f₂:X B₂fAX:X.carrierA (A X) := fun xA (homAEquiv X).symm xAfDX:X.carrierD (D X) := fun xD (homDEquiv X).symm xDfA:X.carrierA P.carrierA := fun xA let h_uniq := ; (homAEquiv P) (Classical.choose h_uniq)fD:X.carrierD P.carrierD := fun xD let h_uniq := ; (homDEquiv P) (Classical.choose h_uniq)fAP:P.carrierA (A P) := fun pA (homAEquiv P).symm pAfDP:P.carrierD (D P) := fun pD (homDEquiv P).symm pDhA_proj: (xA : X.carrierA), p₁ fAP (fA xA) = f₁ fAX xA p₂ fAP (fA xA) = f₂ fAX xAhD_proj: (xD : X.carrierD), p₁ fDP (fD xD) = f₁ fDX xD p₂ fDP (fD xD) = f₂ fDX xDhSrc_comm: (xA : X.carrierA), P.toSrc (fA xA) = fD (X.toSrc xA)hTgt_comm: (xA : X.carrierA), P.toTgt (fA xA) = fD (X.toTgt xA)f:X P := (fA, fD), f':X Phf'₁:p₁ f' = f₁hf'₂:p₂ f' = f₂xD:X.carrierDhp₁:p₁ fDP ((↑f').2 xD) = f₁ fDX xDhp₂:p₂ fDP ((↑f').2 xD) = f₂ fDX xDh_uniq: (y : D P), (fun fDP p₁ fDP = f₁ fDX xD p₂ fDP = f₂ fDX xD) y y = Classical.choose h_left:fDP ((↑f').2 xD) = Classical.choose h_right:fDP (fD xD) = Classical.choose fDP ((↑f').2 xD) = fDP (fD xD) All goals completed! 🐙
Exercise 2 (p. 252)

What is a figure of shape

abbrev A₂ : IrreflexiveGraph := { carrierA := Fin 2 carrierD := Fin 3 toSrc := fun | 0 => 0 | 1 => 1 toTgt := fun | 0 => 1 | 1 => 2 }

in a graph X? What are the various ways in which it can be singular?

Solution: Exercise 2

A figure of shape A_2 in a graph X is a morphism {A_2 \xrightarrow{f} X} that maps the two arrows of A_2 to two arrows (not necessarily distinct) in X and the three dots of A_2 to three dots (not necessarily distinct) in X in such a way as to preserve sources and targets.

def FigA₂ (X : IrreflexiveGraph) := A₂ X

The figure is singular if the two arrows of A_2 are mapped to the same arrow in X or if any two of the three dots of A_2 are mapped to the same dot in X—that is, if the morphism f fails to be injective on either the arrows or the dots.

def FigA₂.IsSingular {X : IrreflexiveGraph} (f : FigA₂ X) : Prop := ¬(Function.Injective f.val.1 Function.Injective f.val.2)

Specifically, the figure is singular if any of the following conditions hold:

(1) the two arrows of A_2 are mapped to the same arrow in X

example {X : IrreflexiveGraph} (f : FigA₂ X) (h : f.val.1 0 = f.val.1 1) : f.IsSingular := X:IrreflexiveGraphf:FigA₂ Xh:(↑f).1 0 = (↑f).1 1f.IsSingular X:IrreflexiveGraphf:FigA₂ Xh:(↑f).1 0 = (↑f).1 1hA:Function.Injective (↑f).1right✝:Function.Injective (↑f).2False exact absurd (hA h) (X:IrreflexiveGraphf:FigA₂ Xh:(↑f).1 0 = (↑f).1 1hA:Function.Injective (↑f).1right✝:Function.Injective (↑f).2¬0 = 1 All goals completed! 🐙)

(2) the first and second dots of A_2 are mapped to the same dot in X

example {X : IrreflexiveGraph} (f : FigA₂ X) (h : f.val.2 0 = f.val.2 1) : f.IsSingular := X:IrreflexiveGraphf:FigA₂ Xh:(↑f).2 0 = (↑f).2 1f.IsSingular X:IrreflexiveGraphf:FigA₂ Xh:(↑f).2 0 = (↑f).2 1left✝:Function.Injective (↑f).1hD:Function.Injective (↑f).2False exact absurd (hD h) (X:IrreflexiveGraphf:FigA₂ Xh:(↑f).2 0 = (↑f).2 1left✝:Function.Injective (↑f).1hD:Function.Injective (↑f).2¬0 = 1 All goals completed! 🐙)

(3) the first and third dots of A_2 are mapped to the same dot in X

example {X : IrreflexiveGraph} (f : FigA₂ X) (h : f.val.2 0 = f.val.2 2) : f.IsSingular := X:IrreflexiveGraphf:FigA₂ Xh:(↑f).2 0 = (↑f).2 2f.IsSingular X:IrreflexiveGraphf:FigA₂ Xh:(↑f).2 0 = (↑f).2 2left✝:Function.Injective (↑f).1hD:Function.Injective (↑f).2False exact absurd (hD h) (X:IrreflexiveGraphf:FigA₂ Xh:(↑f).2 0 = (↑f).2 2left✝:Function.Injective (↑f).1hD:Function.Injective (↑f).2¬0 = 2 All goals completed! 🐙)

(4) the second and third dots of A_2 are mapped to the same dot in X

example {X : IrreflexiveGraph} (f : FigA₂ X) (h : f.val.2 1 = f.val.2 2) : f.IsSingular := X:IrreflexiveGraphf:FigA₂ Xh:(↑f).2 1 = (↑f).2 2f.IsSingular X:IrreflexiveGraphf:FigA₂ Xh:(↑f).2 1 = (↑f).2 2left✝:Function.Injective (↑f).1hD:Function.Injective (↑f).2False exact absurd (hD h) (X:IrreflexiveGraphf:FigA₂ Xh:(↑f).2 1 = (↑f).2 2left✝:Function.Injective (↑f).1hD:Function.Injective (↑f).2¬1 = 2 All goals completed! 🐙)

The case in which all three dots of A_2 are mapped to the same dot in X is covered by any of conditions (2), (3), or (4), since if all three dots are mapped to the same dot, then in particular any two dots are mapped to the same dot.