more progress
This commit is contained in:
parent
0399dca62a
commit
33c42508ad
2 changed files with 45 additions and 79 deletions
|
@ -114,7 +114,11 @@ composite : {A B C : Set}
|
|||
→ A → C
|
||||
composite f g x = g (f x)
|
||||
|
||||
syntax composite f g = g ∘ f
|
||||
_∘_ : {A B C : Set}
|
||||
→ (g : B → C)
|
||||
→ (f : A → B)
|
||||
→ A → C
|
||||
_∘_ g f x = g (f x)
|
||||
|
||||
composite-assoc : {A B C D : Set}
|
||||
→ (f : A → B)
|
||||
|
|
|
@ -51,89 +51,51 @@ main proof:
|
|||
|
||||
```
|
||||
exercise2∙13 : (𝟚 ≃ 𝟚) ≃ 𝟚
|
||||
exercise2∙13 = aux1 , equiv1
|
||||
exercise2∙13 = f , equiv
|
||||
where
|
||||
aux1 : 𝟚 ≃ 𝟚 → 𝟚
|
||||
aux1 (fst , snd) = fst true
|
||||
|
||||
neg : 𝟚 → 𝟚
|
||||
neg true = false
|
||||
neg false = true
|
||||
|
||||
neg-homotopy : (neg ∘ neg) ∼ id
|
||||
neg-homotopy true = refl
|
||||
neg-homotopy false = refl
|
||||
f : 𝟚 ≃ 𝟚 → 𝟚
|
||||
f (fst , snd) = fst true
|
||||
|
||||
open Σ
|
||||
open isequiv
|
||||
|
||||
rev : 𝟚 → (𝟚 ≃ 𝟚)
|
||||
fst (rev true) = id
|
||||
g (snd (rev true)) = id
|
||||
g-id (snd (rev true)) x = refl
|
||||
h (snd (rev true)) = id
|
||||
h-id (snd (rev true)) x = refl
|
||||
fst (rev false) = neg
|
||||
g (snd (rev false)) = neg
|
||||
g-id (snd (rev false)) = neg-homotopy
|
||||
h (snd (rev false)) = neg
|
||||
h-id (snd (rev false)) = neg-homotopy
|
||||
|
||||
equiv1 : isequiv aux1
|
||||
g equiv1 = rev
|
||||
g-id equiv1 true = refl
|
||||
g-id equiv1 false = refl
|
||||
h equiv1 = rev
|
||||
h-id equiv1 e@(f , f-equiv @ (mkIsEquiv g g-id h h-id)) =
|
||||
-- proving that given any equivalence e, that:
|
||||
-- ((aux1 ∘ rev) e ≡ id e)
|
||||
-- (rev (aux1 e) ≡ e)
|
||||
-- (rev (e.fst true) ≡ e)
|
||||
-- since e is a pair, decompose it using Σ-≡ and prove separately that:
|
||||
-- - fst (rev (e.fst true)) ≡ e.fst
|
||||
-- - left side is a function and right side is a function too
|
||||
-- - use function extensionality to show they behave the same
|
||||
-- - somehow use the fact that e.snd.g-id exists
|
||||
-- - snd (rev (e.fst true)) ≡ e.snd
|
||||
-- test1 : (x : 𝟚) → fst (aux1 x) ≡ f x
|
||||
-- test1 x with x , f true
|
||||
-- test1 _ | true , true = {! !}
|
||||
-- test1 _ | true , false = {! !}
|
||||
-- test1 _ | false , y = {! !}
|
||||
|
||||
-- equiv-funcs : (x : 𝟚) → aux1 x ≡ f x
|
||||
|
||||
-- -- if f mapped everything to the same value, then the inverse couldn't exist
|
||||
-- -- how to state this as a proof?
|
||||
|
||||
-- asdf : (x : 𝟚) → neg (f x) ≡ f (neg x)
|
||||
-- -- known that (f ∘ g) x ≡ x
|
||||
-- -- g (f x) ≡ x
|
||||
-- -- g (f true) ≡ true
|
||||
-- -- maybe a proof by contradiction? suppose f true ≡ f false. why doesn't this work if f ∘ g ∼ id?
|
||||
-- -- how to work backwards from the f ∘ g ∼ id? since we have a value `g-id` of that
|
||||
-- asdf true = {! !}
|
||||
-- asdf false = {! !}
|
||||
|
||||
-- ft = f true
|
||||
-- ff = f false
|
||||
|
||||
-- div : ft ≢ ff
|
||||
-- div p =
|
||||
-- let
|
||||
-- id𝟚 : 𝟚 → 𝟚
|
||||
-- id𝟚 = id
|
||||
|
||||
-- wtf : ft ≡ ff
|
||||
-- wtf = p
|
||||
|
||||
-- wtf2 : g ft ≡ g ff
|
||||
-- wtf2 = ap g wtf
|
||||
|
||||
-- in {! !}
|
||||
-- in Σ-≡ (funext test1 , {! !})
|
||||
{! !}
|
||||
g : 𝟚 → 𝟚 ≃ 𝟚
|
||||
g true = id , mkIsEquiv id (λ _ → refl) id (λ _ → refl)
|
||||
g false = neg , mkIsEquiv neg neg-id neg neg-id
|
||||
where
|
||||
test1 : (x : 𝟚 ≃ 𝟚) → aux1 x ≡ {! !}
|
||||
test1 (x , y) = {! !}
|
||||
neg-id : (neg ∘ neg) ∼ id
|
||||
neg-id true = refl
|
||||
neg-id false = refl
|
||||
|
||||
f∘g∼id : f ∘ g ∼ id
|
||||
f∘g∼id true = refl
|
||||
f∘g∼id false = refl
|
||||
|
||||
g∘f∼id : g ∘ f ∼ id
|
||||
g∘f∼id e' @ (f' , ie' @ (mkIsEquiv g' g-id h' h-id)) = {! !}
|
||||
where
|
||||
f-codomain-is-2 : f' true ≢ f' false
|
||||
f-codomain-is-2 p = {! !}
|
||||
|
||||
f-true-is-true-to-id : f' true ≡ true → f' ≡ id
|
||||
f-true-is-true-to-id p = funext prf
|
||||
where
|
||||
prf : (x : 𝟚) → f' x ≡ id x
|
||||
prf true = p
|
||||
prf false with f' false
|
||||
prf false | true = {! !}
|
||||
prf false | false = refl
|
||||
|
||||
equivPrf' : (x : 𝟚) → Σ.fst (g (f' true)) x ≡ f' x
|
||||
equivPrf' x = {! !}
|
||||
|
||||
equivPrf : Σ.fst (g (f' true)) ≡ f'
|
||||
equivPrf = funext equivPrf'
|
||||
|
||||
attempt : (g ∘ f) e' ≡ id e'
|
||||
attempt = posEqLemma ((g ∘ f) e') (id e') equivPrf
|
||||
|
||||
equiv : isequiv f
|
||||
equiv = mkIsEquiv g f∘g∼id g g∘f∼id
|
||||
```
|
||||
|
|
Loading…
Reference in a new issue