computational rules for spoke

Author: 5HT

library/mathematics/homotopy/hs.anders

@@ -39,6 +39,16 @@ def hs-β₂ (S A : U) (X : hs S A → U)
   : Path (X (hub' S A f)) (hs-ind S A X nCenter nHub nSpoke (hub' S A f)) (nHub f (λ (s : S), hs-ind S A X nCenter nHub nSpoke (f s)))
  := idp (X (hub' S A f)) (nHub f (λ (s : S), hs-ind S A X nCenter nHub nSpoke (f s)))
 
+def hs-β₃ (S A : U) (X : hs S A → U)
+    (nCenter : Π (a : A), X (center S A a))
+    (nHub : Π (f : S → hs S A) (nF : Π (s : S), X (f s)), X (hub' S A f))
+    (nSpoke : Π (f : S → hs S A) (nF : Π (s : S), X (f s)) (s : S), PathP (<i> X (spoke' S A f s @ i)) (nHub f nF) (nF s))
+    (f : S → hs S A) (s : S)
+  : Path (PathP (<i> X (spoke' S A f s @ i)) (nHub f (λ (s : S), hs-ind S A X nCenter nHub nSpoke (f s))) (hs-ind S A X nCenter nHub nSpoke (f s)))
+    (<j> hs-ind S A X nCenter nHub nSpoke (spoke' S A f s @ j)) (nSpoke f (λ (s : S), hs-ind S A X nCenter nHub nSpoke (f s)) s)
+ := idp (PathP (<i> X (spoke' S A f s @ i)) (nHub f (λ (s : S), hs-ind S A X nCenter nHub nSpoke (f s))) (hs-ind S A X nCenter nHub nSpoke (f s)))
+        (nSpoke f (λ (s : S), hs-ind S A X nCenter nHub nSpoke (f s)) s)
+
 -- 5) Uniqueness Rule
 def hs-η (S A : U) (X : hs S A → U) (h : Π (z : hs S A), X z) (hs-map : Π (z : hs S A), X z)
  := idp (Π (z : hs S A), X z) h