123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326 |
- (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
|