Built with Alectryon, running Coq+SerAPI v8.18.0+0.18.3. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use instead of Ctrl.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
(** * Induction and recursion principles for the triple join We show that the triple join satisfies symmetrical induction and recursion principles and prove that the recursion principle gives an equivalence of 0-groupoids. We use this in JoinAssoc.v to prove that the join is associative. Our approach parallels what is done in the two-variable case in Join/Core.v, especially starting with [TriJoinRecData] here and [JoinRecData] there. That case is much simpler, so should be read first. *) Section TriJoinStructure. Context {A B C : Type}. Definition TriJoin := Join A (Join B C). Definition join1 : A -> TriJoin := joinl. Definition join2 : B -> TriJoin := fun b => (joinr (joinl b)). Definition join3 : C -> TriJoin := fun c => (joinr (joinr c)). Definition join12 : forall a b, join1 a = join2 b := fun a b => jglue a (joinl b). Definition join13 : forall a c, join1 a = join3 c := fun a c => jglue a (joinr c). Definition join23 : forall b c, join2 b = join3 c := fun b c => ap joinr (jglue b c). Definition join123 : forall a b c, join12 a b @ join23 b c = join13 a c := fun a b c => triangle_v a (jglue b c). End TriJoinStructure. Arguments TriJoin A B C : clear implicits. (** ** [ap_trijoin] and [ap_trijoin_transport] *) (** Functions send triangles to triangles. *) Definition ap_triangle {X Y} (f : X -> Y) {a b c : X} {ab : a = b} {bc : b = c} {ac : a = c} (abc : ab @ bc = ac) : ap f ab @ ap f bc = ap f ac := (ap_pp f ab bc)^ @ ap (ap f) abc. (** This general result abstracts away the situation where [J] is [TriJoin A B C], [a] is [joinl a'] for some [a'], [jr] is [joinr : Join B C -> J], [jg] is [fun w => jglue a' w], and [p] is [jglue b c]. By working in this generality, we can do induction on [p]. This also allows us to inline the proof of [triangle_v]. *)
J, W, P: Type
f: J -> P
a: J
jr: W -> J
jg: forall w : W, a = jr w
b, c: W
p: b = c

ap f (jg b) @ ap f (ap jr p) = ap f (jg c)
J, W, P: Type
f: J -> P
a: J
jr: W -> J
jg: forall w : W, a = jr w
b, c: W
p: b = c

ap f (jg b) @ ap f (ap jr p) = ap f (jg c)
J, W, P: Type
f: J -> P
a: J
jr: W -> J
jg: forall w : W, a = jr w
b, c: W
p: b = c

jg b @ ap jr p = jg c
J, W, P: Type
f: J -> P
a: J
jr: W -> J
jg: forall w : W, a = jr w
b: W

jg b @ ap jr 1 = jg b
apply concat_p1. Defined. (** Functions send the canonical triangles in triple joins to triangles. *)
A, B, C, P: Type
f: TriJoin A B C -> P
a: A
b: B
c: C

ap f (join12 a b) @ ap f (join23 b c) = ap f (join13 a c)
A, B, C, P: Type
f: TriJoin A B C -> P
a: A
b: B
c: C

ap f (join12 a b) @ ap f (join23 b c) = ap f (join13 a c)
nrapply ap_trijoin_general. Defined.
J, W, P: Type
f: J -> P
a: J
jr: W -> J
jg: forall w : W, a = jr w
b, c: W
p: b = c

ap_trijoin_general f a jr jg p = ((1 @@ ap_compose jr f p)^ @ (transport_paths_Fr p (ap f (jg b)))^) @ apD (fun x : W => ap f (jg x)) p
J, W, P: Type
f: J -> P
a: J
jr: W -> J
jg: forall w : W, a = jr w
b, c: W
p: b = c

ap_trijoin_general f a jr jg p = ((1 @@ ap_compose jr f p)^ @ (transport_paths_Fr p (ap f (jg b)))^) @ apD (fun x : W => ap f (jg x)) p
J, W, P: Type
f: J -> P
a: J
jr: W -> J
jg: forall w : W, a = jr w
b: W

ap_trijoin_general f a jr jg 1 = ((1 @@ ap_compose jr f 1)^ @ (transport_paths_Fr 1 (ap f (jg b)))^) @ apD (fun x : W => ap f (jg x)) 1
J, W, P: Type
f: J -> P
a: J
jr: W -> J
jg: forall w : W, a = jr w
b: W

ap_triangle f (concat_p1 (jg b)) = (1 @ ((concat_p1 (ap f (jg b)))^)^) @ 1
J, W, P: Type
f: J -> P
a: J
jr: W -> J
jg: forall w : W, a = jr w
b: W

ap_triangle f (concat_p1 1) = (1 @ ((concat_p1 (ap f 1))^)^) @ 1
reflexivity. Defined.
A, B, C, P: Type
f: TriJoin A B C -> P
a: A
b: B
c: C

ap_trijoin f a b c = ((1 @@ ap_compose joinr f (jglue b c))^ @ (transport_paths_Fr (jglue b c) (ap f (jglue a (joinl b))))^) @ apD (fun x : Join B C => ap f (jglue a x)) (jglue b c)
A, B, C, P: Type
f: TriJoin A B C -> P
a: A
b: B
c: C

ap_trijoin f a b c = ((1 @@ ap_compose joinr f (jglue b c))^ @ (transport_paths_Fr (jglue b c) (ap f (jglue a (joinl b))))^) @ apD (fun x : Join B C => ap f (jglue a x)) (jglue b c)
nrapply ap_trijoin_general_transport. Defined.
J, W, P: Type
f: J -> P
a: J
jr: W -> J
jg: forall w : W, a = jr w
b, c: W
p: b = c

ap_trijoin_general f a jr jg p^ = (1 @@ (ap (ap f) (ap_V jr p) @ ap_V f (ap jr p))) @ moveR_pV (ap f (ap jr p)) (ap f (jg b)) (ap f (jg c)) (ap_trijoin_general f a jr jg p)^
J, W, P: Type
f: J -> P
a: J
jr: W -> J
jg: forall w : W, a = jr w
b, c: W
p: b = c

ap_trijoin_general f a jr jg p^ = (1 @@ (ap (ap f) (ap_V jr p) @ ap_V f (ap jr p))) @ moveR_pV (ap f (ap jr p)) (ap f (jg b)) (ap f (jg c)) (ap_trijoin_general f a jr jg p)^
J, W, P: Type
f: J -> P
a: J
jr: W -> J
jg: forall w : W, a = jr w
b: W

ap_trijoin_general f a jr jg 1^ = (1 @@ (ap (ap f) (ap_V jr 1) @ ap_V f (ap jr 1))) @ moveR_pV (ap f (ap jr 1)) (ap f (jg b)) (ap f (jg b)) (ap_trijoin_general f a jr jg 1)^
J, W, P: Type
f: J -> P
a: J
jr: W -> J
jg: forall w : W, a = jr w
b: W

ap_triangle f (concat_p1 (jg b)) = 1 @ ((concat_p1 (ap f (jg b)) @ (ap_triangle f (concat_p1 (jg b)))^) @ concat_p1 (ap f (jg b)))
by induction (jg b). Defined.
A, B, C, P: Type
f: TriJoin A B C -> P
a: A
b: B
c: C

ap_triangle f (triangle_v a (jglue b c)^) = (1 @@ (ap (ap f) (ap_V joinr (jglue b c)) @ ap_V f (ap joinr (jglue b c)))) @ moveR_pV (ap f (join23 b c)) (ap f (join12 a b)) (ap f (join13 a c)) (ap_trijoin f a b c)^
A, B, C, P: Type
f: TriJoin A B C -> P
a: A
b: B
c: C

ap_triangle f (triangle_v a (jglue b c)^) = (1 @@ (ap (ap f) (ap_V joinr (jglue b c)) @ ap_V f (ap joinr (jglue b c)))) @ moveR_pV (ap f (join23 b c)) (ap f (join12 a b)) (ap f (join13 a c)) (ap_trijoin f a b c)^
nrapply ap_trijoin_general_V. Defined. (** ** The induction principle for the triple join *) (** A lemma that handles the path algebra in the final step. *)
A, BC: Type
P: Join A BC -> Type
a: A
b, c: BC
bc: b = c
j1': P (joinl a)
j2': P (joinr b)
j3': P (joinr c)
j12': transport P (jglue a b) j1' = j2'
j13': transport P (jglue a c) j1' = j3'
j23': transport P (ap joinr bc) j2' = j3'
j123': (transport_pp P (jglue a b) (ap joinr bc) j1' @ ap (transport P (ap joinr bc)) j12') @ j23' = transport2 P (triangle_v a bc) j1' @ j13'

((apD (fun x : BC => transport P (jglue a x) j1') bc)^ @ ap (transport (fun x : BC => P (joinr x)) bc) j12') @ (transport_compose P joinr bc j2' @ j23') = j13'
A, BC: Type
P: Join A BC -> Type
a: A
b, c: BC
bc: b = c
j1': P (joinl a)
j2': P (joinr b)
j3': P (joinr c)
j12': transport P (jglue a b) j1' = j2'
j13': transport P (jglue a c) j1' = j3'
j23': transport P (ap joinr bc) j2' = j3'
j123': (transport_pp P (jglue a b) (ap joinr bc) j1' @ ap (transport P (ap joinr bc)) j12') @ j23' = transport2 P (triangle_v a bc) j1' @ j13'

((apD (fun x : BC => transport P (jglue a x) j1') bc)^ @ ap (transport (fun x : BC => P (joinr x)) bc) j12') @ (transport_compose P joinr bc j2' @ j23') = j13'
A, BC: Type
P: Join A BC -> Type
a: A
b: BC
j1': P (joinl a)
j2', j3': P (joinr b)
j12': transport P (jglue a b) j1' = j2'
j13': transport P (jglue a b) j1' = j3'
j23': transport P (ap joinr 1) j2' = j3'
j123': (transport_pp P (jglue a b) (ap joinr 1) j1' @ ap (transport P (ap joinr 1)) j12') @ j23' = transport2 P (triangle_v a 1) j1' @ j13'

(1 @ ap (transport (fun x : BC => P (joinr x)) 1) j12') @ (1 @ j23') = j13'
A, BC: Type
P: Join A BC -> Type
a: A
b: BC
j1': P (joinl a)
j2', j3': P (joinr b)
j12': transport P (jglue a b) j1' = j2'
j13': transport P (jglue a b) j1' = j3'
j23': transport P (ap joinr 1) j2' = j3'
j123': (transport2 P (concat_p1 (jglue a b)) j1' @ ap (transport P (ap joinr 1)) j12') @ j23' = transport2 P (triangle_v a 1) j1' @ j13'

(1 @ ap (transport (fun x : BC => P (joinr x)) 1) j12') @ (1 @ j23') = j13'
A, BC: Type
P: Join A BC -> Type
a: A
b: BC
j1': P (joinl a)
j2', j3': P (joinr b)
j12': transport P (jglue a b) j1' = j2'
j13': transport P (jglue a b) j1' = j3'
j23': j2' = j3'
j123': (transport2 P (concat_p1 (jglue a b)) j1' @ ap (transport P 1) j12') @ j23' = transport2 P (concat_p1 (jglue a b)) j1' @ j13'

(1 @ ap (transport (fun x : BC => P (joinr x)) 1) j12') @ (1 @ j23') = j13'
A, BC: Type
P: Join A BC -> Type
a: A
b: BC
j1': P (joinl a)
j2', j3': P (joinr b)
j12': transport P (jglue a b) j1' = j2'
j13': transport P (jglue a b) j1' = j3'
j23': j2' = j3'
j123': (transport2 P (concat_p1 (jglue a b)) j1' @ ap idmap j12') @ j23' = transport2 P (concat_p1 (jglue a b)) j1' @ j13'

(1 @ ap idmap j12') @ (1 @ j23') = j13'
A, BC: Type
P: Join A BC -> Type
a: A
b: BC
j1': P (joinl a)
j2', j3': P (joinr b)
j12': transport P (jglue a b) j1' = j2'
j13': transport P (jglue a b) j1' = j3'
j23': j2' = j3'
j123': (transport2 P (concat_p1 (jglue a b)) j1' @ j12') @ j23' = transport2 P (concat_p1 (jglue a b)) j1' @ j13'

(1 @ j12') @ (1 @ j23') = j13'
A, BC: Type
P: Join A BC -> Type
a: A
b: BC
j1': P (joinl a)
j2', j3': P (joinr b)
j12': transport P (jglue a b) j1' = j2'
j13': transport P (jglue a b) j1' = j3'
j23': j2' = j3'
j123': transport2 P (concat_p1 (jglue a b)) j1' @ (j12' @ j23') = transport2 P (concat_p1 (jglue a b)) j1' @ j13'

(1 @ j12') @ (1 @ j23') = j13'
A, BC: Type
P: Join A BC -> Type
a: A
b: BC
j1': P (joinl a)
j2', j3': P (joinr b)
j12': transport P (jglue a b) j1' = j2'
j13': transport P (jglue a b) j1' = j3'
j23': j2' = j3'
j123': j12' @ j23' = j13'

(1 @ j12') @ (1 @ j23') = j13'
A, BC: Type
P: Join A BC -> Type
a: A
b: BC
j1': P (joinl a)
j2', j3': P (joinr b)
j12': transport P (jglue a b) j1' = j2'
j13': transport P (jglue a b) j1' = j3'
j23': j2' = j3'
j123': j12' @ j23' = j13'

j12' @ j23' = j13'
exact j123'. Qed. (** An induction principle for the triple join. Note that the hypotheses are phrased completely in terms of the "constructors" of [TriJoin A B C]. *)
A, B, C: Type
P: TriJoin A B C -> Type
join1': forall a : A, P (join1 a)
join2': forall b : B, P (join2 b)
join3': forall c : C, P (join3 c)
join12': forall (a : A) (b : B), transport P (join12 a b) (join1' a) = join2' b
join13': forall (a : A) (c : C), transport P (join13 a c) (join1' a) = join3' c
join23': forall (b : B) (c : C), transport P (join23 b c) (join2' b) = join3' c
join123': forall (a : A) (b : B) (c : C), (transport_pp P (join12 a b) (join23 b c) (join1' a) @ ap (transport P (join23 b c)) (join12' a b)) @ join23' b c = transport2 P (join123 a b c) (join1' a) @ join13' a c

forall x : TriJoin A B C, P x
A, B, C: Type
P: TriJoin A B C -> Type
join1': forall a : A, P (join1 a)
join2': forall b : B, P (join2 b)
join3': forall c : C, P (join3 c)
join12': forall (a : A) (b : B), transport P (join12 a b) (join1' a) = join2' b
join13': forall (a : A) (c : C), transport P (join13 a c) (join1' a) = join3' c
join23': forall (b : B) (c : C), transport P (join23 b c) (join2' b) = join3' c
join123': forall (a : A) (b : B) (c : C), (transport_pp P (join12 a b) (join23 b c) (join1' a) @ ap (transport P (join23 b c)) (join12' a b)) @ join23' b c = transport2 P (join123 a b c) (join1' a) @ join13' a c

forall x : TriJoin A B C, P x
A, B, C: Type
P: TriJoin A B C -> Type
join1': forall a : A, P (join1 a)
join2': forall b : B, P (join2 b)
join3': forall c : C, P (join3 c)
join12': forall (a : A) (b : B), transport P (join12 a b) (join1' a) = join2' b
join13': forall (a : A) (c : C), transport P (join13 a c) (join1' a) = join3' c
join23': forall (b : B) (c : C), transport P (join23 b c) (join2' b) = join3' c
join123': forall (a : A) (b : B) (c : C), (transport_pp P (join12 a b) (join23 b c) (join1' a) @ ap (transport P (join23 b c)) (join12' a b)) @ join23' b c = transport2 P (join123 a b c) (join1' a) @ join13' a c

forall a : A, P (joinl a)
A, B, C: Type
P: TriJoin A B C -> Type
join1': forall a : A, P (join1 a)
join2': forall b : B, P (join2 b)
join3': forall c : C, P (join3 c)
join12': forall (a : A) (b : B), transport P (join12 a b) (join1' a) = join2' b
join13': forall (a : A) (c : C), transport P (join13 a c) (join1' a) = join3' c
join23': forall (b : B) (c : C), transport P (join23 b c) (join2' b) = join3' c
join123': forall (a : A) (b : B) (c : C), (transport_pp P (join12 a b) (join23 b c) (join1' a) @ ap (transport P (join23 b c)) (join12' a b)) @ join23' b c = transport2 P (join123 a b c) (join1' a) @ join13' a c
forall b : Join B C, P (joinr b)
A, B, C: Type
P: TriJoin A B C -> Type
join1': forall a : A, P (join1 a)
join2': forall b : B, P (join2 b)
join3': forall c : C, P (join3 c)
join12': forall (a : A) (b : B), transport P (join12 a b) (join1' a) = join2' b
join13': forall (a : A) (c : C), transport P (join13 a c) (join1' a) = join3' c
join23': forall (b : B) (c : C), transport P (join23 b c) (join2' b) = join3' c
join123': forall (a : A) (b : B) (c : C), (transport_pp P (join12 a b) (join23 b c) (join1' a) @ ap (transport P (join23 b c)) (join12' a b)) @ join23' b c = transport2 P (join123 a b c) (join1' a) @ join13' a c
forall (a : A) (b : Join B C), transport P (jglue a b) (?P_A a) = ?P_B b
A, B, C: Type
P: TriJoin A B C -> Type
join1': forall a : A, P (join1 a)
join2': forall b : B, P (join2 b)
join3': forall c : C, P (join3 c)
join12': forall (a : A) (b : B), transport P (join12 a b) (join1' a) = join2' b
join13': forall (a : A) (c : C), transport P (join13 a c) (join1' a) = join3' c
join23': forall (b : B) (c : C), transport P (join23 b c) (join2' b) = join3' c
join123': forall (a : A) (b : B) (c : C), (transport_pp P (join12 a b) (join23 b c) (join1' a) @ ap (transport P (join23 b c)) (join12' a b)) @ join23' b c = transport2 P (join123 a b c) (join1' a) @ join13' a c

forall a : A, P (joinl a)
exact join1'.
A, B, C: Type
P: TriJoin A B C -> Type
join1': forall a : A, P (join1 a)
join2': forall b : B, P (join2 b)
join3': forall c : C, P (join3 c)
join12': forall (a : A) (b : B), transport P (join12 a b) (join1' a) = join2' b
join13': forall (a : A) (c : C), transport P (join13 a c) (join1' a) = join3' c
join23': forall (b : B) (c : C), transport P (join23 b c) (join2' b) = join3' c
join123': forall (a : A) (b : B) (c : C), (transport_pp P (join12 a b) (join23 b c) (join1' a) @ ap (transport P (join23 b c)) (join12' a b)) @ join23' b c = transport2 P (join123 a b c) (join1' a) @ join13' a c

forall b : Join B C, P (joinr b)
A, B, C: Type
P: TriJoin A B C -> Type
join1': forall a : A, P (join1 a)
join2': forall b : B, P (join2 b)
join3': forall c : C, P (join3 c)
join12': forall (a : A) (b : B), transport P (join12 a b) (join1' a) = join2' b
join13': forall (a : A) (c : C), transport P (join13 a c) (join1' a) = join3' c
join23': forall (b : B) (c : C), transport P (join23 b c) (join2' b) = join3' c
join123': forall (a : A) (b : B) (c : C), (transport_pp P (join12 a b) (join23 b c) (join1' a) @ ap (transport P (join23 b c)) (join12' a b)) @ join23' b c = transport2 P (join123 a b c) (join1' a) @ join13' a c

forall a : B, (fun x : Join B C => P (joinr x)) (joinl a)
A, B, C: Type
P: TriJoin A B C -> Type
join1': forall a : A, P (join1 a)
join2': forall b : B, P (join2 b)
join3': forall c : C, P (join3 c)
join12': forall (a : A) (b : B), transport P (join12 a b) (join1' a) = join2' b
join13': forall (a : A) (c : C), transport P (join13 a c) (join1' a) = join3' c
join23': forall (b : B) (c : C), transport P (join23 b c) (join2' b) = join3' c
join123': forall (a : A) (b : B) (c : C), (transport_pp P (join12 a b) (join23 b c) (join1' a) @ ap (transport P (join23 b c)) (join12' a b)) @ join23' b c = transport2 P (join123 a b c) (join1' a) @ join13' a c
forall b : C, (fun x : Join B C => P (joinr x)) (joinr b)
A, B, C: Type
P: TriJoin A B C -> Type
join1': forall a : A, P (join1 a)
join2': forall b : B, P (join2 b)
join3': forall c : C, P (join3 c)
join12': forall (a : A) (b : B), transport P (join12 a b) (join1' a) = join2' b
join13': forall (a : A) (c : C), transport P (join13 a c) (join1' a) = join3' c
join23': forall (b : B) (c : C), transport P (join23 b c) (join2' b) = join3' c
join123': forall (a : A) (b : B) (c : C), (transport_pp P (join12 a b) (join23 b c) (join1' a) @ ap (transport P (join23 b c)) (join12' a b)) @ join23' b c = transport2 P (join123 a b c) (join1' a) @ join13' a c
forall (a : B) (b : C), transport (fun x : Join B C => P (joinr x)) (jglue a b) (?P_A a) = ?P_B b
A, B, C: Type
P: TriJoin A B C -> Type
join1': forall a : A, P (join1 a)
join2': forall b : B, P (join2 b)
join3': forall c : C, P (join3 c)
join12': forall (a : A) (b : B), transport P (join12 a b) (join1' a) = join2' b
join13': forall (a : A) (c : C), transport P (join13 a c) (join1' a) = join3' c
join23': forall (b : B) (c : C), transport P (join23 b c) (join2' b) = join3' c
join123': forall (a : A) (b : B) (c : C), (transport_pp P (join12 a b) (join23 b c) (join1' a) @ ap (transport P (join23 b c)) (join12' a b)) @ join23' b c = transport2 P (join123 a b c) (join1' a) @ join13' a c

forall a : B, (fun x : Join B C => P (joinr x)) (joinl a)
exact join2'.
A, B, C: Type
P: TriJoin A B C -> Type
join1': forall a : A, P (join1 a)
join2': forall b : B, P (join2 b)
join3': forall c : C, P (join3 c)
join12': forall (a : A) (b : B), transport P (join12 a b) (join1' a) = join2' b
join13': forall (a : A) (c : C), transport P (join13 a c) (join1' a) = join3' c
join23': forall (b : B) (c : C), transport P (join23 b c) (join2' b) = join3' c
join123': forall (a : A) (b : B) (c : C), (transport_pp P (join12 a b) (join23 b c) (join1' a) @ ap (transport P (join23 b c)) (join12' a b)) @ join23' b c = transport2 P (join123 a b c) (join1' a) @ join13' a c

forall b : C, (fun x : Join B C => P (joinr x)) (joinr b)
exact join3'.
A, B, C: Type
P: TriJoin A B C -> Type
join1': forall a : A, P (join1 a)
join2': forall b : B, P (join2 b)
join3': forall c : C, P (join3 c)
join12': forall (a : A) (b : B), transport P (join12 a b) (join1' a) = join2' b
join13': forall (a : A) (c : C), transport P (join13 a c) (join1' a) = join3' c
join23': forall (b : B) (c : C), transport P (join23 b c) (join2' b) = join3' c
join123': forall (a : A) (b : B) (c : C), (transport_pp P (join12 a b) (join23 b c) (join1' a) @ ap (transport P (join23 b c)) (join12' a b)) @ join23' b c = transport2 P (join123 a b c) (join1' a) @ join13' a c

forall (a : B) (b : C), transport (fun x : Join B C => P (joinr x)) (jglue a b) (join2' a) = join3' b
A, B, C: Type
P: TriJoin A B C -> Type
join1': forall a : A, P (join1 a)
join2': forall b : B, P (join2 b)
join3': forall c : C, P (join3 c)
join12': forall (a : A) (b : B), transport P (join12 a b) (join1' a) = join2' b
join13': forall (a : A) (c : C), transport P (join13 a c) (join1' a) = join3' c
join23': forall (b : B) (c : C), transport P (join23 b c) (join2' b) = join3' c
join123': forall (a : A) (b : B) (c : C), (transport_pp P (join12 a b) (join23 b c) (join1' a) @ ap (transport P (join23 b c)) (join12' a b)) @ join23' b c = transport2 P (join123 a b c) (join1' a) @ join13' a c
b: B
c: C

transport (fun x : Join B C => P (joinr x)) (jglue b c) (join2' b) = join3' c
A, B, C: Type
P: TriJoin A B C -> Type
join1': forall a : A, P (join1 a)
join2': forall b : B, P (join2 b)
join3': forall c : C, P (join3 c)
join12': forall (a : A) (b : B), transport P (join12 a b) (join1' a) = join2' b
join13': forall (a : A) (c : C), transport P (join13 a c) (join1' a) = join3' c
join23': forall (b : B) (c : C), transport P (join23 b c) (join2' b) = join3' c
join123': forall (a : A) (b : B) (c : C), (transport_pp P (join12 a b) (join23 b c) (join1' a) @ ap (transport P (join23 b c)) (join12' a b)) @ join23' b c = transport2 P (join123 a b c) (join1' a) @ join13' a c
b: B
c: C

transport P (ap joinr (jglue b c)) (join2' b) = join3' c
apply join23'.
A, B, C: Type
P: TriJoin A B C -> Type
join1': forall a : A, P (join1 a)
join2': forall b : B, P (join2 b)
join3': forall c : C, P (join3 c)
join12': forall (a : A) (b : B), transport P (join12 a b) (join1' a) = join2' b
join13': forall (a : A) (c : C), transport P (join13 a c) (join1' a) = join3' c
join23': forall (b : B) (c : C), transport P (join23 b c) (join2' b) = join3' c
join123': forall (a : A) (b : B) (c : C), (transport_pp P (join12 a b) (join23 b c) (join1' a) @ ap (transport P (join23 b c)) (join12' a b)) @ join23' b c = transport2 P (join123 a b c) (join1' a) @ join13' a c

forall (a : A) (b : Join B C), transport P (jglue a b) (join1' a) = Join_ind (fun x : Join B C => P (joinr x)) join2' join3' (fun (b0 : B) (c : C) => transport_compose P joinr (jglue b0 c) (join2' b0) @ join23' b0 c) b
A, B, C: Type
P: TriJoin A B C -> Type
join1': forall a : A, P (join1 a)
join2': forall b : B, P (join2 b)
join3': forall c : C, P (join3 c)
join12': forall (a : A) (b : B), transport P (join12 a b) (join1' a) = join2' b
join13': forall (a : A) (c : C), transport P (join13 a c) (join1' a) = join3' c
join23': forall (b : B) (c : C), transport P (join23 b c) (join2' b) = join3' c
join123': forall (a : A) (b : B) (c : C), (transport_pp P (join12 a b) (join23 b c) (join1' a) @ ap (transport P (join23 b c)) (join12' a b)) @ join23' b c = transport2 P (join123 a b c) (join1' a) @ join13' a c
a: A

forall b : Join B C, transport P (jglue a b) (join1' a) = Join_ind (fun x : Join B C => P (joinr x)) join2' join3' (fun (b0 : B) (c : C) => transport_compose P joinr (jglue b0 c) (join2' b0) @ join23' b0 c) b
A, B, C: Type
P: TriJoin A B C -> Type
join1': forall a : A, P (join1 a)
join2': forall b : B, P (join2 b)
join3': forall c : C, P (join3 c)
join12': forall (a : A) (b : B), transport P (join12 a b) (join1' a) = join2' b
join13': forall (a : A) (c : C), transport P (join13 a c) (join1' a) = join3' c
join23': forall (b : B) (c : C), transport P (join23 b c) (join2' b) = join3' c
join123': forall (a : A) (b : B) (c : C), (transport_pp P (join12 a b) (join23 b c) (join1' a) @ ap (transport P (join23 b c)) (join12' a b)) @ join23' b c = transport2 P (join123 a b c) (join1' a) @ join13' a c
a: A

forall a0 : B, (fun x : Join B C => transport P (jglue a x) (join1' a) = Join_ind (fun x0 : Join B C => P (joinr x0)) join2' join3' (fun (b : B) (c : C) => transport_compose P joinr (jglue b c) (join2' b) @ join23' b c) x) (joinl a0)
A, B, C: Type
P: TriJoin A B C -> Type
join1': forall a : A, P (join1 a)
join2': forall b : B, P (join2 b)
join3': forall c : C, P (join3 c)
join12': forall (a : A) (b : B), transport P (join12 a b) (join1' a) = join2' b
join13': forall (a : A) (c : C), transport P (join13 a c) (join1' a) = join3' c
join23': forall (b : B) (c : C), transport P (join23 b c) (join2' b) = join3' c
join123': forall (a : A) (b : B) (c : C), (transport_pp P (join12 a b) (join23 b c) (join1' a) @ ap (transport P (join23 b c)) (join12' a b)) @ join23' b c = transport2 P (join123 a b c) (join1' a) @ join13' a c
a: A
forall b : C, (fun x : Join B C => transport P (jglue a x) (join1' a) = Join_ind (fun x0 : Join B C => P (joinr x0)) join2' join3' (fun (b0 : B) (c : C) => transport_compose P joinr (jglue b0 c) (join2' b0) @ join23' b0 c) x) (joinr b)
A, B, C: Type
P: TriJoin A B C -> Type
join1': forall a : A, P (join1 a)
join2': forall b : B, P (join2 b)
join3': forall c : C, P (join3 c)
join12': forall (a : A) (b : B), transport P (join12 a b) (join1' a) = join2' b
join13': forall (a : A) (c : C), transport P (join13 a c) (join1' a) = join3' c
join23': forall (b : B) (c : C), transport P (join23 b c) (join2' b) = join3' c
join123': forall (a : A) (b : B) (c : C), (transport_pp P (join12 a b) (join23 b c) (join1' a) @ ap (transport P (join23 b c)) (join12' a b)) @ join23' b c = transport2 P (join123 a b c) (join1' a) @ join13' a c
a: A
forall (a0 : B) (b : C), transport (fun x : Join B C => transport P (jglue a x) (join1' a) = Join_ind (fun x0 : Join B C => P (joinr x0)) join2' join3' (fun (b0 : B) (c : C) => transport_compose P joinr (jglue b0 c) (join2' b0) @ join23' b0 c) x) (jglue a0 b) (?P_A a0) = ?P_B b
A, B, C: Type
P: TriJoin A B C -> Type
join1': forall a : A, P (join1 a)
join2': forall b : B, P (join2 b)
join3': forall c : C, P (join3 c)
join12': forall (a : A) (b : B), transport P (join12 a b) (join1' a) = join2' b
join13': forall (a : A) (c : C), transport P (join13 a c) (join1' a) = join3' c
join23': forall (b : B) (c : C), transport P (join23 b c) (join2' b) = join3' c
join123': forall (a : A) (b : B) (c : C), (transport_pp P (join12 a b) (join23 b c) (join1' a) @ ap (transport P (join23 b c)) (join12' a b)) @ join23' b c = transport2 P (join123 a b c) (join1' a) @ join13' a c
a: A

forall a0 : B, (fun x : Join B C => transport P (jglue a x) (join1' a) = Join_ind (fun x0 : Join B C => P (joinr x0)) join2' join3' (fun (b : B) (c : C) => transport_compose P joinr (jglue b c) (join2' b) @ join23' b c) x) (joinl a0)
A, B, C: Type
P: TriJoin A B C -> Type
join1': forall a : A, P (join1 a)
join2': forall b : B, P (join2 b)
join3': forall c : C, P (join3 c)
join12': forall (a : A) (b : B), transport P (join12 a b) (join1' a) = join2' b
join13': forall (a : A) (c : C), transport P (join13 a c) (join1' a) = join3' c
join23': forall (b : B) (c : C), transport P (join23 b c) (join2' b) = join3' c
join123': forall (a : A) (b : B) (c : C), (transport_pp P (join12 a b) (join23 b c) (join1' a) @ ap (transport P (join23 b c)) (join12' a b)) @ join23' b c = transport2 P (join123 a b c) (join1' a) @ join13' a c
a: A

forall a0 : B, transport P (jglue a (joinl a0)) (join1' a) = join2' a0
exact (join12' a).
A, B, C: Type
P: TriJoin A B C -> Type
join1': forall a : A, P (join1 a)
join2': forall b : B, P (join2 b)
join3': forall c : C, P (join3 c)
join12': forall (a : A) (b : B), transport P (join12 a b) (join1' a) = join2' b
join13': forall (a : A) (c : C), transport P (join13 a c) (join1' a) = join3' c
join23': forall (b : B) (c : C), transport P (join23 b c) (join2' b) = join3' c
join123': forall (a : A) (b : B) (c : C), (transport_pp P (join12 a b) (join23 b c) (join1' a) @ ap (transport P (join23 b c)) (join12' a b)) @ join23' b c = transport2 P (join123 a b c) (join1' a) @ join13' a c
a: A

forall b : C, (fun x : Join B C => transport P (jglue a x) (join1' a) = Join_ind (fun x0 : Join B C => P (joinr x0)) join2' join3' (fun (b0 : B) (c : C) => transport_compose P joinr (jglue b0 c) (join2' b0) @ join23' b0 c) x) (joinr b)
A, B, C: Type
P: TriJoin A B C -> Type
join1': forall a : A, P (join1 a)
join2': forall b : B, P (join2 b)
join3': forall c : C, P (join3 c)
join12': forall (a : A) (b : B), transport P (join12 a b) (join1' a) = join2' b
join13': forall (a : A) (c : C), transport P (join13 a c) (join1' a) = join3' c
join23': forall (b : B) (c : C), transport P (join23 b c) (join2' b) = join3' c
join123': forall (a : A) (b : B) (c : C), (transport_pp P (join12 a b) (join23 b c) (join1' a) @ ap (transport P (join23 b c)) (join12' a b)) @ join23' b c = transport2 P (join123 a b c) (join1' a) @ join13' a c
a: A

forall b : C, transport P (jglue a (joinr b)) (join1' a) = join3' b
exact (join13' a).
A, B, C: Type
P: TriJoin A B C -> Type
join1': forall a : A, P (join1 a)
join2': forall b : B, P (join2 b)
join3': forall c : C, P (join3 c)
join12': forall (a : A) (b : B), transport P (join12 a b) (join1' a) = join2' b
join13': forall (a : A) (c : C), transport P (join13 a c) (join1' a) = join3' c
join23': forall (b : B) (c : C), transport P (join23 b c) (join2' b) = join3' c
join123': forall (a : A) (b : B) (c : C), (transport_pp P (join12 a b) (join23 b c) (join1' a) @ ap (transport P (join23 b c)) (join12' a b)) @ join23' b c = transport2 P (join123 a b c) (join1' a) @ join13' a c
a: A

forall (a0 : B) (b : C), transport (fun x : Join B C => transport P (jglue a x) (join1' a) = Join_ind (fun x0 : Join B C => P (joinr x0)) join2' join3' (fun (b0 : B) (c : C) => transport_compose P joinr (jglue b0 c) (join2' b0) @ join23' b0 c) x) (jglue a0 b) ((join12' a : forall a1 : B, (fun x : Join B C => transport P (jglue a x) (join1' a) = Join_ind (fun x0 : Join B C => P (joinr x0)) join2' join3' (fun (b0 : B) (c : C) => transport_compose P joinr (jglue b0 c) (join2' b0) @ join23' b0 c) x) (joinl a1)) a0) = (join13' a : forall b0 : C, (fun x : Join B C => transport P (jglue a x) (join1' a) = Join_ind (fun x0 : Join B C => P (joinr x0)) join2' join3' (fun (b1 : B) (c : C) => transport_compose P joinr (jglue b1 c) (join2' b1) @ join23' b1 c) x) (joinr b0)) b
A, B, C: Type
P: TriJoin A B C -> Type
join1': forall a : A, P (join1 a)
join2': forall b : B, P (join2 b)
join3': forall c : C, P (join3 c)
join12': forall (a : A) (b : B), transport P (join12 a b) (join1' a) = join2' b
join13': forall (a : A) (c : C), transport P (join13 a c) (join1' a) = join3' c
join23': forall (b : B) (c : C), transport P (join23 b c) (join2' b) = join3' c
join123': forall (a : A) (b : B) (c : C), (transport_pp P (join12 a b) (join23 b c) (join1' a) @ ap (transport P (join23 b c)) (join12' a b)) @ join23' b c = transport2 P (join123 a b c) (join1' a) @ join13' a c
a: A
b: B
c: C

transport (fun x : Join B C => transport P (jglue a x) (join1' a) = Join_ind (fun x0 : Join B C => P (joinr x0)) join2' join3' (fun (b : B) (c : C) => transport_compose P joinr (jglue b c) (join2' b) @ join23' b c) x) (jglue b c) (join12' a b) = join13' a c
A, B, C: Type
P: TriJoin A B C -> Type
join1': forall a : A, P (join1 a)
join2': forall b : B, P (join2 b)
join3': forall c : C, P (join3 c)
join12': forall (a : A) (b : B), transport P (join12 a b) (join1' a) = join2' b
join13': forall (a : A) (c : C), transport P (join13 a c) (join1' a) = join3' c
join23': forall (b : B) (c : C), transport P (join23 b c) (join2' b) = join3' c
join123': forall (a : A) (b : B) (c : C), (transport_pp P (join12 a b) (join23 b c) (join1' a) @ ap (transport P (join23 b c)) (join12' a b)) @ join23' b c = transport2 P (join123 a b c) (join1' a) @ join13' a c
a: A
b: B
c: C

((apD (fun x : Join B C => transport P (jglue a x) (join1' a)) (jglue b c))^ @ ap (transport (fun x : Join B C => P (joinr x)) (jglue b c)) (join12' a b)) @ apD (Join_ind (fun x : Join B C => P (joinr x)) join2' join3' (fun (b : B) (c : C) => transport_compose P joinr (jglue b c) (join2' b) @ join23' b c)) (jglue b c) = join13' a c
A, B, C: Type
P: TriJoin A B C -> Type
join1': forall a : A, P (join1 a)
join2': forall b : B, P (join2 b)
join3': forall c : C, P (join3 c)
join12': forall (a : A) (b : B), transport P (join12 a b) (join1' a) = join2' b
join13': forall (a : A) (c : C), transport P (join13 a c) (join1' a) = join3' c
join23': forall (b : B) (c : C), transport P (join23 b c) (join2' b) = join3' c
join123': forall (a : A) (b : B) (c : C), (transport_pp P (join12 a b) (join23 b c) (join1' a) @ ap (transport P (join23 b c)) (join12' a b)) @ join23' b c = transport2 P (join123 a b c) (join1' a) @ join13' a c
a: A
b: B
c: C

apD (Join_ind (fun x : Join B C => P (joinr x)) join2' join3' (fun (b : B) (c : C) => transport_compose P joinr (jglue b c) (join2' b) @ join23' b c)) (jglue b c) = ?Goal
A, B, C: Type
P: TriJoin A B C -> Type
join1': forall a : A, P (join1 a)
join2': forall b : B, P (join2 b)
join3': forall c : C, P (join3 c)
join12': forall (a : A) (b : B), transport P (join12 a b) (join1' a) = join2' b
join13': forall (a : A) (c : C), transport P (join13 a c) (join1' a) = join3' c
join23': forall (b : B) (c : C), transport P (join23 b c) (join2' b) = join3' c
join123': forall (a : A) (b : B) (c : C), (transport_pp P (join12 a b) (join23 b c) (join1' a) @ ap (transport P (join23 b c)) (join12' a b)) @ join23' b c = transport2 P (join123 a b c) (join1' a) @ join13' a c
a: A
b: B
c: C
((apD (fun x : Join B C => transport P (jglue a x) (join1' a)) (jglue b c))^ @ ap (transport (fun x : Join B C => P (joinr x)) (jglue b c)) (join12' a b)) @ ?Goal = join13' a c
A, B, C: Type
P: TriJoin A B C -> Type
join1': forall a : A, P (join1 a)
join2': forall b : B, P (join2 b)
join3': forall c : C, P (join3 c)
join12': forall (a : A) (b : B), transport P (join12 a b) (join1' a) = join2' b
join13': forall (a : A) (c : C), transport P (join13 a c) (join1' a) = join3' c
join23': forall (b : B) (c : C), transport P (join23 b c) (join2' b) = join3' c
join123': forall (a : A) (b : B) (c : C), (transport_pp P (join12 a b) (join23 b c) (join1' a) @ ap (transport P (join23 b c)) (join12' a b)) @ join23' b c = transport2 P (join123 a b c) (join1' a) @ join13' a c
a: A
b: B
c: C

((apD (fun x : Join B C => transport P (jglue a x) (join1' a)) (jglue b c))^ @ ap (transport (fun x : Join B C => P (joinr x)) (jglue b c)) (join12' a b)) @ (transport_compose P joinr (jglue b c) (join2' b) @ join23' b c) = join13' a c
apply trijoin_ind_helper, join123'. Defined. (** ** The recursion principle for the triple join, and many results about it *) (** We'll bundle up the arguments into a record. *) Record TriJoinRecData {A B C P : Type} := { j1 : A -> P; j2 : B -> P; j3 : C -> P; j12 : forall a b, j1 a = j2 b; j13 : forall a c, j1 a = j3 c; j23 : forall b c, j2 b = j3 c; j123 : forall a b c, j12 a b @ j23 b c = j13 a c; }. Arguments TriJoinRecData : clear implicits. Arguments Build_TriJoinRecData {A B C P}%type_scope (j1 j2 j3 j12 j13 j23 j123)%function_scope.
A, B, C, P: Type
f: TriJoinRecData A B C P

TriJoin A B C $-> P
A, B, C, P: Type
f: TriJoinRecData A B C P

TriJoin A B C $-> P
A, B, C, P: Type
f: TriJoinRecData A B C P

A -> P
A, B, C, P: Type
f: TriJoinRecData A B C P
Join B C -> P
A, B, C, P: Type
f: TriJoinRecData A B C P
forall (a : A) (b : Join B C), ?P_A a = ?P_B b
A, B, C, P: Type
f: TriJoinRecData A B C P

A -> P
exact (j1 f).
A, B, C, P: Type
f: TriJoinRecData A B C P

Join B C -> P
A, B, C, P: Type
f: TriJoinRecData A B C P

B -> P
A, B, C, P: Type
f: TriJoinRecData A B C P
C -> P
A, B, C, P: Type
f: TriJoinRecData A B C P
forall (a : B) (b : C), ?P_A a = ?P_B b
A, B, C, P: Type
f: TriJoinRecData A B C P

B -> P
exact (j2 f).
A, B, C, P: Type
f: TriJoinRecData A B C P

C -> P
exact (j3 f).
A, B, C, P: Type
f: TriJoinRecData A B C P

forall (a : B) (b : C), j2 f a = j3 f b
exact (j23 f).
A, B, C, P: Type
f: TriJoinRecData A B C P

forall (a : A) (b : Join B C), j1 f a = Join_rec (j2 f) (j3 f) (j23 f) b
A, B, C, P: Type
f: TriJoinRecData A B C P
a: A

forall b : Join B C, j1 f a = Join_rec (j2 f) (j3 f) (j23 f) b
A, B, C, P: Type
f: TriJoinRecData A B C P
a: A

forall a0 : B, j1 f a = Join_rec (j2 f) (j3 f) (j23 f) (joinl a0)
A, B, C, P: Type
f: TriJoinRecData A B C P
a: A
forall b : C, j1 f a = Join_rec (j2 f) (j3 f) (j23 f) (joinr b)
A, B, C, P: Type
f: TriJoinRecData A B C P
a: A
forall (a0 : B) (b : C), transport (fun x : Join B C => j1 f a = Join_rec (j2 f) (j3 f) (j23 f) x) (jglue a0 b) (?Goal a0) = ?Goal0 b
A, B, C, P: Type
f: TriJoinRecData A B C P
a: A

forall a0 : B, j1 f a = Join_rec (j2 f) (j3 f) (j23 f) (joinl a0)
exact (j12 f a).
A, B, C, P: Type
f: TriJoinRecData A B C P
a: A

forall b : C, j1 f a = Join_rec (j2 f) (j3 f) (j23 f) (joinr b)
exact (j13 f a).
A, B, C, P: Type
f: TriJoinRecData A B C P
a: A

forall (a0 : B) (b : C), transport (fun x : Join B C => j1 f a = Join_rec (j2 f) (j3 f) (j23 f) x) (jglue a0 b) (j12 f a a0) = j13 f a b
A, B, C, P: Type
f: TriJoinRecData A B C P
a: A
b: B
c: C

transport (fun x : Join B C => j1 f a = Join_rec (j2 f) (j3 f) (j23 f) x) (jglue b c) (j12 f a b) = j13 f a c
A, B, C, P: Type
f: TriJoinRecData A B C P
a: A
b: B
c: C

j12 f a b @ ap (Join_rec (j2 f) (j3 f) (j23 f)) (jglue b c) = j13 f a c
exact (1 @@ Join_rec_beta_jglue _ _ _ _ _ @ j123 f a b c). Defined. (** Beta rules for the recursion principle. *) Definition trijoin_rec_beta_join12 {A B C P : Type} (f : TriJoinRecData A B C P) (a : A) (b : B) : ap (trijoin_rec f) (join12 a b) = j12 f a b := Join_rec_beta_jglue _ _ _ _ _. Definition trijoin_rec_beta_join13 {A B C P : Type} (f : TriJoinRecData A B C P) (a : A) (c : C) : ap (trijoin_rec f) (join13 a c) = j13 f a c := Join_rec_beta_jglue _ _ _ _ _.
A, B, C, P: Type
f: TriJoinRecData A B C P
b: B
c: C

ap (trijoin_rec f) (join23 b c) = j23 f b c
A, B, C, P: Type
f: TriJoinRecData A B C P
b: B
c: C

ap (trijoin_rec f) (join23 b c) = j23 f b c
A, B, C, P: Type
f: TriJoinRecData A B C P
b: B
c: C

ap (Join_rec (j1 f) (Join_rec (j2 f) (j3 f) (j23 f)) (fun a : A => Join_ind (fun x : Join B C => j1 f a = Join_rec (j2 f) (j3 f) (j23 f) x) (j12 f a) (j13 f a) (fun (b : B) (c : C) => transport_paths_Fr (jglue b c) (j12 f a b) @ ((1 @@ Join_rec_beta_jglue (j2 f) (j3 f) (j23 f) b c) @ j123 f a b c)))) (ap joinr (jglue b c)) = j23 f b c
A, B, C, P: Type
f: TriJoinRecData A B C P
b: B
c: C

ap (fun x : Join B C => Join_rec (j2 f) (j3 f) (j23 f) x) (jglue b c) = j23 f b c
apply Join_rec_beta_jglue. Defined.
A: Type
x, y, z: A
u0, u1: x = y
p0, p1, r1: y = z
q0, s1, t1: x = z
p: p0 = p1
q: q0 = u0 @ p0
r: p0 = r1
s: u1 @ r1 = s1
t: s1 = t1
u: u0 = u1

((1 @@ p)^ @ q^) @ (((q @ (u @@ 1)) @ ((1 @@ r) @ s)) @ t) = ((u @@ (p^ @ r)) @ s) @ t
A: Type
x, y, z: A
u0, u1: x = y
p0, p1, r1: y = z
q0, s1, t1: x = z
p: p0 = p1
q: q0 = u0 @ p0
r: p0 = r1
s: u1 @ r1 = s1
t: s1 = t1
u: u0 = u1

((1 @@ p)^ @ q^) @ (((q @ (u @@ 1)) @ ((1 @@ r) @ s)) @ t) = ((u @@ (p^ @ r)) @ s) @ t
A: Type
x, y, z: A
u0: x = y
p0: y = z
q0: x = z
q: q0 = u0 @ p0

((1 @@ 1)^ @ q^) @ (((q @ (1 @@ 1)) @ ((1 @@ 1) @ 1)) @ 1) = ((1 @@ (1^ @ 1)) @ 1) @ 1
revert q0 q; by apply paths_ind_r. Defined.
A, B, C, P: Type
f: TriJoinRecData A B C P
a: A
b: B
c: C

ap_trijoin (trijoin_rec f) a b c = ((trijoin_rec_beta_join12 f a b @@ trijoin_rec_beta_join23 f b c) @ j123 f a b c) @ (trijoin_rec_beta_join13 f a c)^
A, B, C, P: Type
f: TriJoinRecData A B C P
a: A
b: B
c: C

ap_trijoin (trijoin_rec f) a b c = ((trijoin_rec_beta_join12 f a b @@ trijoin_rec_beta_join23 f b c) @ j123 f a b c) @ (trijoin_rec_beta_join13 f a c)^
(* Expand the LHS: *)
A, B, C, P: Type
f: TriJoinRecData A B C P
a: A
b: B
c: C

((1 @@ ap_compose joinr (trijoin_rec f) (jglue b c))^ @ (transport_paths_Fr (jglue b c) (ap (trijoin_rec f) (jglue a (joinl b))))^) @ apD (fun x : Join B C => ap (trijoin_rec f) (jglue a x)) (jglue b c) = ((trijoin_rec_beta_join12 f a b @@ trijoin_rec_beta_join23 f b c) @ j123 f a b c) @ (trijoin_rec_beta_join13 f a c)^
A, B, C, P: Type
f: TriJoinRecData A B C P
a: A
b: B
c: C

((1 @@ ap_compose joinr (trijoin_rec f) (jglue b c))^ @ (transport_paths_Fr (jglue b c) (ap (trijoin_rec f) (jglue a (joinl b))))^) @ ((ap (transport (fun b : Join B C => Join_rec (j1 f) (Join_rec (j2 f) (j3 f) (j23 f)) (fun a : A => Join_ind (fun x : Join B C => j1 f a = Join_rec (j2 f) (j3 f) (j23 f) x) (j12 f a) (j13 f a) (fun (b0 : B) (c : C) => transport_paths_Fr (jglue b0 c) (j12 f a b0) @ ((1 @@ Join_rec_beta_jglue (j2 f) (j3 f) (j23 f) b0 c) @ j123 f a b0 c))) (joinl a) = Join_rec (j1 f) (Join_rec (j2 f) (j3 f) (j23 f)) (fun a : A => Join_ind (fun x : Join B C => j1 f a = Join_rec (j2 f) (j3 f) (j23 f) x) (j12 f a) (j13 f a) (fun (b0 : B) (c : C) => transport_paths_Fr (jglue b0 c) (j12 f a b0) @ ((1 @@ Join_rec_beta_jglue (j2 f) (j3 f) (j23 f) b0 c) @ j123 f a b0 c))) (joinr b)) (jglue b c)) (Join_rec_beta_jglue (j1 f) (Join_rec (j2 f) (j3 f) (j23 f)) (fun a : A => Join_ind (fun x : Join B C => j1 f a = Join_rec (j2 f) (j3 f) (j23 f) x) (j12 f a) (j13 f a) (fun (b : B) (c : C) => transport_paths_Fr (jglue b c) (j12 f a b) @ ((1 @@ Join_rec_beta_jglue (j2 f) (j3 f) (j23 f) b c) @ j123 f a b c))) a (joinl b)) @ apD (Join_ind (fun x : Join B C => j1 f a = Join_rec (j2 f) (j3 f) (j23 f) x) (j12 f a) (j13 f a) (fun (b : B) (c : C) => transport_paths_Fr (jglue b c) (j12 f a b) @ ((1 @@ Join_rec_beta_jglue (j2 f) (j3 f) (j23 f) b c) @ j123 f a b c))) (jglue b c)) @ (Join_rec_beta_jglue (j1 f) (Join_rec (j2 f) (j3 f) (j23 f)) (fun a : A => Join_ind (fun x : Join B C => j1 f a = Join_rec (j2 f) (j3 f) (j23 f) x) (j12 f a) (j13 f a) (fun (b : B) (c : C) => transport_paths_Fr (jglue b c) (j12 f a b) @ ((1 @@ Join_rec_beta_jglue (j2 f) (j3 f) (j23 f) b c) @ j123 f a b c))) a (joinr c))^) = ((trijoin_rec_beta_join12 f a b @@ trijoin_rec_beta_join23 f b c) @ j123 f a b c) @ (trijoin_rec_beta_join13 f a c)^
A, B, C, P: Type
f: TriJoinRecData A B C P
a: A
b: B
c: C

((1 @@ ap_compose joinr (trijoin_rec f) (jglue b c))^ @ (transport_paths_Fr (jglue b c) (ap (trijoin_rec f) (jglue a (joinl b))))^) @ ((ap (transport (fun b : Join B C => Join_rec (j1 f) (Join_rec (j2 f) (j3 f) (j23 f)) (fun a : A => Join_ind (fun x : Join B C => j1 f a = Join_rec (j2 f) (j3 f) (j23 f) x) (j12 f a) (j13 f a) (fun (b0 : B) (c : C) => transport_paths_Fr (jglue b0 c) (j12 f a b0) @ ((1 @@ Join_rec_beta_jglue (j2 f) (j3 f) (j23 f) b0 c) @ j123 f a b0 c))) (joinl a) = Join_rec (j1 f) (Join_rec (j2 f) (j3 f) (j23 f)) (fun a : A => Join_ind (fun x : Join B C => j1 f a = Join_rec (j2 f) (j3 f) (j23 f) x) (j12 f a) (j13 f a) (fun (b0 : B) (c : C) => transport_paths_Fr (jglue b0 c) (j12 f a b0) @ ((1 @@ Join_rec_beta_jglue (j2 f) (j3 f) (j23 f) b0 c) @ j123 f a b0 c))) (joinr b)) (jglue b c)) (Join_rec_beta_jglue (j1 f) (Join_rec (j2 f) (j3 f) (j23 f)) (fun a : A => Join_ind (fun x : Join B C => j1 f a = Join_rec (j2 f) (j3 f) (j23 f) x) (j12 f a) (j13 f a) (fun (b : B) (c : C) => transport_paths_Fr (jglue b c) (j12 f a b) @ ((1 @@ Join_rec_beta_jglue (j2 f) (j3 f) (j23 f) b c) @ j123 f a b c))) a (joinl b)) @ (transport_paths_Fr (jglue b c) (j12 f a b) @ ((1 @@ Join_rec_beta_jglue (j2 f) (j3 f) (j23 f) b c) @ j123 f a b c))) @ (Join_rec_beta_jglue (j1 f) (Join_rec (j2 f) (j3 f) (j23 f)) (fun a : A => Join_ind (fun x : Join B C => j1 f a = Join_rec (j2 f) (j3 f) (j23 f) x) (j12 f a) (j13 f a) (fun (b : B) (c : C) => transport_paths_Fr (jglue b c) (j12 f a b) @ ((1 @@ Join_rec_beta_jglue (j2 f) (j3 f) (j23 f) b c) @ j123 f a b c))) a (joinr c))^) = ((trijoin_rec_beta_join12 f a b @@ trijoin_rec_beta_join23 f b c) @ j123 f a b c) @ (trijoin_rec_beta_join13 f a c)^
(* Change [ap (transport __) _] on LHS. *)
A, B, C, P: Type
f: TriJoinRecData A B C P
a: A
b: B
c: C

((1 @@ ap_compose joinr (trijoin_rec f) (jglue b c))^ @ (transport_paths_Fr (jglue b c) (ap (trijoin_rec f) (jglue a (joinl b))))^) @ (((ap (transport (fun b : Join B C => Join_rec (j1 f) (Join_rec (j2 f) (j3 f) (j23 f)) (fun a : A => Join_ind (fun x : Join B C => j1 f a = Join_rec (j2 f) (j3 f) (j23 f) x) (j12 f a) (j13 f a) (fun (b0 : B) (c : C) => transport_paths_Fr (jglue b0 c) (j12 f a b0) @ ((1 @@ Join_rec_beta_jglue (...) (...) (...) b0 c) @ j123 f a b0 c))) (joinl a) = Join_rec (j1 f) (Join_rec (j2 f) (j3 f) (j23 f)) (fun a : A => Join_ind (fun x : Join B C => j1 f a = Join_rec (j2 f) (j3 f) (j23 f) x) (j12 f a) (j13 f a) (fun (b0 : B) (c : C) => transport_paths_Fr (jglue b0 c) (j12 f a b0) @ ((1 @@ Join_rec_beta_jglue (...) (...) (...) b0 c) @ j123 f a b0 c))) (joinr b)) (jglue b c)) (Join_rec_beta_jglue (j1 f) (Join_rec (j2 f) (j3 f) (j23 f)) (fun a : A => Join_ind (fun x : Join B C => j1 f a = Join_rec (j2 f) (j3 f) (j23 f) x) (j12 f a) (j13 f a) (fun (b : B) (c : C) => transport_paths_Fr (jglue b c) (j12 f a b) @ ((1 @@ Join_rec_beta_jglue (j2 f) (j3 f) (j23 f) b c) @ j123 f a b c))) a (joinl b)) @ transport_paths_Fr (jglue b c) (j12 f a b)) @ ((1 @@ Join_rec_beta_jglue (j2 f) (j3 f) (j23 f) b c) @ j123 f a b c)) @ (Join_rec_beta_jglue (j1 f) (Join_rec (j2 f) (j3 f) (j23 f)) (fun a : A => Join_ind (fun x : Join B C => j1 f a = Join_rec (j2 f) (j3 f) (j23 f) x) (j12 f a) (j13 f a) (fun (b : B) (c : C) => transport_paths_Fr (jglue b c) (j12 f a b) @ ((1 @@ Join_rec_beta_jglue (j2 f) (j3 f) (j23 f) b c) @ j123 f a b c))) a (joinr c))^) = ((trijoin_rec_beta_join12 f a b @@ trijoin_rec_beta_join23 f b c) @ j123 f a b c) @ (trijoin_rec_beta_join13 f a c)^
A, B, C, P: Type
f: TriJoinRecData A B C P
a: A
b: B
c: C

((1 @@ ap_compose joinr (trijoin_rec f) (jglue b c))^ @ (transport_paths_Fr (jglue b c) (ap (trijoin_rec f) (jglue a (joinl b))))^) @ (((transport_paths_Fr (jglue b c) (ap (Join_rec (j1 f) (Join_rec (j2 f) (j3 f) (j23 f)) (fun a : A => Join_ind (fun x : Join B C => j1 f a = Join_rec (j2 f) (j3 f) (j23 f) x) (j12 f a) (j13 f a) (fun (b : B) (c : C) => transport_paths_Fr (jglue b c) (j12 f a b) @ ((1 @@ Join_rec_beta_jglue (j2 f) (j3 f) (j23 f) b c) @ j123 f a b c)))) (jglue a (joinl b))) @ ap (fun q : j1 f a = Join_rec (j2 f) (j3 f) (j23 f) (joinl b) => q @ ap (Join_rec (j2 f) (j3 f) (j23 f)) (jglue b c)) (Join_rec_beta_jglue (j1 f) (Join_rec (j2 f) (j3 f) (j23 f)) (fun a : A => Join_ind (fun x : Join B C => j1 f a = Join_rec (j2 f) (j3 f) (j23 f) x) (j12 f a) (j13 f a) (fun (b : B) (c : C) => transport_paths_Fr (jglue b c) (j12 f a b) @ ((1 @@ Join_rec_beta_jglue (j2 f) (j3 f) (j23 f) b c) @ j123 f a b c))) a (joinl b))) @ ((1 @@ Join_rec_beta_jglue (j2 f) (j3 f) (j23 f) b c) @ j123 f a b c)) @ (Join_rec_beta_jglue (j1 f) (Join_rec (j2 f) (j3 f) (j23 f)) (fun a : A => Join_ind (fun x : Join B C => j1 f a = Join_rec (j2 f) (j3 f) (j23 f) x) (j12 f a) (j13 f a) (fun (b : B) (c : C) => transport_paths_Fr (jglue b c) (j12 f a b) @ ((1 @@ Join_rec_beta_jglue (j2 f) (j3 f) (j23 f) b c) @ j123 f a b c))) a (joinr c))^) = ((trijoin_rec_beta_join12 f a b @@ trijoin_rec_beta_join23 f b c) @ j123 f a b c) @ (trijoin_rec_beta_join13 f a c)^
(* Everything that remains is pure path algebra. *) (* [trijoin_rec_beta_join23] expands to something of the form [p^ @ r], so that's what is in the lemma. One can unfold it to see this, but the [Qed] is a bit faster without this: *) (* unfold trijoin_rec_beta_join23. *) (* Note that one of the [ap]s on the LHS computes to [u @@ 1], so that's what is in the lemma: *) (* change (ap (fun q => q @ ?x) ?u) with (u @@ @idpath _ x). *) nrapply trijoin_rec_beta_join123_helper. Qed. (** We're next going to define a map in the other direction. We do it via showing that [TriJoinRecData] is a 0-coherent 1-functor to [Type]. We'll later show that it is a 1-functor to 0-groupoids. *)
A, B, C, P, Q: Type
g: P -> Q
f: TriJoinRecData A B C P

TriJoinRecData A B C Q
A, B, C, P, Q: Type
g: P -> Q
f: TriJoinRecData A B C P

TriJoinRecData A B C Q
A, B, C, P, Q: Type
g: P -> Q
f: TriJoinRecData A B C P

A -> Q
A, B, C, P, Q: Type
g: P -> Q
f: TriJoinRecData A B C P
B -> Q
A, B, C, P, Q: Type
g: P -> Q
f: TriJoinRecData A B C P
C -> Q
A, B, C, P, Q: Type
g: P -> Q
f: TriJoinRecData A B C P
forall (a : A) (b : B), ?j1 a = ?j2 b
A, B, C, P, Q: Type
g: P -> Q
f: TriJoinRecData A B C P
forall (a : A) (c : C), ?j1 a = ?j3 c
A, B, C, P, Q: Type
g: P -> Q
f: TriJoinRecData A B C P
forall (b : B) (c : C), ?j2 b = ?j3 c
A, B, C, P, Q: Type
g: P -> Q
f: TriJoinRecData A B C P
forall (a : A) (b : B) (c : C), ?j12 a b @ ?j23 b c = ?j13 a c
A, B, C, P, Q: Type
g: P -> Q
f: TriJoinRecData A B C P

A -> Q
exact (g o j1 f).
A, B, C, P, Q: Type
g: P -> Q
f: TriJoinRecData A B C P

B -> Q
exact (g o j2 f).
A, B, C, P, Q: Type
g: P -> Q
f: TriJoinRecData A B C P

C -> Q
exact (g o j3 f).
A, B, C, P, Q: Type
g: P -> Q
f: TriJoinRecData A B C P

forall (a : A) (b : B), (g o j1 f) a = (g o j2 f) b
exact (fun a b => ap g (j12 f a b)).
A, B, C, P, Q: Type
g: P -> Q
f: TriJoinRecData A B C P

forall (a : A) (c : C), (g o j1 f) a = (g o j3 f) c
exact (fun a c => ap g (j13 f a c)).
A, B, C, P, Q: Type
g: P -> Q
f: TriJoinRecData A B C P

forall (b : B) (c : C), (g o j2 f) b = (g o j3 f) c
exact (fun b c => ap g (j23 f b c)).
A, B, C, P, Q: Type
g: P -> Q
f: TriJoinRecData A B C P

forall (a : A) (b : B) (c : C), (fun (a0 : A) (b0 : B) => ap g (j12 f a0 b0)) a b @ (fun (b0 : B) (c0 : C) => ap g (j23 f b0 c0)) b c = (fun (a0 : A) (c0 : C) => ap g (j13 f a0 c0)) a c
A, B, C, P, Q: Type
g: P -> Q
f: TriJoinRecData A B C P
a: A
b: B
c: C

ap g (j12 f a b) @ ap g (j23 f b c) = ap g (j13 f a c)
exact (ap_triangle g (j123 f a b c)). (* The last four goals above can also be handled by the induction tactics below, but it's useful to be concrete. *) Defined. (** The triple join itself has canonical [TriJoinRecData]. *) Definition trijoinrecdata_trijoin (A B C : Type) : TriJoinRecData A B C (Join A (Join B C)) := Build_TriJoinRecData join1 join2 join3 join12 join13 join23 join123. (** Combining these gives a function going in the opposite direction to [trijoin_rec]. *) Definition trijoin_rec_inv {A B C P : Type} (f : TriJoin A B C -> P) : TriJoinRecData A B C P := trijoinrecdata_fun f (trijoinrecdata_trijoin A B C). (** Under [Funext], [trijoin_rec] and [trijoin_rec_inv] should be inverse equivalences. We'll avoid [Funext] and show that they are equivalences of 0-groupoids, where we choose the path structures carefully. *) (** ** The graph structure on [TriJoinRecData A B C P] *) (** The type of fillers for a triangular prism with five 2d faces [abc], [abc'], [k12], [k13], [k23]. *) Definition prism {P : Type} {a b c : P} {ab : a = b} {ac : a = c} {bc : b = c} (abc : ab @ bc = ac) {a' b' c' : P} {ab' : a' = b'} {ac' : a' = c'} {bc' : b' = c'} (abc' : ab' @ bc' = ac') {k1 : a = a'} {k2 : b = b'} {k3 : c = c'} (k12 : ab @ k2 = k1 @ ab') (k13 : ac @ k3 = k1 @ ac') (k23 : bc @ k3 = k2 @ bc') := concat_p_pp _ _ _ @ whiskerR abc k3 @ k13 = whiskerL ab k23 @ concat_p_pp _ _ _ @ whiskerR k12 bc' @ concat_pp_p _ _ _ @ whiskerL k1 abc'. (** The "identity" filler is slightly non-trivial, because the fillers for the squares, e.g. [ab @ 1 = 1 @ ab], must be non-trivial. *)
P: Type
a, b, c: P
ab: a = b
ac: a = c
bc: b = c
abc: ab @ bc = ac

prism abc abc (equiv_p1_1q 1) (equiv_p1_1q 1) (equiv_p1_1q 1)
P: Type
a, b, c: P
ab: a = b
ac: a = c
bc: b = c
abc: ab @ bc = ac

prism abc abc (equiv_p1_1q 1) (equiv_p1_1q 1) (equiv_p1_1q 1)
P: Type
a: P

prism 1 1 1 1 1
reflexivity. Defined. (** The paths between elements of [TriJoinRecData A B C P]. Under [Funext], this type will be equivalent to the identity type. But without [Funext], this definition will be more useful. *) Record TriJoinRecPath {A B C P : Type} {f g : TriJoinRecData A B C P} := { h1 : forall a, j1 f a = j1 g a; h2 : forall b, j2 f b = j2 g b; h3 : forall c, j3 f c = j3 g c; h12 : forall a b, j12 f a b @ h2 b = h1 a @ j12 g a b; h13 : forall a c, j13 f a c @ h3 c = h1 a @ j13 g a c; h23 : forall b c, j23 f b c @ h3 c = h2 b @ j23 g b c; h123 : forall a b c, prism (j123 f a b c) (j123 g a b c) (h12 a b) (h13 a c) (h23 b c); }. Arguments TriJoinRecPath {A B C P} f g. (** We also define data for [trijoin_rec] that unbundles the first three components. This lets us talk about paths between two such when the first three components are definitionally equal. This is a common special case, and this set-up greatly simplifies a lot of path algebra in later proofs. *) Record TriJoinRecData' {A B C P : Type} {j1' : A -> P} {j2' : B -> P} {j3' : C -> P} := { j12' : forall a b, j1' a = j2' b; j13' : forall a c, j1' a = j3' c; j23' : forall b c, j2' b = j3' c; j123' : forall a b c, j12' a b @ j23' b c = j13' a c; }. Arguments TriJoinRecData' {A B C P} j1' j2' j3'. Arguments Build_TriJoinRecData' {A B C P}%type_scope (j1' j2' j3' j12' j13' j23' j123')%function_scope. Definition prism' {P : Type} {a b c : P} {ab : a = b} {ac : a = c} {bc : b = c} (abc : ab @ bc = ac) {ab' : a = b} {ac' : a = c} {bc' : b = c} (abc' : ab' @ bc' = ac') (k12 : ab = ab') (k13 : ac = ac') (k23 : bc = bc') := abc @ k13 = (k12 @@ k23) @ abc'. Record TriJoinRecPath' {A B C P : Type} {j1' : A -> P} {j2' : B -> P} {j3' : C -> P} {f g : TriJoinRecData' j1' j2' j3'} := { h12' : forall a b, j12' f a b = j12' g a b; h13' : forall a c, j13' f a c = j13' g a c; h23' : forall b c, j23' f b c = j23' g b c; h123' : forall a b c, prism' (j123' f a b c) (j123' g a b c) (h12' a b) (h13' a c) (h23' b c); }. Arguments TriJoinRecPath' {A B C P} {j1' j2' j3'} f g. (** We can bundle and unbundle these types of data. For unbundling, we just handle [TriJoinRecData] for now. *) Definition bundle_trijoinrecdata {A B C P : Type} {j1' : A -> P} {j2' : B -> P} {j3' : C -> P} (f : TriJoinRecData' j1' j2' j3') : TriJoinRecData A B C P := Build_TriJoinRecData j1' j2' j3' (j12' f) (j13' f) (j23' f) (j123' f). Definition unbundle_trijoinrecdata {A B C P : Type} (f : TriJoinRecData A B C P) : TriJoinRecData' (j1 f) (j2 f) (j3 f) := Build_TriJoinRecData' (j1 f) (j2 f) (j3 f) (j12 f) (j13 f) (j23 f) (j123 f). (** The proof by induction that is easily available to us here is what saves work in more complicated contexts. *)
P: Type
a, b, c: P
ab: a = b
ac: a = c
bc: b = c
abc: ab @ bc = ac
ab': a = b
ac': a = c
bc': b = c
abc': ab' @ bc' = ac'
k12: ab = ab'
k13: ac = ac'
k23: bc = bc'
k123: prism' abc abc' k12 k13 k23

prism abc abc' (equiv_p1_1q k12) (equiv_p1_1q k13) (equiv_p1_1q k23)
P: Type
a, b, c: P
ab: a = b
ac: a = c
bc: b = c
abc: ab @ bc = ac
ab': a = b
ac': a = c
bc': b = c
abc': ab' @ bc' = ac'
k12: ab = ab'
k13: ac = ac'
k23: bc = bc'
k123: prism' abc abc' k12 k13 k23

prism abc abc' (equiv_p1_1q k12) (equiv_p1_1q k13) (equiv_p1_1q k23)
P: Type
a, c: P
ac, bc: a = c
abc: 1 @ bc = ac
ab': a = a
ac', bc': a = c
abc': ab' @ bc' = ac'
k12: 1 = ab'
k13: ac = ac'
k23: bc = bc'
k123: prism' abc abc' k12 k13 k23

prism abc abc' (equiv_p1_1q k12) (equiv_p1_1q k13) (equiv_p1_1q k23)
P: Type
a: P
ac: a = a
abc: 1 @ 1 = ac
ab', ac', bc': a = a
abc': ab' @ bc' = ac'
k12: 1 = ab'
k13: ac = ac'
k23: 1 = bc'
k123: prism' abc abc' k12 k13 k23

prism abc abc' (equiv_p1_1q k12) (equiv_p1_1q k13) (equiv_p1_1q k23)
P: Type
a: P
ab', ac', bc': a = a
abc': ab' @ bc' = ac'
k12: 1 = ab'
k13: 1 @ 1 = ac'
k23: 1 = bc'
k123: prism' 1 abc' k12 k13 k23

prism 1 abc' (equiv_p1_1q k12) (equiv_p1_1q k13) (equiv_p1_1q k23)
P: Type
a: P
ac', bc': a = a
abc': 1 @ bc' = ac'
k13: 1 @ 1 = ac'
k23: 1 = bc'
k123: prism' 1 abc' 1 k13 k23

prism 1 abc' (equiv_p1_1q 1) (equiv_p1_1q k13) (equiv_p1_1q k23)
P: Type
a: P
ac': a = a
abc', k13: 1 @ 1 = ac'
k123: prism' 1 abc' 1 k13 1

prism 1 abc' (equiv_p1_1q 1) (equiv_p1_1q k13) (equiv_p1_1q 1)
P: Type
a: P
abc': 1 @ 1 = 1 @ 1
k123: prism' 1 abc' 1 1 1

prism 1 abc' (equiv_p1_1q 1) (equiv_p1_1q 1) (equiv_p1_1q 1)
P: Type
a: P
abc': 1 @ 1 = 1 @ 1
k123: 1 @ 1 = (1 @@ 1) @ abc'

prism 1 abc' (equiv_p1_1q 1) (equiv_p1_1q 1) (equiv_p1_1q 1)
P: Type
a: P

prism 1 ((1 @@ 1)^ @ (1 @ 1)) (equiv_p1_1q 1) (equiv_p1_1q 1) (equiv_p1_1q 1)
P: Type
a: P

prism 1 1 1 1 1
reflexivity. Defined.
A, B, C, P: Type
j1': A -> P
j2': B -> P
j3': C -> P
f, g: TriJoinRecData' j1' j2' j3'
h: TriJoinRecPath' f g

TriJoinRecPath (bundle_trijoinrecdata f) (bundle_trijoinrecdata g)
A, B, C, P: Type
j1': A -> P
j2': B -> P
j3': C -> P
f, g: TriJoinRecData' j1' j2' j3'
h: TriJoinRecPath' f g

TriJoinRecPath (bundle_trijoinrecdata f) (bundle_trijoinrecdata g)
A, B, C, P: Type
j1': A -> P
j2': B -> P
j3': C -> P
f, g: TriJoinRecData' j1' j2' j3'
h: TriJoinRecPath' f g

forall a : A, j1 (bundle_trijoinrecdata f) a = j1 (bundle_trijoinrecdata g) a
A, B, C, P: Type
j1': A -> P
j2': B -> P
j3': C -> P
f, g: TriJoinRecData' j1' j2' j3'
h: TriJoinRecPath' f g
forall b : B, j2 (bundle_trijoinrecdata f) b = j2 (bundle_trijoinrecdata g) b
A, B, C, P: Type
j1': A -> P
j2': B -> P
j3': C -> P
f, g: TriJoinRecData' j1' j2' j3'
h: TriJoinRecPath' f g
forall c : C, j3 (bundle_trijoinrecdata f) c = j3 (bundle_trijoinrecdata g) c
A, B, C, P: Type
j1': A -> P
j2': B -> P
j3': C -> P
f, g: TriJoinRecData' j1' j2' j3'
h: TriJoinRecPath' f g
forall (a : A) (b : B), j12 (bundle_trijoinrecdata f) a b @ ?h2 b = ?h1 a @ j12 (bundle_trijoinrecdata g) a b
A, B, C, P: Type
j1': A -> P
j2': B -> P
j3': C -> P
f, g: TriJoinRecData' j1' j2' j3'
h: TriJoinRecPath' f g
forall (a : A) (c : C), j13 (bundle_trijoinrecdata f) a c @ ?h3 c = ?h1 a @ j13 (bundle_trijoinrecdata g) a c
A, B, C, P: Type
j1': A -> P
j2': B -> P
j3': C -> P
f, g: TriJoinRecData' j1' j2' j3'
h: TriJoinRecPath' f g
forall (b : B) (c : C), j23 (bundle_trijoinrecdata f) b c @ ?h3 c = ?h2 b @ j23 (bundle_trijoinrecdata g) b c
A, B, C, P: Type
j1': A -> P
j2': B -> P
j3': C -> P
f, g: TriJoinRecData' j1' j2' j3'
h: TriJoinRecPath' f g
forall (a : A) (b : B) (c : C), prism (j123 (bundle_trijoinrecdata f) a b c) (j123 (bundle_trijoinrecdata g) a b c) (?h12 a b) (?h13 a c) (?h23 b c)
A, B, C, P: Type
j1': A -> P
j2': B -> P
j3': C -> P
f, g: TriJoinRecData' j1' j2' j3'
h: TriJoinRecPath' f g

forall (a : A) (b : B), j12 (bundle_trijoinrecdata f) a b @ (fun b0 : B => 1) b = (fun a0 : A => 1) a @ j12 (bundle_trijoinrecdata g) a b
A, B, C, P: Type
j1': A -> P
j2': B -> P
j3': C -> P
f, g: TriJoinRecData' j1' j2' j3'
h: TriJoinRecPath' f g
forall (a : A) (c : C), j13 (bundle_trijoinrecdata f) a c @ (fun c0 : C => 1) c = (fun a0 : A => 1) a @ j13 (bundle_trijoinrecdata g) a c
A, B, C, P: Type
j1': A -> P
j2': B -> P
j3': C -> P
f, g: TriJoinRecData' j1' j2' j3'
h: TriJoinRecPath' f g
forall (b : B) (c : C), j23 (bundle_trijoinrecdata f) b c @ (fun c0 : C => 1) c = (fun b0 : B => 1) b @ j23 (bundle_trijoinrecdata g) b c
A, B, C, P: Type
j1': A -> P
j2': B -> P
j3': C -> P
f, g: TriJoinRecData' j1' j2' j3'
h: TriJoinRecPath' f g
forall (a : A) (b : B) (c : C), prism (j123 (bundle_trijoinrecdata f) a b c) (j123 (bundle_trijoinrecdata g) a b c) (?h12 a b) (?h13 a c) (?h23 b c)
A, B, C, P: Type
j1': A -> P
j2': B -> P
j3': C -> P
f, g: TriJoinRecData' j1' j2' j3'
h: TriJoinRecPath' f g
a: A
b: B

j12 (bundle_trijoinrecdata f) a b = j12 (bundle_trijoinrecdata g) a b
A, B, C, P: Type
j1': A -> P
j2': B -> P
j3': C -> P
f, g: TriJoinRecData' j1' j2' j3'
h: TriJoinRecPath' f g
a: A
c: C
j13 (bundle_trijoinrecdata f) a c = j13 (bundle_trijoinrecdata g) a c
A, B, C, P: Type
j1': A -> P
j2': B -> P
j3': C -> P
f, g: TriJoinRecData' j1' j2' j3'
h: TriJoinRecPath' f g
b: B
c: C
j23 (bundle_trijoinrecdata f) b c = j23 (bundle_trijoinrecdata g) b c
A, B, C, P: Type
j1': A -> P
j2': B -> P
j3': C -> P
f, g: TriJoinRecData' j1' j2' j3'
h: TriJoinRecPath' f g
forall (a : A) (b : B) (c : C), prism (j123 (bundle_trijoinrecdata f) a b c) (j123 (bundle_trijoinrecdata g) a b c) ((fun (a0 : A) (b0 : B) => let X := equiv_fun equiv_p1_1q in X ?Goal@{a:=a0; b:=b0}) a b) ((fun (a0 : A) (c0 : C) => let X := equiv_fun equiv_p1_1q in X ?Goal0@{a:=a0; c:=c0}) a c) ((fun (b0 : B) (c0 : C) => let X := equiv_fun equiv_p1_1q in X ?Goal1@{b:=b0; c:=c0}) b c)
A, B, C, P: Type
j1': A -> P
j2': B -> P
j3': C -> P
f, g: TriJoinRecData' j1' j2' j3'
h: TriJoinRecPath' f g
a: A
b: B

j12 (bundle_trijoinrecdata f) a b = j12 (bundle_trijoinrecdata g) a b
apply (h12' h).
A, B, C, P: Type
j1': A -> P
j2': B -> P
j3': C -> P
f, g: TriJoinRecData' j1' j2' j3'
h: TriJoinRecPath' f g
a: A
c: C

j13 (bundle_trijoinrecdata f) a c = j13 (bundle_trijoinrecdata g) a c
apply (h13' h).
A, B, C, P: Type
j1': A -> P
j2': B -> P
j3': C -> P
f, g: TriJoinRecData' j1' j2' j3'
h: TriJoinRecPath' f g
b: B
c: C

j23 (bundle_trijoinrecdata f) b c = j23 (bundle_trijoinrecdata g) b c
apply (h23' h).
A, B, C, P: Type
j1': A -> P
j2': B -> P
j3': C -> P
f, g: TriJoinRecData' j1' j2' j3'
h: TriJoinRecPath' f g

forall (a : A) (b : B) (c : C), prism (j123 (bundle_trijoinrecdata f) a b c) (j123 (bundle_trijoinrecdata g) a b c) ((fun (a0 : A) (b0 : B) => let X := equiv_fun equiv_p1_1q in X (h12' h a0 b0)) a b) ((fun (a0 : A) (c0 : C) => let X := equiv_fun equiv_p1_1q in X (h13' h a0 c0)) a c) ((fun (b0 : B) (c0 : C) => let X := equiv_fun equiv_p1_1q in X (h23' h b0 c0)) b c)
A, B, C, P: Type
j1': A -> P
j2': B -> P
j3': C -> P
f, g: TriJoinRecData' j1' j2' j3'
h: TriJoinRecPath' f g

forall (a : A) (b : B) (c : C), prism (j123 (bundle_trijoinrecdata f) a b c) (j123 (bundle_trijoinrecdata g) a b c) (equiv_p1_1q (h12' h a b)) (equiv_p1_1q (h13' h a c)) (equiv_p1_1q (h23' h b c))
A, B, C, P: Type
j1': A -> P
j2': B -> P
j3': C -> P
f, g: TriJoinRecData' j1' j2' j3'
h: TriJoinRecPath' f g
a: A
b: B
c: C

prism (j123 (bundle_trijoinrecdata f) a b c) (j123 (bundle_trijoinrecdata g) a b c) (equiv_p1_1q (h12' h a b)) (equiv_p1_1q (h13' h a c)) (equiv_p1_1q (h23' h b c))
apply bundle_prism, (h123' h). Defined. (** A tactic that helps us apply the previous result. *) Ltac bundle_trijoinrecpath := hnf; match goal with |- TriJoinRecPath ?F ?G => refine (bundle_trijoinrecpath (f:=unbundle_trijoinrecdata F) (g:=unbundle_trijoinrecdata G) _) end; snrapply Build_TriJoinRecPath'. (** Using these paths, we can restate the beta rule for [trijoin_rec]. The statement using [TriJoinRecPath'] typechecks only because [trijoin_rec] computes definitionally on the path constructors. *)
A, B, C, P: Type
f: TriJoinRecData A B C P

TriJoinRecPath' (unbundle_trijoinrecdata (trijoin_rec_inv (trijoin_rec f))) (unbundle_trijoinrecdata f)
A, B, C, P: Type
f: TriJoinRecData A B C P

TriJoinRecPath' (unbundle_trijoinrecdata (trijoin_rec_inv (trijoin_rec f))) (unbundle_trijoinrecdata f)
A, B, C, P: Type
f: TriJoinRecData A B C P

forall (a : A) (b : B), ap (trijoin_rec f) (join12 a b) = j12 f a b
A, B, C, P: Type
f: TriJoinRecData A B C P
forall (a : A) (c : C), ap (trijoin_rec f) (join13 a c) = j13 f a c
A, B, C, P: Type
f: TriJoinRecData A B C P
forall (b : B) (c : C), ap (trijoin_rec f) (join23 b c) = j23 f b c
A, B, C, P: Type
f: TriJoinRecData A B C P
forall (a : A) (b : B) (c : C), prism' (ap_triangle (trijoin_rec f) (join123 a b c)) (j123 f a b c) (?Goal a b) (?Goal0 a c) (?Goal1 b c)
A, B, C, P: Type
f: TriJoinRecData A B C P

forall (a : A) (b : B), ap (trijoin_rec f) (join12 a b) = j12 f a b
apply trijoin_rec_beta_join12.
A, B, C, P: Type
f: TriJoinRecData A B C P

forall (a : A) (c : C), ap (trijoin_rec f) (join13 a c) = j13 f a c
apply trijoin_rec_beta_join13.
A, B, C, P: Type
f: TriJoinRecData A B C P

forall (b : B) (c : C), ap (trijoin_rec f) (join23 b c) = j23 f b c
apply trijoin_rec_beta_join23.
A, B, C, P: Type
f: TriJoinRecData A B C P

forall (a : A) (b : B) (c : C), prism' (ap_triangle (trijoin_rec f) (join123 a b c)) (j123 f a b c) (trijoin_rec_beta_join12 f a b) (trijoin_rec_beta_join13 f a c) (trijoin_rec_beta_join23 f b c)
A, B, C, P: Type
f: TriJoinRecData A B C P
a: A
b: B
c: C

prism' (ap_triangle (trijoin_rec f) (join123 a b c)) (j123 f a b c) (trijoin_rec_beta_join12 f a b) (trijoin_rec_beta_join13 f a c) (trijoin_rec_beta_join23 f b c)
A, B, C, P: Type
f: TriJoinRecData A B C P
a: A
b: B
c: C

ap_triangle (trijoin_rec f) (join123 a b c) @ trijoin_rec_beta_join13 f a c = (trijoin_rec_beta_join12 f a b @@ trijoin_rec_beta_join23 f b c) @ j123 f a b c
A, B, C, P: Type
f: TriJoinRecData A B C P
a: A
b: B
c: C

ap_triangle (trijoin_rec f) (join123 a b c) = ((trijoin_rec_beta_join12 f a b @@ trijoin_rec_beta_join23 f b c) @ j123 f a b c) @ (trijoin_rec_beta_join13 f a c)^
nrapply trijoin_rec_beta_join123. Defined. (** We can upgrade this to an unprimed path. This says that [trijoin_rec_inv] is split surjective. *) Definition trijoin_rec_beta {A B C P : Type} (f : TriJoinRecData A B C P) : TriJoinRecPath (trijoin_rec_inv (trijoin_rec f)) f := bundle_trijoinrecpath (trijoin_rec_beta' f). (** ** [trijoin_rec_inv] is an injective map between 0-groupoids *) (** We begin with a general purpose lemma. *)
P: Type
a: P
Q: forall (b c : P) (ab : a = b) (ac : a = c) (bc : b = c), ab @ bc = ac -> Type
s: Q a a 1 1 1 1

forall (b c : P) (ab : a = b) (ac : a = c) (bc : b = c) (abc : ab @ bc = ac), Q b c ab ac bc abc
P: Type
a: P
Q: forall (b c : P) (ab : a = b) (ac : a = c) (bc : b = c), ab @ bc = ac -> Type
s: Q a a 1 1 1 1

forall (b c : P) (ab : a = b) (ac : a = c) (bc : b = c) (abc : ab @ bc = ac), Q b c ab ac bc abc
P: Type
a: P
Q: forall (b c : P) (ab : a = b) (ac : a = c) (bc : b = c), ab @ bc = ac -> Type
s: Q a a 1 1 1 1
b, c: P
ab: a = b
ac: a = c
bc: b = c
abc: ab @ bc = ac

Q b c ab ac bc abc
P: Type
a: P
Q: forall (b c : P) (ab : a = b) (ac : a = c) (bc : b = c), ab @ bc = ac -> Type
s: Q a a 1 1 1 1
c: P
ac, bc: a = c
abc: 1 @ bc = ac

Q a c 1 ac bc abc
P: Type
a: P
Q: forall (b c : P) (ab : a = b) (ac : a = c) (bc : b = c), ab @ bc = ac -> Type
s: Q a a 1 1 1 1
ac: a = a
abc: 1 @ 1 = ac

Q a a 1 ac 1 abc
P: Type
a: P
Q: forall (b c : P) (ab : a = b) (ac : a = c) (bc : b = c), ab @ bc = ac -> Type
s: Q a a 1 1 1 1

Q a a 1 (1 @ 1) 1 1
apply s. Defined. (** This lemma handles the path algebra in the last goal of the next result. *)
J, P: Type
f, g: J -> P
a, b, c: J
ab: a = b
ac: a = c
bc: b = c
abc: ab @ bc = ac
H1: f a = g a
H2: f b = g b
H3: f c = g c
H12: ap f ab @ H2 = H1 @ ap g ab
H13: ap f ac @ H3 = H1 @ ap g ac
H23: ap f bc @ H3 = H2 @ ap g bc
H123: prism (ap_triangle f abc) (ap_triangle g abc) H12 H13 H23

(transport_pp (fun x : J => f x = g x) ab bc H1 @ ap (transport (fun x : J => f x = g x) bc) (transport_paths_FlFr' ab H1 H2 H12)) @ transport_paths_FlFr' bc H2 H3 H23 = transport2 (fun x : J => f x = g x) abc H1 @ transport_paths_FlFr' ac H1 H3 H13
J, P: Type
f, g: J -> P
a, b, c: J
ab: a = b
ac: a = c
bc: b = c
abc: ab @ bc = ac
H1: f a = g a
H2: f b = g b
H3: f c = g c
H12: ap f ab @ H2 = H1 @ ap g ab
H13: ap f ac @ H3 = H1 @ ap g ac
H23: ap f bc @ H3 = H2 @ ap g bc
H123: prism (ap_triangle f abc) (ap_triangle g abc) H12 H13 H23

(transport_pp (fun x : J => f x = g x) ab bc H1 @ ap (transport (fun x : J => f x = g x) bc) (transport_paths_FlFr' ab H1 H2 H12)) @ transport_paths_FlFr' bc H2 H3 H23 = transport2 (fun x : J => f x = g x) abc H1 @ transport_paths_FlFr' ac H1 H3 H13
J, P: Type
f, g: J -> P
a: J
H1: f a = g a

forall (b c : J) (ab : a = b) (ac : a = c) (bc : b = c) (abc : ab @ bc = ac) (H2 : f b = g b) (H3 : f c = g c) (H12 : ap f ab @ H2 = H1 @ ap g ab) (H13 : ap f ac @ H3 = H1 @ ap g ac) (H23 : ap f bc @ H3 = H2 @ ap g bc), prism (ap_triangle f abc) (ap_triangle g abc) H12 H13 H23 -> (transport_pp (fun x : J => f x = g x) ab bc H1 @ ap (transport (fun x : J => f x = g x) bc) (transport_paths_FlFr' ab H1 H2 H12)) @ transport_paths_FlFr' bc H2 H3 H23 = transport2 (fun x : J => f x = g x) abc H1 @ transport_paths_FlFr' ac H1 H3 H13
J, P: Type
f, g: J -> P
a: J
H1: f a = g a

forall (H2 H3 : f a = g a) (H12 : 1 @ H2 = H1 @ 1) (H13 : 1 @ H3 = H1 @ 1) (H23 : 1 @ H3 = H2 @ 1), prism 1 1 H12 H13 H23 -> (1 @ ap (transport (fun x : J => f x = g x) 1) (transport_paths_FlFr' 1 H1 H2 H12)) @ transport_paths_FlFr' 1 H2 H3 H23 = 1 @ transport_paths_FlFr' 1 H1 H3 H13
J, P: Type
f, g: J -> P
a: J
H1: f a = g a

forall (H2 H3 : f a = g a) (H12 : 1 @ H2 = H1 @ 1) (H13 : 1 @ H3 = H1 @ 1) (H23 : 1 @ H3 = H2 @ 1), prism 1 1 H12 H13 H23 -> (1 @ ap idmap (((concat_1p H1)^ @ (concat_p1 (1 @ H1))^) @ (concat_pp_p 1 H1 1 @ ((concat_1p (H1 @ 1) @ H12^) @ concat_1p H2)))) @ (((concat_1p H2)^ @ (concat_p1 (1 @ H2))^) @ (concat_pp_p 1 H2 1 @ ((concat_1p (H2 @ 1) @ H23^) @ concat_1p H3))) = 1 @ (((concat_1p H1)^ @ (concat_p1 (1 @ H1))^) @ (concat_pp_p 1 H1 1 @ ((concat_1p (H1 @ 1) @ H13^) @ concat_1p H3)))
J, P: Type
g: J -> P
a: J
fa: P

forall (H1 H2 H3 : fa = g a) (H12 : 1 @ H2 = H1 @ 1) (H13 : 1 @ H3 = H1 @ 1) (H23 : 1 @ H3 = H2 @ 1), prism 1 1 H12 H13 H23 -> (1 @ ap idmap (((concat_1p H1)^ @ (concat_p1 (1 @ H1))^) @ (concat_pp_p 1 H1 1 @ ((concat_1p (H1 @ 1) @ H12^) @ concat_1p H2)))) @ (((concat_1p H2)^ @ (concat_p1 (1 @ H2))^) @ (concat_pp_p 1 H2 1 @ ((concat_1p (H2 @ 1) @ H23^) @ concat_1p H3))) = 1 @ (((concat_1p H1)^ @ (concat_p1 (1 @ H1))^) @ (concat_pp_p 1 H1 1 @ ((concat_1p (H1 @ 1) @ H13^) @ concat_1p H3)))
J, P: Type
fa, ga: P

forall (H1 H2 H3 : fa = ga) (H12 : 1 @ H2 = H1 @ 1) (H13 : 1 @ H3 = H1 @ 1) (H23 : 1 @ H3 = H2 @ 1), prism 1 1 H12 H13 H23 -> (1 @ ap idmap (((concat_1p H1)^ @ (concat_p1 (1 @ H1))^) @ (concat_pp_p 1 H1 1 @ ((concat_1p (H1 @ 1) @ H12^) @ concat_1p H2)))) @ (((concat_1p H2)^ @ (concat_p1 (1 @ H2))^) @ (concat_pp_p 1 H2 1 @ ((concat_1p (H2 @ 1) @ H23^) @ concat_1p H3))) = 1 @ (((concat_1p H1)^ @ (concat_p1 (1 @ H1))^) @ (concat_pp_p 1 H1 1 @ ((concat_1p (H1 @ 1) @ H13^) @ concat_1p H3)))
J, P: Type
fa, ga: P
H1, H2, H3: fa = ga
H12: 1 @ H2 = H1 @ 1
H13: 1 @ H3 = H1 @ 1
H23: 1 @ H3 = H2 @ 1

prism 1 1 H12 H13 H23 -> (1 @ ap idmap (((concat_1p H1)^ @ (concat_p1 (1 @ H1))^) @ (concat_pp_p 1 H1 1 @ ((concat_1p (H1 @ 1) @ H12^) @ concat_1p H2)))) @ (((concat_1p H2)^ @ (concat_p1 (1 @ H2))^) @ (concat_pp_p 1 H2 1 @ ((concat_1p (H2 @ 1) @ H23^) @ concat_1p H3))) = 1 @ (((concat_1p H1)^ @ (concat_p1 (1 @ H1))^) @ (concat_pp_p 1 H1 1 @ ((concat_1p (H1 @ 1) @ H13^) @ concat_1p H3)))
J, P: Type
fa, ga: P
H1, H2, H3: fa = ga
H12: 1 @ H2 = H1 @ 1
H13: 1 @ H3 = H1 @ 1
H23: 1 @ H3 = H2 @ 1

prism 1 1 H12 H13 H23 -> (1 @ (((concat_1p H1)^ @ (concat_p1 (1 @ H1))^) @ (concat_pp_p 1 H1 1 @ ((concat_1p (H1 @ 1) @ H12^) @ concat_1p H2)))) @ (((concat_1p H2)^ @ (concat_p1 (1 @ H2))^) @ (concat_pp_p 1 H2 1 @ ((concat_1p (H2 @ 1) @ H23^) @ concat_1p H3))) = 1 @ (((concat_1p H1)^ @ (concat_p1 (1 @ H1))^) @ (concat_pp_p 1 H1 1 @ ((concat_1p (H1 @ 1) @ H13^) @ concat_1p H3)))
J, P: Type
fa, ga: P
H2, H3: fa = ga
H13, H23: 1 @ H3 = H2 @ 1

prism 1 1 (equiv_1p_q1 1) H13 H23 -> (1 @ (((concat_1p H2)^ @ (concat_p1 (1 @ H2))^) @ (concat_pp_p 1 H2 1 @ ((concat_1p (H2 @ 1) @ (equiv_1p_q1 1)^) @ concat_1p H2)))) @ (((concat_1p H2)^ @ (concat_p1 (1 @ H2))^) @ (concat_pp_p 1 H2 1 @ ((concat_1p (H2 @ 1) @ H23^) @ concat_1p H3))) = 1 @ (((concat_1p H2)^ @ (concat_p1 (1 @ H2))^) @ (concat_pp_p 1 H2 1 @ ((concat_1p (H2 @ 1) @ H13^) @ concat_1p H3)))
J, P: Type
fa, ga: P
H3: fa = ga
H23: 1 @ H3 = H3 @ 1

prism 1 1 (equiv_1p_q1 1) (equiv_1p_q1 1) H23 -> (1 @ (((concat_1p H3)^ @ (concat_p1 (1 @ H3))^) @ (concat_pp_p 1 H3 1 @ ((concat_1p (H3 @ 1) @ (equiv_1p_q1 1)^) @ concat_1p H3)))) @ (((concat_1p H3)^ @ (concat_p1 (1 @ H3))^) @ (concat_pp_p 1 H3 1 @ ((concat_1p (H3 @ 1) @ H23^) @ concat_1p H3))) = 1 @ (((concat_1p H3)^ @ (concat_p1 (1 @ H3))^) @ (concat_pp_p 1 H3 1 @ ((concat_1p (H3 @ 1) @ (equiv_1p_q1 1)^) @ concat_1p H3)))
J, P: Type
fa: P
H23: 1 @ 1 = 1 @ 1

prism 1 1 (equiv_1p_q1 1) (equiv_1p_q1 1) H23 -> (1 @ (((concat_1p 1)^ @ (concat_p1 (1 @ 1))^) @ (concat_pp_p 1 1 1 @ ((concat_1p (1 @ 1) @ (equiv_1p_q1 1)^) @ concat_1p 1)))) @ (((concat_1p 1)^ @ (concat_p1 (1 @ 1))^) @ (concat_pp_p 1 1 1 @ ((concat_1p (1 @ 1) @ H23^) @ concat_1p 1))) = 1 @ (((concat_1p 1)^ @ (concat_p1 (1 @ 1))^) @ (concat_pp_p 1 1 1 @ ((concat_1p (1 @ 1) @ (equiv_1p_q1 1)^) @ concat_1p 1)))
J, P: Type
fa: P
H23: 1 @ 1 = 1 @ 1
H123: prism 1 1 (equiv_1p_q1 1) (equiv_1p_q1 1) H23

(1 @ (((concat_1p 1)^ @ (concat_p1 (1 @ 1))^) @ (concat_pp_p 1 1 1 @ ((concat_1p (1 @ 1) @ (equiv_1p_q1 1)^) @ concat_1p 1)))) @ (((concat_1p 1)^ @ (concat_p1 (1 @ 1))^) @ (concat_pp_p 1 1 1 @ ((concat_1p (1 @ 1) @ H23^) @ concat_1p 1))) = 1 @ (((concat_1p 1)^ @ (concat_p1 (1 @ 1))^) @ (concat_pp_p 1 1 1 @ ((concat_1p (1 @ 1) @ (equiv_1p_q1 1)^) @ concat_1p 1)))
J, P: Type
fa: P
H23: 1 @ 1 = 1 @ 1
H123: (concat_p_pp 1 1 1 @ whiskerR 1 1) @ equiv_1p_q1 1 = (((whiskerL 1 H23 @ concat_p_pp 1 1 1) @ whiskerR (equiv_1p_q1 1) 1) @ concat_pp_p 1 1 1) @ whiskerL 1 1

(1 @ (((concat_1p 1)^ @ (concat_p1 (1 @ 1))^) @ (concat_pp_p 1 1 1 @ ((concat_1p (1 @ 1) @ (equiv_1p_q1 1)^) @ concat_1p 1)))) @ (((concat_1p 1)^ @ (concat_p1 (1 @ 1))^) @ (concat_pp_p 1 1 1 @ ((concat_1p (1 @ 1) @ H23^) @ concat_1p 1))) = 1 @ (((concat_1p 1)^ @ (concat_p1 (1 @ 1))^) @ (concat_pp_p 1 1 1 @ ((concat_1p (1 @ 1) @ (equiv_1p_q1 1)^) @ concat_1p 1)))
J, P: Type
fa: P
H23: 1 @ 1 = 1 @ 1
H123: (concat_p_pp 1 1 1 @ whiskerR 1 1) @ equiv_1p_q1 1 = (((H23 @ concat_p_pp 1 1 1) @ whiskerR (equiv_1p_q1 1) 1) @ concat_pp_p 1 1 1) @ whiskerL 1 1

(1 @ (((concat_1p 1)^ @ (concat_p1 (1 @ 1))^) @ (concat_pp_p 1 1 1 @ ((concat_1p (1 @ 1) @ (equiv_1p_q1 1)^) @ concat_1p 1)))) @ (((concat_1p 1)^ @ (concat_p1 (1 @ 1))^) @ (concat_pp_p 1 1 1 @ ((concat_1p (1 @ 1) @ H23^) @ concat_1p 1))) = 1 @ (((concat_1p 1)^ @ (concat_p1 (1 @ 1))^) @ (concat_pp_p 1 1 1 @ ((concat_1p (1 @ 1) @ (equiv_1p_q1 1)^) @ concat_1p 1)))
J, P: Type
fa: P
H23: 1 = 1
H123: 1 = (((H23 @ 1) @ 1) @ 1) @ 1

1 @ (1 @ (1 @ ((1 @ H23^) @ 1))) = 1
J, P: Type
fa: P
H23: 1 = 1
H123: 1 = H23

1 @ (1 @ (1 @ ((1 @ H23^) @ 1))) = 1
J, P: Type
fa: P

1 @ (1 @ (1 @ ((1 @ 1^) @ 1))) = 1
reflexivity. Qed. (** [trijoin_rec_inv] is essentially injective, as a map between 0-groupoids. *)
A, B, C, P: Type
f, g: TriJoin A B C -> P
h: TriJoinRecPath (trijoin_rec_inv f) (trijoin_rec_inv g)

f == g
A, B, C, P: Type
f, g: TriJoin A B C -> P
h: TriJoinRecPath (trijoin_rec_inv f) (trijoin_rec_inv g)

f == g
A, B, C, P: Type
f, g: TriJoin A B C -> P
h: TriJoinRecPath (trijoin_rec_inv f) (trijoin_rec_inv g)

forall a : A, (fun x : TriJoin A B C => f x = g x) (join1 a)
A, B, C, P: Type
f, g: TriJoin A B C -> P
h: TriJoinRecPath (trijoin_rec_inv f) (trijoin_rec_inv g)
forall b : B, (fun x : TriJoin A B C => f x = g x) (join2 b)
A, B, C, P: Type
f, g: TriJoin A B C -> P
h: TriJoinRecPath (trijoin_rec_inv f) (trijoin_rec_inv g)
forall c : C, (fun x : TriJoin A B C => f x = g x) (join3 c)
A, B, C, P: Type
f, g: TriJoin A B C -> P
h: TriJoinRecPath (trijoin_rec_inv f) (trijoin_rec_inv g)
forall (a : A) (b : B), transport (fun x : TriJoin A B C => f x = g x) (join12 a b) (?join1' a) = ?join2' b
A, B, C, P: Type
f, g: TriJoin A B C -> P
h: TriJoinRecPath (trijoin_rec_inv f) (trijoin_rec_inv g)
forall (a : A) (c : C), transport (fun x : TriJoin A B C => f x = g x) (join13 a c) (?join1' a) = ?join3' c
A, B, C, P: Type
f, g: TriJoin A B C -> P
h: TriJoinRecPath (trijoin_rec_inv f) (trijoin_rec_inv g)
forall (b : B) (c : C), transport (fun x : TriJoin A B C => f x = g x) (join23 b c) (?join2' b) = ?join3' c
A, B, C, P: Type
f, g: TriJoin A B C -> P
h: TriJoinRecPath (trijoin_rec_inv f) (trijoin_rec_inv g)
forall (a : A) (b : B) (c : C), (transport_pp (fun x : TriJoin A B C => f x = g x) (join12 a b) (join23 b c) (?join1' a) @ ap (transport (fun x : TriJoin A B C => f x = g x) (join23 b c)) (?join12' a b)) @ ?join23' b c = transport2 (fun x : TriJoin A B C => f x = g x) (join123 a b c) (?join1' a) @ ?join13' a c
A, B, C, P: Type
f, g: TriJoin A B C -> P
h: TriJoinRecPath (trijoin_rec_inv f) (trijoin_rec_inv g)

forall b : B, (fun x : TriJoin A B C => f x = g x) (join2 b)
A, B, C, P: Type
f, g: TriJoin A B C -> P
h: TriJoinRecPath (trijoin_rec_inv f) (trijoin_rec_inv g)
forall c : C, (fun x : TriJoin A B C => f x = g x) (join3 c)
A, B, C, P: Type
f, g: TriJoin A B C -> P
h: TriJoinRecPath (trijoin_rec_inv f) (trijoin_rec_inv g)
forall (a : A) (b : B), transport (fun x : TriJoin A B C => f x = g x) (join12 a b) (h1 h a) = ?join2' b
A, B, C, P: Type
f, g: TriJoin A B C -> P
h: TriJoinRecPath (trijoin_rec_inv f) (trijoin_rec_inv g)
forall (a : A) (c : C), transport (fun x : TriJoin A B C => f x = g x) (join13 a c) (h1 h a) = ?join3' c
A, B, C, P: Type
f, g: TriJoin A B C -> P
h: TriJoinRecPath (trijoin_rec_inv f) (trijoin_rec_inv g)
forall (b : B) (c : C), transport (fun x : TriJoin A B C => f x = g x) (join23 b c) (?join2' b) = ?join3' c
A, B, C, P: Type
f, g: TriJoin A B C -> P
h: TriJoinRecPath (trijoin_rec_inv f) (trijoin_rec_inv g)
forall (a : A) (b : B) (c : C), (transport_pp (fun x : TriJoin A B C => f x = g x) (join12 a b) (join23 b c) (h1 h a) @ ap (transport (fun x : TriJoin A B C => f x = g x) (join23 b c)) (?join12' a b)) @ ?join23' b c = transport2 (fun x : TriJoin A B C => f x = g x) (join123 a b c) (h1 h a) @ ?join13' a c
A, B, C, P: Type
f, g: TriJoin A B C -> P
h: TriJoinRecPath (trijoin_rec_inv f) (trijoin_rec_inv g)

forall c : C, (fun x : TriJoin A B C => f x = g x) (join3 c)
A, B, C, P: Type
f, g: TriJoin A B C -> P
h: TriJoinRecPath (trijoin_rec_inv f) (trijoin_rec_inv g)
forall (a : A) (b : B), transport (fun x : TriJoin A B C => f x = g x) (join12 a b) (h1 h a) = h2 h b
A, B, C, P: Type
f, g: TriJoin A B C -> P
h: TriJoinRecPath (trijoin_rec_inv f) (trijoin_rec_inv g)
forall (a : A) (c : C), transport (fun x : TriJoin A B C => f x = g x) (join13 a c) (h1 h a) = ?join3' c
A, B, C, P: Type
f, g: TriJoin A B C -> P
h: TriJoinRecPath (trijoin_rec_inv f) (trijoin_rec_inv g)
forall (b : B) (c : C), transport (fun x : TriJoin A B C => f x = g x) (join23 b c) (h2 h b) = ?join3' c
A, B, C, P: Type
f, g: TriJoin A B C -> P
h: TriJoinRecPath (trijoin_rec_inv f) (trijoin_rec_inv g)
forall (a : A) (b : B) (c : C), (transport_pp (fun x : TriJoin A B C => f x = g x) (join12 a b) (join23 b c) (h1 h a) @ ap (transport (fun x : TriJoin A B C => f x = g x) (join23 b c)) (?join12' a b)) @ ?join23' b c = transport2 (fun x : TriJoin A B C => f x = g x) (join123 a b c) (h1 h a) @ ?join13' a c
A, B, C, P: Type
f, g: TriJoin A B C -> P
h: TriJoinRecPath (trijoin_rec_inv f) (trijoin_rec_inv g)

forall (a : A) (b : B), transport (fun x : TriJoin A B C => f x = g x) (join12 a b) (h1 h a) = h2 h b
A, B, C, P: Type
f, g: TriJoin A B C -> P
h: TriJoinRecPath (trijoin_rec_inv f) (trijoin_rec_inv g)
forall (a : A) (c : C), transport (fun x : TriJoin A B C => f x = g x) (join13 a c) (h1 h a) = h3 h c
A, B, C, P: Type
f, g: TriJoin A B C -> P
h: TriJoinRecPath (trijoin_rec_inv f) (trijoin_rec_inv g)
forall (b : B) (c : C), transport (fun x : TriJoin A B C => f x = g x) (join23 b c) (h2 h b) = h3 h c
A, B, C, P: Type
f, g: TriJoin A B C -> P
h: TriJoinRecPath (trijoin_rec_inv f) (trijoin_rec_inv g)
forall (a : A) (b : B) (c : C), (transport_pp (fun x : TriJoin A B C => f x = g x) (join12 a b) (join23 b c) (h1 h a) @ ap (transport (fun x : TriJoin A B C => f x = g x) (join23 b c)) (?join12' a b)) @ ?join23' b c = transport2 (fun x : TriJoin A B C => f x = g x) (join123 a b c) (h1 h a) @ ?join13' a c
A, B, C, P: Type
f, g: TriJoin A B C -> P
h: TriJoinRecPath (trijoin_rec_inv f) (trijoin_rec_inv g)
a: A
b: B

ap f (join12 a b) @ h2 h b = h1 h a @ ap g (join12 a b)
A, B, C, P: Type
f, g: TriJoin A B C -> P
h: TriJoinRecPath (trijoin_rec_inv f) (trijoin_rec_inv g)
a: A
c: C
ap f (join13 a c) @ h3 h c = h1 h a @ ap g (join13 a c)
A, B, C, P: Type
f, g: TriJoin A B C -> P
h: TriJoinRecPath (trijoin_rec_inv f) (trijoin_rec_inv g)
b: B
c: C
ap f (join23 b c) @ h3 h c = h2 h b @ ap g (join23 b c)
A, B, C, P: Type
f, g: TriJoin A B C -> P
h: TriJoinRecPath (trijoin_rec_inv f) (trijoin_rec_inv g)
forall (a : A) (b : B) (c : C), (transport_pp (fun x : TriJoin A B C => f x = g x) (join12 a b) (join23 b c) (h1 h a) @ ap (transport (fun x : TriJoin A B C => f x = g x) (join23 b c)) ((fun (a0 : A) (b0 : B) => transport_paths_FlFr' (join12 a0 b0) (h1 h a0) (h2 h b0) ?Goal@{a:=a0; b:=b0}) a b)) @ (fun (b0 : B) (c0 : C) => transport_paths_FlFr' (join23 b0 c0) (h2 h b0) (h3 h c0) ?Goal1@{b:=b0; c:=c0}) b c = transport2 (fun x : TriJoin A B C => f x = g x) (join123 a b c) (h1 h a) @ (fun (a0 : A) (c0 : C) => transport_paths_FlFr' (join13 a0 c0) (h1 h a0) (h3 h c0) ?Goal0@{a:=a0; c:=c0}) a c
A, B, C, P: Type
f, g: TriJoin A B C -> P
h: TriJoinRecPath (trijoin_rec_inv f) (trijoin_rec_inv g)
a: A
c: C

ap f (join13 a c) @ h3 h c = h1 h a @ ap g (join13 a c)
A, B, C, P: Type
f, g: TriJoin A B C -> P
h: TriJoinRecPath (trijoin_rec_inv f) (trijoin_rec_inv g)
b: B
c: C
ap f (join23 b c) @ h3 h c = h2 h b @ ap g (join23 b c)
A, B, C, P: Type
f, g: TriJoin A B C -> P
h: TriJoinRecPath (trijoin_rec_inv f) (trijoin_rec_inv g)
forall (a : A) (b : B) (c : C), (transport_pp (fun x : TriJoin A B C => f x = g x) (join12 a b) (join23 b c) (h1 h a) @ ap (transport (fun x : TriJoin A B C => f x = g x) (join23 b c)) ((fun (a0 : A) (b0 : B) => transport_paths_FlFr' (join12 a0 b0) (h1 h a0) (h2 h b0) (h12 h a0 b0)) a b)) @ (fun (b0 : B) (c0 : C) => transport_paths_FlFr' (join23 b0 c0) (h2 h b0) (h3 h c0) ?Goal0@{b:=b0; c:=c0}) b c = transport2 (fun x : TriJoin A B C => f x = g x) (join123 a b c) (h1 h a) @ (fun (a0 : A) (c0 : C) => transport_paths_FlFr' (join13 a0 c0) (h1 h a0) (h3 h c0) ?Goal@{a:=a0; c:=c0}) a c
A, B, C, P: Type
f, g: TriJoin A B C -> P
h: TriJoinRecPath (trijoin_rec_inv f) (trijoin_rec_inv g)
b: B
c: C

ap f (join23 b c) @ h3 h c = h2 h b @ ap g (join23 b c)
A, B, C, P: Type
f, g: TriJoin A B C -> P
h: TriJoinRecPath (trijoin_rec_inv f) (trijoin_rec_inv g)
forall (a : A) (b : B) (c : C), (transport_pp (fun x : TriJoin A B C => f x = g x) (join12 a b) (join23 b c) (h1 h a) @ ap (transport (fun x : TriJoin A B C => f x = g x) (join23 b c)) ((fun (a0 : A) (b0 : B) => transport_paths_FlFr' (join12 a0 b0) (h1 h a0) (h2 h b0) (h12 h a0 b0)) a b)) @ (fun (b0 : B) (c0 : C) => transport_paths_FlFr' (join23 b0 c0) (h2 h b0) (h3 h c0) ?Goal@{b:=b0; c:=c0}) b c = transport2 (fun x : TriJoin A B C => f x = g x) (join123 a b c) (h1 h a) @ (fun (a0 : A) (c0 : C) => transport_paths_FlFr' (join13 a0 c0) (h1 h a0) (h3 h c0) (h13 h a0 c0)) a c
A, B, C, P: Type
f, g: TriJoin A B C -> P
h: TriJoinRecPath (trijoin_rec_inv f) (trijoin_rec_inv g)

forall (a : A) (b : B) (c : C), (transport_pp (fun x : TriJoin A B C => f x = g x) (join12 a b) (join23 b c) (h1 h a) @ ap (transport (fun x : TriJoin A B C => f x = g x) (join23 b c)) ((fun (a0 : A) (b0 : B) => transport_paths_FlFr' (join12 a0 b0) (h1 h a0) (h2 h b0) (h12 h a0 b0)) a b)) @ (fun (b0 : B) (c0 : C) => transport_paths_FlFr' (join23 b0 c0) (h2 h b0) (h3 h c0) (h23 h b0 c0)) b c = transport2 (fun x : TriJoin A B C => f x = g x) (join123 a b c) (h1 h a) @ (fun (a0 : A) (c0 : C) => transport_paths_FlFr' (join13 a0 c0) (h1 h a0) (h3 h c0) (h13 h a0 c0)) a c
A, B, C, P: Type
f, g: TriJoin A B C -> P
h: TriJoinRecPath (trijoin_rec_inv f) (trijoin_rec_inv g)
a: A
b: B
c: C

(transport_pp (fun x : TriJoin A B C => f x = g x) (join12 a b) (join23 b c) (h1 h a) @ ap (transport (fun x : TriJoin A B C => f x = g x) (join23 b c)) (transport_paths_FlFr' (join12 a b) (h1 h a) (h2 h b) (h12 h a b))) @ transport_paths_FlFr' (join23 b c) (h2 h b) (h3 h c) (h23 h b c) = transport2 (fun x : TriJoin A B C => f x = g x) (join123 a b c) (h1 h a) @ transport_paths_FlFr' (join13 a c) (h1 h a) (h3 h c) (h13 h a c)
A, B, C, P: Type
f, g: TriJoin A B C -> P
h: TriJoinRecPath (trijoin_rec_inv f) (trijoin_rec_inv g)
a: A
b: B
c: C

prism (ap_triangle f (join123 a b c)) (ap_triangle g (join123 a b c)) (h12 h a b) (h13 h a c) (h23 h b c)
exact (h123 h a b c). Defined. (** ** Lemmas and tactics about triangles and prisms We now introduce several lemmas and tactics that will dispense with some routine goals. The idea is that a generic triangle can be assumed to be trivial on the first vertex, and a generic prism can be assumed to be the identity on the domain. In order to apply the [triangle_ind] and [prism_ind] lemmas that make this precise, we need to generalize various terms in the goal. *) (** This destructs a seven component term [f], tries to generalize each piece evaluated appropriately, and clears all pieces. If called with [a], [b] and [c] all valid terms, we expect all seven components to be generalized. But one can also call it with one of [a], [b] and [c] a dummy value (e.g. [_X_]) that causes four of the [generalize] tactics to fail. In this case, four components will be simply cleared, and three will be generalized and cleared, so this applies when the goal only depends on three of the seven components. *) Ltac generalize_some f a b c := let f1 := fresh in let f2 := fresh in let f3 := fresh in let f12 := fresh in let f13 := fresh in let f23 := fresh in let f123 := fresh in destruct f as [f1 f2 f3 f12 f13 f23 f123]; cbn; try generalize (f123 a b c); clear f123; try generalize (f23 b c); clear f23; try generalize (f13 a c); clear f13; try generalize (f12 a b); clear f12; try generalize (f3 c); clear f3; try generalize (f2 b); clear f2; try generalize (f1 a); clear f1. (* No easy way to skip the "last" one, since we don't know which will be the last to be generalized. *) (** Use this with [f : TriJoinRecData A B C P], [a : A], [b : B], [c : C]. *) Ltac triangle_ind f a b c := generalize_some f a b c; intro f; (* [generalize_some] goes one step too far, so intro the last variable. *) apply triangle_ind. (** Use this with [f : TriJoinRecData A B C P]. Two of the arguments [a], [b] and [c] should be elements of [A], [B] and [C], respectively, and the third should be a dummy value (e.g. [_X_]) that causes the generalize tactic to fail. It applies to goals that only depend on the components of [f] involving just two of [A], [B] and [C]. *) Ltac triangle_ind_two f a b c := generalize_some f a b c; intro f; (* [generalize_some] goes one step too far, so intro the last variable. *) apply paths_ind. (** The prism analog of the function [triangle_ind] from earlier in the file. To prove something about all prisms, it's enough to prove it for the "identity" prism. Note that we don't specialize to a prism concentrated on a single vertex, since sometimes we have to deal with a composite of two prisms. *)
P: Type
a, b, c: P
ab: a = b
ac: a = c
bc: b = c
abc: ab @ bc = ac
Q: forall (a' b' c' : P) (ab' : a' = b') (ac' : a' = c') (bc' : b' = c') (abc' : ab' @ bc' = ac') (k1 : a = a') (k2 : b = b') (k3 : c = c') (k12 : ab @ k2 = k1 @ ab') (k13 : ac @ k3 = k1 @ ac') (k23 : bc @ k3 = k2 @ bc'), prism abc abc' k12 k13 k23 -> Type
s: Q a b c ab ac bc abc 1 1 1 (equiv_p1_1q 1) (equiv_p1_1q 1) (equiv_p1_1q 1) (prism_id abc)

forall (a' b' c' : P) (ab' : a' = b') (ac' : a' = c') (bc' : b' = c') (abc' : ab' @ bc' = ac') (k1 : a = a') (k2 : b = b') (k3 : c = c') (k12 : ab @ k2 = k1 @ ab') (k13 : ac @ k3 = k1 @ ac') (k23 : bc @ k3 = k2 @ bc') (k123 : prism abc abc' k12 k13 k23), Q a' b' c' ab' ac' bc' abc' k1 k2 k3 k12 k13 k23 k123
P: Type
a, b, c: P
ab: a = b
ac: a = c
bc: b = c
abc: ab @ bc = ac
Q: forall (a' b' c' : P) (ab' : a' = b') (ac' : a' = c') (bc' : b' = c') (abc' : ab' @ bc' = ac') (k1 : a = a') (k2 : b = b') (k3 : c = c') (k12 : ab @ k2 = k1 @ ab') (k13 : ac @ k3 = k1 @ ac') (k23 : bc @ k3 = k2 @ bc'), prism abc abc' k12 k13 k23 -> Type
s: Q a b c ab ac bc abc 1 1 1 (equiv_p1_1q 1) (equiv_p1_1q 1) (equiv_p1_1q 1) (prism_id abc)

forall (a' b' c' : P) (ab' : a' = b') (ac' : a' = c') (bc' : b' = c') (abc' : ab' @ bc' = ac') (k1 : a = a') (k2 : b = b') (k3 : c = c') (k12 : ab @ k2 = k1 @ ab') (k13 : ac @ k3 = k1 @ ac') (k23 : bc @ k3 = k2 @ bc') (k123 : prism abc abc' k12 k13 k23), Q a' b' c' ab' ac' bc' abc' k1 k2 k3 k12 k13 k23 k123
P: Type
a, b, c: P
ab: a = b
ac: a = c
bc: b = c
abc: ab @ bc = ac
Q: forall (a' b' c' : P) (ab' : a' = b') (ac' : a' = c') (bc' : b' = c') (abc' : ab' @ bc' = ac') (k1 : a = a') (k2 : b = b') (k3 : c = c') (k12 : ab @ k2 = k1 @ ab') (k13 : ac @ k3 = k1 @ ac') (k23 : bc @ k3 = k2 @ bc'), prism abc abc' k12 k13 k23 -> Type
s: Q a b c ab ac bc abc 1 1 1 (equiv_p1_1q 1) (equiv_p1_1q 1) (equiv_p1_1q 1) (prism_id abc)
a', b', c': P
ab': a' = b'
ac': a' = c'
bc': b' = c'
abc': ab' @ bc' = ac'
k1: a = a'
k2: b = b'
k3: c = c'
k12: ab @ k2 = k1 @ ab'
k13: ac @ k3 = k1 @ ac'
k23: bc @ k3 = k2 @ bc'
k123: prism abc abc' k12 k13 k23

Q a' b' c' ab' ac' bc' abc' k1 k2 k3 k12 k13 k23 k123
P: Type
a, b, c: P
ab: a = b
ac: a = c
bc: b = c
abc: ab @ bc = ac
Q: forall (a' b' c' : P) (ab' : a' = b') (ac' : a' = c') (bc' : b' = c') (abc' : ab' @ bc' = ac') (k1 : a = a') (k2 : b = b') (k3 : c = c') (k12 : ab @ k2 = k1 @ ab') (k13 : ac @ k3 = k1 @ ac') (k23 : bc @ k3 = k2 @ bc'), prism abc abc' k12 k13 k23 -> Type
s: Q a b c ab ac bc abc 1 1 1 (equiv_p1_1q 1) (equiv_p1_1q 1) (equiv_p1_1q 1) (prism_id abc)
ab': a = b
ac': a = c
bc': b = c
abc': ab' @ bc' = ac'
k12: ab @ 1 = 1 @ ab'
k13: ac @ 1 = 1 @ ac'
k23: bc @ 1 = 1 @ bc'
k123: prism abc abc' k12 k13 k23

Q a b c ab' ac' bc' abc' 1 1 1 k12 k13 k23 k123
P: Type
a, b, c: P
ab: a = b
ac: a = c
bc: b = c
abc: ab @ bc = ac
Q: forall (a' b' c' : P) (ab' : a' = b') (ac' : a' = c') (bc' : b' = c') (abc' : ab' @ bc' = ac') (k1 : a = a') (k2 : b = b') (k3 : c = c') (k12 : ab @ k2 = k1 @ ab') (k13 : ac @ k3 = k1 @ ac') (k23 : bc @ k3 = k2 @ bc'), prism abc abc' k12 k13 k23 -> Type
s: Q a b c ab ac bc abc 1 1 1 (equiv_p1_1q 1) (equiv_p1_1q 1) (equiv_p1_1q 1) (prism_id abc)
ab': a = b
ac': a = c
bc': b = c
abc': ab' @ bc' = ac'
k12: ab @ 1 = 1 @ ab'
k13: ac @ 1 = 1 @ ac'
k23: bc @ 1 = 1 @ bc'

forall k123 : prism abc abc' k12 k13 k23, Q a b c ab' ac' bc' abc' 1 1 1 k12 k13 k23 k123
P: Type
a, b, c: P
ab: a = b
ac: a = c
bc: b = c
abc: ab @ bc = ac
Q: forall (a' b' c' : P) (ab' : a' = b') (ac' : a' = c') (bc' : b' = c') (abc' : ab' @ bc' = ac') (k1 : a = a') (k2 : b = b') (k3 : c = c') (k12 : ab @ k2 = k1 @ ab') (k13 : ac @ k3 = k1 @ ac') (k23 : bc @ k3 = k2 @ bc'), prism abc abc' k12 k13 k23 -> Type
s: Q a b c ab ac bc abc 1 1 1 (equiv_p1_1q 1) (equiv_p1_1q 1) (equiv_p1_1q 1) (prism_id abc)
ac': a = c
bc': b = c
abc': ab @ bc' = ac'
k13: ac @ 1 = 1 @ ac'
k23: bc @ 1 = 1 @ bc'

forall k123 : prism abc abc' (equiv_p1_1q 1) k13 k23, Q a b c ab ac' bc' abc' 1 1 1 (equiv_p1_1q 1) k13 k23 k123
P: Type
a, b, c: P
ab: a = b
ac: a = c
bc: b = c
abc: ab @ bc = ac
Q: forall (a' b' c' : P) (ab' : a' = b') (ac' : a' = c') (bc' : b' = c') (abc' : ab' @ bc' = ac') (k1 : a = a') (k2 : b = b') (k3 : c = c') (k12 : ab @ k2 = k1 @ ab') (k13 : ac @ k3 = k1 @ ac') (k23 : bc @ k3 = k2 @ bc'), prism abc abc' k12 k13 k23 -> Type
s: Q a b c ab ac bc abc 1 1 1 (equiv_p1_1q 1) (equiv_p1_1q 1) (equiv_p1_1q 1) (prism_id abc)
bc': b = c
abc': ab @ bc' = ac
k23: bc @ 1 = 1 @ bc'

forall k123 : prism abc abc' (equiv_p1_1q 1) (equiv_p1_1q 1) k23, Q a b c ab ac bc' abc' 1 1 1 (equiv_p1_1q 1) (equiv_p1_1q 1) k23 k123
P: Type
a, b, c: P
ab: a = b
ac: a = c
bc: b = c
abc: ab @ bc = ac
Q: forall (a' b' c' : P) (ab' : a' = b') (ac' : a' = c') (bc' : b' = c') (abc' : ab' @ bc' = ac') (k1 : a = a') (k2 : b = b') (k3 : c = c') (k12 : ab @ k2 = k1 @ ab') (k13 : ac @ k3 = k1 @ ac') (k23 : bc @ k3 = k2 @ bc'), prism abc abc' k12 k13 k23 -> Type
s: Q a b c ab ac bc abc 1 1 1 (equiv_p1_1q 1) (equiv_p1_1q 1) (equiv_p1_1q 1) (prism_id abc)
abc': ab @ bc = ac

forall k123 : prism abc abc' (equiv_p1_1q 1) (equiv_p1_1q 1) (equiv_p1_1q 1), Q a b c ab ac bc abc' 1 1 1 (equiv_p1_1q 1) (equiv_p1_1q 1) (equiv_p1_1q 1) k123
P: Type
a: P
Q: forall (a' b' c' : P) (ab' : a' = b') (ac' : a' = c') (bc' : b' = c') (abc' : ab' @ bc' = ac') (k1 : a = a') (k2 : a = b') (k3 : a = c') (k12 : 1 @ k2 = k1 @ ab') (k13 : 1 @ k3 = k1 @ ac') (k23 : 1 @ k3 = k2 @ bc'), prism 1 abc' k12 k13 k23 -> Type
s: Q a a a 1 1 1 1 1 1 1 1 1 1 1
abc': 1 = 1

forall k123 : prism 1 abc' 1 1 1, Q a a a 1 1 1 abc' 1 1 1 1 1 1 k123
P: Type
a: P
Q: forall (a' b' c' : P) (ab' : a' = b') (ac' : a' = c') (bc' : b' = c') (abc' : ab' @ bc' = ac') (k1 : a = a') (k2 : a = b') (k3 : a = c') (k12 : 1 @ k2 = k1 @ ab') (k13 : 1 @ k3 = k1 @ ac') (k23 : 1 @ k3 = k2 @ bc'), prism 1 abc' k12 k13 k23 -> Type
s: Q a a a 1 1 1 1 1 1 1 1 1 1 1
abc': 1 = 1

forall k123 : 1 = 1 @ whiskerL 1 abc', Q a a a 1 1 1 abc' 1 1 1 1 1 1 k123
P: Type
a: P
Q: forall (a' b' c' : P) (ab' : a' = b') (ac' : a' = c') (bc' : b' = c') (abc' : ab' @ bc' = ac') (k1 : a = a') (k2 : a = b') (k3 : a = c') (k12 : 1 @ k2 = k1 @ ab') (k13 : 1 @ k3 = k1 @ ac') (k23 : 1 @ k3 = k2 @ bc'), prism 1 abc' k12 k13 k23 -> Type
s: Q a a a 1 1 1 1 1 1 1 1 1 1 1
abc': 1 = 1
k123': 1 = abc'

Q a a a 1 1 1 abc' 1 1 1 1 1 1 (equiv_concat_r (concat_1p (whiskerL 1 abc') @ whiskerL_1p_1 abc')^ 1 k123')
P: Type
a: P
Q: forall (a' b' c' : P) (ab' : a' = b') (ac' : a' = c') (bc' : b' = c') (abc' : ab' @ bc' = ac') (k1 : a = a') (k2 : a = b') (k3 : a = c') (k12 : 1 @ k2 = k1 @ ab') (k13 : 1 @ k3 = k1 @ ac') (k23 : 1 @ k3 = k2 @ bc'), prism 1 abc' k12 k13 k23 -> Type
s: Q a a a 1 1 1 1 1 1 1 1 1 1 1

Q a a a 1 1 1 1 1 1 1 1 1 1 (equiv_concat_r (concat_1p (whiskerL 1 1) @ whiskerL_1p_1 1)^ 1 1)
P: Type
a: P
Q: forall (a' b' c' : P) (ab' : a' = b') (ac' : a' = c') (bc' : b' = c') (abc' : ab' @ bc' = ac') (k1 : a = a') (k2 : a = b') (k3 : a = c') (k12 : 1 @ k2 = k1 @ ab') (k13 : 1 @ k3 = k1 @ ac') (k23 : 1 @ k3 = k2 @ bc'), prism 1 abc' k12 k13 k23 -> Type
s: Q a a a 1 1 1 1 1 1 1 1 1 1 1

Q a a a 1 1 1 1 1 1 1 1 1 1 1
exact s. Defined. (** Use this with [f g : TriJoinRecData A B C P], [h : TriJoinRecPath f g] (so [g] is the *co*domain of [h]), [a : A], [b : B], [c : C]. *) Ltac prism_ind g h a b c := generalize_some h a b c; generalize_some g a b c; apply prism_ind. (** Use this with [f g : TriJoinRecData A B C P], [h : TriJoinRecPath f g] (so [g] is the *co*domain of [h]). Two of the arguments [a], [b] and [c] should be elements of [A], [B] and [C], respectively, and the third should be a dummy value (e.g. [_X_]) that causes the generalize tactic to fail. It applies to goals that only depend on the components of [g] and [h] involving just two of [A], [B] and [C]. So it is dealing with one square face of the prism. *) Ltac prism_ind_two g h a b c := generalize_some h a b c; generalize_some g a b c; apply square_ind. (* From Join/Core.v *) (** ** Use the WildCat library to organize things *) (** We begin by showing that [TriJoinRecData A B C P] is a 0-groupoid, one piece at a time. *) Global Instance isgraph_trijoinrecdata (A B C P : Type) : IsGraph (TriJoinRecData A B C P) := {| Hom := TriJoinRecPath |}.
A, B, C, P: Type

Is01Cat (TriJoinRecData A B C P)
A, B, C, P: Type

Is01Cat (TriJoinRecData A B C P)
A, B, C, P: Type

forall a : TriJoinRecData A B C P, a $-> a
A, B, C, P: Type
forall a b c : TriJoinRecData A B C P, (b $-> c) -> (a $-> b) -> a $-> c
A, B, C, P: Type

forall a : TriJoinRecData A B C P, a $-> a
A, B, C, P: Type
f: TriJoinRecData A B C P

f $-> f
A, B, C, P: Type
f: TriJoinRecData A B C P

forall (a : A) (b : B), j12' (unbundle_trijoinrecdata f) a b = j12' (unbundle_trijoinrecdata f) a b
A, B, C, P: Type
f: TriJoinRecData A B C P
forall (a : A) (c : C), j13' (unbundle_trijoinrecdata f) a c = j13' (unbundle_trijoinrecdata f) a c
A, B, C, P: Type
f: TriJoinRecData A B C P
forall (b : B) (c : C), j23' (unbundle_trijoinrecdata f) b c = j23' (unbundle_trijoinrecdata f) b c
A, B, C, P: Type
f: TriJoinRecData A B C P
forall (a : A) (b : B) (c : C), prism' (j123' (unbundle_trijoinrecdata f) a b c) (j123' (unbundle_trijoinrecdata f) a b c) (?h12' a b) (?h13' a c) (?h23' b c)
A, B, C, P: Type
f: TriJoinRecData A B C P

forall (a : A) (b : B) (c : C), prism' (j123' (unbundle_trijoinrecdata f) a b c) (j123' (unbundle_trijoinrecdata f) a b c) ((fun (a0 : A) (b0 : B) => 1) a b) ((fun (a0 : A) (c0 : C) => 1) a c) ((fun (b0 : B) (c0 : C) => 1) b c)
A, B, C, P: Type
f: TriJoinRecData A B C P
a: A
b: B
c: C

prism' (j123' (unbundle_trijoinrecdata f) a b c) (j123' (unbundle_trijoinrecdata f) a b c) 1 1 1
(* Can finish with: [by triangle_ind f a b c.] *)
A, B, C, P: Type
f: TriJoinRecData A B C P
a: A
b: B
c: C

j123' (unbundle_trijoinrecdata f) a b c @ 1 = (1 @@ 1) @ j123' (unbundle_trijoinrecdata f) a b c
A, B, C, P: Type
f: TriJoinRecData A B C P
a: A
b: B
c: C

j123 f a b c @ 1 = 1 @ j123 f a b c
apply concat_p1_1p.
A, B, C, P: Type

forall a b c : TriJoinRecData A B C P, (b $-> c) -> (a $-> b) -> a $-> c
A, B, C, P: Type
f1, f2, f3: TriJoinRecData A B C P
k2: f2 $-> f3
k1: f1 $-> f2

f1 $-> f3
A, B, C, P: Type
f1, f2, f3: TriJoinRecData A B C P
k2: f2 $-> f3
k1: f1 $-> f2
a: A

j1 f1 a = j1 f3 a
A, B, C, P: Type
f1, f2, f3: TriJoinRecData A B C P
k2: f2 $-> f3
k1: f1 $-> f2
b: B
j2 f1 b = j2 f3 b
A, B, C, P: Type
f1, f2, f3: TriJoinRecData A B C P
k2: f2 $-> f3
k1: f1 $-> f2
c: C
j3 f1 c = j3 f3 c
A, B, C, P: Type
f1, f2, f3: TriJoinRecData A B C P
k2: f2 $-> f3
k1: f1 $-> f2
a: A
b: B
j12 f1 a b @ ?Goal0 = ?Goal @ j12 f3 a b
A, B, C, P: Type
f1, f2, f3: TriJoinRecData A B C P
k2: f2 $-> f3
k1: f1 $-> f2
a: A
c: C
j13 f1 a c @ ?Goal1 = ?Goal @ j13 f3 a c
A, B, C, P: Type
f1, f2, f3: TriJoinRecData A B C P
k2: f2 $-> f3
k1: f1 $-> f2
b: B
c: C
j23 f1 b c @ ?Goal1 = ?Goal0 @ j23 f3 b c
A, B, C, P: Type
f1, f2, f3: TriJoinRecData A B C P
k2: f2 $-> f3
k1: f1 $-> f2
a: A
b: B
c: C
prism (j123 f1 a b c) (j123 f3 a b c) ?Goal2 ?Goal3 ?Goal4
A, B, C, P: Type
f1, f2, f3: TriJoinRecData A B C P
k2: f2 $-> f3
k1: f1 $-> f2
a: A

j1 f1 a = j1 f3 a
exact (h1 k1 a @ h1 k2 a).
A, B, C, P: Type
f1, f2, f3: TriJoinRecData A B C P
k2: f2 $-> f3
k1: f1 $-> f2
b: B

j2 f1 b = j2 f3 b
exact (h2 k1 b @ h2 k2 b).
A, B, C, P: Type
f1, f2, f3: TriJoinRecData A B C P
k2: f2 $-> f3
k1: f1 $-> f2
c: C

j3 f1 c = j3 f3 c
exact (h3 k1 c @ h3 k2 c).
A, B, C, P: Type
f1, f2, f3: TriJoinRecData A B C P
k2: f2 $-> f3
k1: f1 $-> f2
a: A
b: B

j12 f1 a b @ (h2 k1 b @ h2 k2 b) = (h1 k1 a @ h1 k2 a) @ j12 f3 a b
A, B, C, P: Type
f1, f2: TriJoinRecData A B C P
k1: f1 $-> f2
a: A
b: B

j12 f1 a b @ (h2 k1 b @ 1) = (h1 k1 a @ 1) @ j12 f2 a b
A, B, C, P: Type
f1: TriJoinRecData A B C P
a: A
b: B

j12 f1 a b @ (1 @ 1) = (1 @ 1) @ j12 f1 a b
by triangle_ind_two f1 a b _X_.
A, B, C, P: Type
f1, f2, f3: TriJoinRecData A B C P
k2: f2 $-> f3
k1: f1 $-> f2
a: A
c: C

j13 f1 a c @ (h3 k1 c @ h3 k2 c) = (h1 k1 a @ h1 k2 a) @ j13 f3 a c
A, B, C, P: Type
f1, f2: TriJoinRecData A B C P
k1: f1 $-> f2
a: A
c: C

j13 f1 a c @ (h3 k1 c @ 1) = (h1 k1 a @ 1) @ j13 f2 a c
A, B, C, P: Type
f1: TriJoinRecData A B C P
a: A
c: C

j13 f1 a c @ (1 @ 1) = (1 @ 1) @ j13 f1 a c
by triangle_ind_two f1 a _X_ c.
A, B, C, P: Type
f1, f2, f3: TriJoinRecData A B C P
k2: f2 $-> f3
k1: f1 $-> f2
b: B
c: C

j23 f1 b c @ (h3 k1 c @ h3 k2 c) = (h2 k1 b @ h2 k2 b) @ j23 f3 b c
A, B, C, P: Type
f1, f2: TriJoinRecData A B C P
k1: f1 $-> f2
b: B
c: C

j23 f1 b c @ (h3 k1 c @ 1) = (h2 k1 b @ 1) @ j23 f2 b c
A, B, C, P: Type
f1: TriJoinRecData A B C P
b: B
c: C

j23 f1 b c @ (1 @ 1) = (1 @ 1) @ j23 f1 b c
by triangle_ind_two f1 _X_ b c.
A, B, C, P: Type
f1, f2, f3: TriJoinRecData A B C P
k2: f2 $-> f3
k1: f1 $-> f2
a: A
b: B
c: C

prism (j123 f1 a b c) (j123 f3 a b c) ((fun (H : forall a : A, j1 f2 a = j1 f3 a) (H0 : forall b : B, j2 f2 b = j2 f3 b) (H1 : forall c : C, j3 f2 c = j3 f3 c) (H2 : forall (a : A) (b : B), j12 f2 a b @ H0 b = H a @ j12 f3 a b) (H3 : forall (a : A) (c : C), j13 f2 a c @ H1 c = H a @ j13 f3 a c) (H4 : forall (b : B) (c : C), j23 f2 b c @ H1 c = H0 b @ j23 f3 b c) (H5 : forall (a : A) (b : B) (c : C), prism (j123 f2 a b c) (j123 f3 a b c) (H2 a b) (H3 a c) (H4 b c)) => (fun (H6 : A -> P) (H7 : B -> P) (H8 : C -> P) (H9 : forall (a : A) (b : B), H6 a = H7 b) (H10 : forall (a : A) (c : C), H6 a = H8 c) (H11 : forall (b : B) (c : C), H7 b = H8 c) (H12 : forall (a : A) (b : B) (c : C), H9 a b @ H11 b c = H10 a c) => square_ind (j1 f2 a) (j2 f2 b) (j12 f2 a b) (fun (a' b' : P) (ab' : a' = b') (ha : j1 f2 a = a') (hb : j2 f2 b = b') (_ : j12 f2 a b @ hb = ha @ ab') => j12 f1 a b @ (h2 k1 b @ hb) = (h1 k1 a @ ha) @ ab') ((fun (H13 : forall a : A, j1 f1 a = j1 f2 a) (H14 : forall b : B, j2 f1 b = j2 f2 b) (H15 : forall c : C, j3 f1 c = j3 f2 c) (H16 : forall (a : A) (b : B), j12 f1 a b @ H14 b = H13 a @ j12 f2 a b) (H17 : forall (a : A) (c : C), j13 f1 a c @ H15 c = H13 a @ j13 f2 a c) (H18 : forall (b : B) (c : C), j23 f1 b c @ H15 c = H14 b @ j23 f2 b c) (H19 : forall (a : A) (b : B) (c : C), prism (j123 f1 a b c) (j123 f2 a b c) (H16 a b) (H17 a c) (H18 b c)) => (fun (H20 : A -> P) (H21 : B -> P) (H22 : C -> P) (H23 : forall (a : A) (b : B), H20 a = H21 b) (H24 : forall (a : A) (c : C), H20 a = H22 c) (H25 : forall (b : B) (c : C), H21 b = H22 c) (H26 : forall (a : A) (b : B) (c : C), H23 a b @ H25 b c = H24 a c) => square_ind (j1 f1 a) (j2 f1 b) (j12 f1 a b) (fun (a' b' : P) (ab' : a' = b') (ha : j1 f1 a = a') (hb : j2 f1 b = b') (_ : ... @ hb = ha @ ab') => j12 f1 a b @ (hb @ 1) = (ha @ 1) @ ab') ((fun (H27 : ...) (H28 : ...) (H29 : ...) (H30 : ...) (H31 : ...) (H32 : ...) (H33 : ...) => ... ... ... ... : ... = ...) (j1 f1) (j2 f1) (j3 f1) (j12 f1) (j13 f1) (j23 f1) (j123 f1)) (H20 a) (H21 b) (H23 a b) : forall (p : j1 f1 a = j1 {| j1 := H20; j2 := H21; j3 := H22; j12 := H23; j13 := H24; j23 := H25; j123 := H26 |} a) (p0 : j2 f1 b = j2 {| j1 := H20; j2 := H21; j3 := H22; j12 := H23; j13 := H24; j23 := H25; j123 := H26 |} b), j12 f1 a b @ p0 = p @ j12 {| ...; ...; ...; ...; ...; ...; ... |} a b -> j12 f1 a b @ (p0 @ 1) = (p @ 1) @ j12 {| ...; ...; ...; ...; ...; ...; ... |} a b) (j1 f2) (j2 f2) (j3 f2) (j12 f2) (j13 f2) (j23 f2) (j123 f2) (H13 a) (H14 b) (H16 a b) : j12 f1 a b @ (h2 {| h1 := H13; h2 := H14; h3 := H15; h12 := H16; h13 := H17; h23 := H18; h123 := H19 |} b @ 1) = (h1 {| h1 := H13; h2 := H14; h3 := H15; h12 := H16; h13 := H17; h23 := H18; h123 := H19 |} a @ 1) @ j12 f2 a b) (h1 k1) (h2 k1) (h3 k1) (h12 k1) (h13 k1) (h23 k1) (h123 k1)) (H6 a) (H7 b) (H9 a b) : forall (p : j1 f2 a = j1 {| j1 := H6; j2 := H7; j3 := H8; j12 := H9; j13 := H10; j23 := H11; j123 := H12 |} a) (p0 : j2 f2 b = j2 {| j1 := H6; j2 := H7; j3 := H8; j12 := H9; j13 := H10; j23 := H11; j123 := H12 |} b), j12 f2 a b @ p0 = p @ j12 {| j1 := H6; j2 := H7; j3 := H8; j12 := H9; j13 := H10; j23 := H11; j123 := H12 |} a b -> j12 f1 a b @ (h2 k1 b @ p0) = (h1 k1 a @ p) @ j12 {| j1 := H6; j2 := H7; j3 := H8; j12 := H9; j13 := H10; j23 := H11; j123 := H12 |} a b) (j1 f3) (j2 f3) (j3 f3) (j12 f3) (j13 f3) (j23 f3) (j123 f3) (H a) (H0 b) (H2 a b) : j12 f1 a b @ (h2 k1 b @ h2 {| h1 := H; h2 := H0; h3 := H1; h12 := H2; h13 := H3; h23 := H4; h123 := H5 |} b) = (h1 k1 a @ h1 {| h1 := H; h2 := H0; h3 := H1; h12 := H2; h13 := H3; h23 := H4; h123 := H5 |} a) @ j12 f3 a b) (h1 k2) (h2 k2) (h3 k2) (h12 k2) (h13 k2) (h23 k2) (h123 k2)) ((fun (H : forall a : A, j1 f2 a = j1 f3 a) (H0 : forall b : B, j2 f2 b = j2 f3 b) (H1 : forall c : C, j3 f2 c = j3 f3 c) (H2 : forall (a : A) (b : B), j12 f2 a b @ H0 b = H a @ j12 f3 a b) (H3 : forall (a : A) (c : C), j13 f2 a c @ H1 c = H a @ j13 f3 a c) (H4 : forall (b : B) (c : C), j23 f2 b c @ H1 c = H0 b @ j23 f3 b c) (H5 : forall (a : A) (b : B) (c : C), prism (j123 f2 a b c) (j123 f3 a b c) (H2 a b) (H3 a c) (H4 b c)) => (fun (H6 : A -> P) (H7 : B -> P) (H8 : C -> P) (H9 : forall (a : A) (b : B), H6 a = H7 b) (H10 : forall (a : A) (c : C), H6 a = H8 c) (H11 : forall (b : B) (c : C), H7 b = H8 c) (H12 : forall (a : A) (b : B) (c : C), H9 a b @ H11 b c = H10 a c) => square_ind (j1 f2 a) (j3 f2 c) (j13 f2 a c) (fun (a' b' : P) (ab' : a' = b') (ha : j1 f2 a = a') (hb : j3 f2 c = b') (_ : j13 f2 a c @ hb = ha @ ab') => j13 f1 a c @ (h3 k1 c @ hb) = (h1 k1 a @ ha) @ ab') ((fun (H13 : forall a : A, j1 f1 a = j1 f2 a) (H14 : forall b : B, j2 f1 b = j2 f2 b) (H15 : forall c : C, j3 f1 c = j3 f2 c) (H16 : forall (a : A) (b : B), j12 f1 a b @ H14 b = H13 a @ j12 f2 a b) (H17 : forall (a : A) (c : C), j13 f1 a c @ H15 c = H13 a @ j13 f2 a c) (H18 : forall (b : B) (c : C), j23 f1 b c @ H15 c = H14 b @ j23 f2 b c) (H19 : forall (a : A) (b : B) (c : C), prism (j123 f1 a b c) (j123 f2 a b c) (H16 a b) (H17 a c) (H18 b c)) => (fun (H20 : A -> P) (H21 : B -> P) (H22 : C -> P) (H23 : forall (a : A) (b : B), H20 a = H21 b) (H24 : forall (a : A) (c : C), H20 a = H22 c) (H25 : forall (b : B) (c : C), H21 b = H22 c) (H26 : forall (a : A) (b : B) (c : C), H23 a b @ H25 b c = H24 a c) => square_ind (j1 f1 a) (j3 f1 c) (j13 f1 a c) (fun (a' b' : P) (ab' : a' = b') (ha : j1 f1 a = a') (hb : j3 f1 c = b') (_ : ... @ hb = ha @ ab') => j13 f1 a c @ (hb @ 1) = (ha @ 1) @ ab') ((fun (H27 : ...) (H28 : ...) (H29 : ...) (H30 : ...) (H31 : ...) (H32 : ...) (H33 : ...) => ... ... ... ... : ... = ...) (j1 f1) (j2 f1) (j3 f1) (j12 f1) (j13 f1) (j23 f1) (j123 f1)) (H20 a) (H22 c) (H24 a c) : forall (p : j1 f1 a = j1 {| j1 := H20; j2 := H21; j3 := H22; j12 := H23; j13 := H24; j23 := H25; j123 := H26 |} a) (p0 : j3 f1 c = j3 {| j1 := H20; j2 := H21; j3 := H22; j12 := H23; j13 := H24; j23 := H25; j123 := H26 |} c), j13 f1 a c @ p0 = p @ j13 {| ...; ...; ...; ...; ...; ...; ... |} a c -> j13 f1 a c @ (p0 @ 1) = (p @ 1) @ j13 {| ...; ...; ...; ...; ...; ...; ... |} a c) (j1 f2) (j2 f2) (j3 f2) (j12 f2) (j13 f2) (j23 f2) (j123 f2) (H13 a) (H15 c) (H17 a c) : j13 f1 a c @ (h3 {| h1 := H13; h2 := H14; h3 := H15; h12 := H16; h13 := H17; h23 := H18; h123 := H19 |} c @ 1) = (h1 {| h1 := H13; h2 := H14; h3 := H15; h12 := H16; h13 := H17; h23 := H18; h123 := H19 |} a @ 1) @ j13 f2 a c) (h1 k1) (h2 k1) (h3 k1) (h12 k1) (h13 k1) (h23 k1) (h123 k1)) (H6 a) (H8 c) (H10 a c) : forall (p : j1 f2 a = j1 {| j1 := H6; j2 := H7; j3 := H8; j12 := H9; j13 := H10; j23 := H11; j123 := H12 |} a) (p0 : j3 f2 c = j3 {| j1 := H6; j2 := H7; j3 := H8; j12 := H9; j13 := H10; j23 := H11; j123 := H12 |} c), j13 f2 a c @ p0 = p @ j13 {| j1 := H6; j2 := H7; j3 := H8; j12 := H9; j13 := H10; j23 := H11; j123 := H12 |} a c -> j13 f1 a c @ (h3 k1 c @ p0) = (h1 k1 a @ p) @ j13 {| j1 := H6; j2 := H7; j3 := H8; j12 := H9; j13 := H10; j23 := H11; j123 := H12 |} a c) (j1 f3) (j2 f3) (j3 f3) (j12 f3) (j13 f3) (j23 f3) (j123 f3) (H a) (H1 c) (H3 a c) : j13 f1 a c @ (h3 k1 c @ h3 {| h1 := H; h2 := H0; h3 := H1; h12 := H2; h13 := H3; h23 := H4; h123 := H5 |} c) = (h1 k1 a @ h1 {| h1 := H; h2 := H0; h3 := H1; h12 := H2; h13 := H3; h23 := H4; h123 := H5 |} a) @ j13 f3 a c) (h1 k2) (h2 k2) (h3 k2) (h12 k2) (h13 k2) (h23 k2) (h123 k2)) ((fun (H : forall a : A, j1 f2 a = j1 f3 a) (H0 : forall b : B, j2 f2 b = j2 f3 b) (H1 : forall c : C, j3 f2 c = j3 f3 c) (H2 : forall (a : A) (b : B), j12 f2 a b @ H0 b = H a @ j12 f3 a b) (H3 : forall (a : A) (c : C), j13 f2 a c @ H1 c = H a @ j13 f3 a c) (H4 : forall (b : B) (c : C), j23 f2 b c @ H1 c = H0 b @ j23 f3 b c) (H5 : forall (a : A) (b : B) (c : C), prism (j123 f2 a b c) (j123 f3 a b c) (H2 a b) (H3 a c) (H4 b c)) => (fun (H6 : A -> P) (H7 : B -> P) (H8 : C -> P) (H9 : forall (a : A) (b : B), H6 a = H7 b) (H10 : forall (a : A) (c : C), H6 a = H8 c) (H11 : forall (b : B) (c : C), H7 b = H8 c) (H12 : forall (a : A) (b : B) (c : C), H9 a b @ H11 b c = H10 a c) => square_ind (j2 f2 b) (j3 f2 c) (j23 f2 b c) (fun (a' b' : P) (ab' : a' = b') (ha : j2 f2 b = a') (hb : j3 f2 c = b') (_ : j23 f2 b c @ hb = ha @ ab') => j23 f1 b c @ (h3 k1 c @ hb) = (h2 k1 b @ ha) @ ab') ((fun (H13 : forall a : A, j1 f1 a = j1 f2 a) (H14 : forall b : B, j2 f1 b = j2 f2 b) (H15 : forall c : C, j3 f1 c = j3 f2 c) (H16 : forall (a : A) (b : B), j12 f1 a b @ H14 b = H13 a @ j12 f2 a b) (H17 : forall (a : A) (c : C), j13 f1 a c @ H15 c = H13 a @ j13 f2 a c) (H18 : forall (b : B) (c : C), j23 f1 b c @ H15 c = H14 b @ j23 f2 b c) (H19 : forall (a : A) (b : B) (c : C), prism (j123 f1 a b c) (j123 f2 a b c) (H16 a b) (H17 a c) (H18 b c)) => (fun (H20 : A -> P) (H21 : B -> P) (H22 : C -> P) (H23 : forall (a : A) (b : B), H20 a = H21 b) (H24 : forall (a : A) (c : C), H20 a = H22 c) (H25 : forall (b : B) (c : C), H21 b = H22 c) (H26 : forall (a : A) (b : B) (c : C), H23 a b @ H25 b c = H24 a c) => square_ind (j2 f1 b) (j3 f1 c) (j23 f1 b c) (fun (a' b' : P) (ab' : a' = b') (ha : j2 f1 b = a') (hb : j3 f1 c = b') (_ : ... @ hb = ha @ ab') => j23 f1 b c @ (hb @ 1) = (ha @ 1) @ ab') ((fun (H27 : ...) (H28 : ...) (H29 : ...) (H30 : ...) (H31 : ...) (H32 : ...) (H33 : ...) => ... ... ... ... : ... = ...) (j1 f1) (j2 f1) (j3 f1) (j12 f1) (j13 f1) (j23 f1) (j123 f1)) (H21 b) (H22 c) (H25 b c) : forall (p : j2 f1 b = j2 {| j1 := H20; j2 := H21; j3 := H22; j12 := H23; j13 := H24; j23 := H25; j123 := H26 |} b) (p0 : j3 f1 c = j3 {| j1 := H20; j2 := H21; j3 := H22; j12 := H23; j13 := H24; j23 := H25; j123 := H26 |} c), j23 f1 b c @ p0 = p @ j23 {| ...; ...; ...; ...; ...; ...; ... |} b c -> j23 f1 b c @ (p0 @ 1) = (p @ 1) @ j23 {| ...; ...; ...; ...; ...; ...; ... |} b c) (j1 f2) (j2 f2) (j3 f2) (j12 f2) (j13 f2) (j23 f2) (j123 f2) (H14 b) (H15 c) (H18 b c) : j23 f1 b c @ (h3 {| h1 := H13; h2 := H14; h3 := H15; h12 := H16; h13 := H17; h23 := H18; h123 := H19 |} c @ 1) = (h2 {| h1 := H13; h2 := H14; h3 := H15; h12 := H16; h13 := H17; h23 := H18; h123 := H19 |} b @ 1) @ j23 f2 b c) (h1 k1) (h2 k1) (h3 k1) (h12 k1) (h13 k1) (h23 k1) (h123 k1)) (H7 b) (H8 c) (H11 b c) : forall (p : j2 f2 b = j2 {| j1 := H6; j2 := H7; j3 := H8; j12 := H9; j13 := H10; j23 := H11; j123 := H12 |} b) (p0 : j3 f2 c = j3 {| j1 := H6; j2 := H7; j3 := H8; j12 := H9; j13 := H10; j23 := H11; j123 := H12 |} c), j23 f2 b c @ p0 = p @ j23 {| j1 := H6; j2 := H7; j3 := H8; j12 := H9; j13 := H10; j23 := H11; j123 := H12 |} b c -> j23 f1 b c @ (h3 k1 c @ p0) = (h2 k1 b @ p) @ j23 {| j1 := H6; j2 := H7; j3 := H8; j12 := H9; j13 := H10; j23 := H11; j123 := H12 |} b c) (j1 f3) (j2 f3) (j3 f3) (j12 f3) (j13 f3) (j23 f3) (j123 f3) (H0 b) (H1 c) (H4 b c) : j23 f1 b c @ (h3 k1 c @ h3 {| h1 := H; h2 := H0; h3 := H1; h12 := H2; h13 := H3; h23 := H4; h123 := H5 |} c) = (h2 k1 b @ h2 {| h1 := H; h2 := H0; h3 := H1; h12 := H2; h13 := H3; h23 := H4; h123 := H5 |} b) @ j23 f3 b c) (h1 k2) (h2 k2) (h3 k2) (h12 k2) (h13 k2) (h23 k2) (h123 k2))
A, B, C, P: Type
f1, f2, f3: TriJoinRecData A B C P
k2: f2 $-> f3
k1: f1 $-> f2
a: A
b: B
c: C

prism (j123 f1 a b c) (j123 f3 a b c) (square_ind (j1 f2 a) (j2 f2 b) (j12 f2 a b) (fun (a' b' : P) (ab' : a' = b') (ha : j1 f2 a = a') (hb : j2 f2 b = b') (_ : j12 f2 a b @ hb = ha @ ab') => j12 f1 a b @ (h2 k1 b @ hb) = (h1 k1 a @ ha) @ ab') (square_ind (j1 f1 a) (j2 f1 b) (j12 f1 a b) (fun (a' b' : P) (ab' : a' = b') (ha : j1 f1 a = a') (hb : j2 f1 b = b') (_ : j12 f1 a b @ hb = ha @ ab') => j12 f1 a b @ (hb @ 1) = (ha @ 1) @ ab') (paths_ind (j1 f1 a) (fun (y : P) (p : j1 f1 a = y) => p @ 1 = 1 @ p) 1 (j2 f1 b) (j12 f1 a b)) (j1 f2 a) (j2 f2 b) (j12 f2 a b) (h1 k1 a) (h2 k1 b) (h12 k1 a b)) (j1 f3 a) (j2 f3 b) (j12 f3 a b) (h1 k2 a) (h2 k2 b) (h12 k2 a b)) (square_ind (j1 f2 a) (j3 f2 c) (j13 f2 a c) (fun (a' b' : P) (ab' : a' = b') (ha : j1 f2 a = a') (hb : j3 f2 c = b') (_ : j13 f2 a c @ hb = ha @ ab') => j13 f1 a c @ (h3 k1 c @ hb) = (h1 k1 a @ ha) @ ab') (square_ind (j1 f1 a) (j3 f1 c) (j13 f1 a c) (fun (a' b' : P) (ab' : a' = b') (ha : j1 f1 a = a') (hb : j3 f1 c = b') (_ : j13 f1 a c @ hb = ha @ ab') => j13 f1 a c @ (hb @ 1) = (ha @ 1) @ ab') (paths_ind (j1 f1 a) (fun (y : P) (p : j1 f1 a = y) => p @ 1 = 1 @ p) 1 (j3 f1 c) (j13 f1 a c)) (j1 f2 a) (j3 f2 c) (j13 f2 a c) (h1 k1 a) (h3 k1 c) (h13 k1 a c)) (j1 f3 a) (j3 f3 c) (j13 f3 a c) (h1 k2 a) (h3 k2 c) (h13 k2 a c)) (square_ind (j2 f2 b) (j3 f2 c) (j23 f2 b c) (fun (a' b' : P) (ab' : a' = b') (ha : j2 f2 b = a') (hb : j3 f2 c = b') (_ : j23 f2 b c @ hb = ha @ ab') => j23 f1 b c @ (h3 k1 c @ hb) = (h2 k1 b @ ha) @ ab') (square_ind (j2 f1 b) (j3 f1 c) (j23 f1 b c) (fun (a' b' : P) (ab' : a' = b') (ha : j2 f1 b = a') (hb : j3 f1 c = b') (_ : j23 f1 b c @ hb = ha @ ab') => j23 f1 b c @ (hb @ 1) = (ha @ 1) @ ab') (paths_ind (j2 f1 b) (fun (y : P) (p : j2 f1 b = y) => p @ 1 = 1 @ p) 1 (j3 f1 c) (j23 f1 b c)) (j2 f2 b) (j3 f2 c) (j23 f2 b c) (h2 k1 b) (h3 k1 c) (h23 k1 b c)) (j2 f3 b) (j3 f3 c) (j23 f3 b c) (h2 k2 b) (h3 k2 c) (h23 k2 b c))
A, B, C, P: Type
f1, f2: TriJoinRecData A B C P
k1: f1 $-> f2
a: A
b: B
c: C

prism (j123 f1 a b c) (j123 f2 a b c) (square_ind (j1 f2 a) (j2 f2 b) (j12 f2 a b) (fun (a' b' : P) (ab' : a' = b') (ha : j1 f2 a = a') (hb : j2 f2 b = b') (_ : j12 f2 a b @ hb = ha @ ab') => j12 f1 a b @ (h2 k1 b @ hb) = (h1 k1 a @ ha) @ ab') (square_ind (j1 f1 a) (j2 f1 b) (j12 f1 a b) (fun (a' b' : P) (ab' : a' = b') (ha : j1 f1 a = a') (hb : j2 f1 b = b') (_ : j12 f1 a b @ hb = ha @ ab') => j12 f1 a b @ (hb @ 1) = (ha @ 1) @ ab') (paths_ind (j1 f1 a) (fun (y : P) (p : j1 f1 a = y) => p @ 1 = 1 @ p) 1 (j2 f1 b) (j12 f1 a b)) (j1 f2 a) (j2 f2 b) (j12 f2 a b) (h1 k1 a) (h2 k1 b) (h12 k1 a b)) (j1 f2 a) (j2 f2 b) (j12 f2 a b) 1 1 (equiv_p1_1q 1)) (square_ind (j1 f2 a) (j3 f2 c) (j13 f2 a c) (fun (a' b' : P) (ab' : a' = b') (ha : j1 f2 a = a') (hb : j3 f2 c = b') (_ : j13 f2 a c @ hb = ha @ ab') => j13 f1 a c @ (h3 k1 c @ hb) = (h1 k1 a @ ha) @ ab') (square_ind (j1 f1 a) (j3 f1 c) (j13 f1 a c) (fun (a' b' : P) (ab' : a' = b') (ha : j1 f1 a = a') (hb : j3 f1 c = b') (_ : j13 f1 a c @ hb = ha @ ab') => j13 f1 a c @ (hb @ 1) = (ha @ 1) @ ab') (paths_ind (j1 f1 a) (fun (y : P) (p : j1 f1 a = y) => p @ 1 = 1 @ p) 1 (j3 f1 c) (j13 f1 a c)) (j1 f2 a) (j3 f2 c) (j13 f2 a c) (h1 k1 a) (h3 k1 c) (h13 k1 a c)) (j1 f2 a) (j3 f2 c) (j13 f2 a c) 1 1 (equiv_p1_1q 1)) (square_ind (j2 f2 b) (j3 f2 c) (j23 f2 b c) (fun (a' b' : P) (ab' : a' = b') (ha : j2 f2 b = a') (hb : j3 f2 c = b') (_ : j23 f2 b c @ hb = ha @ ab') => j23 f1 b c @ (h3 k1 c @ hb) = (h2 k1 b @ ha) @ ab') (square_ind (j2 f1 b) (j3 f1 c) (j23 f1 b c) (fun (a' b' : P) (ab' : a' = b') (ha : j2 f1 b = a') (hb : j3 f1 c = b') (_ : j23 f1 b c @ hb = ha @ ab') => j23 f1 b c @ (hb @ 1) = (ha @ 1) @ ab') (paths_ind (j2 f1 b) (fun (y : P) (p : j2 f1 b = y) => p @ 1 = 1 @ p) 1 (j3 f1 c) (j23 f1 b c)) (j2 f2 b) (j3 f2 c) (j23 f2 b c) (h2 k1 b) (h3 k1 c) (h23 k1 b c)) (j2 f2 b) (j3 f2 c) (j23 f2 b c) 1 1 (equiv_p1_1q 1))
A, B, C, P: Type
f1: TriJoinRecData A B C P
a: A
b: B
c: C

prism (j123 f1 a b c) (j123 f1 a b c) (equiv_ind (fun r : j12 f1 a b = j12 f1 a b => (concat_p1 (j12 f1 a b) @ r) @ (concat_1p (j12 f1 a b))^) (fun _ : j12 f1 a b @ 1 = 1 @ j12 f1 a b => j12 f1 a b @ (1 @ 1) = (1 @ 1) @ j12 f1 a b) (fun k' : j12 f1 a b = j12 f1 a b => match k' in (_ = p) return (j12 f1 a b @ (1 @ 1) = (1 @ 1) @ p) with | 1 => match j12 f1 a b as p0 in (_ = p) return (forall Q : forall (a' b' : P) (ab' : a' = b') (ha : j1 f1 a = a') (hb : p = b'), p0 @ hb = ha @ ab' -> Type, Q (j1 f1 a) p p0 1 1 ((concat_p1 p0 @ 1) @ (concat_1p p0)^) -> Q (j1 f1 a) p p0 1 1 ((concat_p1 p0 @ 1) @ (concat_1p p0)^)) with | 1 => fun Q : forall (a' b' : P) (ab' : a' = b') (ha : j1 f1 a = a') (hb : j1 f1 a = b'), 1 @ hb = ha @ ab' -> Type => idmap end (fun (a' b' : P) (ab' : a' = b') (ha : j1 f1 a = a') (hb : j2 f1 b = b') (_ : j12 f1 a b @ hb = ha @ ab') => j12 f1 a b @ (1 @ hb) = (1 @ ha) @ ab') (square_ind (j1 f1 a) (j2 f1 b) (j12 f1 a b) (fun (a' b' : P) (ab' : a' = b') (ha : j1 f1 a = a') (hb : j2 f1 b = b') (_ : j12 f1 a b @ hb = ha @ ab') => j12 f1 a b @ (hb @ 1) = (ha @ 1) @ ab') (paths_ind (j1 f1 a) (fun (y : P) (p : j1 f1 a = y) => p @ 1 = 1 @ p) 1 (j2 f1 b) (j12 f1 a b)) (j1 f1 a) (j2 f1 b) (j12 f1 a b) 1 1 (equiv_p1_1q 1)) end) ((concat_p1 (j12 f1 a b) @ 1) @ (concat_1p (j12 f1 a b))^)) (equiv_ind (fun r : j13 f1 a c = j13 f1 a c => (concat_p1 (j13 f1 a c) @ r) @ (concat_1p (j13 f1 a c))^) (fun _ : j13 f1 a c @ 1 = 1 @ j13 f1 a c => j13 f1 a c @ (1 @ 1) = (1 @ 1) @ j13 f1 a c) (fun k' : j13 f1 a c = j13 f1 a c => match k' in (_ = p) return (j13 f1 a c @ (1 @ 1) = (1 @ 1) @ p) with | 1 => match j13 f1 a c as p0 in (_ = p) return (forall Q : forall (a' b' : P) (ab' : a' = b') (ha : j1 f1 a = a') (hb : p = b'), p0 @ hb = ha @ ab' -> Type, Q (j1 f1 a) p p0 1 1 ((concat_p1 p0 @ 1) @ (concat_1p p0)^) -> Q (j1 f1 a) p p0 1 1 ((concat_p1 p0 @ 1) @ (concat_1p p0)^)) with | 1 => fun Q : forall (a' b' : P) (ab' : a' = b') (ha : j1 f1 a = a') (hb : j1 f1 a = b'), 1 @ hb = ha @ ab' -> Type => idmap end (fun (a' b' : P) (ab' : a' = b') (ha : j1 f1 a = a') (hb : j3 f1 c = b') (_ : j13 f1 a c @ hb = ha @ ab') => j13 f1 a c @ (1 @ hb) = (1 @ ha) @ ab') (square_ind (j1 f1 a) (j3 f1 c) (j13 f1 a c) (fun (a' b' : P) (ab' : a' = b') (ha : j1 f1 a = a') (hb : j3 f1 c = b') (_ : j13 f1 a c @ hb = ha @ ab') => j13 f1 a c @ (hb @ 1) = (ha @ 1) @ ab') (paths_ind (j1 f1 a) (fun (y : P) (p : j1 f1 a = y) => p @ 1 = 1 @ p) 1 (j3 f1 c) (j13 f1 a c)) (j1 f1 a) (j3 f1 c) (j13 f1 a c) 1 1 (equiv_p1_1q 1)) end) ((concat_p1 (j13 f1 a c) @ 1) @ (concat_1p (j13 f1 a c))^)) (equiv_ind (fun r : j23 f1 b c = j23 f1 b c => (concat_p1 (j23 f1 b c) @ r) @ (concat_1p (j23 f1 b c))^) (fun _ : j23 f1 b c @ 1 = 1 @ j23 f1 b c => j23 f1 b c @ (1 @ 1) = (1 @ 1) @ j23 f1 b c) (fun k' : j23 f1 b c = j23 f1 b c => match k' in (_ = p) return (j23 f1 b c @ (1 @ 1) = (1 @ 1) @ p) with | 1 => match j23 f1 b c as p0 in (_ = p) return (forall Q : forall (a' b' : P) (ab' : a' = b') (ha : j2 f1 b = a') (hb : p = b'), p0 @ hb = ha @ ab' -> Type, Q (j2 f1 b) p p0 1 1 ((concat_p1 p0 @ 1) @ (concat_1p p0)^) -> Q (j2 f1 b) p p0 1 1 ((concat_p1 p0 @ 1) @ (concat_1p p0)^)) with | 1 => fun Q : forall (a' b' : P) (ab' : a' = b') (ha : j2 f1 b = a') (hb : j2 f1 b = b'), 1 @ hb = ha @ ab' -> Type => idmap end (fun (a' b' : P) (ab' : a' = b') (ha : j2 f1 b = a') (hb : j3 f1 c = b') (_ : j23 f1 b c @ hb = ha @ ab') => j23 f1 b c @ (1 @ hb) = (1 @ ha) @ ab') (square_ind (j2 f1 b) (j3 f1 c) (j23 f1 b c) (fun (a' b' : P) (ab' : a' = b') (ha : j2 f1 b = a') (hb : j3 f1 c = b') (_ : j23 f1 b c @ hb = ha @ ab') => j23 f1 b c @ (hb @ 1) = (ha @ 1) @ ab') (paths_ind (j2 f1 b) (fun (y : P) (p : j2 f1 b = y) => p @ 1 = 1 @ p) 1 (j3 f1 c) (j23 f1 b c)) (j2 f1 b) (j3 f1 c) (j23 f1 b c) 1 1 (equiv_p1_1q 1)) end) ((concat_p1 (j23 f1 b c) @ 1) @ (concat_1p (j23 f1 b c))^))
by triangle_ind f1 a b c. Defined.
A, B, C, P: Type

Is0Gpd (TriJoinRecData A B C P)
A, B, C, P: Type

Is0Gpd (TriJoinRecData A B C P)
A, B, C, P: Type

forall a b : TriJoinRecData A B C P, (a $-> b) -> b $-> a
A, B, C, P: Type
f, g: TriJoinRecData A B C P
h: f $-> g

g $-> f
A, B, C, P: Type
f, g: TriJoinRecData A B C P
h: f $-> g
a: A

j1 g a = j1 f a
A, B, C, P: Type
f, g: TriJoinRecData A B C P
h: f $-> g
b: B
j2 g b = j2 f b
A, B, C, P: Type
f, g: TriJoinRecData A B C P
h: f $-> g
c: C
j3 g c = j3 f c
A, B, C, P: Type
f, g: TriJoinRecData A B C P
h: f $-> g
a: A
b: B
j12 g a b @ ?Goal0 = ?Goal @ j12 f a b
A, B, C, P: Type
f, g: TriJoinRecData A B C P
h: f $-> g
a: A
c: C
j13 g a c @ ?Goal1 = ?Goal @ j13 f a c
A, B, C, P: Type
f, g: TriJoinRecData A B C P
h: f $-> g
b: B
c: C
j23 g b c @ ?Goal1 = ?Goal0 @ j23 f b c
A, B, C, P: Type
f, g: TriJoinRecData A B C P
h: f $-> g
a: A
b: B
c: C
prism (j123 g a b c) (j123 f a b c) ?Goal2 ?Goal3 ?Goal4
A, B, C, P: Type
f, g: TriJoinRecData A B C P
h: f $-> g
a: A

j1 g a = j1 f a
exact (h1 h a)^.
A, B, C, P: Type
f, g: TriJoinRecData A B C P
h: f $-> g
b: B

j2 g b = j2 f b
exact (h2 h b)^.
A, B, C, P: Type
f, g: TriJoinRecData A B C P
h: f $-> g
c: C

j3 g c = j3 f c
exact (h3 h c)^.
A, B, C, P: Type
f, g: TriJoinRecData A B C P
h: f $-> g
a: A
b: B

j12 g a b @ (h2 h b)^ = (h1 h a)^ @ j12 f a b
A, B, C, P: Type
f: TriJoinRecData A B C P
a: A
b: B

j12 f a b @ 1^ = 1^ @ j12 f a b
by triangle_ind_two f a b _X_.
A, B, C, P: Type
f, g: TriJoinRecData A B C P
h: f $-> g
a: A
c: C

j13 g a c @ (h3 h c)^ = (h1 h a)^ @ j13 f a c
A, B, C, P: Type
f: TriJoinRecData A B C P
a: A
c: C

j13 f a c @ 1^ = 1^ @ j13 f a c
by triangle_ind_two f a _X_ c.
A, B, C, P: Type
f, g: TriJoinRecData A B C P
h: f $-> g
b: B
c: C

j23 g b c @ (h3 h c)^ = (h2 h b)^ @ j23 f b c
A, B, C, P: Type
f: TriJoinRecData A B C P
b: B
c: C

j23 f b c @ 1^ = 1^ @ j23 f b c
by triangle_ind_two f _X_ b c.
A, B, C, P: Type
f, g: TriJoinRecData A B C P
h: f $-> g
a: A
b: B
c: C

prism (j123 g a b c) (j123 f a b c) ((fun (H : forall a : A, j1 f a = j1 g a) (H0 : forall b : B, j2 f b = j2 g b) (H1 : forall c : C, j3 f c = j3 g c) (H2 : forall (a : A) (b : B), j12 f a b @ H0 b = H a @ j12 g a b) (H3 : forall (a : A) (c : C), j13 f a c @ H1 c = H a @ j13 g a c) (H4 : forall (b : B) (c : C), j23 f b c @ H1 c = H0 b @ j23 g b c) (H5 : forall (a : A) (b : B) (c : C), prism (j123 f a b c) (j123 g a b c) (H2 a b) (H3 a c) (H4 b c)) => (fun (H6 : A -> P) (H7 : B -> P) (H8 : C -> P) (H9 : forall (a : A) (b : B), H6 a = H7 b) (H10 : forall (a : A) (c : C), H6 a = H8 c) (H11 : forall (b : B) (c : C), H7 b = H8 c) (H12 : forall (a : A) (b : B) (c : C), H9 a b @ H11 b c = H10 a c) => square_ind (j1 f a) (j2 f b) (j12 f a b) (fun (a' b' : P) (ab' : a' = b') (ha : j1 f a = a') (hb : j2 f b = b') (_ : j12 f a b @ hb = ha @ ab') => ab' @ hb^ = ha^ @ j12 f a b) ((fun (H13 : A -> P) (H14 : B -> P) (H15 : C -> P) (H16 : forall (a : A) (b : B), H13 a = H14 b) (H17 : forall (a : A) (c : C), H13 a = H15 c) (H18 : forall (b : B) (c : C), H14 b = H15 c) (H19 : forall (a : A) (b : B) (c : C), H16 a b @ H18 b c = H17 a c) => (fun f : P => paths_ind f (fun (y : P) (p : f = y) => p @ 1 = 1 @ p) 1) (H13 a) (H14 b) (H16 a b) : j12 {| j1 := H13; j2 := H14; j3 := H15; j12 := H16; j13 := H17; j23 := H18; j123 := H19 |} a b @ 1^ = 1^ @ j12 {| j1 := H13; j2 := H14; j3 := H15; j12 := H16; j13 := H17; j23 := H18; j123 := H19 |} a b) (j1 f) (j2 f) (j3 f) (j12 f) (j13 f) (j23 f) (j123 f)) (H6 a) (H7 b) (H9 a b) : forall (p : j1 f a = j1 {| j1 := H6; j2 := H7; j3 := H8; j12 := H9; j13 := H10; j23 := H11; j123 := H12 |} a) (p0 : j2 f b = j2 {| j1 := H6; j2 := H7; j3 := H8; j12 := H9; j13 := H10; j23 := H11; j123 := H12 |} b), j12 f a b @ p0 = p @ j12 {| j1 := H6; j2 := H7; j3 := H8; j12 := H9; j13 := H10; j23 := H11; j123 := H12 |} a b -> j12 {| j1 := H6; j2 := H7; j3 := H8; j12 := H9; j13 := H10; j23 := H11; j123 := H12 |} a b @ p0^ = p^ @ j12 f a b) (j1 g) (j2 g) (j3 g) (j12 g) (j13 g) (j23 g) (j123 g) (H a) (H0 b) (H2 a b) : j12 g a b @ (h2 {| h1 := H; h2 := H0; h3 := H1; h12 := H2; h13 := H3; h23 := H4; h123 := H5 |} b)^ = (h1 {| h1 := H; h2 := H0; h3 := H1; h12 := H2; h13 := H3; h23 := H4; h123 := H5 |} a)^ @ j12 f a b) (h1 h) (h2 h) (h3 h) (h12 h) (h13 h) (h23 h) (h123 h)) ((fun (H : forall a : A, j1 f a = j1 g a) (H0 : forall b : B, j2 f b = j2 g b) (H1 : forall c : C, j3 f c = j3 g c) (H2 : forall (a : A) (b : B), j12 f a b @ H0 b = H a @ j12 g a b) (H3 : forall (a : A) (c : C), j13 f a c @ H1 c = H a @ j13 g a c) (H4 : forall (b : B) (c : C), j23 f b c @ H1 c = H0 b @ j23 g b c) (H5 : forall (a : A) (b : B) (c : C), prism (j123 f a b c) (j123 g a b c) (H2 a b) (H3 a c) (H4 b c)) => (fun (H6 : A -> P) (H7 : B -> P) (H8 : C -> P) (H9 : forall (a : A) (b : B), H6 a = H7 b) (H10 : forall (a : A) (c : C), H6 a = H8 c) (H11 : forall (b : B) (c : C), H7 b = H8 c) (H12 : forall (a : A) (b : B) (c : C), H9 a b @ H11 b c = H10 a c) => square_ind (j1 f a) (j3 f c) (j13 f a c) (fun (a' b' : P) (ab' : a' = b') (ha : j1 f a = a') (hb : j3 f c = b') (_ : j13 f a c @ hb = ha @ ab') => ab' @ hb^ = ha^ @ j13 f a c) ((fun (H13 : A -> P) (H14 : B -> P) (H15 : C -> P) (H16 : forall (a : A) (b : B), H13 a = H14 b) (H17 : forall (a : A) (c : C), H13 a = H15 c) (H18 : forall (b : B) (c : C), H14 b = H15 c) (H19 : forall (a : A) (b : B) (c : C), H16 a b @ H18 b c = H17 a c) => (fun f : P => paths_ind f (fun (y : P) (p : f = y) => p @ 1 = 1 @ p) 1) (H13 a) (H15 c) (H17 a c) : j13 {| j1 := H13; j2 := H14; j3 := H15; j12 := H16; j13 := H17; j23 := H18; j123 := H19 |} a c @ 1^ = 1^ @ j13 {| j1 := H13; j2 := H14; j3 := H15; j12 := H16; j13 := H17; j23 := H18; j123 := H19 |} a c) (j1 f) (j2 f) (j3 f) (j12 f) (j13 f) (j23 f) (j123 f)) (H6 a) (H8 c) (H10 a c) : forall (p : j1 f a = j1 {| j1 := H6; j2 := H7; j3 := H8; j12 := H9; j13 := H10; j23 := H11; j123 := H12 |} a) (p0 : j3 f c = j3 {| j1 := H6; j2 := H7; j3 := H8; j12 := H9; j13 := H10; j23 := H11; j123 := H12 |} c), j13 f a c @ p0 = p @ j13 {| j1 := H6; j2 := H7; j3 := H8; j12 := H9; j13 := H10; j23 := H11; j123 := H12 |} a c -> j13 {| j1 := H6; j2 := H7; j3 := H8; j12 := H9; j13 := H10; j23 := H11; j123 := H12 |} a c @ p0^ = p^ @ j13 f a c) (j1 g) (j2 g) (j3 g) (j12 g) (j13 g) (j23 g) (j123 g) (H a) (H1 c) (H3 a c) : j13 g a c @ (h3 {| h1 := H; h2 := H0; h3 := H1; h12 := H2; h13 := H3; h23 := H4; h123 := H5 |} c)^ = (h1 {| h1 := H; h2 := H0; h3 := H1; h12 := H2; h13 := H3; h23 := H4; h123 := H5 |} a)^ @ j13 f a c) (h1 h) (h2 h) (h3 h) (h12 h) (h13 h) (h23 h) (h123 h)) ((fun (H : forall a : A, j1 f a = j1 g a) (H0 : forall b : B, j2 f b = j2 g b) (H1 : forall c : C, j3 f c = j3 g c) (H2 : forall (a : A) (b : B), j12 f a b @ H0 b = H a @ j12 g a b) (H3 : forall (a : A) (c : C), j13 f a c @ H1 c = H a @ j13 g a c) (H4 : forall (b : B) (c : C), j23 f b c @ H1 c = H0 b @ j23 g b c) (H5 : forall (a : A) (b : B) (c : C), prism (j123 f a b c) (j123 g a b c) (H2 a b) (H3 a c) (H4 b c)) => (fun (H6 : A -> P) (H7 : B -> P) (H8 : C -> P) (H9 : forall (a : A) (b : B), H6 a = H7 b) (H10 : forall (a : A) (c : C), H6 a = H8 c) (H11 : forall (b : B) (c : C), H7 b = H8 c) (H12 : forall (a : A) (b : B) (c : C), H9 a b @ H11 b c = H10 a c) => square_ind (j2 f b) (j3 f c) (j23 f b c) (fun (a' b' : P) (ab' : a' = b') (ha : j2 f b = a') (hb : j3 f c = b') (_ : j23 f b c @ hb = ha @ ab') => ab' @ hb^ = ha^ @ j23 f b c) ((fun (H13 : A -> P) (H14 : B -> P) (H15 : C -> P) (H16 : forall (a : A) (b : B), H13 a = H14 b) (H17 : forall (a : A) (c : C), H13 a = H15 c) (H18 : forall (b : B) (c : C), H14 b = H15 c) (H19 : forall (a : A) (b : B) (c : C), H16 a b @ H18 b c = H17 a c) => (fun f : P => paths_ind f (fun (y : P) (p : f = y) => p @ 1 = 1 @ p) 1) (H14 b) (H15 c) (H18 b c) : j23 {| j1 := H13; j2 := H14; j3 := H15; j12 := H16; j13 := H17; j23 := H18; j123 := H19 |} b c @ 1^ = 1^ @ j23 {| j1 := H13; j2 := H14; j3 := H15; j12 := H16; j13 := H17; j23 := H18; j123 := H19 |} b c) (j1 f) (j2 f) (j3 f) (j12 f) (j13 f) (j23 f) (j123 f)) (H7 b) (H8 c) (H11 b c) : forall (p : j2 f b = j2 {| j1 := H6; j2 := H7; j3 := H8; j12 := H9; j13 := H10; j23 := H11; j123 := H12 |} b) (p0 : j3 f c = j3 {| j1 := H6; j2 := H7; j3 := H8; j12 := H9; j13 := H10; j23 := H11; j123 := H12 |} c), j23 f b c @ p0 = p @ j23 {| j1 := H6; j2 := H7; j3 := H8; j12 := H9; j13 := H10; j23 := H11; j123 := H12 |} b c -> j23 {| j1 := H6; j2 := H7; j3 := H8; j12 := H9; j13 := H10; j23 := H11; j123 := H12 |} b c @ p0^ = p^ @ j23 f b c) (j1 g) (j2 g) (j3 g) (j12 g) (j13 g) (j23 g) (j123 g) (H0 b) (H1 c) (H4 b c) : j23 g b c @ (h3 {| h1 := H; h2 := H0; h3 := H1; h12 := H2; h13 := H3; h23 := H4; h123 := H5 |} c)^ = (h2 {| h1 := H; h2 := H0; h3 := H1; h12 := H2; h13 := H3; h23 := H4; h123 := H5 |} b)^ @ j23 f b c) (h1 h) (h2 h) (h3 h) (h12 h) (h13 h) (h23 h) (h123 h))
A, B, C, P: Type
f: TriJoinRecData A B C P
a: A
b: B
c: C

prism (j123 f a b c) (j123 f a b c) (square_ind (j1 f a) (j2 f b) (j12 f a b) (fun (a' b' : P) (ab' : a' = b') (ha : j1 f a = a') (hb : j2 f b = b') (_ : j12 f a b @ hb = ha @ ab') => ab' @ hb^ = ha^ @ j12 f a b) (paths_ind (j1 f a) (fun (y : P) (p : j1 f a = y) => p @ 1 = 1 @ p) 1 (j2 f b) (j12 f a b)) (j1 f a) (j2 f b) (j12 f a b) 1 1 (equiv_p1_1q 1)) (square_ind (j1 f a) (j3 f c) (j13 f a c) (fun (a' b' : P) (ab' : a' = b') (ha : j1 f a = a') (hb : j3 f c = b') (_ : j13 f a c @ hb = ha @ ab') => ab' @ hb^ = ha^ @ j13 f a c) (paths_ind (j1 f a) (fun (y : P) (p : j1 f a = y) => p @ 1 = 1 @ p) 1 (j3 f c) (j13 f a c)) (j1 f a) (j3 f c) (j13 f a c) 1 1 (equiv_p1_1q 1)) (square_ind (j2 f b) (j3 f c) (j23 f b c) (fun (a' b' : P) (ab' : a' = b') (ha : j2 f b = a') (hb : j3 f c = b') (_ : j23 f b c @ hb = ha @ ab') => ab' @ hb^ = ha^ @ j23 f b c) (paths_ind (j2 f b) (fun (y : P) (p : j2 f b = y) => p @ 1 = 1 @ p) 1 (j3 f c) (j23 f b c)) (j2 f b) (j3 f c) (j23 f b c) 1 1 (equiv_p1_1q 1))
by triangle_ind f a b c. Defined. Definition trijoinrecdata_0gpd (A B C P : Type) : ZeroGpd := Build_ZeroGpd (TriJoinRecData A B C P) _ _ _. (** ** [trijoinrecdata_0gpd A B C] is a 1-functor from [Type] to [ZeroGpd] It's a 1-functor that lands in [ZeroGpd], and the morphisms of [ZeroGpd] are 0-functors, so it's easy to get confused about the levels. *) (** First we need to show that the induced map is a morphism in [ZeroGpd], i.e. that it is a 0-functor. *)
A, B, C, P, Q: Type
g: P -> Q

Is0Functor (trijoinrecdata_fun g)
A, B, C, P, Q: Type
g: P -> Q

Is0Functor (trijoinrecdata_fun g)
A, B, C, P, Q: Type
g: P -> Q

forall a b : TriJoinRecData A B C P, (a $-> b) -> trijoinrecdata_fun g a $-> trijoinrecdata_fun g b
A, B, C, P, Q: Type
g: P -> Q
f1, f2: TriJoinRecData A B C P
h: f1 $-> f2

trijoinrecdata_fun g f1 $-> trijoinrecdata_fun g f2
A, B, C, P, Q: Type
g: P -> Q
f1, f2: TriJoinRecData A B C P
h: f1 $-> f2
a: A

g (j1 f1 a) = g (j1 f2 a)
A, B, C, P, Q: Type
g: P -> Q
f1, f2: TriJoinRecData A B C P
h: f1 $-> f2
b: B
g (j2 f1 b) = g (j2 f2 b)
A, B, C, P, Q: Type
g: P -> Q
f1, f2: TriJoinRecData A B C P
h: f1 $-> f2
c: C
g (j3 f1 c) = g (j3 f2 c)
A, B, C, P, Q: Type
g: P -> Q
f1, f2: TriJoinRecData A B C P
h: f1 $-> f2
a: A
b: B
ap g (j12 f1 a b) @ ?Goal0 = ?Goal @ ap g (j12 f2 a b)
A, B, C, P, Q: Type
g: P -> Q
f1, f2: TriJoinRecData A B C P
h: f1 $-> f2
a: A
c: C
ap g (j13 f1 a c) @ ?Goal1 = ?Goal @ ap g (j13 f2 a c)
A, B, C, P, Q: Type
g: P -> Q
f1, f2: TriJoinRecData A B C P
h: f1 $-> f2
b: B
c: C
ap g (j23 f1 b c) @ ?Goal1 = ?Goal0 @ ap g (j23 f2 b c)
A, B, C, P, Q: Type
g: P -> Q
f1, f2: TriJoinRecData A B C P
h: f1 $-> f2
a: A
b: B
c: C
prism (ap_triangle g (j123 f1 a b c)) (ap_triangle g (j123 f2 a b c)) ?Goal2 ?Goal3 ?Goal4
A, B, C, P, Q: Type
g: P -> Q
f1, f2: TriJoinRecData A B C P
h: f1 $-> f2
a: A

j1 f1 a = j1 f2 a
A, B, C, P, Q: Type
g: P -> Q
f1, f2: TriJoinRecData A B C P
h: f1 $-> f2
b: B
j2 f1 b = j2 f2 b
A, B, C, P, Q: Type
g: P -> Q
f1, f2: TriJoinRecData A B C P
h: f1 $-> f2
c: C
j3 f1 c = j3 f2 c
A, B, C, P, Q: Type
g: P -> Q
f1, f2: TriJoinRecData A B C P
h: f1 $-> f2
a: A
b: B
ap g (j12 f1 a b) @ ap g ?Goal4 = ap g ?Goal3 @ ap g (j12 f2 a b)
A, B, C, P, Q: Type
g: P -> Q
f1, f2: TriJoinRecData A B C P
h: f1 $-> f2
a: A
c: C
ap g (j13 f1 a c) @ ap g ?Goal5 = ap g ?Goal3 @ ap g (j13 f2 a c)
A, B, C, P, Q: Type
g: P -> Q
f1, f2: TriJoinRecData A B C P
h: f1 $-> f2
b: B
c: C
ap g (j23 f1 b c) @ ap g ?Goal5 = ap g ?Goal4 @ ap g (j23 f2 b c)
A, B, C, P, Q: Type
g: P -> Q
f1, f2: TriJoinRecData A B C P
h: f1 $-> f2
a: A
b: B
c: C
prism (ap_triangle g (j123 f1 a b c)) (ap_triangle g (j123 f2 a b c)) ?Goal ?Goal0 ?Goal1
A, B, C, P, Q: Type
g: P -> Q
f1, f2: TriJoinRecData A B C P
h: f1 $-> f2
b: B

j2 f1 b = j2 f2 b
A, B, C, P, Q: Type
g: P -> Q
f1, f2: TriJoinRecData A B C P
h: f1 $-> f2
c: C
j3 f1 c = j3 f2 c
A, B, C, P, Q: Type
g: P -> Q
f1, f2: TriJoinRecData A B C P
h: f1 $-> f2
a: A
b: B
ap g (j12 f1 a b) @ ap g ?Goal3 = ap g (h1 h a) @ ap g (j12 f2 a b)
A, B, C, P, Q: Type
g: P -> Q
f1, f2: TriJoinRecData A B C P
h: f1 $-> f2
a: A
c: C
ap g (j13 f1 a c) @ ap g ?Goal4 = ap g (h1 h a) @ ap g (j13 f2 a c)
A, B, C, P, Q: Type
g: P -> Q
f1, f2: TriJoinRecData A B C P
h: f1 $-> f2
b: B
c: C
ap g (j23 f1 b c) @ ap g ?Goal4 = ap g ?Goal3 @ ap g (j23 f2 b c)
A, B, C, P, Q: Type
g: P -> Q
f1, f2: TriJoinRecData A B C P
h: f1 $-> f2
a: A
b: B
c: C
prism (ap_triangle g (j123 f1 a b c)) (ap_triangle g (j123 f2 a b c)) ?Goal ?Goal0 ?Goal1
A, B, C, P, Q: Type
g: P -> Q
f1, f2: TriJoinRecData A B C P
h: f1 $-> f2
c: C

j3 f1 c = j3 f2 c
A, B, C, P, Q: Type
g: P -> Q
f1, f2: TriJoinRecData A B C P
h: f1 $-> f2
a: A
b: B
ap g (j12 f1 a b) @ ap g (h2 h b) = ap g (h1 h a) @ ap g (j12 f2 a b)
A, B, C, P, Q: Type
g: P -> Q
f1, f2: TriJoinRecData A B C P
h: f1 $-> f2
a: A
c: C
ap g (j13 f1 a c) @ ap g ?Goal3 = ap g (h1 h a) @ ap g (j13 f2 a c)
A, B, C, P, Q: Type
g: P -> Q
f1, f2: TriJoinRecData A B C P
h: f1 $-> f2
b: B
c: C
ap g (j23 f1 b c) @ ap g ?Goal3 = ap g (h2 h b) @ ap g (j23 f2 b c)
A, B, C, P, Q: Type
g: P -> Q
f1, f2: TriJoinRecData A B C P
h: f1 $-> f2
a: A
b: B
c: C
prism (ap_triangle g (j123 f1 a b c)) (ap_triangle g (j123 f2 a b c)) ?Goal ?Goal0 ?Goal1
A, B, C, P, Q: Type
g: P -> Q
f1, f2: TriJoinRecData A B C P
h: f1 $-> f2
a: A
b: B

ap g (j12 f1 a b) @ ap g (h2 h b) = ap g (h1 h a) @ ap g (j12 f2 a b)
A, B, C, P, Q: Type
g: P -> Q
f1, f2: TriJoinRecData A B C P
h: f1 $-> f2
a: A
c: C
ap g (j13 f1 a c) @ ap g (h3 h c) = ap g (h1 h a) @ ap g (j13 f2 a c)
A, B, C, P, Q: Type
g: P -> Q
f1, f2: TriJoinRecData A B C P
h: f1 $-> f2
b: B
c: C
ap g (j23 f1 b c) @ ap g (h3 h c) = ap g (h2 h b) @ ap g (j23 f2 b c)
A, B, C, P, Q: Type
g: P -> Q
f1, f2: TriJoinRecData A B C P
h: f1 $-> f2
a: A
b: B
c: C
prism (ap_triangle g (j123 f1 a b c)) (ap_triangle g (j123 f2 a b c)) ?Goal ?Goal0 ?Goal1
A, B, C, P, Q: Type
g: P -> Q
f1, f2: TriJoinRecData A B C P
h: f1 $-> f2
a: A
b: B

j12 f1 a b @ h2 h b = h1 h a @ j12 f2 a b
A, B, C, P, Q: Type
g: P -> Q
f1, f2: TriJoinRecData A B C P
h: f1 $-> f2
a: A
c: C
j13 f1 a c @ h3 h c = h1 h a @ j13 f2 a c
A, B, C, P, Q: Type
g: P -> Q
f1, f2: TriJoinRecData A B C P
h: f1 $-> f2
b: B
c: C
j23 f1 b c @ h3 h c = h2 h b @ j23 f2 b c
A, B, C, P, Q: Type
g: P -> Q
f1, f2: TriJoinRecData A B C P
h: f1 $-> f2
a: A
b: B
c: C
prism (ap_triangle g (j123 f1 a b c)) (ap_triangle g (j123 f2 a b c)) (((ap_pp g (j12 f1 a b) (h2 h b))^ @ ap (ap g) ?Goal0) @ ap_pp g (h1 h a) (j12 f2 a b)) (((ap_pp g (j13 f1 a c) (h3 h c))^ @ ap (ap g) ?Goal1) @ ap_pp g (h1 h a) (j13 f2 a c)) (((ap_pp g (j23 f1 b c) (h3 h c))^ @ ap (ap g) ?Goal2) @ ap_pp g (h2 h b) (j23 f2 b c))
A, B, C, P, Q: Type
g: P -> Q
f1, f2: TriJoinRecData A B C P
h: f1 $-> f2
a: A
c: C

j13 f1 a c @ h3 h c = h1 h a @ j13 f2 a c
A, B, C, P, Q: Type
g: P -> Q
f1, f2: TriJoinRecData A B C P
h: f1 $-> f2
b: B
c: C
j23 f1 b c @ h3 h c = h2 h b @ j23 f2 b c
A, B, C, P, Q: Type
g: P -> Q
f1, f2: TriJoinRecData A B C P
h: f1 $-> f2
a: A
b: B
c: C
prism (ap_triangle g (j123 f1 a b c)) (ap_triangle g (j123 f2 a b c)) (((ap_pp g (j12 f1 a b) (h2 h b))^ @ ap (ap g) (h12 h a b)) @ ap_pp g (h1 h a) (j12 f2 a b)) (((ap_pp g (j13 f1 a c) (h3 h c))^ @ ap (ap g) ?Goal0) @ ap_pp g (h1 h a) (j13 f2 a c)) (((ap_pp g (j23 f1 b c) (h3 h c))^ @ ap (ap g) ?Goal1) @ ap_pp g (h2 h b) (j23 f2 b c))
A, B, C, P, Q: Type
g: P -> Q
f1, f2: TriJoinRecData A B C P
h: f1 $-> f2
b: B
c: C

j23 f1 b c @ h3 h c = h2 h b @ j23 f2 b c
A, B, C, P, Q: Type
g: P -> Q
f1, f2: TriJoinRecData A B C P
h: f1 $-> f2
a: A
b: B
c: C
prism (ap_triangle g (j123 f1 a b c)) (ap_triangle g (j123 f2 a b c)) (((ap_pp g (j12 f1 a b) (h2 h b))^ @ ap (ap g) (h12 h a b)) @ ap_pp g (h1 h a) (j12 f2 a b)) (((ap_pp g (j13 f1 a c) (h3 h c))^ @ ap (ap g) (h13 h a c)) @ ap_pp g (h1 h a) (j13 f2 a c)) (((ap_pp g (j23 f1 b c) (h3 h c))^ @ ap (ap g) ?Goal0) @ ap_pp g (h2 h b) (j23 f2 b c))
A, B, C, P, Q: Type
g: P -> Q
f1, f2: TriJoinRecData A B C P
h: f1 $-> f2
a: A
b: B
c: C

prism (ap_triangle g (j123 f1 a b c)) (ap_triangle g (j123 f2 a b c)) (((ap_pp g (j12 f1 a b) (h2 h b))^ @ ap (ap g) (h12 h a b)) @ ap_pp g (h1 h a) (j12 f2 a b)) (((ap_pp g (j13 f1 a c) (h3 h c))^ @ ap (ap g) (h13 h a c)) @ ap_pp g (h1 h a) (j13 f2 a c)) (((ap_pp g (j23 f1 b c) (h3 h c))^ @ ap (ap g) (h23 h b c)) @ ap_pp g (h2 h b) (j23 f2 b c))
A, B, C, P, Q: Type
g: P -> Q
f1: TriJoinRecData A B C P
a: A
b: B
c: C

prism (ap_triangle g (j123 f1 a b c)) (ap_triangle g (j123 f1 a b c)) (((ap_pp g (j12 f1 a b) 1)^ @ ap (ap g) (equiv_p1_1q 1)) @ ap_pp g 1 (j12 f1 a b)) (((ap_pp g (j13 f1 a c) 1)^ @ ap (ap g) (equiv_p1_1q 1)) @ ap_pp g 1 (j13 f1 a c)) (((ap_pp g (j23 f1 b c) 1)^ @ ap (ap g) (equiv_p1_1q 1)) @ ap_pp g 1 (j23 f1 b c))
A, B, C, P, Q: Type
g: P -> Q
a: A
b: B
c: C
f1: P

prism 1 1 1 1 1
reflexivity. Defined. (** [trijoinrecdata_0gpd A B C] is a 0-functor from [Type] to [ZeroGpd] (one level up). *)
A, B, C: Type

Is0Functor (trijoinrecdata_0gpd A B C)
A, B, C: Type

Is0Functor (trijoinrecdata_0gpd A B C)
A, B, C: Type

forall a b : Type, (a $-> b) -> trijoinrecdata_0gpd A B C a $-> trijoinrecdata_0gpd A B C b
A, B, C, P, Q: Type
g: P $-> Q

trijoinrecdata_0gpd A B C P $-> trijoinrecdata_0gpd A B C Q
A, B, C, P, Q: Type
g: P $-> Q

trijoinrecdata_0gpd A B C P -> trijoinrecdata_0gpd A B C Q
A, B, C, P, Q: Type
g: P $-> Q
Is0Functor ?fun_0gpd
A, B, C, P, Q: Type
g: P $-> Q

trijoinrecdata_0gpd A B C P -> trijoinrecdata_0gpd A B C Q
exact (trijoinrecdata_fun g).
A, B, C, P, Q: Type
g: P $-> Q

Is0Functor (trijoinrecdata_fun g)
apply is0functor_trijoinrecdata_fun. Defined. (** [trijoinrecdata_0gpd A B C] is a 1-functor from [Type] to [ZeroGpd]. *)
A, B, C: Type

Is1Functor (trijoinrecdata_0gpd A B C)
A, B, C: Type

Is1Functor (trijoinrecdata_0gpd A B C)
A, B, C: Type

forall (a b : Type) (f g : a $-> b), f $== g -> fmap (trijoinrecdata_0gpd A B C) f $== fmap (trijoinrecdata_0gpd A B C) g
A, B, C: Type
forall a : Type, fmap (trijoinrecdata_0gpd A B C) (Id a) $== Id (trijoinrecdata_0gpd A B C a)
A, B, C: Type
forall (a b c : Type) (f : a $-> b) (g : b $-> c), fmap (trijoinrecdata_0gpd A B C) (g $o f) $== fmap (trijoinrecdata_0gpd A B C) g $o fmap (trijoinrecdata_0gpd A B C) f
(* If [g1 g2 : P -> Q] are homotopic, then the induced maps are homotopic: *)
A, B, C: Type

forall (a b : Type) (f g : a $-> b), f $== g -> fmap (trijoinrecdata_0gpd A B C) f $== fmap (trijoinrecdata_0gpd A B C) g
A, B, C, P, Q: Type
g1, g2: P -> Q
h: g1 == g2
f: TriJoinRecData A B C P

TriJoinRecPath (trijoinrecdata_fun g1 f) (trijoinrecdata_fun g2 f)
A, B, C, P, Q: Type
g1, g2: P -> Q
h: g1 == g2
f: TriJoinRecData A B C P
a: A

g1 (j1 f a) = g2 (j1 f a)
A, B, C, P, Q: Type
g1, g2: P -> Q
h: g1 == g2
f: TriJoinRecData A B C P
b: B
g1 (j2 f b) = g2 (j2 f b)
A, B, C, P, Q: Type
g1, g2: P -> Q
h: g1 == g2
f: TriJoinRecData A B C P
c: C
g1 (j3 f c) = g2 (j3 f c)
A, B, C, P, Q: Type
g1, g2: P -> Q
h: g1 == g2
f: TriJoinRecData A B C P
a: A
b: B
ap g1 (j12 f a b) @ ?Goal2 = ?Goal1 @ ap g2 (j12 f a b)
A, B, C, P, Q: Type
g1, g2: P -> Q
h: g1 == g2
f: TriJoinRecData A B C P
a: A
c: C
ap g1 (j13 f a c) @ ?Goal3 = ?Goal1 @ ap g2 (j13 f a c)
A, B, C, P, Q: Type
g1, g2: P -> Q
h: g1 == g2
f: TriJoinRecData A B C P
b: B
c: C
ap g1 (j23 f b c) @ ?Goal3 = ?Goal2 @ ap g2 (j23 f b c)
A, B, C, P, Q: Type
g1, g2: P -> Q
h: g1 == g2
f: TriJoinRecData A B C P
a: A
b: B
c: C
prism (ap_triangle g1 (j123 f a b c)) (ap_triangle g2 (j123 f a b c)) ?Goal4 ?Goal5 ?Goal6
A, B, C, P, Q: Type
g1, g2: P -> Q
h: g1 == g2
f: TriJoinRecData A B C P
a: A
b: B

ap g1 (j12 f a b) @ h (j2 f b) = h (j1 f a) @ ap g2 (j12 f a b)
A, B, C, P, Q: Type
g1, g2: P -> Q
h: g1 == g2
f: TriJoinRecData A B C P
a: A
c: C
ap g1 (j13 f a c) @ h (j3 f c) = h (j1 f a) @ ap g2 (j13 f a c)
A, B, C, P, Q: Type
g1, g2: P -> Q
h: g1 == g2
f: TriJoinRecData A B C P
b: B
c: C
ap g1 (j23 f b c) @ h (j3 f c) = h (j2 f b) @ ap g2 (j23 f b c)
A, B, C, P, Q: Type
g1, g2: P -> Q
h: g1 == g2
f: TriJoinRecData A B C P
a: A
b: B
c: C
prism (ap_triangle g1 (j123 f a b c)) (ap_triangle g2 (j123 f a b c)) ?Goal1 ?Goal2 ?Goal3
A, B, C, P, Q: Type
g1, g2: P -> Q
h: g1 == g2
f: TriJoinRecData A B C P
a: A
b: B
c: C

prism (ap_triangle g1 (j123 f a b c)) (ap_triangle g2 (j123 f a b c)) (concat_Ap h (j12 f a b)) (concat_Ap h (j13 f a c)) (concat_Ap h (j23 f b c))
A, B, C, P, Q: Type
g1, g2: P -> Q
h: g1 == g2
a: A
b: B
c: C
f: P

prism 1 1 (concat_1p_p1 (h f)) (concat_1p_p1 (h f)) (concat_1p_p1 (h f))
by induction (h f). (* The identity map [P -> P] is sent to a map homotopic to the identity. *)
A, B, C: Type

forall a : Type, fmap (trijoinrecdata_0gpd A B C) (Id a) $== Id (trijoinrecdata_0gpd A B C a)
A, B, C, P: Type
f: trijoinrecdata_0gpd A B C P

TriJoinRecPath (trijoinrecdata_fun idmap f) f
A, B, C, P: Type
f: trijoinrecdata_0gpd A B C P
a: A
b: B

ap idmap (j12 f a b) = j12 f a b
A, B, C, P: Type
f: trijoinrecdata_0gpd A B C P
a: A
c: C
ap idmap (j13 f a c) = j13 f a c
A, B, C, P: Type
f: trijoinrecdata_0gpd A B C P
b: B
c: C
ap idmap (j23 f b c) = j23 f b c
A, B, C, P: Type
f: trijoinrecdata_0gpd A B C P
a: A
b: B
c: C
prism' (ap_triangle idmap (j123 f a b c)) (j123 f a b c) ?Goal0 ?Goal1 ?Goal2
A, B, C, P: Type
f: trijoinrecdata_0gpd A B C P
a: A
b: B
c: C

prism' (ap_triangle idmap (j123 f a b c)) (j123 f a b c) (ap_idmap (j12 f a b)) (ap_idmap (j13 f a c)) (ap_idmap (j23 f b c))
by triangle_ind f a b c. (* It respects composition. *)
A, B, C: Type

forall (a b c : Type) (f : a $-> b) (g : b $-> c), fmap (trijoinrecdata_0gpd A B C) (g $o f) $== fmap (trijoinrecdata_0gpd A B C) g $o fmap (trijoinrecdata_0gpd A B C) f
A, B, C, P, Q, R: Type
g1: P $-> Q
g2: Q $-> R
f: trijoinrecdata_0gpd A B C P

TriJoinRecPath (trijoinrecdata_fun (fun x : P => g2 (g1 x)) f) (trijoinrecdata_fun g2 (trijoinrecdata_fun g1 f))
A, B, C, P, Q, R: Type
g1: P $-> Q
g2: Q $-> R
f: trijoinrecdata_0gpd A B C P
a: A
b: B

ap (fun x : P => g2 (g1 x)) (j12 f a b) = ap g2 (ap g1 (j12 f a b))
A, B, C, P, Q, R: Type
g1: P $-> Q
g2: Q $-> R
f: trijoinrecdata_0gpd A B C P
a: A
c: C
ap (fun x : P => g2 (g1 x)) (j13 f a c) = ap g2 (ap g1 (j13 f a c))
A, B, C, P, Q, R: Type
g1: P $-> Q
g2: Q $-> R
f: trijoinrecdata_0gpd A B C P
b: B
c: C
ap (fun x : P => g2 (g1 x)) (j23 f b c) = ap g2 (ap g1 (j23 f b c))
A, B, C, P, Q, R: Type
g1: P $-> Q
g2: Q $-> R
f: trijoinrecdata_0gpd A B C P
a: A
b: B
c: C
prism' (ap_triangle (fun x : P => g2 (g1 x)) (j123 f a b c)) (ap_triangle g2 (ap_triangle g1 (j123 f a b c))) ?Goal ?Goal0 ?Goal1
A, B, C, P, Q, R: Type
g1: P $-> Q
g2: Q $-> R
f: trijoinrecdata_0gpd A B C P
a: A
b: B
c: C

prism' (ap_triangle (fun x : P => g2 (g1 x)) (j123 f a b c)) (ap_triangle g2 (ap_triangle g1 (j123 f a b c))) (ap_compose g1 g2 (j12 f a b)) (ap_compose g1 g2 (j13 f a c)) (ap_compose g1 g2 (j23 f b c))
by triangle_ind f a b c. Defined. Definition trijoinrecdata_0gpd_fun (A B C : Type) : Fun11 Type ZeroGpd := Build_Fun11 _ _ (trijoinrecdata_0gpd A B C). (** By the Yoneda lemma, it follows from [TriJoinRecData] being a 1-functor that given [TriJoinRecData] in [J], we get a map [(J -> P) $-> (TriJoinRecData A B C P)] of 0-groupoids which is natural in [P]. Below we will specialize to the case where [J] is [TriJoin A B C] with the canonical [TriJoinRecData]. *)
A, B, C, J: Type
f: TriJoinRecData A B C J

NatTrans (opyon_0gpd J) (trijoinrecdata_0gpd_fun A B C)
A, B, C, J: Type
f: TriJoinRecData A B C J

NatTrans (opyon_0gpd J) (trijoinrecdata_0gpd_fun A B C)
A, B, C, J: Type
f: TriJoinRecData A B C J

opyon_0gpd J $=> trijoinrecdata_0gpd_fun A B C
A, B, C, J: Type
f: TriJoinRecData A B C J
Is1Natural (opyon_0gpd J) (trijoinrecdata_0gpd_fun A B C) ?alpha
A, B, C, J: Type
f: TriJoinRecData A B C J

opyon_0gpd J $=> trijoinrecdata_0gpd_fun A B C
rapply opyoneda_0gpd; exact f.
A, B, C, J: Type
f: TriJoinRecData A B C J

Is1Natural (opyon_0gpd J) (trijoinrecdata_0gpd_fun A B C) (opyoneda_0gpd J (trijoinrecdata_0gpd_fun A B C) f)
exact _. Defined. (** Thus we get a map [(TriJoin A B C -> P) $-> (TriJoinRecData A B C P)] of 0-groupoids, natural in [P]. The underlying map is [trijoin_rec_inv A B C P]. *) Definition trijoin_rec_inv_nattrans (A B C : Type) : NatTrans (opyon_0gpd (TriJoin A B C)) (trijoinrecdata_0gpd_fun A B C) := trijoin_nattrans_recdata (trijoinrecdata_trijoin A B C). (** This natural transformation is in fact a natural equivalence of 0-groupoids. *)
A, B, C: Type

NatEquiv (opyon_0gpd (TriJoin A B C)) (trijoinrecdata_0gpd_fun A B C)
A, B, C: Type

NatEquiv (opyon_0gpd (TriJoin A B C)) (trijoinrecdata_0gpd_fun A B C)
A, B, C: Type

NatTrans (opyon_0gpd (TriJoin A B C)) (trijoinrecdata_0gpd_fun A B C)
A, B, C: Type
forall a : Type, CatIsEquiv (?alpha a)
A, B, C: Type

forall a : Type, CatIsEquiv (trijoin_rec_inv_nattrans A B C a)
A, B, C, P: Type

CatIsEquiv (trijoin_rec_inv_nattrans A B C P)
A, B, C, P: Type

IsSurjInj (trijoin_rec_inv_nattrans A B C P)
A, B, C, P: Type

SplEssSurj (trijoin_rec_inv_nattrans A B C P)
A, B, C, P: Type
forall x y : opyon_0gpd (TriJoin A B C) P, trijoin_rec_inv_nattrans A B C P x $== trijoin_rec_inv_nattrans A B C P y -> x $== y
A, B, C, P: Type

SplEssSurj (trijoin_rec_inv_nattrans A B C P)
A, B, C, P: Type
f: TriJoinRecData A B C P

{a : opyon_0gpd (TriJoin A B C) P & trijoin_rec_inv_nattrans A B C P a $== f}
A, B, C, P: Type
f: TriJoinRecData A B C P

trijoin_rec_inv_nattrans A B C P (trijoin_rec f) $== f
apply trijoin_rec_beta.
A, B, C, P: Type

forall x y : opyon_0gpd (TriJoin A B C) P, trijoin_rec_inv_nattrans A B C P x $== trijoin_rec_inv_nattrans A B C P y -> x $== y
exact (@isinj_trijoin_rec_inv A B C P). Defined. (** It will be handy to name the inverse natural equivalence. *) Definition trijoin_rec_natequiv (A B C : Type) := natequiv_inverse (trijoin_rec_inv_natequiv A B C). (** [trijoin_rec_natequiv A B C P] is an equivalence of 0-groupoids whose underlying function is definitionally [trijoin_rec]. *) Local Definition trijoin_rec_natequiv_check (A B C P : Type) : equiv_fun_0gpd (trijoin_rec_natequiv A B C P) = @trijoin_rec A B C P := idpath. (** It follows that [trijoin_rec A B C P] is a 0-functor. *)
A, B, C, P: Type

Is0Functor trijoin_rec
A, B, C, P: Type

Is0Functor trijoin_rec
A, B, C, P: Type

Is0Functor (equiv_fun_0gpd (trijoin_rec_natequiv A B C P))
exact _. Defined. (** And that [trijoin_rec A B C] is natural. The [$==] in the statement is just [==], but we use WildCat notation so that we can invert and compose these with WildCat notation. *)
A, B, C, P, Q: Type
g: P -> Q
f: TriJoinRecData A B C P

trijoin_rec (trijoinrecdata_fun g f) $== g o trijoin_rec f
A, B, C, P, Q: Type
g: P -> Q
f: TriJoinRecData A B C P

trijoin_rec (trijoinrecdata_fun g f) $== g o trijoin_rec f
exact (isnat (trijoin_rec_natequiv A B C) g f). Defined. (** It is also useful to record this. *) Definition issect_trijoin_rec_inv {A B C P : Type} (f : TriJoin A B C -> P) : trijoin_rec (trijoin_rec_inv f) $== f := cate_issect (trijoin_rec_inv_natequiv A B C P) f. (** This comes up a lot as well, and if you inline the proof, you get an ugly goal. *)
A, B, C, P: Type
f: TriJoinRecData A B C P
g: TriJoin A B C -> P
p: f $== trijoin_rec_inv g

trijoin_rec f == g
A, B, C, P: Type
f: TriJoinRecData A B C P
g: TriJoin A B C -> P
p: f $== trijoin_rec_inv g

trijoin_rec f == g
exact (moveR_equiv_V_0gpd (trijoin_rec_inv_natequiv A B C P) _ _ p). Defined. (** * Functoriality of the triple join *) (** ** Precomposition of [TriJoinRecData] *) (** First observe that we can precompose [k : TriJoinRecData] with a triple of maps. *) Definition trijoinrecdata_tricomp {A B C A' B' C' P} (k : TriJoinRecData A B C P) (f : A' -> A) (g : B' -> B) (h : C' -> C) : TriJoinRecData A' B' C' P := {| j1 := j1 k o f; j2 := j2 k o g; j3 := j3 k o h; j12 := fun a b => j12 k (f a) (g b); j13 := fun a c => j13 k (f a) (h c); j23 := fun b c => j23 k (g b) (h c); j123 := fun a b c => j123 k (f a) (g b) (h c); |}. (** Precomposition with a triple respects paths. *)
A, B, C, A', B', C', P: Type
k, l: TriJoinRecData A B C P
p: k $== l
f: A' -> A
g: B' -> B
h: C' -> C

trijoinrecdata_tricomp k f g h $== trijoinrecdata_tricomp l f g h
A, B, C, A', B', C', P: Type
k, l: TriJoinRecData A B C P
p: k $== l
f: A' -> A
g: B' -> B
h: C' -> C

trijoinrecdata_tricomp k f g h $== trijoinrecdata_tricomp l f g h
(* This line is not needed, but clarifies the proof. *)
A, B, C, A', B', C', P: Type
k, l: TriJoinRecData A B C P
h4: forall a : A, j1 k a = j1 l a
h5: forall b : B, j2 k b = j2 l b
h6: forall c : C, j3 k c = j3 l c
h14: forall (a : A) (b : B), j12 k a b @ h5 b = h4 a @ j12 l a b
h15: forall (a : A) (c : C), j13 k a c @ h6 c = h4 a @ j13 l a c
h24: forall (b : B) (c : C), j23 k b c @ h6 c = h5 b @ j23 l b c
h124: forall (a : A) (b : B) (c : C), prism (j123 k a b c) (j123 l a b c) (h14 a b) (h15 a c) (h24 b c)
f: A' -> A
g: B' -> B
h: C' -> C

{| j1 := fun x : A' => j1 k (f x); j2 := fun x : B' => j2 k (g x); j3 := fun x : C' => j3 k (h x); j12 := fun (a : A') (b : B') => j12 k (f a) (g b); j13 := fun (a : A') (c : C') => j13 k (f a) (h c); j23 := fun (b : B') (c : C') => j23 k (g b) (h c); j123 := fun (a : A') (b : B') (c : C') => j123 k (f a) (g b) (h c) |} $== {| j1 := fun x : A' => j1 l (f x); j2 := fun x : B' => j2 l (g x); j3 := fun x : C' => j3 l (h x); j12 := fun (a : A') (b : B') => j12 l (f a) (g b); j13 := fun (a : A') (c : C') => j13 l (f a) (h c); j23 := fun (b : B') (c : C') => j23 l (g b) (h c); j123 := fun (a : A') (b : B') (c : C') => j123 l (f a) (g b) (h c) |}
snrapply Build_TriJoinRecPath; intros; cbn; apply_hyp. (* E.g., the first goal is [j1 k (f a) = j1 l (f a)], and this is solved by [h1 p (f a)]. We just precompose all fields of [p] with [f], [g] and [h]. *) Defined. (** Homotopies between the triple are also respected. *)
A, B, C, A', B', C', P: Type
k: TriJoinRecData A B C P
f, f': A' -> A
g, g': B' -> B
h, h': C' -> C
p: f == f'
q: g == g'
r: h == h'

trijoinrecdata_tricomp k f g h $== trijoinrecdata_tricomp k f' g' h'
A, B, C, A', B', C', P: Type
k: TriJoinRecData A B C P
f, f': A' -> A
g, g': B' -> B
h, h': C' -> C
p: f == f'
q: g == g'
r: h == h'

trijoinrecdata_tricomp k f g h $== trijoinrecdata_tricomp k f' g' h'
A, B, C, A', B', C', P: Type
k: TriJoinRecData A B C P
f, f': A' -> A
g, g': B' -> B
h, h': C' -> C
p: f == f'
q: g == g'
r: h == h'
a: A'

j1 k (f a) = j1 k (f' a)
A, B, C, A', B', C', P: Type
k: TriJoinRecData A B C P
f, f': A' -> A
g, g': B' -> B
h, h': C' -> C
p: f == f'
q: g == g'
r: h == h'
b: B'
j2 k (g b) = j2 k (g' b)
A, B, C, A', B', C', P: Type
k: TriJoinRecData A B C P
f, f': A' -> A
g, g': B' -> B
h, h': C' -> C
p: f == f'
q: g == g'
r: h == h'
c: C'
j3 k (h c) = j3 k (h' c)
A, B, C, A', B', C', P: Type
k: TriJoinRecData A B C P
f, f': A' -> A
g, g': B' -> B
h, h': C' -> C
p: f == f'
q: g == g'
r: h == h'
a: A'
b: B'
j12 k (f a) (g b) @ ?Goal0 = ?Goal @ j12 k (f' a) (g' b)
A, B, C, A', B', C', P: Type
k: TriJoinRecData A B C P
f, f': A' -> A
g, g': B' -> B
h, h': C' -> C
p: f == f'
q: g == g'
r: h == h'
a: A'
c: C'
j13 k (f a) (h c) @ ?Goal1 = ?Goal @ j13 k (f' a) (h' c)
A, B, C, A', B', C', P: Type
k: TriJoinRecData A B C P
f, f': A' -> A
g, g': B' -> B
h, h': C' -> C
p: f == f'
q: g == g'
r: h == h'
b: B'
c: C'
j23 k (g b) (h c) @ ?Goal1 = ?Goal0 @ j23 k (g' b) (h' c)
A, B, C, A', B', C', P: Type
k: TriJoinRecData A B C P
f, f': A' -> A
g, g': B' -> B
h, h': C' -> C
p: f == f'
q: g == g'
r: h == h'
a: A'
b: B'
c: C'
prism (j123 k (f a) (g b) (h c)) (j123 k (f' a) (g' b) (h' c)) ?Goal2 ?Goal3 ?Goal4
A, B, C, A', B', C', P: Type
k: TriJoinRecData A B C P
f, f': A' -> A
g, g': B' -> B
h, h': C' -> C
p: f == f'
q: g == g'
r: h == h'
a: A'

j1 k (f a) = j1 k (f' a)
apply ap, p.
A, B, C, A', B', C', P: Type
k: TriJoinRecData A B C P
f, f': A' -> A
g, g': B' -> B
h, h': C' -> C
p: f == f'
q: g == g'
r: h == h'
b: B'

j2 k (g b) = j2 k (g' b)
apply ap, q.
A, B, C, A', B', C', P: Type
k: TriJoinRecData A B C P
f, f': A' -> A
g, g': B' -> B
h, h': C' -> C
p: f == f'
q: g == g'
r: h == h'
c: C'

j3 k (h c) = j3 k (h' c)
apply ap, r.
A, B, C, A', B', C', P: Type
k: TriJoinRecData A B C P
f, f': A' -> A
g, g': B' -> B
h, h': C' -> C
p: f == f'
q: g == g'
r: h == h'
a: A'
b: B'

j12 k (f a) (g b) @ ap (j2 k) (q b) = ap (j1 k) (p a) @ j12 k (f' a) (g' b)
induction (p a), (q b); by apply equiv_p1_1q.
A, B, C, A', B', C', P: Type
k: TriJoinRecData A B C P
f, f': A' -> A
g, g': B' -> B
h, h': C' -> C
p: f == f'
q: g == g'
r: h == h'
a: A'
c: C'

j13 k (f a) (h c) @ ap (j3 k) (r c) = ap (j1 k) (p a) @ j13 k (f' a) (h' c)
induction (p a), (r c); by apply equiv_p1_1q.
A, B, C, A', B', C', P: Type
k: TriJoinRecData A B C P
f, f': A' -> A
g, g': B' -> B
h, h': C' -> C
p: f == f'
q: g == g'
r: h == h'
b: B'
c: C'

j23 k (g b) (h c) @ ap (j3 k) (r c) = ap (j2 k) (q b) @ j23 k (g' b) (h' c)
induction (q b), (r c); by apply equiv_p1_1q.
A, B, C, A', B', C', P: Type
k: TriJoinRecData A B C P
f, f': A' -> A
g, g': B' -> B
h, h': C' -> C
p: f == f'
q: g == g'
r: h == h'
a: A'
b: B'
c: C'

prism (j123 k (f a) (g b) (h c)) (j123 k (f' a) (g' b) (h' c)) (let p0 := p a in let a0 := f' a in paths_rect A (f a) (fun (a1 : A) (p1 : f a = a1) => j12 k (f a) (g b) @ ap (j2 k) (q b) = ap (j1 k) p1 @ j12 k a1 (g' b)) (let p1 := q b in let b0 := g' b in match p1 as p in (_ = b1) return (j12 k (f a) (g b) @ ap (j2 k) p = ap (j1 k) 1 @ j12 k (f a) b1) with | 1 => let X := equiv_fun equiv_p1_1q in X 1 end) a0 p0) (let p0 := p a in let a0 := f' a in paths_rect A (f a) (fun (a1 : A) (p1 : f a = a1) => j13 k (f a) (h c) @ ap (j3 k) (r c) = ap (j1 k) p1 @ j13 k a1 (h' c)) (let p1 := r c in let c0 := h' c in match p1 as p in (_ = c1) return (j13 k (f a) (h c) @ ap (j3 k) p = ap (j1 k) 1 @ j13 k (f a) c1) with | 1 => let X := equiv_fun equiv_p1_1q in X 1 end) a0 p0) (let p0 := q b in let b0 := g' b in paths_rect B (g b) (fun (b1 : B) (p1 : g b = b1) => j23 k (g b) (h c) @ ap (j3 k) (r c) = ap (j2 k) p1 @ j23 k b1 (h' c)) (let p1 := r c in let c0 := h' c in match p1 as p in (_ = c1) return (j23 k (g b) (h c) @ ap (j3 k) p = ap (j2 k) 1 @ j23 k (g b) c1) with | 1 => let X := equiv_fun equiv_p1_1q in X 1 end) b0 p0)
induction (p a), (q b), (r c); apply prism_id. Defined. (** ** Functoriality of [TriJoin] via [functor_trijoin] *) (** To define [functor_trijoin], we simply precompose the canonical [TriJoinRecData] with [f], [g] and [h]. For example, this has [j1 := join1 o f] and [j12 := fun a b => join12 (f a) (g b)]. *) Definition functor_trijoin {A B C A' B' C'} (f : A -> A') (g : B -> B') (h : C -> C') : TriJoin A B C -> TriJoin A' B' C' := trijoin_rec (trijoinrecdata_tricomp (trijoinrecdata_trijoin A' B' C') f g h). (** We use [functor_trijoin] to express a partial functoriality of [trijoin_rec] in [A], [B] and [C]. *)
A, B, C, A', B', C', P: Type
k: TriJoinRecData A' B' C' P
f: A -> A'
g: B -> B'
h: C -> C'

trijoin_rec k o functor_trijoin f g h == trijoin_rec (trijoinrecdata_tricomp k f g h)
A, B, C, A', B', C', P: Type
k: TriJoinRecData A' B' C' P
f: A -> A'
g: B -> B'
h: C -> C'

trijoin_rec k o functor_trijoin f g h == trijoin_rec (trijoinrecdata_tricomp k f g h)
(* On the LHS, we use naturality of the [trijoin_rec] inside [functor_trijoin]: *)
A, B, C, A', B', C', P: Type
k: TriJoinRecData A' B' C' P
f: A -> A'
g: B -> B'
h: C -> C'

trijoin_rec (trijoinrecdata_fun (trijoin_rec k) (trijoinrecdata_tricomp (trijoinrecdata_trijoin A' B' C') f g h)) $== trijoin_rec (trijoinrecdata_tricomp k f g h)
A, B, C, A', B', C', P: Type
k: TriJoinRecData A' B' C' P
f: A -> A'
g: B -> B'
h: C -> C'

trijoinrecdata_fun (trijoin_rec k) (trijoinrecdata_tricomp (trijoinrecdata_trijoin A' B' C') f g h) $-> trijoinrecdata_tricomp k f g h
(* Just to clarify to the reader what is going on: *)
A, B, C, A', B', C', P: Type
k: TriJoinRecData A' B' C' P
f: A -> A'
g: B -> B'
h: C -> C'

trijoinrecdata_tricomp (trijoin_rec_inv (trijoin_rec k)) f g h $-> trijoinrecdata_tricomp k f g h
exact (trijoinrecdata_tricomp_0fun (trijoin_rec_beta k) f g h). Defined. (** Now we have all of the tools to efficiently prove functoriality. *)
A, B, C, A', B', C', A'', B'', C'': Type
f: A -> A'
g: B -> B'
h: C -> C'
f': A' -> A''
g': B' -> B''
h': C' -> C''

functor_trijoin (f' o f) (g' o g) (h' o h) == functor_trijoin f' g' h' o functor_trijoin f g h
A, B, C, A', B', C', A'', B'', C'': Type
f: A -> A'
g: B -> B'
h: C -> C'
f': A' -> A''
g': B' -> B''
h': C' -> C''

functor_trijoin (f' o f) (g' o g) (h' o h) == functor_trijoin f' g' h' o functor_trijoin f g h
A, B, C, A', B', C', A'', B'', C'': Type
f: A -> A'
g: B -> B'
h: C -> C'
f': A' -> A''
g': B' -> B''
h': C' -> C''

functor_trijoin f' g' h' o functor_trijoin f g h == functor_trijoin (f' o f) (g' o g) (h' o h)
nrapply trijoin_rec_functor_trijoin. Defined.
A, B, C: Type

functor_trijoin idmap idmap idmap == (idmap : TriJoin A B C -> TriJoin A B C)
A, B, C: Type

functor_trijoin idmap idmap idmap == (idmap : TriJoin A B C -> TriJoin A B C)
A, B, C: Type

trijoinrecdata_tricomp (trijoinrecdata_trijoin A B C) idmap idmap idmap $== trijoin_rec_inv idmap
A, B, C: Type

trijoinrecdata_trijoin A B C $== trijoinrecdata_fun idmap (trijoinrecdata_trijoin A B C)
A, B, C: Type

trijoinrecdata_fun idmap (trijoinrecdata_trijoin A B C) $== trijoinrecdata_trijoin A B C
exact (fmap_id (trijoinrecdata_0gpd A B C) _ (trijoinrecdata_trijoin A B C)). Defined.
A, B, C, A', B', C': Type
f, f': A -> A'
g, g': B -> B'
h, h': C -> C'
p: f == f'
q: g == g'
r: h == h'

functor_trijoin f g h == functor_trijoin f' g' h'
A, B, C, A', B', C': Type
f, f': A -> A'
g, g': B -> B'
h, h': C -> C'
p: f == f'
q: g == g'
r: h == h'

functor_trijoin f g h == functor_trijoin f' g' h'
A, B, C, A', B', C': Type
f, f': A -> A'
g, g': B -> B'
h, h': C -> C'
p: f == f'
q: g == g'
r: h == h'

trijoin_rec (trijoinrecdata_tricomp (trijoinrecdata_trijoin A' B' C') f g h) == trijoin_rec (trijoinrecdata_tricomp (trijoinrecdata_trijoin A' B' C') f' g' h')
A, B, C, A', B', C': Type
f, f': A -> A'
g, g': B -> B'
h, h': C -> C'
p: f == f'
q: g == g'
r: h == h'

trijoinrecdata_tricomp (trijoinrecdata_trijoin A' B' C') f g h $-> trijoinrecdata_tricomp (trijoinrecdata_trijoin A' B' C') f' g' h'
apply (trijoinrecdata_tricomp2 _ p q r). Defined.
A, B, C, A', B', C': Type
f: A -> A'
IsEquiv0: IsEquiv f
g: B -> B'
IsEquiv1: IsEquiv g
h: C -> C'
IsEquiv2: IsEquiv h

IsEquiv (functor_trijoin f g h)
A, B, C, A', B', C': Type
f: A -> A'
IsEquiv0: IsEquiv f
g: B -> B'
IsEquiv1: IsEquiv g
h: C -> C'
IsEquiv2: IsEquiv h

IsEquiv (functor_trijoin f g h)
(* This proof is almost identical to the proof of [isequiv_functor_join]. *)
A, B, C, A', B', C': Type
f: A -> A'
IsEquiv0: IsEquiv f
g: B -> B'
IsEquiv1: IsEquiv g
h: C -> C'
IsEquiv2: IsEquiv h

TriJoin A' B' C' -> TriJoin A B C
A, B, C, A', B', C': Type
f: A -> A'
IsEquiv0: IsEquiv f
g: B -> B'
IsEquiv1: IsEquiv g
h: C -> C'
IsEquiv2: IsEquiv h
functor_trijoin f g h o ?g == idmap
A, B, C, A', B', C': Type
f: A -> A'
IsEquiv0: IsEquiv f
g: B -> B'
IsEquiv1: IsEquiv g
h: C -> C'
IsEquiv2: IsEquiv h
?g o functor_trijoin f g h == idmap
A, B, C, A', B', C': Type
f: A -> A'
IsEquiv0: IsEquiv f
g: B -> B'
IsEquiv1: IsEquiv g
h: C -> C'
IsEquiv2: IsEquiv h

TriJoin A' B' C' -> TriJoin A B C
apply (functor_trijoin f^-1 g^-1 h^-1).
A, B, C, A', B', C': Type
f: A -> A'
IsEquiv0: IsEquiv f
g: B -> B'
IsEquiv1: IsEquiv g
h: C -> C'
IsEquiv2: IsEquiv h

functor_trijoin f g h o functor_trijoin f^-1 g^-1 h^-1 == idmap
A, B, C, A', B', C': Type
f: A -> A'
IsEquiv0: IsEquiv f
g: B -> B'
IsEquiv1: IsEquiv g
h: C -> C'
IsEquiv2: IsEquiv h

functor_trijoin f g h o functor_trijoin f^-1 g^-1 h^-1 == ?Goal
A, B, C, A', B', C': Type
f: A -> A'
IsEquiv0: IsEquiv f
g: B -> B'
IsEquiv1: IsEquiv g
h: C -> C'
IsEquiv2: IsEquiv h
?Goal == idmap
A, B, C, A', B', C': Type
f: A -> A'
IsEquiv0: IsEquiv f
g: B -> B'
IsEquiv1: IsEquiv g
h: C -> C'
IsEquiv2: IsEquiv h

functor_trijoin (fun x : A' => f (f^-1 x)) (fun x : B' => g (g^-1 x)) (fun x : C' => h (h^-1 x)) == idmap
A, B, C, A', B', C': Type
f: A -> A'
IsEquiv0: IsEquiv f
g: B -> B'
IsEquiv1: IsEquiv g
h: C -> C'
IsEquiv2: IsEquiv h

functor_trijoin (fun x : A' => f (f^-1 x)) (fun x : B' => g (g^-1 x)) (fun x : C' => h (h^-1 x)) == ?Goal
A, B, C, A', B', C': Type
f: A -> A'
IsEquiv0: IsEquiv f
g: B -> B'
IsEquiv1: IsEquiv g
h: C -> C'
IsEquiv2: IsEquiv h
?Goal == idmap
A, B, C, A', B', C': Type
f: A -> A'
IsEquiv0: IsEquiv f
g: B -> B'
IsEquiv1: IsEquiv g
h: C -> C'
IsEquiv2: IsEquiv h

functor_trijoin idmap idmap idmap == idmap
apply functor_trijoin_idmap.
A, B, C, A', B', C': Type
f: A -> A'
IsEquiv0: IsEquiv f
g: B -> B'
IsEquiv1: IsEquiv g
h: C -> C'
IsEquiv2: IsEquiv h

functor_trijoin f^-1 g^-1 h^-1 o functor_trijoin f g h == idmap
A, B, C, A', B', C': Type
f: A -> A'
IsEquiv0: IsEquiv f
g: B -> B'
IsEquiv1: IsEquiv g
h: C -> C'
IsEquiv2: IsEquiv h

functor_trijoin f^-1 g^-1 h^-1 o functor_trijoin f g h == ?Goal
A, B, C, A', B', C': Type
f: A -> A'
IsEquiv0: IsEquiv f
g: B -> B'
IsEquiv1: IsEquiv g
h: C -> C'
IsEquiv2: IsEquiv h
?Goal == idmap
A, B, C, A', B', C': Type
f: A -> A'
IsEquiv0: IsEquiv f
g: B -> B'
IsEquiv1: IsEquiv g
h: C -> C'
IsEquiv2: IsEquiv h

functor_trijoin (fun x : A => f^-1 (f x)) (fun x : B => g^-1 (g x)) (fun x : C => h^-1 (h x)) == idmap
A, B, C, A', B', C': Type
f: A -> A'
IsEquiv0: IsEquiv f
g: B -> B'
IsEquiv1: IsEquiv g
h: C -> C'
IsEquiv2: IsEquiv h

functor_trijoin (fun x : A => f^-1 (f x)) (fun x : B => g^-1 (g x)) (fun x : C => h^-1 (h x)) == ?Goal
A, B, C, A', B', C': Type
f: A -> A'
IsEquiv0: IsEquiv f
g: B -> B'
IsEquiv1: IsEquiv g
h: C -> C'
IsEquiv2: IsEquiv h
?Goal == idmap
A, B, C, A', B', C': Type
f: A -> A'
IsEquiv0: IsEquiv f
g: B -> B'
IsEquiv1: IsEquiv g
h: C -> C'
IsEquiv2: IsEquiv h

functor_trijoin idmap idmap idmap == idmap
apply functor_trijoin_idmap. Defined. Definition equiv_functor_trijoin {A B C A' B' C'} (f : A <~> A') (g : B <~> B') (h : C <~> C') : TriJoin A B C <~> TriJoin A' B' C' := Build_Equiv _ _ (functor_trijoin f g h) _. (** ** The relationship between [functor_trijoin] and [functor_join]. *) (** While [functor_trijoin] is convenient to work with, we want to know that [functor_trijoin f g h] is homotopic to [functor_join f (functor_join g h)]. This is worked out using the next three results. *) (** A lemma that handles the path algebra in the next result. [BC] here is [Join B C] there, [bc] here is [jglue b c] there, [bc'] here is [jg g b c] there, and [beta_jg] here is [Join_rec_beta_jglue _ _ _ b c] there. *)
A, BC, A', P: Type
f: A -> A'
g: BC -> P
a: A
b, c: BC
bc: b = c
bc': g b = g c
beta_jg: ap g bc = bc'

ap_triangle (functor_join f g) (triangle_v a bc) @ functor_join_beta_jglue f g a c = (functor_join_beta_jglue f g a b @@ ((ap_compose joinr (functor_join f g) bc)^ @ (ap_compose g joinr bc @ ap (ap joinr) beta_jg))) @ triangle_v (f a) bc'
A, BC, A', P: Type
f: A -> A'
g: BC -> P
a: A
b, c: BC
bc: b = c
bc': g b = g c
beta_jg: ap g bc = bc'

ap_triangle (functor_join f g) (triangle_v a bc) @ functor_join_beta_jglue f g a c = (functor_join_beta_jglue f g a b @@ ((ap_compose joinr (functor_join f g) bc)^ @ (ap_compose g joinr bc @ ap (ap joinr) beta_jg))) @ triangle_v (f a) bc'
A, BC, A', P: Type
f: A -> A'
g: BC -> P
a: A
b: BC

ap_triangle (functor_join f g) (concat_p1 (jglue a b)) @ functor_join_beta_jglue f g a b = (functor_join_beta_jglue f g a b @@ 1) @ concat_p1 (jglue (f a) (g b))
A, BC, A', P: Type
f: A -> A'
g: BC -> P
a: A
b: BC

ap_triangle (functor_join f g) (concat_p1 (jglue a b)) @ functor_join_beta_jglue f g a b = concat_p1 (ap (functor_join f g) (jglue a b)) @ functor_join_beta_jglue f g a b
A, BC, A', P: Type
f: A -> A'
g: BC -> P
a: A
b: BC
concat_p1 (ap (functor_join f g) (jglue a b)) @ functor_join_beta_jglue f g a b = (functor_join_beta_jglue f g a b @@ 1) @ concat_p1 (jglue (f a) (g b))
A, BC, A', P: Type
f: A -> A'
g: BC -> P
a: A
b: BC

ap_triangle (functor_join f g) (concat_p1 (jglue a b)) @ functor_join_beta_jglue f g a b = concat_p1 (ap (functor_join f g) (jglue a b)) @ functor_join_beta_jglue f g a b
A, BC, A', P: Type
f: A -> A'
g: BC -> P
a: A
b: BC

ap_triangle (functor_join f g) (concat_p1 (jglue a b)) = concat_p1 (ap (functor_join f g) (jglue a b))
A, BC, A', P: Type
f: A -> A'
g: BC -> P
a: A
b: BC

(ap_pp (functor_join f g) (jglue a b) 1)^ @ ap (ap (functor_join f g)) (concat_p1 (jglue a b)) = concat_p1 (ap (functor_join f g) (jglue a b))
A, BC, A', P: Type
f: A -> A'
g: BC -> P
a: A
b: BC

ap_pp (functor_join f g) (jglue a b) 1 @ concat_p1 (ap (functor_join f g) (jglue a b)) = ap (ap (functor_join f g)) (concat_p1 (jglue a b))
exact (ap_pp_concat_p1 (functor_join f g) (jglue a b)).
A, BC, A', P: Type
f: A -> A'
g: BC -> P
a: A
b: BC

concat_p1 (ap (functor_join f g) (jglue a b)) @ functor_join_beta_jglue f g a b = (functor_join_beta_jglue f g a b @@ 1) @ concat_p1 (jglue (f a) (g b))
A, BC, A', P: Type
f: A -> A'
g: BC -> P
a: A
b: BC

(concat_p1 (ap (functor_join f g) (jglue a b)))^ @ ((functor_join_beta_jglue f g a b @@ 1) @ concat_p1 (jglue (f a) (g b))) = functor_join_beta_jglue f g a b
exact (concat_p_pp _ _ _ @ whiskerR_p1 _). Defined. (** We'll generalize the situation a bit to keep things less verbose. [join_rec g] here will be [functor_join g h] in the next result. Maybe this extra generality will also be useful sometime? *)
A, B, C, A', P: Type
f: A -> A'
g: JoinRecData B C P

functor_join f (join_rec g) == trijoin_rec {| j1 := joinl o f; j2 := joinr o jl g; j3 := joinr o jr g; j12 := fun (a : A) (b : B) => jglue (f a) (jl g b); j13 := fun (a : A) (c : C) => jglue (f a) (jr g c); j23 := fun (b : B) (c : C) => ap joinr (jg g b c); j123 := fun (a : A) (b : B) (c : C) => triangle_v (f a) (jg g b c) |}
A, B, C, A', P: Type
f: A -> A'
g: JoinRecData B C P

functor_join f (join_rec g) == trijoin_rec {| j1 := joinl o f; j2 := joinr o jl g; j3 := joinr o jr g; j12 := fun (a : A) (b : B) => jglue (f a) (jl g b); j13 := fun (a : A) (c : C) => jglue (f a) (jr g c); j23 := fun (b : B) (c : C) => ap joinr (jg g b c); j123 := fun (a : A) (b : B) (c : C) => triangle_v (f a) (jg g b c) |}
(* Recall that [trijoin_rec] is defined to be the inverse of [trijoin_rec_inv_natequiv ...]. *)
A, B, C, A', P: Type
f: A -> A'
g: JoinRecData B C P

equiv_fun_0gpd (trijoin_rec_inv_natequiv A B C (Join A' P)) (functor_join f (join_rec g)) $== {| j1 := fun x : A => joinl (f x); j2 := fun x : B => joinr (jl g x); j3 := fun x : C => joinr (jr g x); j12 := fun (a : A) (b : B) => jglue (f a) (jl g b); j13 := fun (a : A) (c : C) => jglue (f a) (jr g c); j23 := fun (b : B) (c : C) => ap joinr (jg g b c); j123 := fun (a : A) (b : B) (c : C) => triangle_v (f a) (jg g b c) |}
(* The next two lines aren't needed, but clarify the goal. *)
A, B, C, A', P: Type
f: A -> A'
g: JoinRecData B C P

TriJoinRecPath (trijoinrecdata_fun (functor_join f (join_rec g)) (trijoinrecdata_trijoin A B C)) {| j1 := fun x : A => joinl (f x); j2 := fun x : B => joinr (jl g x); j3 := fun x : C => joinr (jr g x); j12 := fun (a : A) (b : B) => jglue (f a) (jl g b); j13 := fun (a : A) (c : C) => jglue (f a) (jr g c); j23 := fun (b : B) (c : C) => ap joinr (jg g b c); j123 := fun (a : A) (b : B) (c : C) => triangle_v (f a) (jg g b c) |}
A, B, C, A', P: Type
f: A -> A'
g: JoinRecData B C P

TriJoinRecPath {| j1 := fun x : A => joinl (f x); j2 := fun x : B => joinr (jl g x); j3 := fun x : C => joinr (jr g x); j12 := fun (a : A) (b : B) => ap (functor_join f (join_rec g)) (join12 a b); j13 := fun (a : A) (c : C) => ap (functor_join f (join_rec g)) (join13 a c); j23 := fun (b : B) (c : C) => ap (functor_join f (join_rec g)) (join23 b c); j123 := fun (a : A) (b : B) (c : C) => ap_triangle (functor_join f (join_rec g)) (join123 a b c) |} {| j1 := fun x : A => joinl (f x); j2 := fun x : B => joinr (jl g x); j3 := fun x : C => joinr (jr g x); j12 := fun (a : A) (b : B) => jglue (f a) (jl g b); j13 := fun (a : A) (c : C) => jglue (f a) (jr g c); j23 := fun (b : B) (c : C) => ap joinr (jg g b c); j123 := fun (a : A) (b : B) (c : C) => triangle_v (f a) (jg g b c) |}
A, B, C, A', P: Type
f: A -> A'
g: JoinRecData B C P
a: A
b: B

ap (functor_join f (join_rec g)) (join12 a b) = jglue (f a) (jl g b)
A, B, C, A', P: Type
f: A -> A'
g: JoinRecData B C P
a: A
c: C
ap (functor_join f (join_rec g)) (join13 a c) = jglue (f a) (jr g c)
A, B, C, A', P: Type
f: A -> A'
g: JoinRecData B C P
b: B
c: C
ap (functor_join f (join_rec g)) (join23 b c) = ap joinr (jg g b c)
A, B, C, A', P: Type
f: A -> A'
g: JoinRecData B C P
a: A
b: B
c: C
prism' (ap_triangle (functor_join f (join_rec g)) (join123 a b c)) (triangle_v (f a) (jg g b c)) ?Goal ?Goal0 ?Goal1
A, B, C, A', P: Type
f: A -> A'
g: JoinRecData B C P
a: A
b: B

ap (functor_join f (join_rec g)) (join12 a b) = jglue (f a) (jl g b)
exact (functor_join_beta_jglue f _ a (joinl b)).
A, B, C, A', P: Type
f: A -> A'
g: JoinRecData B C P
a: A
c: C

ap (functor_join f (join_rec g)) (join13 a c) = jglue (f a) (jr g c)
exact (functor_join_beta_jglue f _ a (joinr c)).
A, B, C, A', P: Type
f: A -> A'
g: JoinRecData B C P
b: B
c: C

ap (functor_join f (join_rec g)) (join23 b c) = ap joinr (jg g b c)
A, B, C, A', P: Type
f: A -> A'
g: JoinRecData B C P
b: B
c: C

ap (functor_join f (join_rec g)) (ap joinr (jglue b c)) = ap joinr (jg g b c)
A, B, C, A', P: Type
f: A -> A'
g: JoinRecData B C P
b: B
c: C

ap (fun x : Join B C => functor_join f (join_rec g) (joinr x)) (jglue b c) = ap joinr (jg g b c)
A, B, C, A', P: Type
f: A -> A'
g: JoinRecData B C P
b: B
c: C

ap (fun x : Join B C => joinr (join_rec g x)) (jglue b c) = ap joinr (jg g b c)
A, B, C, A', P: Type
f: A -> A'
g: JoinRecData B C P
b: B
c: C

ap joinr (ap (join_rec g) (jglue b c)) = ap joinr (jg g b c)
A, B, C, A', P: Type
f: A -> A'
g: JoinRecData B C P
b: B
c: C

ap (join_rec g) (jglue b c) = jg g b c
apply join_rec_beta_jg.
A, B, C, A', P: Type
f: A -> A'
g: JoinRecData B C P
a: A
b: B
c: C

prism' (ap_triangle (functor_join f (join_rec g)) (join123 a b c)) (triangle_v (f a) (jg g b c)) (functor_join_beta_jglue f (join_rec g) a (joinl b)) (functor_join_beta_jglue f (join_rec g) a (joinr c)) ((ap_compose joinr (functor_join f (join_rec g)) (jglue b c))^ @ (ap_compose (join_rec g) joinr (jglue b c) @ ap (ap joinr) (join_rec_beta_jg g b c) : ap (fun x : Join B C => functor_join f (join_rec g) (joinr x)) (jglue b c) = ap joinr (jg g b c)) : ap (functor_join f (join_rec g)) (join23 b c) = ap joinr (jg g b c))
A, B, C, A', P: Type
f: A -> A'
g: JoinRecData B C P
a: A
b: B
c: C

ap_triangle (functor_join f (join_rec g)) (join123 a b c) @ functor_join_beta_jglue f (join_rec g) a (joinr c) = (functor_join_beta_jglue f (join_rec g) a (joinl b) @@ ((ap_compose joinr (functor_join f (join_rec g)) (jglue b c))^ @ (ap_compose (join_rec g) joinr (jglue b c) @ ap (ap joinr) (join_rec_beta_jg g b c)))) @ triangle_v (f a) (jg g b c)
A, B, C, A', P: Type
f: A -> A'
g: JoinRecData B C P
a: A
b: B
c: C

ap_triangle (functor_join f (join_rec g)) (triangle_v a (jglue b c)) @ functor_join_beta_jglue f (join_rec g) a (joinr c) = (functor_join_beta_jglue f (join_rec g) a (joinl b) @@ ((ap_compose joinr (functor_join f (join_rec g)) (jglue b c))^ @ (ap_compose (join_rec g) joinr (jglue b c) @ ap (ap joinr) (join_rec_beta_jg g b c)))) @ triangle_v (f a) (jg g b c)
exact (ap_triangle_functor_join f (join_rec g) a (jglue b c) (jg g b c) (Join_rec_beta_jglue _ _ _ b c)). Defined. Definition functor_trijoin_as_functor_join {A B C A' B' C'} (f : A -> A') (g : B -> B') (h : C -> C') : functor_join f (functor_join g h) == functor_trijoin f g h := functor_join_join_rec f (functor_join_recdata g h).