Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

freud

  • Loading branch information...
commit e87bad495e041c45f7d13f333dc96ce442a94ece 1 parent 55ff01a
Dan Licata authored
2  badpostulates
View
@@ -2,5 +2,5 @@
#!/bin/bash
-find . -name "*.agda" | grep -v "oldlib" | xargs grep postulate | grep -v "HoTT Axiom" | grep -v "scraps" | grep -v "in-progress"
+find . -name "*.agda" | grep -v "oldlib" | xargs grep postulate | grep -v "HoTT Axiom" | grep -v "Agda Primitive" | grep -v "scraps" | grep -v "in-progress"
199 homotopy/Freudenthal.agda
View
@@ -34,29 +34,33 @@ module homotopy.Freudenthal where
decode' : Trunc k X Trunc k (Path {(Susp X)} No No)
decode' = Trunc-func up
- Codes-mer : X (Trunc k X) (Trunc k X)
- Codes-mer = wedge-rec nX (connected-Trunc _ _ _ nX) Trunc-level k< {base} {[ base ]} (λ x' x') (λ x [ x ]) id
-
- Codes-mer-βa : (\ b -> Codes-mer base b) ≃ (\ x -> x)
- Codes-mer-βa = wedge-rec-βa nX (connected-Trunc _ _ _ nX) Trunc-level k< (λ x x) (λ x [ x ]) id
-
- Codes-mer-βb : (\ a -> Codes-mer a [ base ]) ≃ (\ x -> [ x ])
- Codes-mer-βb = wedge-rec-βb nX (connected-Trunc _ _ _ nX) Trunc-level k< (λ x x) (λ x [ x ]) id
-
- Codes-mer-isequiv : (x : X) -> IsEquiv (Codes-mer x)
- Codes-mer-isequiv = ConnectedFib.everywhere n' {a = base}
- nX
- (λ x' IsEquiv (Codes-mer x') ,
- raise-level (-1<= -2<n') (IsEquiv-HProp (Codes-mer x'))) -- need n' is S - for this
- (transport IsEquiv (! Codes-mer-βa) (snd id-equiv))
-
- Codes-mer-inv-base : IsEquiv.g (Codes-mer-isequiv base) ≃ (\ x -> x)
- Codes-mer-inv-base = transport-IsEquiv-g (! Codes-mer-βa) (snd id-equiv) ∘ ap IsEquiv.g
- (ConnectedFib.everywhereβ n' nX
- (λ x'
- IsEquiv (Codes-mer x') ,
- raise-level (-1<= -2<n') (IsEquiv-HProp (Codes-mer x')))
- (transport IsEquiv (! Codes-mer-βa) (snd id-equiv)))
+ abstract
+ Codes-mer : X (Trunc k X) (Trunc k X)
+ Codes-mer = wedge-rec nX (connected-Trunc _ _ _ nX) Trunc-level k< {base} {[ base ]} (λ x' x') (λ x [ x ]) id
+
+ Codes-mer-βa : (\ b -> Codes-mer base b) ≃ (\ x -> x)
+ Codes-mer-βa = wedge-rec-βa nX (connected-Trunc _ _ _ nX) Trunc-level k< (λ x x) (λ x [ x ]) id
+
+ Codes-mer-βb : (\ a -> Codes-mer a [ base ]) ≃ (\ x -> [ x ])
+ Codes-mer-βb = wedge-rec-βb nX (connected-Trunc _ _ _ nX) Trunc-level k< (λ x x) (λ x [ x ]) id
+
+ Codes-mer-coh : ap≃ Codes-mer-βb {base} ≃ ap≃ Codes-mer-βa {[ base ]}
+ Codes-mer-coh = ∘-unit-l (ap≃ Codes-mer-βa) ∘ wedge-rec-coh nX (connected-Trunc _ _ _ nX) Trunc-level k< (λ x x) (λ x [ x ]) id
+
+ Codes-mer-isequiv : (x : X) -> IsEquiv (Codes-mer x)
+ Codes-mer-isequiv = ConnectedFib.everywhere n' {a0 = base}
+ nX
+ (λ x' IsEquiv (Codes-mer x') ,
+ raise-level (-1<= -2<n') (IsEquiv-HProp (Codes-mer x'))) -- need n' is S - for this
+ (transport IsEquiv (! Codes-mer-βa) (snd id-equiv))
+
+ Codes-mer-inv-base : IsEquiv.g (Codes-mer-isequiv base) ≃ (\ x -> x)
+ Codes-mer-inv-base = transport-IsEquiv-g (! Codes-mer-βa) (snd id-equiv) ∘ ap IsEquiv.g
+ (ConnectedFib.β n' nX
+ (λ x'
+ IsEquiv (Codes-mer x') ,
+ raise-level (-1<= -2<n') (IsEquiv-HProp (Codes-mer x')))
+ (transport IsEquiv (! Codes-mer-βa) (snd id-equiv)))
Codes-mer-equiv : (x : X) -> Equiv (Trunc k X) (Trunc k X)
Codes-mer-equiv x = (Codes-mer x) , Codes-mer-isequiv x
@@ -69,35 +73,34 @@ module homotopy.Freudenthal where
NType-Codes : (x : Susp X) -> NType k (Codes x)
NType-Codes = Susp-elim _ Trunc-level Trunc-level (λ _ HProp-unique (NType-is-HProp _) _ _)
-{-
encode0 : {x : Susp X} Path No x Codes x
encode0 α = transport Codes α [ base ]
encode : {x : Susp X} P x Codes x
encode{x} tα = Trunc-rec (NType-Codes x) encode0 tα
- encode-decode' : (c : Codes No) → encode (decode' c) ≃ c
- encode-decode' = Trunc-elim _ (λ _path-preserves-level Trunc-level)
- xencode (decode' [ x ]) ≃〈 id 〉
- transport Codes (! (mer base) ∘ mer x) [ base ] ≃〈 ap≃ (transport-ap-assoc Codes (! (mer base) ∘ mer x))
- coe (ap Codes (! (mer base) ∘ mer x)) [ base ] ≃〈 ap (λ x' → coe x' [ base ]) (ap- Codes (! (mer base)) (mer x)) 〉
- coe (ap Codes (! (mer base))ap Codes (mer x)) [ base ] ≃〈 ap≃ (transport-∘ (λ x' → x') (ap Codes (! (mer base))) (ap Codes (mer x))) 〉
- coe (ap Codes (! (mer base)))
- (coe (ap Codes (mer x)) [ base ]) ≃〈 ap (\ x -> (coe (ap Codes (! (mer base))) (coe x [ base ]))) Susp-rec/βmer 〉
- coe (ap Codes (! (mer base)))
- (coe (ua (Codes-mer-equiv x)) [ base ]) ≃〈 ap (coe (ap Codes (! (mer base)))) (ap≃ (type≃β (Codes-mer-equiv x))) 〉
- coe (ap Codes (! (mer base)))
- (Codes-mer x [ base ]) ≃〈 ap (λ x' → coe (ap Codes (! (mer base))) x') (ap≃ Codes-mer-βb) 〉
- coe (ap Codes (! (mer base)))
- [ x ] ≃〈 ap (λ y → coe y [ x ]) (ap-! Codes (mer base))
- coe (! (ap Codes (mer base)))
- [ x ] ≃〈 ap (λ y → coe (! y) [ x ]) Susp-rec/βmer 〉
- coe (! (ua (Codes-mer-equiv base)))
- [ x ] ≃〈 ap≃ (type≃β! (Codes-mer-equiv base))
- IsEquiv.g (snd (Codes-mer-equiv base))
- [ x ] ≃〈 ap≃ Codes-mer-inv-base {[ x ]} 〉
- [ x ] ∎)
--}
+ abstract
+ encode-decode' : (c : Codes No) encode (decode' c) ≃ c
+ encode-decode' = Trunc-elim _ _ path-preserves-level Trunc-level)
+ (λ x encode (decode' [ x ]) ≃〈 id
+ transport Codes (! (mer base) ∘ mer x) [ base ] ≃〈 ap≃ (transport-ap-assoc Codes (! (mer base)mer x)) 〉
+ coe (ap Codes (! (mer base) ∘ mer x)) [ base ] ≃〈 ap (λ x' coe x' [ base ]) (ap-∘ Codes (! (mer base)) (mer x)) 〉
+ coe (ap Codes (! (mer base)) ∘ ap Codes (mer x)) [ base ] ≃〈 ap≃ (transport-∘ (λ x' x') (ap Codes (! (mer base))) (ap Codes (mer x))) 〉
+ coe (ap Codes (! (mer base)))
+ (coe (ap Codes (mer x)) [ base ]) ≃〈 ap (\ x -> (coe (ap Codes (! (mer base))) (coe x [ base ]))) Susp-rec/βmer 〉
+ coe (ap Codes (! (mer base)))
+ (coe (ua (Codes-mer-equiv x)) [ base ]) ≃〈 ap (coe (ap Codes (! (mer base)))) (ap≃ (type≃β (Codes-mer-equiv x))) 〉
+ coe (ap Codes (! (mer base)))
+ (Codes-mer x [ base ]) ≃〈 ap (λ x' coe (ap Codes (! (mer base))) x') (ap≃ Codes-mer-βb) 〉
+ coe (ap Codes (! (mer base)))
+ [ x ] ≃〈 ap (λ y coe y [ x ]) (ap-! Codes (mer base))
+ coe (! (ap Codes (mer base)))
+ [ x ] ≃〈 ap (λ y coe (! y) [ x ]) Susp-rec/βmer 〉
+ coe (! (ua (Codes-mer-equiv base)))
+ [ x ] ≃〈 ap≃ (type≃β! (Codes-mer-equiv base))
+ IsEquiv.g (snd (Codes-mer-equiv base))
+ [ x ] ≃〈 ap≃ Codes-mer-inv-base {[ x ]} 〉
+ [ x ] ∎)
decode : {x} -> Codes x P x
decode {x} = Susp-elim (\ x -> Codes x P x)
@@ -105,59 +108,59 @@ module homotopy.Freudenthal where
(Trunc-func (λ x' mer x'))
(λ x'
transport (λ x0 Codes x0 P x0) (mer x') decode' ≃〈 transport-→ Codes P (mer x') decode' 〉
- transport P (mer x') o decode' o transport Codes (! (mer x')) ≃〈 {!λ≃ (STS x')!}
+ transport P (mer x') o decode' o transport Codes (! (mer x')) ≃〈 move-posto-with-transport-left Codes (mer x') (transport P (mer x') o decode') (Trunc-func (λ x0 mer x0)) (λ≃ (STS x'))
(Trunc-func (λ x0 mer x0) ∎))
x where
- STS : x' c -> transport P (mer x') (decode' c) ≃
- Trunc-func mer (transport Codes (mer x') c)
- STS x' = Trunc-elim _ (λ _ path-preserves-level Trunc-level)
- (λ x0 wedge-elim nX nX
- (λ x1 x2
- (transport P (mer x1) (decode' [ x2 ]) ≃
- Trunc-func mer (transport Codes (mer x1) [ x2 ]))
- , path-preserves-level (Trunc-level {k})) -- a little slack here, but would tightening it help?
- k<
- {base}{base}
- (λ b' transport P (mer base) (decode' [ b' ]) ≃〈 id 〉
- transport P (mer base) [ (up b') ] ≃〈 ap≃ (transport-Trunc (Path No) (mer base))
- [ transport (Path No) (mer base) (up b') ] ≃〈 ap [_] (transport-Path-right (mer base) (up b')) 〉
- [ (mer base) ∘ ! (mer base) ∘ mer b' ] ≃〈 ap [_] (!-inv-r-front (mer base) (mer b')) 〉
- [ mer b' ] ≃〈 id
- Trunc-func mer [ b' ] ≃〈 ap (Trunc-func mer) (! (ap≃ Codes-mer-βa))
- (Trunc-func mer (Codes-mer base [ b' ])) ≃〈 ap (Trunc-func mer) (! (ap≃ (type≃β (Codes-mer-equiv base)))) 〉
- (Trunc-func mer (coe (ua (Codes-mer-equiv base)) [ b' ])) ≃〈 ap (Trunc-func mer) (ap (λ x1 coe x1 [ b' ]) (! Susp-rec/βmer)) 〉
- (Trunc-func mer (coe (ap Codes (mer base)) [ b' ])) ≃〈 ap (Trunc-func mer) (! (ap≃ (transport-ap-assoc Codes (mer base)))) 〉
- (Trunc-func mer (transport Codes (mer base) [ b' ]) ∎))
- (λ a' transport P (mer a') (decode' [ base ]) ≃〈 id 〉
- transport P (mer a') [ up base ] ≃〈 ap≃ (transport-Trunc (Path No) (mer a'))
- [ transport (Path No) (mer a') (up base) ] ≃〈 ap [_] (transport-Path-right (mer a') (up base)) 〉
- [ (mer a') ∘ ! (mer base) ∘ mer base ] ≃〈 ap [_] (!-inv-l-back (mer a') (mer base)) 〉 -- difference 1
- [ (mer a') ] ≃〈 id 〉
- Trunc-func mer [ a' ] ≃〈 ap (Trunc-func mer) (! (ap≃ Codes-mer-βb)) 〉 -- difference 2
- (Trunc-func mer (Codes-mer a' [ base ])) ≃〈 ap (Trunc-func mer) (! (ap≃ (type≃β (Codes-mer-equiv a'))))
- (Trunc-func mer (coe (ua (Codes-mer-equiv a')) [ base ])) ≃〈 ap (Trunc-func mer) (ap (λ x1 coe x1 [ base ]) (! Susp-rec/βmer)) 〉
- (Trunc-func mer (coe (ap Codes (mer a')) [ base ])) ≃〈 ap (Trunc-func mer) (! (ap≃ (transport-ap-assoc Codes (mer a')))) 〉
- (Trunc-func mer (transport Codes (mer a') [ base ]) ∎))
- (ap2
- (λ x1 y
- transport P (mer base) (decode' [ base ]) ≃〈 id 〉
- transport P (mer base) [ up base ] ≃〈 ap≃ (transport-Trunc (Path No) (mer base))
- [ transport (Path No) (mer base) (up base) ] ≃〈 ap [_] (transport-Path-right (mer base) (up base)) 〉
- [ mer base ∘ ! (mer base) ∘ mer base ] ≃〈 x1
- [ mer base ] ≃〈 id
- Trunc-func mer [ base ] ≃〈 y
- Trunc-func mer (Codes-mer base [ base ]) ≃〈 ap (Trunc-func mer) (! (ap≃ (type≃β (Codes-mer-equiv base))))
- Trunc-func mer (coe (ua (Codes-mer-equiv base)) [ base ]) ≃〈 ap (Trunc-func mer) (ap (λ x2 coe x2 [ base ]) (! Susp-rec/βmer))
- Trunc-func mer (coe (ap Codes (mer base)) [ base ]) ≃〈 ap (Trunc-func mer) (! (ap≃ (transport-ap-assoc Codes (mer base)))) 〉 (Trunc-func mer (transport Codes (mer base) [ base ]) ∎))
- (coh1 (mer base)) coh2)
- x' x0)
- where coh1 : {k A} {a a' : A} (p : a ≃ a') -> ap ([_]{k}) (!-inv-r-front p p) ≃ ap ([_]{k}) (!-inv-l-back p p)
- coh1 id = id
-
- coh2 : ap (Trunc-func mer) (! (ap≃ Codes-mer-βa {[ base ]})) ≃ ap (Trunc-func mer) (! (ap≃ Codes-mer-βb {base}))
- coh2 = ap (λ x0 ap (Trunc-func mer) (! x0)) {!!}
-
-{-
+ abstract
+ STS : x' c -> transport P (mer x') (decode' c) ≃
+ Trunc-func mer (transport Codes (mer x') c)
+ STS x' = Trunc-elim _ (λ _ path-preserves-level Trunc-level)
+ (λ x0 wedge-elim nX nX
+ (λ x1 x2
+ (transport P (mer x1) (decode' [ x2 ])
+ Trunc-func mer (transport Codes (mer x1) [ x2 ]))
+ , path-preserves-level (Trunc-level {k})) -- a little slack here, but would tightening it help?
+ k<
+ {base}{base}
+ (λ b' transport P (mer base) (decode' [ b' ]) ≃〈 id
+ transport P (mer base) [ (up b') ] ≃〈 ap(transport-Trunc (Path No) (mer base)) 〉
+ [ transport (Path No) (mer base) (up b') ] ≃〈 ap [_] (transport-Path-right (mer base) (up b')) 〉
+ [ (mer base) ∘ ! (mer base) ∘ mer b' ] ≃〈 ap [_] (!-inv-r-front (mer base) (mer b'))
+ [ mer b' ] ≃〈 id
+ Trunc-func mer [ b' ] ≃〈 ap (Trunc-func mer) (! (ap≃ Codes-mer-βa)) 〉
+ (Trunc-func mer (Codes-mer base [ b' ])) ≃〈 ap (Trunc-func mer) (! (ap≃ (type≃β (Codes-mer-equiv base)))) 〉
+ (Trunc-func mer (coe (ua (Codes-mer-equiv base)) [ b' ])) ≃〈 ap (Trunc-func mer) (ap (λ x1 coe x1 [ b' ]) (! Susp-rec/βmer)) 〉
+ (Trunc-func mer (coe (ap Codes (mer base)) [ b' ])) ≃〈 ap (Trunc-func mer) (! (ap≃ (transport-ap-assoc Codes (mer base)))) 〉
+ (Trunc-func mer (transport Codes (mer base) [ b' ]) ∎))
+ (λ a' transport P (mer a') (decode' [ base ]) ≃〈 id
+ transport P (mer a') [ up base ] ≃〈 ap(transport-Trunc (Path No) (mer a')) 〉
+ [ transport (Path No) (mer a') (up base) ] ≃〈 ap [_] (transport-Path-right (mer a') (up base)) 〉
+ [ (mer a') ∘ ! (mer base) ∘ mer base ] ≃〈 ap [_] (!-inv-l-back (mer a') (mer base)) 〉 -- difference 1
+ [ (mer a') ] ≃〈 id 〉
+ Trunc-func mer [ a' ] ≃〈 ap (Trunc-func mer) (! (ap≃ Codes-mer-βb))-- difference 2
+ (Trunc-func mer (Codes-mer a' [ base ])) ≃〈 ap (Trunc-func mer) (! (ap≃ (type≃β (Codes-mer-equiv a')))) 〉
+ (Trunc-func mer (coe (ua (Codes-mer-equiv a')) [ base ])) ≃〈 ap (Trunc-func mer) (ap (λ x1 coe x1 [ base ]) (! Susp-rec/βmer)) 〉
+ (Trunc-func mer (coe (ap Codes (mer a')) [ base ])) ≃〈 ap (Trunc-func mer) (! (ap≃ (transport-ap-assoc Codes (mer a')))) 〉
+ (Trunc-func mer (transport Codes (mer a') [ base ]) ∎))
+ (ap2
+ (λ x1 y
+ transport P (mer base) (decode' [ base ]) ≃〈 id
+ transport P (mer base) [ up base ] ≃〈 ap(transport-Trunc (Path No) (mer base)) 〉
+ [ transport (Path No) (mer base) (up base) ] ≃〈 ap [_] (transport-Path-right (mer base) (up base))
+ [ mer base ∘ ! (mer base) ∘ mer base ] ≃〈 x1
+ [ mer base ] ≃〈 id
+ Trunc-func mer [ base ] ≃〈 y
+ Trunc-func mer (Codes-mer base [ base ]) ≃〈 ap (Trunc-func mer) (! (ap≃ (type≃β (Codes-mer-equiv base))))
+ Trunc-func mer (coe (ua (Codes-mer-equiv base)) [ base ]) ≃〈 ap (Trunc-func mer) (ap (λ x2 coe x2 [ base ]) (! Susp-rec/βmer))〉
+ Trunc-func mer (coe (ap Codes (mer base)) [ base ]) ≃〈 ap (Trunc-func mer) (! (ap≃ (transport-ap-assoc Codes (mer base)))) 〉 (Trunc-func mer (transport Codes (mer base) [ base ]) ∎))
+ (coh1 (mer base)) coh2)
+ x' x0)
+ where coh1 : {k A} {a a' : A} (p : a ≃ a') -> ap ([_]{k}) (!-inv-r-front p p) ≃ ap ([_]{k}) (!-inv-l-back p p)
+ coh1 id = id
+
+ coh2 : ap (Trunc-func mer) (! (ap≃ Codes-mer-βa {[ base ]})) ≃ ap (Trunc-func mer) (! (ap≃ Codes-mer-βb {base}))
+ coh2 = ap (λ x0 ap (Trunc-func mer) (! x0)) (! Codes-mer-coh)
+
decode-encode : {x : Susp X} (α : P x) -> decode (encode α) ≃ α
decode-encode tα = Trunc-elim (\ α -> decode (encode α) ≃ α) (λ x path-preserves-level Trunc-level)
(path-induction (λ _ p decode (encode [ p ]) ≃ [ p ]) (ap [_] (!-inv-l (mer base))))
@@ -165,4 +168,4 @@ module homotopy.Freudenthal where
theorem : Trunc k X ≃ Trunc k (Path {(Susp X)} No No)
theorem = ua (improve (hequiv decode' encode encode-decode' decode-encode))
--}
+
2  lib/BasicTypes.agda
View
@@ -22,6 +22,8 @@ module lib.BasicTypes where
open import lib.Maybe public
open import lib.List public
open import lib.Monoid public
+ open import lib.Char public
+ open import lib.String public
open import lib.Universe public
open import lib.Truncations public
7 lib/Functions.agda
View
@@ -60,13 +60,6 @@ module lib.Functions where
(\ x -> transport (\ γ -> B γ x) δ (f x))
transport-Π-post' _ id f = id
- -- transportitution extension for Γ,x:A⁻ in DTT
- pair≃⁻ : {A : Set} {B : A -> Set} {p q : Σ B}
- -> (α : (fst p) ≃ (fst q)) -> (snd p) ≃ transport B (! α) (snd q)
- -> p ≃ q
- pair≃⁻ {A}{B}{p}{q} α β =
- pair≃ α (ap≃ (ap (λ x transport B x) (!-inv-r α) ∘ ! (transport-∘ B α (! α))) ∘ ap (transport B α) β)
-
transport-Π : {Γ} (A : Γ -> Set) (B : (γ : Γ) -> A γ -> Set)
1 θ2 : Γ} (δ : θ1 ≃ θ2) (f : (x : A θ1) -> B θ1 x)
-> transport (\ γ -> (x : A γ) -> B γ x) δ f ≃
230 lib/NConnected.agda
View
@@ -13,9 +13,6 @@ open Truncation
module lib.NConnected where
- postulate
- plus2-comm : m n -> plus2 m n ≃ plus2 n m
-
Connected : TLevel -> Type -> Type
Connected n A = NType -2 (Trunc n A)
@@ -39,17 +36,16 @@ module lib.NConnected where
lemma1 = λ≃ (λ x out-of-contractible (Trunc-rec (NTypes-level n) (λ x' P x')) c x [ a0 ])
lemma : P ≃ (\ _ -> P a0)
- lemma = P ≃〈 id 〉
- Trunc-rec (NTypes-level n) (λ x' P x') o [_] ≃〈 ap (λ f f o ([_]{S n})) lemma1 〉
- (\ _ -> P a0) o ([_]{S n}) ≃〈 id 〉
- ((λ _ P a0) ∎)
- postulate
- β : (n : TLevel) {A : Type} {a0 : A}
- -> (cA : Connected (S n) A)
- -> (P : A NTypes n)
- -> (p0 : fst (P a0))
- -> everywhere n cA P p0 a0 ≃ p0
+ lemma = ap (λ f f o ([_]{S n})) lemma1
+ β : (n : TLevel) {A : Type} {a0 : A}
+ -> (cA : Connected (S n) A)
+ -> (P : A NTypes n)
+ -> (p0 : fst (P a0))
+ -> everywhere n cA P p0 a0 ≃ p0
+ β n cA P p0 = {!!}
+
+{-
η : (n : TLevel) {A : Type} {a0 : A}
-> (cA : Connected (S n) A)
-> (P : A → NTypes n)
@@ -65,8 +61,7 @@ module lib.NConnected where
-> f a0 ≃ g a0
-> f ≃ g
ext n {a0 = a0} cA P f g on-a0 = ! (η n cA P (f a0) g (! on-a0)) ∘ η n cA P (f a0) f id
-
-{-
+
eqv : (n : TLevel) {A : Type} {a : A}
-> Connected (S n) A
-> (P : A → NTypes n)
@@ -99,27 +94,50 @@ module lib.NConnected where
Path (α1 ∘ ! (h a0)) α2) ≃〈 ap (λ B Σ B) (λ≃ (λ h flip≃ ∘ flip-triangle≃ α1 α2 (h a0))) 〉
Σ (\ h -> h a0 ≃ ! α2 ∘ α1) ≃〈 id 〉
Extensions A a0 (λ a Path (f1 a) (f2 a)) (! α2 ∘ α1) ∎
-
- Extensions-level : {m n} {A : Type} (cA : Connected (S m) A)
- (a0 : A) (C : A -> NTypes (plus2 n m)) (c0 : fst (C a0))
- -> NType n (Extensions A a0 (fst o C) c0)
- Extensions-level {m}{ -2} cA a0 C c0 =
- ntype ((ConnectedFib.everywhere m cA C c0 , ConnectedFib.β m cA C c0) ,
- (λ {(f , α) pair≃ (λ≃
- (ConnectedFib.everywhere
- m {_} {a0} cA
- (λ a Path (ConnectedFib.everywhere m cA C c0 a) (f a) , path-preserves-level (snd (C a)))
- (! α ∘ ConnectedFib.β m cA C c0)))
- FIXME})) where
- postulate FIXME : {A} -> A
- Extensions-level {m}{S n} cA a0 C c0 =
- ntype (λ e1 e2 transport (NType n)
- (! (Extensions-Path (fst o C) c0 e1 e2))
- (Extensions-level {_} {n} cA a0 (\ a -> (Path (fst e1 a) (fst e2 a), use-level (snd (C a)) _ _))
- (! (snd e2) ∘ snd e1)))
abstract
- wedge-elim1' : {m n} {A B : Type}
+ Extensions-level : {m n} {A : Type} (cA : Connected (S m) A)
+ (a0 : A) (C : A -> NTypes (plus2 n m)) (c0 : fst (C a0))
+ -> NType n (Extensions A a0 (fst o C) c0)
+ Extensions-level {m}{ -2} cA a0 C c0 =
+ ntype ((ConnectedFib.everywhere m cA C c0 , ConnectedFib.β m cA C c0) ,
+ (λ {(f , α) pair≃ (λ≃ (ConnectedFib.everywhere m {_} {a0} cA
+ (λ a Path (ConnectedFib.everywhere m cA C c0 a) (f a) , path-preserves-level (snd (C a)))
+ (! α ∘ ConnectedFib.β m cA C c0)))
+ (transport (λ f' f' a0 ≃ c0)
+ (λ≃
+ (ConnectedFib.everywhere m cA
+ (λ a
+ Path (ConnectedFib.everywhere m cA C c0 a) (f a) ,
+ path-preserves-level (snd (C a)))
+ (! α ∘ ConnectedFib.β m cA C c0)))
+ (ConnectedFib.β m cA C c0) ≃〈 transport-Path-pre' (λ f' f' a0) (λ≃ (ConnectedFib.everywhere m cA (λ a Path (ConnectedFib.everywhere m cA C c0 a) (f a) , path-preserves-level (snd (C a))) (! α ∘ ConnectedFib.β m cA C c0))) (ConnectedFib.β m cA C c0) 〉
+ (ConnectedFib.β m cA C c0) ∘
+ ! (ap≃ (λ≃
+ (ConnectedFib.everywhere m cA
+ (λ a
+ Path (ConnectedFib.everywhere m cA C c0 a) (f a) ,
+ path-preserves-level (snd (C a)))
+ (! α ∘ ConnectedFib.β m cA C c0))) {a0}) ≃〈 ap (λ x ConnectedFib.β m cA C c0 ∘ ! x) (Π≃β (ConnectedFib.everywhere m cA (λ a Path (ConnectedFib.everywhere m cA C c0 a) (f a) , path-preserves-level (snd (C a))) (! α ∘ ConnectedFib.β m cA C c0))) 〉
+ (ConnectedFib.β m cA C c0) ∘
+ ! ((ConnectedFib.everywhere m cA
+ (λ a
+ Path (ConnectedFib.everywhere m cA C c0 a) (f a) ,
+ path-preserves-level (snd (C a)))
+ (! α ∘ ConnectedFib.β m cA C c0)) a0) ≃〈 ap (λ x ConnectedFib.β m cA C c0 ∘ ! x) (ConnectedFib.β m cA (λ a Path (ConnectedFib.everywhere m cA C c0 a) (f a) , path-preserves-level (snd (C a))) (! α ∘ ConnectedFib.β m cA C c0)) 〉
+ (ConnectedFib.β m cA C c0) ∘
+ ! (! α ∘ ConnectedFib.β m cA C c0) ≃〈 ap (_∘_ (ConnectedFib.β m cA C c0)) (!-∘ (! α) (ConnectedFib.β m cA C c0)) 〉
+ (ConnectedFib.β m cA C c0) ∘ ! (ConnectedFib.β m cA C c0) ∘ ! (! α) ≃〈 !-inv-r-front (ConnectedFib.β m cA C c0) (! (! α)) 〉
+ ! (! α) ≃〈 !-invol α 〉
+ α ∎)}))
+ Extensions-level {m}{S n} cA a0 C c0 =
+ ntype (λ e1 e2 transport (NType n)
+ (! (Extensions-Path (fst o C) c0 e1 e2))
+ (Extensions-level {_} {n} cA a0 (\ a -> (Path (fst e1 a) (fst e2 a), use-level (snd (C a)) _ _))
+ (! (snd e2) ∘ snd e1)))
+
+ abstract
+ wedge-elim' : {m n} {A B : Type}
(cA : Connected (S m) A)
(cB : Connected (S n) B)
(C : A B NTypes (plus2 m n))
@@ -127,80 +145,27 @@ module lib.NConnected where
-> (fa0 : (b' : B) -> fst (C a0 b'))
-> (fb0 : (a' : A) -> fst (C a' b0))
-> fa0 b0 ≃ fb0 a0
- -> (a' : A) -> Extensions _ b0 (fst o (C a')) (fb0 a')
- wedge-elim1'{m}{n}{A}{B} cA cB C {a0}{b0} fa0 fb0 agree a =
+ -> (a : A) -> Extensions B b0 (\ b -> fst (C a b)) (fb0 a)
+ wedge-elim'{m}{n}{A}{B} cA cB C {a0}{b0} fa0 fb0 agree a =
(ConnectedFib.everywhere m {_} {a0} cA
- (λ a' Extensions _ b0 (fst o (C a')) (fb0 a') ,
+ (λ a' Extensions _ b0 (\ b -> fst (C a' b)) (fb0 a') ,
Extensions-level {n} {m} cB b0 (C a') (fb0 a'))
(fa0 , agree)
a)
-{-
- wedge-elim2' : ∀ {m n} {A B : Type}
- (cA : Connected (S m) A)
- (cB : Connected (S n) B)
- (C : A → B → NTypes (plus2 m n))
- {a0 : A} {b0 : B}
- -> (fa0 : (b' : B) -> fst (C a0 b'))
- -> (fb0 : (a' : A) -> fst (C a' b0))
- -> fa0 b0 ≃ fb0 a0
- -> (b' : B) -> Extensions _ a0 (\a' -> fst (C a' b')) (fa0 b')
- wedge-elim2'{m}{n}{A}{B} cA cB C {a0}{b0} fa0 fb0 agree b =
- (ConnectedFib.everywhere n {_} {b0} cB
- (λ b' → Extensions _ _ (\a' -> fst (C a' b')) (fa0 b') ,
- Extensions-level {m} {n} cA a0 (\ a' -> fst (C a' b') , transport (λ x → NType x (fst (C a' b'))) (plus2-comm m n) (snd (C a' b'))) (fa0 b'))
- (fb0 , ! agree)
- b)
--}
-
wedge-elim : {m n p} {A B : Type}
(cA : Connected (S m) A)
(cB : Connected (S n) B)
(C : A B NTypes p)
(app : p <=tl plus2 m n)
{a0 : A} {b0 : B}
- -> (fa0 : (b' : B) -> fst (C a0 b'))
- -> (fb0 : (a' : A) -> fst (C a' b0))
- -> fa0 b0 ≃ fb0 a0
- -> (a' : A) -> (b' : B) -> fst (C a' b')
- wedge-elim{m}{n}{p}{A}{B} cA cB C app fa0 fb0 agree a' =
- fst (wedge-elim1' cA cB (λ a b fst (C a b) , raise-level app (snd (C a b))) fa0 fb0 agree a')
-
-{-
- wedge-elim2 : ∀ {m n p} {A B : Type}
- (cA : Connected (S m) A)
- (cB : Connected (S n) B)
- (C : A → B → NTypes p)
- (app : p <=tl plus2 m n)
- {a0 : A} {b0 : B}
- -> (fa0 : (b' : B) -> fst (C a0 b'))
- -> (fb0 : (a' : A) -> fst (C a' b0))
+ -> (fa0 : (b : B) -> fst (C a0 b))
+ -> (fb0 : (a : A) -> fst (C a b0))
-> fa0 b0 ≃ fb0 a0
- -> (a' : A) -> (b' : B) -> fst (C a' b')
- wedge-elim2{m}{n}{p}{A}{B} cA cB C app fa0 fb0 agree a' b' =
- fst (wedge-elim2' cA cB (λ a b → fst (C a b) , raise-level app (snd (C a b))) fa0 fb0 agree b') a'
+ -> (a : A) -> (b : B) -> fst (C a b)
+ wedge-elim{m}{n}{p}{A}{B} cA cB C app fa0 fb0 agree a =
+ fst (wedge-elim' cA cB (λ a' b' fst (C a' b') , raise-level app (snd (C a' b'))) fa0 fb0 agree a)
-
- same : ∀ {m n p} {A B : Type}
- (cA : Connected (S m) A)
- (cB : Connected (S n) B)
- (C : A → B → NTypes p)
- (app : p <=tl plus2 m n)
- {a0 : A} {b0 : B}
- -> (fa0 : (b' : B) -> fst (C a0 b'))
- -> (fb0 : (a' : A) -> fst (C a' b0))
- -> (agree : fa0 b0 ≃ fb0 a0)
- -> (a' : A) -> (b' : B) -> (wedge-elim cA cB C app fa0 fb0 agree a' b')
- ≃ (wedge-elim2 cA cB C app fa0 fb0 agree a' b')
- same {m}{n}{p} cA cB C app {a0}{b0} fa0 fb0 agree a' b' =
- wedge-elim {m} {n} {p} cA cB
- (λ a b →
- wedge-elim cA cB C app fa0 fb0 agree a b ≃
- wedge-elim2 cA cB C app fa0 fb0 agree a b
- , {!!})
- app{a0}{b0} {!!} {!!} {!!} a' b'
--}
-
wedge-elim-βa : {m}{n}{p} {A B : Type}
(cA : Connected (S m) A) (cB : Connected (S n) B) (C : A B NTypes p)
(app : p <=tl (plus2 m n)){a0 : A} {b0 : B}
@@ -211,7 +176,7 @@ module lib.NConnected where
wedge-elim-βa{m}{n}{p} cA cB C app{a0}{b0} fa0 fb0 agree =
let C = (λ a b fst (C a b) , raise-level app (snd (C a b)))
in
- ap fst
+ fst
(ConnectedFib.β m cA
(λ a'
Extensions _ _ (fst o C a') (fb0 a') ,
@@ -226,41 +191,36 @@ module lib.NConnected where
-> (agree : fa0 b0 ≃ fb0 a0)
-> (\ a -> wedge-elim cA cB C app fa0 fb0 agree a b0) ≃ fb0
wedge-elim-βb {m}{n}{p}{A}{B} cA cB C app{a0}{b0} fa0 fb0 agree =
- let C = (λ a b fst (C a b) , raise-level app (snd (C a b)))
+ λ≃ (\ a -> snd (wedge-elim' cA cB (λ a b fst (C a b) , raise-level app (snd (C a b))) fa0 fb0 agree a))
+
+ wedge-elim-coh : {m}{n}{p} {A B : Type}
+ (cA : Connected (S m) A) (cB : Connected (S n) B) (C : A B NTypes p)
+ (app : p <=tl (plus2 m n)){a0 : A} {b0 : B}
+ -> (fa0 : (b : B) -> fst (C a0 b))
+ -> (fb0 : (a : A) -> fst (C a b0))
+ -> (agree : fa0 b0 ≃ fb0 a0)
+ -> ap≃ (wedge-elim-βb cA cB C app fa0 fb0 agree) {a0}
+ ≃ agree ∘ ap≃ (wedge-elim-βa cA cB C app fa0 fb0 agree) {b0}
+ wedge-elim-coh cA cB C app {a0}{b0} fa0 fb0 agree =
+ let C' = (λ a b fst (C a b) , raise-level app (snd (C a b)))
in
- λ≃ (\ a ->
- ap≃
- (fst≃
- (ConnectedFib.everywhere m {a0 = a0} cA
- (λ a'
- ConnectedFib.everywhere m {_} {a0} cA
- (λ a1
- Extensions _ _ (fst o C a1) (fb0 a1) ,
- Extensions-level {n} {m} cB b0 (C a1) (fb0 a1))
- (fa0 , agree) a'
- ≃ {!fb0!}
- , path-preserves-level (Extensions-level {n} {m} cB b0 (C _) (fb0 _)))
- {!!} a)))
- {-
- λ≃ (\ a ->
- ConnectedFib.everywhere m {a0 = a0} cA (λ a' → wedge-elim cA cB C app fa0 fb0 agree a' b0 ≃ fb0 a' ,
- {!not an m-type!})
- (agree ∘ ap≃ (wedge-elim-βa cA cB C app fa0 fb0 agree)) a)
- -}
- {-
- ext : Extensions _ a0 (λ a → wedge-elim cA cB C app{a0}{b0} fa0 fb0 agree a b0 ≃ fb0 a)
- (agree ∘ ap≃ (wedge-elim-βa cA cB C app fa0 fb0 agree))
- ext = ConnectedFib.everywhere m {a0 = a0} cA
- (λ a →
- Extensions _ a0
- (λ a' →
- wedge-elim cA cB C app {a0} {b0} fa0 fb0 agree a' b0 ≃ fb0 a')
- (agree ∘ ap≃ (wedge-elim-βa cA cB C app fa0 fb0 agree))
- , {!!})
- {!!} {!a!}
- -}
-
---
+ ap≃ (wedge-elim-βb cA cB C app fa0 fb0 agree) {a0} ≃〈 Π≃β (\ a -> snd (wedge-elim' cA cB (λ a b fst (C a b) , raise-level app (snd (C a b))) fa0 fb0 agree a)) 〉
+ snd (wedge-elim' cA cB (λ a b fst (C a b) , raise-level app (snd (C a b))) fa0 fb0 agree a0) ≃〈 id 〉
+ snd (ConnectedFib.everywhere _ {_} {a0} cA
+ (λ a' Extensions _ b0 (λ b fst (C' a' b)) (fb0 a') ,
+ Extensions-level cB b0 (C' a') (fb0 a'))
+ (fa0 , agree) a0) ≃〈 snd≃⁻
+ (ConnectedFib.β _ cA
+ (λ a'
+ Extensions _ _ (fst o C' a') (fb0 a') ,
+ Extensions-level cB b0 (C' a') (fb0 a'))
+ (fa0 , agree)) 〉
+ transport (λ f f b0 ≃ fb0 a0)
+ (! (wedge-elim-βa cA cB C app fa0 fb0 agree))
+ agree ≃〈 transport-Path-pre' (λ f f b0) (! (wedge-elim-βa cA cB C app fa0 fb0 agree)) agree 〉
+ agree ∘ ! (ap≃ (! (wedge-elim-βa cA cB C app fa0 fb0 agree)) {b0}) ≃〈 ap (_∘_ agree) (! (ap-! (λ f f b0) (! (wedge-elim-βa cA cB C app fa0 fb0 agree)))) 〉
+ agree ∘ (ap≃ (! (! (wedge-elim-βa cA cB C app fa0 fb0 agree))) {b0}) ≃〈 ap (\ x -> agree ∘ ap≃ x {b0}) (!-invol (wedge-elim-βa cA cB C app fa0 fb0 agree)) 〉
+ (agree ∘ ap≃ (wedge-elim-βa cA cB C app fa0 fb0 agree) {b0} ∎)
wedge-rec : {m n p} {A B C : Type}
-> Connected (S m) A
@@ -298,6 +258,16 @@ module lib.NConnected where
-> (\ a' -> wedge-rec cA cB nC ap fa fb agree a' b) ≃ fb
wedge-rec-βb cA cB nC = wedge-elim-βb cA cB (\ _ _ -> _ , nC)
+ wedge-rec-coh : {m}{n}{p} {A B C : Type}
+ (cA : Connected (S m) A) (cB : Connected (S n) B) (nC : NType p C)
+ (app : p <=tl (plus2 m n)){a0 : A} {b0 : B}
+ -> (fa0 : B C)
+ -> (fb0 : A C)
+ -> (agree : fa0 b0 ≃ fb0 a0)
+ -> ap≃ (wedge-rec-βb cA cB nC app fa0 fb0 agree) {a0}
+ ≃ agree ∘ ap≃ (wedge-rec-βa cA cB nC app fa0 fb0 agree) {b0}
+ wedge-rec-coh cA cB nC = wedge-elim-coh cA cB (\ _ _ -> _ , nC)
+
{-
7 lib/Paths.agda
View
@@ -110,6 +110,13 @@ module lib.Paths where
≃ (b ≃ transport B α b')
move-transport-right-!≃ B id = id
+ move-posto-with-transport-left : {A D : Type} (C : A Type) {M M' : A}
+ (α : M ≃ M')
+ (f : C M D) (g : C M' D)
+ -> f ≃ (g o transport C α)
+ -> (f o transport C (! α)) ≃ g
+ move-posto-with-transport-left C id f g = λ x x
+
cancel-left≃ : {A} {m1 m2 : A}
(q : m1 ≃ m2)
(p : m1 ≃ m1)
10 lib/Prods.agda
View
@@ -51,6 +51,16 @@ module lib.Prods where
Σ≃β2' {p = x , y} {q = .x , .y} id id = id
-}
+ -- subst extension for Γ,x:A⁻ in DTT
+ pair≃⁻ : {A : Set} {B : A -> Set} {p q : Σ B}
+ -> (α : (fst p) ≃ (fst q)) -> (snd p) ≃ transport B (! α) (snd q)
+ -> p ≃ q
+ pair≃⁻ {A}{B}{p}{q} α β =
+ pair≃ α (ap≃ (ap (λ x transport B x) (!-inv-r α) ∘ ! (transport-∘ B α (! α))) ∘ ap (transport B α) β)
+
+ snd≃⁻ : {A : Type} {B : A -> Type} {p q : Σ B} -> (c : p ≃ q) -> (snd p) ≃ transport B (! (fst≃ c)) (snd q)
+ snd≃⁻ {p = p} {q = .p} id = id
+
module ΣPath where
eqv : {A : Type} {B : A Type} {p q : Σ B}
Please sign in to comment.
Something went wrong with that request. Please try again.