| 123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778 |
- ;; TO JEST TYLKO WERSJA ROBOCZA, NIE SPRAWDZANA KOMPUTEROWO
- ;; MOŻE ZAWIERAĆ BŁĘDY
- (set xd-1a
- (Pi (A (Universe 0)) (a A)
- (alfa (Id (refl a) (refl a)))
- (beta (Id (refl a) (refl a)))
- (Id
- ;; alfa o beta
- (concat (Id a a) (refl a) (refl a) (refl a) alfa beta)
- ;; alfa gwiazdka beta
- (horizontal-composition A a a a
- (refl a) (refl a) (refl a) (refl a)
- alfa beta)))
- (lambda (A (Universe 0)) (a A)
- (alfa (Id (refl a) (refl a)))
- (beta (Id (refl a) (refl a)))
- (refl (concat (Id a a) (refl a) (refl a) (refl a) alfa beta)))) ;; (refl to-drugie) też by było
- (set xd-2a
- (Pi (A (Universe 0)) (a A)
- (alfa (Id (refl a) (refl a)))
- (beta (Id (refl a) (refl a)))
- (Id
- ;; alfa gwiazdka' beta
- (horizontal-composition-2 A a a a
- (refl a) (refl a) (refl a) (refl a)
- alfa beta)
- ;; beta o alfa
- (concat (Id a a) (refl a) (refl a) (refl a) beta alfa)
- ))
- (lambda (A (Universe 0)) (a A)
- (alfa (Id (refl a) (refl a)))
- (beta (Id (refl a) (refl a)))
- (refl (concat (Id a a) (refl a) (refl a) (refl a) beta alfa)))) ;; (refl to-drugie) też by było
- (set hc-eq-hc2
- (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))
- (horizontal-composition A a b c p q r s alfa beta)
- (horizontal-composition-2 A a b c p q r s alfa beta))
- (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))
- ;;TODO 4xJ (alfa, beta, p ,r) + (refl (refl a))
- ))
- (set eh
- (Pi (A (Universe 0)) (a A)
- (alfa (Id (refl a) (refl a)))
- (beta (Id (refl a) (refl a)))
- (Id ;KOZACKIE TWIERDZENIE :DDDDD
- (concat (Id a a) (refl a) (refl a) (refl a) alfa beta)
- (concat (Id a a) (refl a) (refl a) (refl a) beta alfa)))
- (lambda (A (Universe 0)) (a A)
- (alfa (Id (refl a) (refl a)))
- (beta (Id (refl a) (refl a)))
- (concat
- (Id (refl a) (refl a))
- (concat (Id a a) (refl a) (refl a) (refl a) alfa beta)
- (horizontal-composition-2 A a a a (refl a) (refl a) (refl a) (refl a) alfa beta)
- (concat (Id a a) (refl a) (refl a) (refl a) beta alfa)
- (concat (Id (refl a) (refl a))
- (concat (Id a a) (refl a) (refl a) (refl a) alfa beta)
- (horizontal-composition A a a a (refl a) (refl a) (refl a) (refl a) alfa beta)
- (horizontal-composition-2 A a a a (refl a) (refl a) (refl a) (refl a) alfa beta)
- (xd-1a A a alfa beta)
- (hc-eq-hc2 A a a a (refl a) (refl a) (refl a) (refl a) alfa beta))
- (xd-2a A a alfa beta))))
|
