Przemek-K0/Eckmann-Hilton.prmk

(set reverse
     (Pi (A (Universe 0)) (x A) (y A) (p (Id x y)) (Id y x)) 
     (lambda (A (Universe 0))
       (J
        ;;typFunc
        (lambda (x A) (y A) (p (Id x y))
          (Id y x))
        ;;reflFunc
        (lambda (x A) (refl x)))))

;; dowód że `x = x` po odwróceniu dalej daje `x = x`
(set reverse-comp-check
     (Pi (A (Universe 0)) (x A)
         (Id (refl x) ((((reverse A) x) x) (refl x))))
     (lambda (A (Universe 0)) (x A)
       (refl (refl x))))

(set concat
     (Pi (A (Universe 0))
         (Pi (x A)
             (Pi (y A)
                 (Pi (z A)
                     (Pi (xy (Id x y))
                         (Pi (yz (Id y z))
                             (Id x z)))))))
     (lambda (A (Universe 0))
       (lambda (x A)
         (lambda (y A)
           (lambda (z A)
             (lambda (xy (Id x y))
               (lambda (yz (Id y z))
                 ((((((J
                        (lambda (x A)
                          (lambda (y A)
                            (lambda (p (Id x y))
                              (Pi (z A)
                                  (Pi (q (Id y z))
                                      (Id x z))))))
                        (lambda (x A)
                          (lambda (z A)
                            (lambda (p (Id x z))
                              p))))
                      x)
                     y)
                    xy)
                   z)
                  yz))))))))

;;dowód że `reflx o reflx = reflx`
(set concat-comp-check
     (Pi (A (Universe 0))
         (Pi (x A)
             (Id
              (refl x)
              ((((((concat A) x) x) x) (refl x)) (refl x)))))
     (lambda (A (Universe 0))
       (lambda (x A)
         (refl (refl x)))))

(set p-eq-p-refl
     (Pi (A (Universe 0))
         (Pi (x A)
             (Pi (y A)
                 (Pi (p (Id x y))
                     (Id p ((((((concat A) x) y) y) p) (refl y)))))))
     (lambda (A (Universe 0))
       (J
        (lambda (x A)
             (lambda (y A)
                 (lambda (p (Id x y))
                     (Id p ((((((concat A) x) y) y) p) (refl y))))))
        (lambda (x A) (refl (refl x))))))

(set p-eq-refl-p
     (Pi (A (Universe 0))
         (Pi (x A)
             (Pi (y A)
                 (Pi (p (Id x y))
                     (Id p ((((((concat A) x) x) y) (refl x)) p))))))
     (lambda (A (Universe 0))
       (J
        (lambda (x A)
             (lambda (y A)
                 (lambda (p (Id x y))
                     (Id p ((((((concat A) x) x) y) (refl x)) p)))))
        (lambda (x A) (refl (refl x))))))

(set p-inv-p-eq-refl-y
     (Pi (A (Universe 0))(Pi (x A) (Pi (y A) (Pi (p (Id x y))
                                                 (Id
                                                  ((((((concat A) y) x) y)
                                                    ((((reverse A) x) y) p))
                                                   p)
                                                  (refl y))))))
     (lambda (A (Universe 0))
       (J (lambda (x A) (lambda (y A) (lambda (p (Id x y))
                              (Id ((((((concat A) y) x) y)
                                    ((((reverse A) x) y) p))
                                   p)
                                  (refl y)))))
          (lambda (x A) (refl (refl x))))))


(set p-p-inv-eq-refl-x
     (Pi (A (Universe 0))(Pi (x A) (Pi (y A) (Pi (p (Id x y))
                                                 (Id ((((((concat A) x) y) x)
                                                       p)
                                                      ((((reverse A) x) y) p))
                                                     (refl x))))))
     (lambda (A (Universe 0))
       (J (lambda (x A) (lambda (y A) (lambda (p (Id x y))
                              (Id ((((((concat A) x) y) x)
                                    p )
                                   ((((reverse A) x) y) p))
                                  (refl x)))))
          (lambda (x A) (refl (refl x))))))

(set p-inv-inv-eq-p
     (Pi (A (Universe 0))
         (Pi (x A)
             (Pi (y A)
                 (Pi (p (Id x y))
                     (Id
                      ((((reverse A) y) x)     ((((reverse A) x) y) p))
                      p)))))
     (lambda (A (Universe 0))
       (lambda (x A)
         (lambda (y A)
           (lambda (p (Id x y))

             ((J
               (lambda (x A)
                 (lambda (y A)
                   (lambda (p (Id x y))
                     (Id
                      ((((reverse A) y) x)     ((((reverse A) x) y) p))
                      p)
                     )))
               (lambda (x A)
                 (refl (refl x))))
              x
              y
              p))))))

;; p o (q o r) = (p o q) o r
(set id-kolejnosc-dzialan
     (Pi (A (Universe 0)) (x A) (y A) (z A) (w A)
         (p (Id x y)) (q (Id y z)) (r (Id z w))
         (Id 
          (concat A x y w p (concat A y z w q r))
          (concat A x z w (concat A x y z p q) r)))
     (lambda (A (Universe 0)) (x A) (y A) (z A)(w A)
         (p (Id x y)) (q (Id y z)) (r (Id z w))

         ((J ; x y p z w q r
            ;;D1
            (lambda (x A) (y A) (p (Id x y))
              (Pi (z A) (w A)
                  (q (Id y z)) (r (Id z w))
                  (Id 
                   (concat A x y w p (concat A y z w q r))
                   (concat A x z w (concat A x y z p q) r))))
            ;;refl for D1
            ;;todo coś przed J
            (lambda (x A) (z A) (w A)
              (q (Id x z)) ( r (Id z w))
              ((J ;D2 x z q w r
                 (lambda (x A) (z A) (q (Id x z))
                   (Pi (w A) (r (Id z w))
                       (Id
                        (concat A x x w (refl x) (concat A x z w q r))
                        (concat A x z w (concat A x x z (refl x) q) r))))
                 ;;d2 refl
                                        ;nie trzeba (lambda (x A) (w A) (r (Id x w)))
                 (J ;D3
                  (lambda (x A) (w A) (r (Id x w))
                    (Id
                     (concat A x x w (refl x) (concat A x x w (refl x) r))
                     (concat A x x w (concat A x x x (refl x) (refl x)) r)
                     ))
                  ;;refld d3
                  (lambda (x A) (refl (refl x)))
                  )
                 )
               x z q w r))
            
            
            
            )
          x y p z w q r )
         
         ))

