Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

formalization

  • Loading branch information...
commit 6cc406815a933e3259a92a244795f2a96c8bb98e 1 parent 99b056a
@dlicata335 authored
View
4 homotopy/FreudenthalIteratedSuspension1.agda
@@ -17,8 +17,7 @@ open import homotopy.KG1
module homotopy.FreudenthalIteratedSuspension1 (A : Type)
(a0 : A)
(A-Connected : Connected (S (S -2)) A)
- (A-level : NType (tl 1) A)
- (H-A : H-Structure A a0) where
+ where
Susp'^ : Positive Type
Susp'^ n = (Susp^ (n -1pn) A)
@@ -34,6 +33,7 @@ module homotopy.FreudenthalIteratedSuspension1 (A : Type)
Susp'^-Connected' (S (S n')) = coe (ap (λ x NType -2 (Trunc (S (tl (pos2nat n'))) (Susp^ x A))) (ap pos2nat (pos2nat-+1np n')))
(Susp'^-Connected (pos2nat (S n')))
+
Susp'^-Connected'' : (n : Positive) Connected (tlp n) (Susp'^ (n +1))
Susp'^-Connected'' n = coe (ap (λ x NType -2 (Trunc x (Susp^ (pos2nat n) A))) (tl-pos2nat-tlp n ∘ ! (-2ptl-S (S n))))
(Susp'^-Connected' (n +1))
View
2  homotopy/KGn.agda
@@ -22,7 +22,7 @@ module homotopy.KGn where
(A-level : NType (tl 1) A)
(H-A : H-Structure A a0) where
- module FS = homotopy.FreudenthalIteratedSuspension1 A a0 A-Connected A-level H-A
+ module FS = homotopy.FreudenthalIteratedSuspension1 A a0 A-Connected
KG : Positive Type
KG n = Trunc (tlp n) (FS.Susp'^ n)
View
5 homotopy/Pi2HSusp.agda
@@ -96,9 +96,8 @@ module homotopy.Pi2HSusp (A : Type)
decode {x} = Susp-elim (\ x -> Codes x P x)
decode'
(λ a [ (mer a) ])
- (λ a transport-→-from-square Codes P (mer a)
- decode' (λ a' [ (mer a') ])
- (λ≃ (STS a)))
+ (λ a transport-→-from-square Codes P (mer a) decode' (λ a' [ mer a' ])
+ (λ≃ (STS a)))
x where
abstract
STS : (a a' : A) transport P (mer a) (decode' a') ≃ [ mer (transport Codes (mer a) a') ]
Please sign in to comment.
Something went wrong with that request. Please try again.