Built with Alectryon, running Coq+SerAPI v8.19.0+0.19.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. *)SectionTriJoinStructure.Context {ABC : Type}.DefinitionTriJoin := Join A (Join B C).Definitionjoin1 : A -> TriJoin := joinl.Definitionjoin2 : B -> TriJoin := funb => (joinr (joinl b)).Definitionjoin3 : C -> TriJoin := func => (joinr (joinr c)).Definitionjoin12 : forallab, join1 a = join2 b := funab => jglue a (joinl b).Definitionjoin13 : forallac, join1 a = join3 c := funac => jglue a (joinr c).Definitionjoin23 : forallbc, join2 b = join3 c := funbc => ap joinr (jglue b c).Definitionjoin123 : forallabc, join12 a b @ join23 b c = join13 a c := funabc => triangle_v a (jglue b c).EndTriJoinStructure.Arguments TriJoin A B C : clear implicits.(** ** [ap_trijoin] and [ap_trijoin_transport] *)(** Functions send triangles to triangles. *)Definitionap_triangle {XY} (f : X -> Y)
{abc : 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: forallw : 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: forallw : 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: forallw : 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: forallw : 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)
napply ap_trijoin_general.Defined.
J, W, P: Type f: J -> P a: J jr: W -> J jg: forallw : 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 (funx : W => ap f (jg x)) p
J, W, P: Type f: J -> P a: J jr: W -> J jg: forallw : 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 (funx : W => ap f (jg x)) p
J, W, P: Type f: J -> P a: J jr: W -> J jg: forallw : 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 (funx : W => ap f (jg x)) 1
J, W, P: Type f: J -> P a: J jr: W -> J jg: forallw : 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: forallw : 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 (funx : 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 (funx : Join B C => ap f (jglue a x)) (jglue b c)
napply ap_trijoin_general_transport.Defined.
J, W, P: Type f: J -> P a: J jr: W -> J jg: forallw : 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: forallw : 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: forallw : 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: forallw : 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)))
byinduction (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)^
napply 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 (funx : BC => transport P (jglue a x) j1') bc)^ @
ap (transport (funx : 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 (funx : BC => transport P (jglue a x) j1') bc)^ @
ap (transport (funx : 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 (funx : 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 (funx : 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 (funx : 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': foralla : A, P (join1 a) join2': forallb : B, P (join2 b) join3': forallc : 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
forallx : TriJoin A B C, P x
A, B, C: Type P: TriJoin A B C -> Type join1': foralla : A, P (join1 a) join2': forallb : B, P (join2 b) join3': forallc : 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
forallx : TriJoin A B C, P x
A, B, C: Type P: TriJoin A B C -> Type join1': foralla : A, P (join1 a) join2': forallb : B, P (join2 b) join3': forallc : 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
foralla : A, P (joinl a)
A, B, C: Type P: TriJoin A B C -> Type join1': foralla : A, P (join1 a) join2': forallb : B, P (join2 b) join3': forallc : 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
forallb : Join B C, P (joinr b)
A, B, C: Type P: TriJoin A B C -> Type join1': foralla : A, P (join1 a) join2': forallb : B, P (join2 b) join3': forallc : 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': foralla : A, P (join1 a) join2': forallb : B, P (join2 b) join3': forallc : 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
foralla : A, P (joinl a)
exact join1'.
A, B, C: Type P: TriJoin A B C -> Type join1': foralla : A, P (join1 a) join2': forallb : B, P (join2 b) join3': forallc : 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
forallb : Join B C, P (joinr b)
A, B, C: Type P: TriJoin A B C -> Type join1': foralla : A, P (join1 a) join2': forallb : B, P (join2 b) join3': forallc : 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
foralla : B,
(funx : Join B C => P (joinr x)) (joinl a)
A, B, C: Type P: TriJoin A B C -> Type join1': foralla : A, P (join1 a) join2': forallb : B, P (join2 b) join3': forallc : 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
forallb : C,
(funx : Join B C => P (joinr x)) (joinr b)
A, B, C: Type P: TriJoin A B C -> Type join1': foralla : A, P (join1 a) join2': forallb : B, P (join2 b) join3': forallc : 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 (funx : 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': foralla : A, P (join1 a) join2': forallb : B, P (join2 b) join3': forallc : 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
foralla : B,
(funx : Join B C => P (joinr x)) (joinl a)
exact join2'.
A, B, C: Type P: TriJoin A B C -> Type join1': foralla : A, P (join1 a) join2': forallb : B, P (join2 b) join3': forallc : 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
forallb : C,
(funx : Join B C => P (joinr x)) (joinr b)
exact join3'.
A, B, C: Type P: TriJoin A B C -> Type join1': foralla : A, P (join1 a) join2': forallb : B, P (join2 b) join3': forallc : 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 (funx : Join B C => P (joinr x))
(jglue a b) (join2' a) =
join3' b
A, B, C: Type P: TriJoin A B C -> Type join1': foralla : A, P (join1 a) join2': forallb : B, P (join2 b) join3': forallc : 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 (funx : Join B C => P (joinr x))
(jglue b c) (join2' b) =
join3' c
A, B, C: Type P: TriJoin A B C -> Type join1': foralla : A, P (join1 a) join2': forallb : B, P (join2 b) join3': forallc : 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': foralla : A, P (join1 a) join2': forallb : B, P (join2 b) join3': forallc : 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 (funx : 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': foralla : A, P (join1 a) join2': forallb : B, P (join2 b) join3': forallc : 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
forallb : Join B C,
transport P (jglue a b) (join1' a) =
Join_ind (funx : 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': foralla : A, P (join1 a) join2': forallb : B, P (join2 b) join3': forallc : 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
foralla0 : B,
(funx : Join B C =>
transport P (jglue a x) (join1' a) =
Join_ind (funx0 : 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': foralla : A, P (join1 a) join2': forallb : B, P (join2 b) join3': forallc : 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
forallb : C,
(funx : Join B C =>
transport P (jglue a x) (join1' a) =
Join_ind (funx0 : 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': foralla : A, P (join1 a) join2': forallb : B, P (join2 b) join3': forallc : 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
(funx : Join B C =>
transport P (jglue a x) (join1' a) =
Join_ind (funx0 : 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': foralla : A, P (join1 a) join2': forallb : B, P (join2 b) join3': forallc : 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
foralla0 : B,
(funx : Join B C =>
transport P (jglue a x) (join1' a) =
Join_ind (funx0 : 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': foralla : A, P (join1 a) join2': forallb : B, P (join2 b) join3': forallc : 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
foralla0 : 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': foralla : A, P (join1 a) join2': forallb : B, P (join2 b) join3': forallc : 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
forallb : C,
(funx : Join B C =>
transport P (jglue a x) (join1' a) =
Join_ind (funx0 : 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': foralla : A, P (join1 a) join2': forallb : B, P (join2 b) join3': forallc : 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
forallb : 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': foralla : A, P (join1 a) join2': forallb : B, P (join2 b) join3': forallc : 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
(funx : Join B C =>
transport P (jglue a x) (join1' a) =
Join_ind (funx0 : 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
:
foralla1 : B,
(funx : Join B C =>
transport P (jglue a x) (join1' a) =
Join_ind (funx0 : 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
:
forallb0 : C,
(funx : Join B C =>
transport P (jglue a x) (join1' a) =
Join_ind (funx0 : 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': foralla : A, P (join1 a) join2': forallb : B, P (join2 b) join3': forallc : 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
(funx : Join B C =>
transport P (jglue a x) (join1' a) =
Join_ind (funx0 : 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': foralla : A, P (join1 a) join2': forallb : B, P (join2 b) join3': forallc : 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
(funx : Join B C =>
transport P (jglue a x) (join1' a))
(jglue b c))^ @
ap
(transport (funx : Join B C => P (joinr x))
(jglue b c)) (join12' a b)) @
apD
(Join_ind (funx : 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': foralla : A, P (join1 a) join2': forallb : B, P (join2 b) join3': forallc : 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 (funx : 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': foralla : A, P (join1 a) join2': forallb : B, P (join2 b) join3': forallc : 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
(funx : Join B C =>
transport P (jglue a x) (join1' a))
(jglue b c))^ @
ap
(transport (funx : 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': foralla : A, P (join1 a) join2': forallb : B, P (join2 b) join3': forallc : 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
(funx : Join B C =>
transport P (jglue a x) (join1' a))
(jglue b c))^ @
ap
(transport (funx : 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. *)RecordTriJoinRecData {ABCP : Type} := {
j1 : A -> P;
j2 : B -> P;
j3 : C -> P;
j12 : forallab, j1 a = j2 b;
j13 : forallac, j1 a = j3 c;
j23 : forallbc, j2 b = j3 c;
j123 : forallabc, 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
forallb : 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
foralla0 : 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
forallb : 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
(funx : 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
foralla0 : 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
forallb : 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
(funx : 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
(funx : 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. *)Definitiontrijoin_rec_beta_join12 {ABCP : 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 _ _ _ _ _.Definitiontrijoin_rec_beta_join13 {ABCP : 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))
(funa : A =>
Join_ind
(funx : 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
(funx : 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
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
(funx : 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
(funb : Join B C =>
Join_rec (j1 f)
(Join_rec (j2 f) (j3 f) (j23 f))
(funa : A =>
Join_ind
(funx : 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))
(funa : A =>
Join_ind
(funx : 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))
(funa : A =>
Join_ind
(funx : 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
(funx : 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))
(funa : A =>
Join_ind
(funx : 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
(funb : Join B C =>
Join_rec (j1 f)
(Join_rec (j2 f) (j3 f) (j23 f))
(funa : A =>
Join_ind
(funx : 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))
(funa : A =>
Join_ind
(funx : 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))
(funa : A =>
Join_ind
(funx : 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))
(funa : A =>
Join_ind
(funx : 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
(funb : Join B C =>
Join_rec (j1 f)
(Join_rec (j2 f) (j3 f) (j23 f))
(funa : A =>
Join_ind
(funx : 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))
(funa : A =>
Join_ind
(funx : 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))
(funa : A =>
Join_ind
(funx : 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))
(funa : A =>
Join_ind
(funx : 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))
(funa : A =>
Join_ind
(funx : 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
(funq : 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))
(funa : A =>
Join_ind
(funx : 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))
(funa : A =>
Join_ind
(funx : 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). *)napply 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 (funab => 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 (funac => 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 (funbc => 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]. *)Definitiontrijoinrecdata_trijoin (ABC : 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]. *)Definitiontrijoin_rec_inv {ABCP : 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]. *)Definitionprism {P : Type}
{abc : 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
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. *)RecordTriJoinRecPath {ABCP : Type} {fg : TriJoinRecData A B C P} := {
h1 : foralla, j1 f a = j1 g a;
h2 : forallb, j2 f b = j2 g b;
h3 : forallc, j3 f c = j3 g c;
h12 : forallab, j12 f a b @ h2 b = h1 a @ j12 g a b;
h13 : forallac, j13 f a c @ h3 c = h1 a @ j13 g a c;
h23 : forallbc, j23 f b c @ h3 c = h2 b @ j23 g b c;
h123 : forallabc, 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. *)RecordTriJoinRecData' {ABCP : Type} {j1' : A -> P} {j2' : B -> P} {j3' : C -> P} := {
j12' : forallab, j1' a = j2' b;
j13' : forallac, j1' a = j3' c;
j23' : forallbc, j2' b = j3' c;
j123' : forallabc, 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.Definitionprism' {P : Type} {abc : 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'.RecordTriJoinRecPath' {ABCP : Type} {j1' : A -> P} {j2' : B -> P} {j3' : C -> P}
{fg : TriJoinRecData' j1' j2' j3'} := {
h12' : forallab, j12' f a b = j12' g a b;
h13' : forallac, j13' f a c = j13' g a c;
h23' : forallbc, j23' f b c = j23' g b c;
h123' : forallabc, 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. *)Definitionbundle_trijoinrecdata {ABCP : 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).Definitionunbundle_trijoinrecdata {ABCP : 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
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
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
A, B, C, P: Type j1': A -> P j2': B -> P j3': C -> P f, g: TriJoinRecData' j1' j2' j3' h: TriJoinRecPath' f g
foralla : 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
forallb : 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
forallc : 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 @
(funb0 : B => 1) b =
(funa0 : 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 @
(func0 : C => 1) c =
(funa0 : 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 @
(func0 : C => 1) c =
(funb0 : 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) =>
letX := equiv_fun equiv_p1_1q in
X ?Goal@{a:=a0; b:=b0}) a b)
((fun (a0 : A) (c0 : C) =>
letX := equiv_fun equiv_p1_1q in
X ?Goal0@{a:=a0; c:=c0}) a c)
((fun (b0 : B) (c0 : C) =>
letX := 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) =>
letX := equiv_fun equiv_p1_1q in X (h12' h a0 b0))
a b)
((fun (a0 : A) (c0 : C) =>
letX := equiv_fun equiv_p1_1q in X (h13' h a0 c0))
a c)
((fun (b0 : B) (c0 : C) =>
letX := 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. *)Ltacbundle_trijoinrecpath :=
hnf;
match goal with |- TriJoinRecPath ?F?G =>
refine (bundle_trijoinrecpath (f:=unbundle_trijoinrecdata F)
(g:=unbundle_trijoinrecdata G) _) end;
snapply 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. *)
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)^
napply trijoin_rec_beta_join123.Defined.(** We can upgrade this to an unprimed path. This says that [trijoin_rec_inv] is split surjective. *)Definitiontrijoin_rec_beta {ABCP : 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 (bc : P) (ab : a = b) (ac : a = c)
(bc : b = c), ab @ bc = ac -> Type s: Q a a 1111
forall (bc : 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 (bc : P) (ab : a = b) (ac : a = c)
(bc : b = c), ab @ bc = ac -> Type s: Q a a 1111
forall (bc : 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 (bc : P) (ab : a = b) (ac : a = c)
(bc : b = c), ab @ bc = ac -> Type s: Q a a 1111 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 (bc : P) (ab : a = b) (ac : a = c)
(bc : b = c), ab @ bc = ac -> Type s: Q a a 1111 c: P ac, bc: a = c abc: 1 @ bc = ac
Q a c 1 ac bc abc
P: Type a: P Q: forall (bc : P) (ab : a = b) (ac : a = c)
(bc : b = c), ab @ bc = ac -> Type s: Q a a 1111 ac: a = a abc: 1 @ 1 = ac
Q a a 1 ac 1 abc
P: Type a: P Q: forall (bc : P) (ab : a = b) (ac : a = c)
(bc : b = c), ab @ bc = ac -> Type s: Q a a 1111
Q a a 1 (1 @ 1) 11
apply s.Defined.(** We need to explicitly reason about the proof given by [transport_paths FlFr] so we give it a name here. *)
A, B: Type f, g: A -> B x1, x2: A p: x1 = x2 q: f x1 = g x1 r: f x2 = g x2 h: ap f p @ r = q @ ap g p
transport (funx : A => f x = g x) p q = r
A, B: Type f, g: A -> B x1, x2: A p: x1 = x2 q: f x1 = g x1 r: f x2 = g x2 h: ap f p @ r = q @ ap g p
transport (funx : A => f x = g x) p q = r
by transport_paths FlFr.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 (funx : J => f x = g x) ab bc H1 @
ap (transport (funx : J => f x = g x) bc)
(transport_paths_FlFr' ab H1 H2 H12)) @
transport_paths_FlFr' bc H2 H3 H23 =
transport2 (funx : 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 (funx : J => f x = g x) ab bc H1 @
ap (transport (funx : J => f x = g x) bc)
(transport_paths_FlFr' ab H1 H2 H12)) @
transport_paths_FlFr' bc H2 H3 H23 =
transport2 (funx : 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 (bc : 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 (funx : J => f x = g x) ab bc H1 @
ap (transport (funx : J => f x = g x) bc)
(transport_paths_FlFr' ab H1 H2 H12)) @
transport_paths_FlFr' bc H2 H3 H23 =
transport2 (funx : 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 (H2H3 : f a = g a)
(H12 : 1 @ H2 = H1 @ 1) (H13 : 1 @ H3 = H1 @ 1)
(H23 : 1 @ H3 = H2 @ 1),
prism 11 H12 H13 H23 ->
(1 @
ap (transport (funx : 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
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)
foralla : A,
(funx : 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)
forallb : B,
(funx : 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)
forallc : C,
(funx : 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 (funx : 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 (funx : 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 (funx : 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 (funx : TriJoin A B C => f x = g x)
(join12 a b) (join23 b c) (?join1' a) @
ap
(transport (funx : TriJoin A B C => f x = g x)
(join23 b c)) (?join12' a b)) @ ?join23' b c =
transport2 (funx : 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)
forallb : B,
(funx : 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)
forallc : C,
(funx : 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 (funx : 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 (funx : 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 (funx : 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 (funx : TriJoin A B C => f x = g x)
(join12 a b) (join23 b c) (h1 h a) @
ap
(transport (funx : TriJoin A B C => f x = g x)
(join23 b c)) (?join12' a b)) @ ?join23' b c =
transport2 (funx : 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)
forallc : C,
(funx : 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 (funx : 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 (funx : 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 (funx : 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 (funx : TriJoin A B C => f x = g x)
(join12 a b) (join23 b c) (h1 h a) @
ap
(transport (funx : TriJoin A B C => f x = g x)
(join23 b c)) (?join12' a b)) @ ?join23' b c =
transport2 (funx : 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 (funx : 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 (funx : 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 (funx : 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 (funx : TriJoin A B C => f x = g x)
(join12 a b) (join23 b c) (h1 h a) @
ap
(transport (funx : TriJoin A B C => f x = g x)
(join23 b c)) (?join12' a b)) @ ?join23' b c =
transport2 (funx : 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 (funx : TriJoin A B C => f x = g x)
(join12 a b) (join23 b c) (h1 h a) @
ap
(transport (funx : 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 (funx : 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 (funx : TriJoin A B C => f x = g x)
(join12 a b) (join23 b c) (h1 h a) @
ap
(transport (funx : 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 (funx : 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 (funx : TriJoin A B C => f x = g x)
(join12 a b) (join23 b c) (h1 h a) @
ap
(transport (funx : 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 (funx : 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 (funx : TriJoin A B C => f x = g x)
(join12 a b) (join23 b c) (h1 h a) @
ap
(transport (funx : 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 (funx : 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 (funx : TriJoin A B C => f x = g x)
(join12 a b) (join23 b c) (h1 h a) @
ap
(transport (funx : 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 (funx : 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. *)Ltacgeneralize_some f a b c :=
letf1 := freshinletf2 := freshinletf3 := freshinletf12 := freshinletf13 := freshinletf23 := freshinletf123 := freshindestruct f as [f1 f2 f3 f12 f13 f23 f123]; cbn;
trygeneralize (f123 a b c); clear f123;
trygeneralize (f23 b c); clear f23;
trygeneralize (f13 a c); clear f13;
trygeneralize (f12 a b); clear f12;
trygeneralize (f3 c); clear f3;
trygeneralize (f2 b); clear f2;
trygeneralize (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]. *)Ltactriangle_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]. *)Ltactriangle_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 111 (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 111 (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 111 (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 111
(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' 111 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 111
(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'
forallk123 : prism abc abc' k12 k13 k23,
Q a b c ab' ac' bc' abc' 111 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 111
(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'
forallk123 : prism abc abc' (equiv_p1_1q 1) k13 k23,
Q a b c ab ac' bc' abc' 111
(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 111
(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'
forallk123 : prism abc abc' (equiv_p1_1q 1)
(equiv_p1_1q 1) k23,
Q a b c ab ac bc' abc' 111
(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 111
(equiv_p1_1q 1) (equiv_p1_1q 1)
(equiv_p1_1q 1) (prism_id abc) abc': ab @ bc = ac
forallk123 : prism abc abc' (equiv_p1_1q 1)
(equiv_p1_1q 1)
(equiv_p1_1q 1),
Q a b c ab ac bc abc' 111
(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 11111111111 abc': 1 = 1
forallk123 : prism 1 abc' 111,
Q a a a 111 abc' 111111 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 11111111111 abc': 1 = 1
forallk123 : 1 = 1 @ whiskerL 1 abc',
Q a a a 111 abc' 111111 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 11111111111 abc': 1 = 1 k123': 1 = abc'
Q a a a 111 abc' 111111
(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 11111111111
Q a a a 1111111111
(equiv_concat_r
(concat_1p (whiskerL 11) @ whiskerL_1p_1 1)^ 11)
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 11111111111
Q a a a 11111111111
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]. *)Ltacprism_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. *)Ltacprism_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. *)Instanceisgraph_trijoinrecdata (ABCP : 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
foralla : TriJoinRecData A B C P, a $-> a
A, B, C, P: Type
forallabc : TriJoinRecData A B C P,
(b $-> c) -> (a $-> b) -> a $-> c
A, B, C, P: Type
foralla : 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) 111
(* 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
forallabc : 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 : foralla : A, j1 f2 a = j1 f3 a)
(H0 : forallb : B, j2 f2 b = j2 f3 b)
(H1 : forallc : 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 : foralla : A, j1 f1 a = j1 f2 a)
(H14 : forallb : B, j2 f1 b = j2 f2 b)
(H15 : forallc : 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 : foralla : A, j1 f2 a = j1 f3 a)
(H0 : forallb : B, j2 f2 b = j2 f3 b)
(H1 : forallc : 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 : foralla : A, j1 f1 a = j1 f2 a)
(H14 : forallb : B, j2 f1 b = j2 f2 b)
(H15 : forallc : 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 : foralla : A, j1 f2 a = j1 f3 a)
(H0 : forallb : B, j2 f2 b = j2 f3 b)
(H1 : forallc : 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 : foralla : A, j1 f1 a = j1 f2 a)
(H14 : forallb : B, j2 f1 b = j2 f2 b)
(H15 : forallc : 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) 11 (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) 11 (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) 11 (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
(concat_lr (concat_p1 (j12 f1 a b))
(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)
(funk' : 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
(forallQ : 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 11
((concat_p1 p0 @ 1) @ (concat_1p p0)^) ->
Q (j1 f1 a) p p0 11
((concat_p1 p0 @ 1) @ (concat_1p p0)^))
with
| 1 =>
funQ : 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) 11 (equiv_p1_1q 1))
end)
((concat_p1 (j12 f1 a b) @ 1) @
(concat_1p (j12 f1 a b))^))
(equiv_ind
(concat_lr (concat_p1 (j13 f1 a c))
(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)
(funk' : 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
(forallQ : 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 11
((concat_p1 p0 @ 1) @ (concat_1p p0)^) ->
Q (j1 f1 a) p p0 11
((concat_p1 p0 @ 1) @ (concat_1p p0)^))
with
| 1 =>
funQ : 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) 11 (equiv_p1_1q 1))
end)
((concat_p1 (j13 f1 a c) @ 1) @
(concat_1p (j13 f1 a c))^))
(equiv_ind
(concat_lr (concat_p1 (j23 f1 b c))
(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)
(funk' : 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
(forallQ : 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 11
((concat_p1 p0 @ 1) @ (concat_1p p0)^) ->
Q (j2 f1 b) p p0 11
((concat_p1 p0 @ 1) @ (concat_1p p0)^))
with
| 1 =>
funQ : 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) 11 (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
forallab : 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 : foralla : A, j1 f a = j1 g a)
(H0 : forallb : B, j2 f b = j2 g b)
(H1 : forallc : 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) =>
(funf : 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 : foralla : A, j1 f a = j1 g a)
(H0 : forallb : B, j2 f b = j2 g b)
(H1 : forallc : 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) =>
(funf : 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 : foralla : A, j1 f a = j1 g a)
(H0 : forallb : B, j2 f b = j2 g b)
(H1 : forallc : 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) =>
(funf : 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) 11 (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) 11 (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) 11 (equiv_p1_1q 1))
by triangle_ind f a b c.Defined.Definitiontrijoinrecdata_0gpd (ABCP : 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
forallab : 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 11111
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
forallab : 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
zerogpd_graph (trijoinrecdata_0gpd A B C P) ->
zerogpd_graph (trijoinrecdata_0gpd A B C Q)
A, B, C, P, Q: Type g: P $-> Q
Is0Functor ?F
A, B, C, P, Q: Type g: P $-> Q
zerogpd_graph (trijoinrecdata_0gpd A B C P) ->
zerogpd_graph (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 (ab : Type) (fg : a $-> b),
f $== g ->
fmap (trijoinrecdata_0gpd A B C) f $==
fmap (trijoinrecdata_0gpd A B C) g
A, B, C: Type
foralla : Type,
fmap (trijoinrecdata_0gpd A B C) (Id a) $==
Id (trijoinrecdata_0gpd A B C a)
A, B, C: Type
forall (abc : 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 (ab : Type) (fg : 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
byinduction (h f).(* The identity map [P -> P] is sent to a map homotopic to the identity. *)
A, B, C: Type
foralla : Type,
fmap (trijoinrecdata_0gpd A B C) (Id a) $==
Id (trijoinrecdata_0gpd A B C a)
A, B, C, P: Type f: zerogpd_graph (trijoinrecdata_0gpd A B C P)
TriJoinRecPath (trijoinrecdata_fun idmap f) f
A, B, C, P: Type f: zerogpd_graph (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: zerogpd_graph (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: zerogpd_graph (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: zerogpd_graph (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: zerogpd_graph (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 (abc : 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: zerogpd_graph (trijoinrecdata_0gpd A B C P)
A, B, C, P, Q, R: Type g1: P $-> Q g2: Q $-> R f: zerogpd_graph (trijoinrecdata_0gpd A B C P) a: A b: B
ap (funx : 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: zerogpd_graph (trijoinrecdata_0gpd A B C P) a: A c: C
ap (funx : 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: zerogpd_graph (trijoinrecdata_0gpd A B C P) b: B c: C
ap (funx : 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: zerogpd_graph (trijoinrecdata_0gpd A B C P) a: A b: B c: C
prism'
(ap_triangle (funx : 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: zerogpd_graph (trijoinrecdata_0gpd A B C P) a: A b: B c: C
prism'
(ap_triangle (funx : 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.Definitiontrijoinrecdata_0gpd_fun (ABC : 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]. *)Definitiontrijoin_rec_inv_nattrans (ABC : 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
foralla : Type, CatIsEquiv (?alpha a)
A, B, C: Type
foralla : 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
forallxy : zerogpd_graph (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 : zerogpd_graph (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
forallxy : zerogpd_graph (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. *)Definitiontrijoin_rec_natequiv (ABC : 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 Definitiontrijoin_rec_natequiv_check (ABCP : 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. *)Definitionissect_trijoin_rec_inv {ABCP : 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. *)Definitiontrijoinrecdata_tricomp {ABCA'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 := funab => j12 k (f a) (g b);
j13 := funac => j13 k (f a) (h c);
j23 := funbc => j23 k (g b) (h c);
j123 := funabc => 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: foralla : A, j1 k a = j1 l a h5: forallb : B, j2 k b = j2 l b h6: forallc : 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 := funx : A' => j1 k (f x);
j2 := funx : B' => j2 k (g x);
j3 := funx : 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 := funx : A' => j1 l (f x);
j2 := funx : B' => j2 l (g x);
j3 := funx : 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)
|}
snapply 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); byapply 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); byapply 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); byapply 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))
(letp0 := p a inleta0 := 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))
(letp1 := q b inletb0 := g' b inmatch
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 => letX := equiv_fun equiv_p1_1q in X 1end) a0 p0)
(letp0 := p a inleta0 := 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))
(letp1 := r c inletc0 := h' c inmatch
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 => letX := equiv_fun equiv_p1_1q in X 1end) a0 p0)
(letp0 := q b inletb0 := 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))
(letp1 := r c inletc0 := h' c inmatch
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 => letX := equiv_fun equiv_p1_1q in X 1end) 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)]. *)Definitionfunctor_trijoin {ABCA'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)
napply 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'
exact (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
exact (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 (funx : A' => f (f^-1 x))
(funx : B' => g (g^-1 x))
(funx : 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 (funx : A' => f (f^-1 x))
(funx : B' => g (g^-1 x))
(funx : 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 (funx : A => f^-1 (f x))
(funx : B => g^-1 (g x))
(funx : 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 (funx : A => f^-1 (f x))
(funx : B => g^-1 (g x))
(funx : 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
exact functor_trijoin_idmap.Defined.Definitionequiv_functor_trijoin {ABCA'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 := funx : A => joinl (f x);
j2 := funx : B => joinr (jl g x);
j3 := funx : 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 := funx : A => joinl (f x);
j2 := funx : B => joinr (jl g x);
j3 := funx : 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 := funx : A => joinl (f x);
j2 := funx : B => joinr (jl g x);
j3 := funx : 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 := funx : A => joinl (f x);
j2 := funx : B => joinr (jl g x);
j3 := funx : 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
(funx : 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 (funx : 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
(funx : 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.Definitionfunctor_trijoin_as_functor_join {ABCA'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).