Construct the morphism for equivalence 2
I must still show that they are inverses.
This commit is contained in:
parent
0ced448fa6
commit
e25ef31907
src/Cat
|
@ -327,6 +327,7 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
|
||||||
asTypeIso : TypeIsomorphism (idToIso A B)
|
asTypeIso : TypeIsomorphism (idToIso A B)
|
||||||
asTypeIso = toIso _ _ univalent
|
asTypeIso = toIso _ _ univalent
|
||||||
|
|
||||||
|
-- FIXME Rename
|
||||||
inverse-from-to-iso' : AreInverses (idToIso A B) isoToId
|
inverse-from-to-iso' : AreInverses (idToIso A B) isoToId
|
||||||
inverse-from-to-iso' = snd iso
|
inverse-from-to-iso' = snd iso
|
||||||
|
|
||||||
|
@ -377,6 +378,62 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
|
||||||
where
|
where
|
||||||
lem : p~ <<< p* ≡ identity
|
lem : p~ <<< p* ≡ identity
|
||||||
lem = fst (snd (snd (idToIso _ _ p)))
|
lem = fst (snd (snd (idToIso _ _ p)))
|
||||||
|
module _ {A B X : Object} (iso : A ≅ B) where
|
||||||
|
private
|
||||||
|
p : A ≡ B
|
||||||
|
p = isoToId iso
|
||||||
|
p-dom : Arrow A X ≡ Arrow B X
|
||||||
|
p-dom = cong (λ x → Arrow x X) p
|
||||||
|
p-cod : Arrow X A ≡ Arrow X B
|
||||||
|
p-cod = cong (λ x → Arrow X x) p
|
||||||
|
lem : ∀ {A B} {x : A ≅ B} → idToIso A B (isoToId x) ≡ x
|
||||||
|
lem {x = x} i = snd inverse-from-to-iso' i x
|
||||||
|
|
||||||
|
open Σ iso renaming (fst to ι) using ()
|
||||||
|
open Σ (snd iso) renaming (fst to ι~ ; snd to inv)
|
||||||
|
|
||||||
|
coe-dom : {f : Arrow A X} → coe p-dom f ≡ f <<< ι~
|
||||||
|
coe-dom {f} = begin
|
||||||
|
coe p-dom f
|
||||||
|
≡⟨ 9-1-9 p refl f ⟩
|
||||||
|
fst (idToIso _ _ refl) <<< f <<< fst (snd (idToIso _ _ p))
|
||||||
|
≡⟨ cong (λ φ → φ <<< f <<< fst (snd (idToIso _ _ p))) subst-neutral ⟩
|
||||||
|
identity <<< f <<< fst (snd (idToIso _ _ p))
|
||||||
|
≡⟨ cong (λ φ → identity <<< f <<< φ) (cong (λ x → (fst (snd x))) lem) ⟩
|
||||||
|
identity <<< f <<< ι~
|
||||||
|
≡⟨ cong (_<<< ι~) leftIdentity ⟩
|
||||||
|
f <<< ι~ ∎
|
||||||
|
|
||||||
|
coe-cod : {f : Arrow X A} → coe p-cod f ≡ ι <<< f
|
||||||
|
coe-cod {f} = begin
|
||||||
|
coe p-cod f
|
||||||
|
≡⟨ 9-1-9 refl p f ⟩
|
||||||
|
fst (idToIso _ _ p) <<< f <<< fst (snd (idToIso _ _ refl))
|
||||||
|
≡⟨ cong (λ φ → fst (idToIso _ _ p) <<< f <<< φ) subst-neutral ⟩
|
||||||
|
fst (idToIso _ _ p) <<< f <<< identity
|
||||||
|
≡⟨ cong (λ φ → φ <<< f <<< identity) (cong fst lem) ⟩
|
||||||
|
ι <<< f <<< identity
|
||||||
|
≡⟨ sym isAssociative ⟩
|
||||||
|
ι <<< (f <<< identity)
|
||||||
|
≡⟨ cong (ι <<<_) rightIdentity ⟩
|
||||||
|
ι <<< f ∎
|
||||||
|
|
||||||
|
module _ {f : Arrow A X} {g : Arrow B X} (q : PathP (λ i → p-dom i) f g) where
|
||||||
|
domain-twist : g ≡ f <<< ι~
|
||||||
|
domain-twist = begin
|
||||||
|
g ≡⟨ sym (coe-lem q) ⟩
|
||||||
|
coe p-dom f ≡⟨ coe-dom ⟩
|
||||||
|
f <<< ι~ ∎
|
||||||
|
|
||||||
|
-- This can probably also just be obtained from the above my taking the
|
||||||
|
-- symmetric isomorphism.
|
||||||
|
domain-twist0 : f ≡ g <<< ι
|
||||||
|
domain-twist0 = begin
|
||||||
|
f ≡⟨ sym rightIdentity ⟩
|
||||||
|
f <<< identity ≡⟨ cong (f <<<_) (sym (fst inv)) ⟩
|
||||||
|
f <<< (ι~ <<< ι) ≡⟨ isAssociative ⟩
|
||||||
|
f <<< ι~ <<< ι ≡⟨ cong (_<<< ι) (sym domain-twist) ⟩
|
||||||
|
g <<< ι ∎
|
||||||
|
|
||||||
-- | All projections are propositions.
|
-- | All projections are propositions.
|
||||||
module Propositionality where
|
module Propositionality where
|
||||||
|
|
|
@ -238,7 +238,7 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
|
||||||
-- I have `φ p` in scope, but surely `p` and `x` are the same - though
|
-- I have `φ p` in scope, but surely `p` and `x` are the same - though
|
||||||
-- perhaps not definitonally.
|
-- perhaps not definitonally.
|
||||||
, (λ{ (iso , x) → ℂ.isoToId iso , x})
|
, (λ{ (iso , x) → ℂ.isoToId iso , x})
|
||||||
, funExt (λ{ (p , q , r) → Σ≡ (sym iso-id-inv) (toPathP {A = λ i → {!!}} {!!})})
|
, funExt (λ{ (p , q , r) → Σ≡ (sym iso-id-inv) {!!}})
|
||||||
, funExt (λ x → Σ≡ (sym id-iso-inv) {!!})
|
, funExt (λ x → Σ≡ (sym id-iso-inv) {!!})
|
||||||
step2
|
step2
|
||||||
: Σ (X ℂ.≅ Y) (λ iso
|
: Σ (X ℂ.≅ Y) (λ iso
|
||||||
|
@ -249,55 +249,9 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
|
||||||
)
|
)
|
||||||
≈ ((X , xa , xb) ≅ (Y , ya , yb))
|
≈ ((X , xa , xb) ≅ (Y , ya , yb))
|
||||||
step2
|
step2
|
||||||
= ( λ{ ((f , f~ , inv-f) , p , q)
|
= ( λ{ (iso@(f , f~ , inv-f) , p , q)
|
||||||
→
|
→ ( f , sym (ℂ.domain-twist0 iso p) , sym (ℂ.domain-twist0 iso q))
|
||||||
let
|
, ( f~ , sym (ℂ.domain-twist iso p) , sym (ℂ.domain-twist iso q))
|
||||||
r : X ≡ Y
|
|
||||||
r = ℂ.isoToId (f , f~ , inv-f)
|
|
||||||
r-arrow : (ℂ.Arrow X A) ≡ (ℂ.Arrow Y A)
|
|
||||||
r-arrow i = ℂ.Arrow (r i) A
|
|
||||||
t : coe r-arrow xa ≡ ℂ.identity ℂ.<<< xa ℂ.<<< f~
|
|
||||||
t = {!? ≡ ?!}
|
|
||||||
lem : ∀ {A B} {x : A ℂ.≅ B} → ℂ.idToIso A B (ℂ.isoToId x) ≡ x
|
|
||||||
lem = λ{ {x = x} i → snd ℂ.inverse-from-to-iso' i x}
|
|
||||||
lem' : ∀ {A B} {x : A ≡ B} → ℂ.isoToId (ℂ.idToIso _ _ x) ≡ x
|
|
||||||
lem' = λ{ {x = x} i → fst ℂ.inverse-from-to-iso' i x}
|
|
||||||
h : ya ≡ xa ℂ.<<< f~
|
|
||||||
h = begin
|
|
||||||
ya ≡⟨ sym (coe-lem p) ⟩
|
|
||||||
coe r-arrow xa
|
|
||||||
≡⟨ ℂ.9-1-9 r refl xa ⟩
|
|
||||||
fst (ℂ.idToIso _ _ refl) ℂ.<<< xa ℂ.<<< fst (snd (ℂ.idToIso _ _ r))
|
|
||||||
≡⟨ cong (λ φ → φ ℂ.<<< xa ℂ.<<< fst (snd (ℂ.idToIso _ _ r))) subst-neutral ⟩
|
|
||||||
ℂ.identity ℂ.<<< xa ℂ.<<< fst (snd (ℂ.idToIso _ _ r))
|
|
||||||
≡⟨ cong (λ φ → ℂ.identity ℂ.<<< xa ℂ.<<< φ) (cong (λ x → (fst (snd x))) lem) ⟩
|
|
||||||
ℂ.identity ℂ.<<< xa ℂ.<<< f~
|
|
||||||
≡⟨ cong (ℂ._<<< f~) ℂ.leftIdentity ⟩
|
|
||||||
xa ℂ.<<< f~ ∎
|
|
||||||
complicated : Y ≡ X
|
|
||||||
complicated = (λ z → sym (ℂ.isoToId (f , f~ , inv-f)) z)
|
|
||||||
in
|
|
||||||
( f , (begin
|
|
||||||
ℂ [ ya ∘ f ] ≡⟨⟩
|
|
||||||
ya ℂ.<<< f ≡⟨ sym ℂ.leftIdentity ⟩
|
|
||||||
ℂ.identity ℂ.<<< (ya ℂ.<<< f)
|
|
||||||
≡⟨ ℂ.isAssociative ⟩
|
|
||||||
ℂ.identity ℂ.<<< ya ℂ.<<< f
|
|
||||||
≡⟨ cong (λ φ → φ ℂ.<<< ya ℂ.<<< f) (sym subst-neutral) ⟩
|
|
||||||
fst (ℂ.idToIso _ _ refl) ℂ.<<< ya ℂ.<<< f
|
|
||||||
≡⟨ cong (λ φ → fst (ℂ.idToIso _ _ refl) ℂ.<<< ya ℂ.<<< φ)
|
|
||||||
(begin
|
|
||||||
f ≡⟨ {!cong (λ x → (fst (snd x))) ((lem {x = f~ , f , swap inv-f}))!} ⟩
|
|
||||||
-- f ≡⟨ cong fst (sym (lem {f , f~ , inv-f})) ⟩
|
|
||||||
-- fst ( ℂ.idToIso X Y ( ℂ.isoToId (f , f~ , inv-f))) ≡⟨ {!fst inv-f!} ⟩
|
|
||||||
fst (snd (ℂ.idToIso Y X (λ z → sym (ℂ.isoToId (f , f~ , inv-f)) z))) ∎)
|
|
||||||
⟩
|
|
||||||
_ ℂ.<<< ya ℂ.<<< fst (snd (ℂ.idToIso _ _ _))
|
|
||||||
≡⟨ sym (ℂ.9-1-9 (sym r) refl ya) ⟩
|
|
||||||
coe (sym r-arrow) ya
|
|
||||||
≡⟨ coe-lem (λ i → p (~ i)) ⟩
|
|
||||||
xa ∎) , {!!})
|
|
||||||
, ( f~ , sym h , {!!})
|
|
||||||
, lemA (fst inv-f)
|
, lemA (fst inv-f)
|
||||||
, lemA (snd inv-f)
|
, lemA (snd inv-f)
|
||||||
}
|
}
|
||||||
|
@ -308,26 +262,26 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
|
||||||
iso = fst f , fst f~ , cong fst inv-f , cong fst inv-f~
|
iso = fst f , fst f~ , cong fst inv-f , cong fst inv-f~
|
||||||
p : X ≡ Y
|
p : X ≡ Y
|
||||||
p = ℂ.isoToId iso
|
p = ℂ.isoToId iso
|
||||||
lem : xa ≡ _
|
pA : ℂ.Arrow X A ≡ ℂ.Arrow Y A
|
||||||
lem = begin
|
pA = cong (λ x → ℂ.Arrow x A) p
|
||||||
xa ≡⟨ sym (fst (snd f)) ⟩
|
pB : ℂ.Arrow X B ≡ ℂ.Arrow Y B
|
||||||
ya ℂ.<<< fst f ≡⟨ sym ℂ.leftIdentity ⟩
|
pB = cong (λ x → ℂ.Arrow x B) p
|
||||||
ℂ.identity ℂ.<<< (ya ℂ.<<< fst f) ≡⟨ ℂ.isAssociative ⟩
|
k0 = begin
|
||||||
ℂ.identity ℂ.<<< ya ℂ.<<< fst f ≡⟨ {!sym (ℂ.9-1-9 ? refl ya)!} ⟩
|
coe pB xb ≡⟨ ℂ.coe-dom iso ⟩
|
||||||
_ ℂ.<<< ya ℂ.<<< _ ≡⟨ sym (ℂ.9-1-9 (sym p) refl ya) ⟩
|
xb ℂ.<<< fst f~ ≡⟨ snd (snd f~) ⟩
|
||||||
coe (λ i → ℂ.Arrow (p (~ i)) A) ya ∎
|
yb ∎
|
||||||
lem0 = begin
|
k1 = begin
|
||||||
xa ≡⟨ {!!} ⟩
|
coe pA xa ≡⟨ ℂ.coe-dom iso ⟩
|
||||||
coe _ xa ≡⟨ {!!} ⟩
|
xa ℂ.<<< fst f~ ≡⟨ fst (snd f~) ⟩
|
||||||
ya ℂ.<<< fst f ∎
|
ya ∎
|
||||||
helper : PathP (λ i → ℂ.Arrow (p i) A) xa ya
|
helper : PathP (λ i → pA i) xa ya
|
||||||
helper = {!snd f!}
|
helper = coe-lem-inv k1
|
||||||
in iso , ? , {!!}})
|
in iso , coe-lem-inv k1 , coe-lem-inv k0})
|
||||||
, record
|
, record
|
||||||
{ fst = funExt (λ x → lemSig
|
{ fst = funExt (λ x → lemSig
|
||||||
(λ x → propSig prop0 (λ _ → prop1))
|
(λ x → propSig prop0 (λ _ → prop1))
|
||||||
_ _
|
_ _
|
||||||
(Σ≡ {!ℂ!} (ℂ.propIsomorphism _ _ _)))
|
(Σ≡ {!!} (ℂ.propIsomorphism _ _ _)))
|
||||||
; snd = funExt (λ{ (f , _) → lemSig propIsomorphism _ _ {!refl!}})
|
; snd = funExt (λ{ (f , _) → lemSig propIsomorphism _ _ {!refl!}})
|
||||||
}
|
}
|
||||||
where
|
where
|
||||||
|
|
Loading…
Reference in a new issue