;; to będzie potrzebne do Whiser-R żeby udowodnić
;; (p o refl_b = p) == (p = q) == (q = q o refl_b)
(set concat-2
     (Pi (A (Universe 0))
         (a A) (b A) 
         (p (Id a b)) (q (Id a b)) (r (Id a b))
         (h (Id p q)) (i (Id q r))
         (Id p r))
     (lambda (A (Universe 0))
         (a A) (b A) 
         (p (Id a b)) (q (Id a b)) (r (Id a b))
         (h (Id p q)) (i (Id q r))
         (concat (Id a b) p q r h i)))
;;to było łatwe a ja się spodziewałem że będzie trudne

(set whisker-r
     (Pi (A (Universe 0))
         (a A) (b A) (c A)
         (p (Id a b)) (q (Id a b)) (r (Id b c))
         (alfa (Id p q))
         (Id
          (concat A a b c p r)
          (concat A a b c q r)))
     (lambda (A (Universe 0))
         (a A) (b A) (c A)
         (p (Id a b)) (q (Id a b)) (r (Id b c))
         (alfa (Id p q))
         ((J
           (lambda (b A) (c A) (r (Id b c))
             (Pi (a A) (p (Id a b)) (q (Id a b)) (alfa (Id p q))
                 (Id
                  (concat A a b c p r)
                  (concat A a b c q r))))
            (lambda (b A)              (a A) (p (Id a b)) (q (Id a b)) (alfa (Id p q))
              (concat (Id a b)
                      (concat A a b b p (refl b)); p o refl
                      p
                      (concat A a b b q (refl b)) ; q o refl
                      (reverse (Id a b) p (concat A a b b p (refl b)) (p-eq-p-refl A a b p));  p o refl = p
                      (concat (Id a b)
                              p
                              q
                              (concat A a b b q (refl b)); q o refl
                              alfa
                              (p-eq-p-refl A a b q); q = q o refl
                              ))))
          b c r a p q alfa)))

(set whisker-l
     (Pi (A (Universe 0))
         (a A) (b A) (c A)
         (p (Id a b)) (r (Id b c)) (s (Id b c))
         (beta (Id r s))
         (Id
          (concat A a b c p r)
          (concat A a b c p s)))
     (lambda (A (Universe 0))
         (a A) (b A) (c A)
         (p (Id a b)) (r (Id b c)) (s (Id b c))
         (beta (Id r s))
         ((J
           (lambda (a A) (b A) (p (Id a b))
             (Pi (c A) (r (Id b c)) (s (Id b c)) (beta (Id r s))
                 (Id
                  (concat A a b c p r)
                  (concat A a b c p s))))
            (lambda (b A)  (c A) (r (Id b c)) (s (Id b c)) (beta (Id r s))
              (concat (Id b c) ;;;;;;;;;;;;
                      (concat A b b c (refl b) r) ; refl o r
                      r
                      (concat A b b c (refl b) s)  ; refl o s
                      (reverse (Id b c) r (concat A b b c (refl b) r) (p-eq-refl-p A b c r)) ; reflb o r = r
                      (concat (Id b c)
                              r
                              s
                              (concat A b b c (refl b) s); refl o s
                              beta
                              (p-eq-refl-p A b c s); s = refl o s
                              ))))
          a b p c r s beta)))

;; (alfa o_r r) o (q o_l beta)
(set horizontal-composition
     (Pi (A (Universe 0))
         (a A) (b A) (c A)
         (p (Id a b)) (q (Id a b))
         (r (Id b c)) (s (Id b c))
         (alfa (Id p q)) (beta (Id r s))
         (Id
          (concat A a b c p r)
          (concat A a b c q s)))
     (lambda (A (Universe 0))
         (a A) (b A) (c A)
         (p (Id a b)) (q (Id a b))
         (r (Id b c)) (s (Id b c))
         (alfa (Id p q)) (beta (Id r s))

         (concat
          (Id a c)
          (concat A a b c p r)
          (concat A a b c q r)
          (concat A a b c q s)
          (whisker-r A a b c p q r alfa)
          (whisker-l A a b c q r s beta))))


;; (p o_l beta) o (alfa o_r s)
(set horizontal-composition-2
     (Pi (A (Universe 0))
         (a A) (b A) (c A)
         (p (Id a b)) (q (Id a b))
         (r (Id b c)) (s (Id b c))
         (alfa (Id p q)) (beta (Id r s))
         (Id
          (concat A a b c p r)
          (concat A a b c q s)))
     (lambda (A (Universe 0))
         (a A) (b A) (c A)
         (p (Id a b)) (q (Id a b))
         (r (Id b c)) (s (Id b c))
         (alfa (Id p q)) (beta (Id r s))

         (concat
          (Id a c)
          (concat A a b c p r)
          (concat A a b c p s)
          (concat A a b c q s)
          (whisker-l A a b c p r s beta)
          (whisker-r A a b c p q s alfa))))

;; Jeszcze dużo do Eckmana-Hiltona 
tt