Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

stuff

  • Loading branch information...
commit b8229fe324bf93924537fa258561fe761caf66bc 1 parent 383286f
@dlicata335 authored
View
108 computational-interp/Cube.agda
@@ -78,6 +78,9 @@ module computational-interp.Cube where
(b : (b : B a) P (reflo n b))
(c : CubeOver B n (refl n a)) P c
cubeover-induction = {!!}
+
+ apd-Cube : {A : Type} {B : A Type} (n : Nat) (f : (x : A) B x) (a : Cube n A) CubeOver B n a
+ apd-Cube n f c = {!!}
ctxops : {A : Type} {B : A Type} (n : Nat)
@@ -133,88 +136,23 @@ module computational-interp.Cube where
conjecture a1 a2 α = ua (improve (hequiv (λ {(((a1' , b1) , (a2' , b2) , αβ) , eq) {!(b1 , b2 , ?)!}})
(λ {(b1 , b2 , β) ((a1 , b1) , (a2 , b2) , pair= α β) , {!!}}) {!!} {!!}))
- module Coprod (A : Type) (B : Type) where
-
- eqv : Paths' (Either A B) == Either (Paths' A) (Paths' B)
- eqv = ap2 Either (! (contract-Paths' {A})) (! (contract-Paths' {B})) ∘ (contract-Paths' {Either A B})
-
- C : (x y : Either A B) Type
- C (Inl a) (Inl a') = a == a'
- C (Inr b) (Inr b') = b == b'
- C _ _ = Void
-
- step : (a : A) coe (! eqv) (Inl ((a , a) , id)) == ((Inl a , Inl a) , id)
- step = {!!}
-
- e' : (p : Either A B × Either A B) Equiv (Σ \ (q : Paths' (Either A B)) fst q == p) (C (fst p) (snd p))
- e' p = improve (hequiv l {!!} {!!} {!!}) where
- l : (Σ \ (q : Paths' (Either A B)) fst q == p) _
- l = {!!}
-
- e : (p : Either A B × Either A B) Equiv (Σ \ (q : Either (Paths' A) (Paths' B)) fst (coe (! eqv) q) == p) (C (fst p) (snd p))
- e p = improve (hequiv l (r p) {!!} {!!}) where
- l : Σ (λ q fst (coe (! eqv) q) == p) -> _
- l (Inl ((x , .x) , id) , eq) = path-induction (λ p₁ eq₁ C (fst p₁) (snd p₁)) (transport (λ x₁ C (fst (fst x₁)) (snd (fst x₁))) (! (step x)) id) eq
- l (Inr ((y , .y) , id) , eq) = {!!}
-
- r : (p : Either A B × Either A B) (C (fst p) (snd p)) -> (Σ \ (q : Either (Paths' A) (Paths' B)) fst (coe (! eqv) q) == p)
- r (Inl x , Inl y) c = (Inl ((x , y) , c)) , {!!}
- r (Inl x , Inr y) ()
- r (Inr x , Inl y) c = {!!}
- r (Inr x , Inr y) c = {!!}
-{-
- C : (a a' : A) → Either (Paths' A) (Paths' B) → Type
- C a a' (Inl ((a1 , a1'), p)) = (a == a1) × (a' == a1')
- C a a' (Inr _) = Void
-
- coprod2 : (a a' : A) (p : Paths' (Either A B)) → C a a' (coe eqv p) == (fst p == (Inl a , Inl a'))
- coprod2 a a' ((Inl x , .(Inl x)) , id) = {!!}
- coprod2 a a' ((Inr x , .(Inr x)) , id) = {!!}
-
- coprod3 : (a a' : A) (p : Either (Paths' A) (Paths' B)) → C a a' p == (fst (coe (! eqv) p) == (Inl a , Inl a'))
- coprod3 a a' (Inl ((x , .x) , id)) = (a == x) × (a' == x) ≃〈 {!!} 〉
- Path {(Either A B × Either A B)} (Inl x , Inl x) (Inl a , Inl a') ≃〈 {!!} 〉
- (fst (coe (! eqv) (Inl ((x , x) , id))) == (Inl a , Inl a') ∎)
- coprod3 a a' (Inr ((x , .x) , id)) = {!!}
--}
-
-{-
-
-
- fiberwise-eqv : {A : Type} {B B' : A → Type} → (f : (a : A) → B a → B' a)
- → IsEquiv {(Σ B)} {(Σ B')} (fiberwise-to-total f)
- → (a : A) → B a == B' a
- fiberwise-eqv f (isequiv g α β _) a = ua (improve (hequiv (f a) (λ b' → coe {!!} (snd (g (a , b')))) {!!} {!!}))
-
- movearg : ∀ {A B} → Equiv (A → Paths' B) (Σ (λ (p₁ : (A → B) × (A → B)) → (x : A) → fst p₁ x == snd p₁ x))
- movearg = improve (hequiv ((λ f →
- ((\ x -> fst (fst (f x))) , (λ x₁ → snd (fst (f x₁)))) ,
- (λ x₁ → snd (f x₁))))
- (λ x x₁ → ((fst (fst x) x₁) , (snd (fst x) x₁)) , (snd x x₁))
- (λ _ → id) (λ _ → id))
-
- funext : {A B : Type} (f g : A → B) → (f == g) == ((x : A) → f x == g x)
- funext {A} {B} f g = fiberwise-eqv {A = (A → B) × (A → B)} {B = \ p → fst p == snd p} {B' = \ p → (x : A) → fst p x == snd p x}
- (λ {(f , g) → λ p₁ x → ap≃ p₁ {x}})
- STS
- (f , g) where
- tot : (Paths' (A → B)) → Σ (λ (p₁ : (A → B) × (A → B)) → (x : A) → fst p₁ x == snd p₁ x)
- tot = fiberwise-to-total {A = (A → B) × (A → B)} {B = \ p → fst p == snd p} {B' = \ p → (x : A) → fst p x == snd p x} (λ {(f , g) → λ p₁ x → ap≃ p₁ {x}})
-
- e : Equiv (Paths' (A → B)) (Σ (λ (p₁ : (A → B) × (A → B)) → (x : A) → fst p₁ x == snd p₁ x))
- e = movearg ∘equiv coe-equiv eqv
-
- STS : IsEquiv {Paths' (A → B)} {Σ (λ (p₁ : (A → B) × (A → B)) → (x : A) → fst p₁ x == snd p₁ x)}
- tot
- STS = transport IsEquiv (fst e ≃〈 {!!} 〉
- fst movearg o coe eqv ≃〈 {!!} 〉
- fst movearg o coe (! (ap (\ y -> A → y) (contract-Paths' {B}))) o coe (contract-Paths' {A → B}) ≃〈 {!!} 〉
- fst movearg o coe (ap (\ y -> A → y) (! (contract-Paths' {B}))) o coe (contract-Paths' {A → B}) ≃〈 {!!} 〉
- fst movearg o (\ z -> coe (! (contract-Paths' {B})) o z) o coe (contract-Paths' {A → B}) ≃〈 {!!} 〉
- ((λ f →
- ((\ x -> fst (fst (f x))) , (λ x₁ → snd (fst (f x₁)))) ,
- (λ x₁ → snd (f x₁)))) o (\ z -> coe (! (contract-Paths' {B})) o z) o coe (contract-Paths' {A → B}) ≃〈 {!!} 〉
- (\ p -> fst p , λ x → ap≃ (snd p) {x}) ≃〈 {!!} 〉
- tot ∎)
- (snd e)
--}
+ test : {Γ : Type} {A : Γ Type} {M N : (x : Γ) A x} (θ : Γ) Type
+ test {Γ}{A}{M}{N} θ = CubeOver
+ (λ (p₁ : Σ (λ (θ₁ : Γ) A θ₁ × A θ₁))
+ fst (snd p₁) == snd (snd p₁))
+ 0 (θ , (M θ) , (N θ))
+
+ up' : {n} {Γ : Type} {A : Γ Type} {M N : (x : Γ) A x} (θ : Cube n Γ)
+ CubeOver (\ x -> M x == N x) n θ
+ CubeOver A (S n) (θ , θ , id)
+ up' {n} {M = M} {N = N} θ c = (pair n θ (apd-Cube n M θ) , (pair n θ (apd-Cube n M θ) , {!fst c!})) , {!!}
+
+ CubeOver' : {A : Type} (B : A Type) (n : Nat) Cube n A Type
+ CubeOver' B Z a = B a
+ CubeOver' B (S n) (a1 , a2 , α) = Σ (λ (x : CubeOver' B n a1)
+ Σ (λ (y : CubeOver' B n a2)
+ PathOver (CubeOver' B n) α x y))
+
+ pair' : {A : Type} {B : A Type} (n : Nat) (Σ \ (a : Cube n A) CubeOver' B n a) Cube n (Σ B)
+ pair' Z p = p
+ pair' (S n) ((a1 , a2 , α) , (b1 , b2 , β)) = pair' n (a1 , b1) , pair' n (a2 , b2) , ap (pair' n) (pair= α β)
View
16 computational-interp/ua-implies-funext/Funext2.agda
@@ -8,8 +8,8 @@ module Funext2 where
Homotopies A B = (Σ \ (fg : (A -> B) × (A B)) (x : A) fst fg x == snd fg x)
-- uses η for Σ
- swap : {A B} Equiv (A Paths B) (Homotopies A B)
- swap = (improve (hequiv (λ h ((λ x fst (fst (h x))) , (λ x snd (fst (h x)))) , (λ x snd (h x)))
+ rearrange : {A B} (A Paths B) (Homotopies A B)
+ rearrange = (improve (hequiv (λ h ((λ x fst (fst (h x))) , (λ x snd (fst (h x)))) , (λ x snd (h x)))
(λ i λ x ((fst (fst i) x) , (snd (fst i) x)) , snd i x)
(λ _ id) (λ _ id)))
-- this can be written with AC, but it's too annoying to do the beta reduction if you write it this way
@@ -19,15 +19,15 @@ module Funext2 where
funextt : {A B} Equiv (Paths (A B)) (Homotopies A B)
funextt {A} {B} = Paths (A B) ≃〈 contract-Paths≃ {A B} 〉
(A B) ≃〈 coe-equiv (ap (λ y A y) (ua (!equiv (contract-Paths≃ {B})))) 〉
- (A Paths B) ≃〈 swap
+ (A Paths B) ≃〈 rearrange
Homotopies A B ∎∎
funextt-id : {A B} (f : A B) fst funextt ((f , f) , id) == ((f , f) , λ x id)
funextt-id {A} f = fst funextt ((f , f) , id) =〈 id 〉
- fst swap (coe (ap (λ y A y) (ua (!equiv (contract-Paths≃)))) f) =〈 ap (fst swap) (ap= (! (transport-ap-assoc' (λ x x) (λ y A y) (ua (!equiv contract-Paths≃))))) 〉
- fst swap (transport (λ y A y) (ua (!equiv (contract-Paths≃))) f) =〈 ap (fst swap) (transport-→-post (ua (!equiv contract-Paths≃)) f) 〉
- fst swap (coe (ua (!equiv (contract-Paths≃))) o f) =〈 ap (λ z fst swap (z o f)) (type=β (!equiv contract-Paths≃)) 〉
- fst swap (fst (!equiv (contract-Paths≃)) o f) =〈 id 〉
+ fst rearrange (coe (ap (λ y A y) (ua (!equiv (contract-Paths≃)))) f) =〈 ap (fst rearrange) (ap= (! (transport-ap-assoc' (λ x x) (λ y A y) (ua (!equiv contract-Paths≃))))) 〉
+ fst rearrange (transport (λ y A y) (ua (!equiv (contract-Paths≃))) f) =〈 ap (fst rearrange) (transport-→-post (ua (!equiv contract-Paths≃)) f) 〉
+ fst rearrange (coe (ua (!equiv (contract-Paths≃))) o f) =〈 ap (λ z fst rearrange (z o f)) (type=β (!equiv contract-Paths≃)) 〉
+ fst rearrange (fst (!equiv (contract-Paths≃)) o f) =〈 id 〉
((f , f) , (λ x id)) ∎
preserves-fst : {A B} (α : Paths (A B))
@@ -37,7 +37,7 @@ module Funext2 where
funext : {A B : Type} (f g : A B) (f == g) ≃ ((x : A) f x == g x)
funext {A}{B} f g = fiberwise-equiv-from-total≃ funextt preserves-fst (f , g)
- funext-id : {A B : Type} (f : A B) fst (funext f f) id == (λ x id)
+ funext-id : {A B : Type} (f : A B) fst (funext f f) (id {_}{f}) == (λ x id{_}{f x})
funext-id {A} f = _ =〈 fiberwise-equiv-from-total≃-β funextt preserves-fst (f , f) id 〉
(transport (λ fg (x : A) Id (fst fg x) (snd fg x))
(ap fst (funextt-id f))
View
56 computational-interp/ua-implies-funext/FunextDep.agda
@@ -5,12 +5,6 @@ open import Funext2 using (funext ; funext-ap=)
module FunextDep where
- Homotopies : (A : Type) (A Type) Type
- Homotopies A B = (Σ \ (fg : ((x : A) -> B x) × ((x : A) B x)) (x : A) fst fg x == snd fg x)
-
- Π : (A : Type) (B : A Type) Type
- Π A B = (x : A) B x
-
λ= : {A B : Type} {f g : A B} ((x : A) f x == g x) f == g
λ= α = IsEquiv.g (snd (funext _ _)) α
@@ -18,37 +12,13 @@ module FunextDep where
ap=λ= : {A B : Type} {f g : A B} ((\ α x ap={_}{_}{f}{g} α {x}) o (λ= {_}{_}{f}{g})) == (λ x x)
ap=λ= = λ= (λ x IsEquiv.β (snd (funext _ _)) x ∘ ! (funext-ap= (λ= x)))
+ Π : (A : Type) (B : A Type) Type
+ Π A B = (x : A) B x
+
transport-Π-post : {A : Type} {B B' : A Type} (e : B == B')
transport (\ B Π A B) e == (λ f x coe (ap= e) (f x))
transport-Π-post id = id
-{- trying to do it directly doesn't seem to work either
-
- transport-Π-post'' : {A : Type} {B B' : A → Type} (e : (x : A) → B x == B' x)
- → transport (\ B → Π A B) (λ= (\ x -> (e x))) == (λ f → λ x → coe (e x) (f x))
- transport-Π-post'' e = ap {M = (λ α x → ap= α {x}) o λ=} {N = λ x → x}
- (λ z → λ f x → coe (z (λ x₁ → (e x₁)) x) (f x)) ap=λ= ∘ transport-Π-post (λ= (λ x → (e x)))
-
- map : (A : Type) (B : A → Type)
- {f g : Π A B} → ((x : A) → f x == g x) → f == g
- map A B {f}{g}α = apd {A → Σ B} {λ f₁ → (x : A) → B (fst (f₁ x))} {λ a → a , f a} {λ a → a , g a}
- (λ f₁ → λ x → snd (f₁ x))
- (λ= {A = A} {B = Σ B} {f = λ a → a , f a} {g = λ a → a , g a} (λ x → pair= id (α x)))
- ∘ ! (transport (λ f₁ → (x : A) → B (fst (f₁ x))) (λ= (λ x → pair= id (α x))) f =〈 {!!} 〉
- transport (λ f₁ → (x : A) → B (f₁ x)) (λ= (λ x → ap fst (pair={B = B} id (α x)))) f =〈 {!!} 〉
- transport (λ f₁ → (x : A) → B (f₁ x)) (λ= (\ x -> id)) f =〈 {!transport-Π-post {B = !} 〉
- transport (λ B → (x : A) → (B x)) (λ= (\ x -> id)) f =〈 ap= (transport-Π-post'' (λ x → id)) 〉
- f ∎)
--}
-
- -- uses η for Σ
- swap : {A B} Equiv ((x : A) Paths (B x)) (Homotopies A B)
- swap = (improve (hequiv (λ h ((λ x fst (fst (h x))) , (λ x snd (fst (h x)))) , (λ x snd (h x)))
- (λ i λ x ((fst (fst i) x) , (snd (fst i) x)) , snd i x)
- (λ _ id) (λ _ id)))
- -- this can be written with AC, but it's too annoying to do the beta reduction if you write it this way
- -- (apΣ-l' (AC {A = A} {B = λ _ → B} {C = λ _ _ → B})) ∘ ua (AC {A = A} {B = λ _ → B × B} {C = λ _ b1b2 → fst b1b2 == snd b1b2})
-
_od_ : {A : Type} {B : A Type} {C : A Type} (g : (x : A) B x C x) (f : Π A B) (x : A) C x
g od f = \ x -> g x (f x)
@@ -67,18 +37,30 @@ module FunextDep where
STS : (\ x -> (coe o ua{B x}{B' x})) od e == \ x -> fst (e x)
STS = ap (λ z z od e) Stuck
+
+ Homotopies : (A : Type) (A Type) Type
+ Homotopies A B = (Σ \ (fg : (Π A B) × (Π A B)) (x : A) fst fg x == snd fg x)
+
+ -- uses η for Σ
+ rearrange : {A B} Equiv ((x : A) Paths (B x)) (Homotopies A B)
+ rearrange = (improve (hequiv (λ h ((λ x fst (fst (h x))) , (λ x snd (fst (h x)))) , (λ x snd (h x)))
+ (λ i λ x ((fst (fst i) x) , (snd (fst i) x)) , snd i x)
+ (λ _ id) (λ _ id)))
+ -- this can be written with AC, but it's too annoying to do the beta reduction if you write it this way
+ -- (apΣ-l' (AC {A = A} {B = λ _ → B} {C = λ _ _ → B})) ∘ ua (AC {A = A} {B = λ _ → B × B} {C = λ _ b1b2 → fst b1b2 == snd b1b2})
+
abstract
funextt : {A B} Equiv (Paths ((x : A) B x)) (Homotopies A B)
funextt {A} {B} = Paths ((x : A) B x) ≃〈 contract-Paths≃ 〉
((x : A) B x) ≃〈 coe-equiv (ap {M = B} {N = Paths o B} (\ B -> Π A B) (IsEquiv.g (snd (funext _ _)) (λ x ua (!equiv contract-Paths≃)))) 〉
- ((x : A) Paths (B x)) ≃〈 swap
+ ((x : A) Paths (B x)) ≃〈 rearrange
Homotopies A B ∎∎
funextt-id : {A} {B : A Type} (f : (x : A) B x) fst funextt ((f , f) , id) == ((f , f) , λ x id)
funextt-id {A}{B} f = fst funextt ((f , f) , id) =〈 id 〉
- fst swap (coe (ap {M = B} {N = Paths o B} (λ y (x : A) y x) (IsEquiv.g (snd (funext _ _)) (λ x ua (!equiv contract-Paths≃)))) f) =〈 {!!} 〉
- fst swap (transport (λ y Π A y) (λ= (λ x ua (!equiv contract-Paths≃))) f) =〈 ap (fst swap) (transport-Π-post' (λ x !equiv contract-Paths≃) _) 〉
- fst swap (\ x -> fst (!equiv (contract-Paths≃ {B x})) (f x)) =〈 id 〉
+ fst rearrange (coe (ap {M = B} {N = Paths o B} (λ y (x : A) y x) (IsEquiv.g (snd (funext _ _)) (λ x ua (!equiv contract-Paths≃)))) f) =〈 {!!} 〉
+ fst rearrange (transport (λ y Π A y) (λ= (λ x ua (!equiv contract-Paths≃))) f) =〈 ap (fst rearrange) (transport-Π-post' (λ x !equiv contract-Paths≃) _) 〉
+ fst rearrange (\ x -> fst (!equiv (contract-Paths≃ {B x})) (f x)) =〈 id 〉
(((f , f) , (λ x id)) ∎)
preserves-fst : {A} {B : A Type} (α : Paths ((x : A) B x))
View
19 homotopy/pinsn-paper/intro.tex
@@ -42,17 +42,18 @@ \section{Introduction}
One basic question in algebraic topology is calculating the
\emph{homotopy groups} of a space. Given a space $X$ with a
-distinguished point $x_0$, the \emph{fundamental group of $X$ at the point $x_0$} (denoted
-$\pi_1(X,x_0)$) is the group of loops at $x_0$ up to homotopy, with composition as the group operation.
-This fundamental group is the first in a sequence of \emph{homotopy
- groups}, which provide higher-dimensional information about a space:
-the homotopy groups $\pi_n(X,x_0)$ ``count'' the $n$-dimensional loops in
-that space up to homotopy. $\pi_2(X,x_0)$ is the group of homotopies between
+distinguished point $x_0$, the \emph{fundamental group of $X$ at the
+ point $x_0$} (denoted $\pi_1(X,x_0)$) is the group of loops at $x_0$
+up to homotopy, with composition as the group operation. This
+fundamental group is the first in a sequence of \emph{homotopy groups},
+which provide higher-dimensional information about a space: the homotopy
+groups $\pi_n(X,x_0)$ ``count'' the $n$-dimensional loops in that space
+up to homotopy. $\pi_2(X,x_0)$ is the group of homotopies between
$\dsd{id}_{{x_0}}$ and itself, $\pi_3(X,x_0)$ is the group of homotopies
between $\dsd{id}_{\dsd{id}_{{x_0}}}$ and itself, and so on.
-\emph{Calculating a homotopy group $\pi_n(X,x_0)$} is to construct a group isomorphism
-between $\pi_n(X,x_0)$ and some explicit description of a group,
-such as \Z\/ or $\Z_k$ (\Z\/ mod $k$).
+\emph{Calculating a homotopy group $\pi_n(X,x_0)$} is to construct a
+group isomorphism between $\pi_n(X,x_0)$ and some explicit description
+of a group, such as \Z\/ or $\Z_k$ (\Z\/ mod $k$).
The homotopy groups of a space can be difficult to calculate. This is
true even for spaces as simple as the $n$-dimensional spheres (the
View
5 lib/Paths.agda
@@ -409,8 +409,3 @@ module lib.Paths where
-> (f : A -> B)
-> Path (jayfrompm2 (\ _ _ _ -> B) P f) (f N)
fire-jay-const2 {A}{B} P f = jay (λ x y p Path (jayfrompm2 (λ _ _ _ B) p f) (f y)) P (\ _ -> id)
-
-
- transport-→-post : {C A B : Set} (δ : B ≃ C) (f : A -> B)
- -> transport (\ X -> A -> X) δ f ≃ (transport (\ X -> X) δ o f)
- transport-→-post id f = id
Please sign in to comment.
Something went wrong with that request. Please try again.