Make AreInveres an alias for \Sigma
This commit is contained in:
parent
e6a2e3a0f0
commit
1c963db7e6
|
@ -54,30 +54,23 @@ module _ (ℓ : Level) where
|
||||||
module _ (x y : isIso f) where
|
module _ (x y : isIso f) where
|
||||||
module x = Σ x renaming (fst to inverse ; snd to areInverses)
|
module x = Σ x renaming (fst to inverse ; snd to areInverses)
|
||||||
module y = Σ y renaming (fst to inverse ; snd to areInverses)
|
module y = Σ y renaming (fst to inverse ; snd to areInverses)
|
||||||
module xA = AreInverses x.areInverses
|
|
||||||
module yA = AreInverses y.areInverses
|
|
||||||
-- I had a lot of difficulty using the corresponding proof where
|
-- I had a lot of difficulty using the corresponding proof where
|
||||||
-- AreInverses is defined. This is sadly a bit anti-modular. The
|
-- AreInverses is defined. This is sadly a bit anti-modular. The
|
||||||
-- reason for my troubles is probably related to the type of objects
|
-- reason for my troubles is probably related to the type of objects
|
||||||
-- being hSet's rather than sets.
|
-- being hSet's rather than sets.
|
||||||
p : ∀ {f} g → isProp (AreInverses {A = A} {B} f g)
|
p : ∀ {f} g → isProp (AreInverses {A = A} {B} f g)
|
||||||
p {f} g xx yy i = record
|
p {f} g xx yy i = ve-re , re-ve
|
||||||
{ verso-recto = ve-re
|
|
||||||
; recto-verso = re-ve
|
|
||||||
}
|
|
||||||
where
|
where
|
||||||
module xxA = AreInverses xx
|
|
||||||
module yyA = AreInverses yy
|
|
||||||
ve-re : g ∘ f ≡ idFun _
|
ve-re : g ∘ f ≡ idFun _
|
||||||
ve-re = arrowsAreSets {A = hA} {B = hA} _ _ xxA.verso-recto yyA.verso-recto i
|
ve-re = arrowsAreSets {A = hA} {B = hA} _ _ (fst xx) (fst yy) i
|
||||||
re-ve : f ∘ g ≡ idFun _
|
re-ve : f ∘ g ≡ idFun _
|
||||||
re-ve = arrowsAreSets {A = hB} {B = hB} _ _ xxA.recto-verso yyA.recto-verso i
|
re-ve = arrowsAreSets {A = hB} {B = hB} _ _ (snd xx) (snd yy) i
|
||||||
1eq : x.inverse ≡ y.inverse
|
1eq : x.inverse ≡ y.inverse
|
||||||
1eq = begin
|
1eq = begin
|
||||||
x.inverse ≡⟨⟩
|
x.inverse ≡⟨⟩
|
||||||
x.inverse ∘ idFun _ ≡⟨ cong (λ φ → x.inverse ∘ φ) (sym yA.recto-verso) ⟩
|
x.inverse ∘ idFun _ ≡⟨ cong (λ φ → x.inverse ∘ φ) (sym (snd y.areInverses)) ⟩
|
||||||
x.inverse ∘ (f ∘ y.inverse) ≡⟨⟩
|
x.inverse ∘ (f ∘ y.inverse) ≡⟨⟩
|
||||||
(x.inverse ∘ f) ∘ y.inverse ≡⟨ cong (λ φ → φ ∘ y.inverse) xA.verso-recto ⟩
|
(x.inverse ∘ f) ∘ y.inverse ≡⟨ cong (λ φ → φ ∘ y.inverse) (fst x.areInverses) ⟩
|
||||||
idFun _ ∘ y.inverse ≡⟨⟩
|
idFun _ ∘ y.inverse ≡⟨⟩
|
||||||
y.inverse ∎
|
y.inverse ∎
|
||||||
2eq : (λ i → AreInverses f (1eq i)) [ x.areInverses ≡ y.areInverses ]
|
2eq : (λ i → AreInverses f (1eq i)) [ x.areInverses ≡ y.areInverses ]
|
||||||
|
@ -99,10 +92,7 @@ module _ (ℓ : Level) where
|
||||||
re-ve : (e : fst p ≡ fst q) → (f {p} {q} ∘ g {p} {q}) e ≡ e
|
re-ve : (e : fst p ≡ fst q) → (f {p} {q} ∘ g {p} {q}) e ≡ e
|
||||||
re-ve e = refl
|
re-ve e = refl
|
||||||
inv : AreInverses (f {p} {q}) (g {p} {q})
|
inv : AreInverses (f {p} {q}) (g {p} {q})
|
||||||
inv = record
|
inv = funExt ve-re , funExt re-ve
|
||||||
{ verso-recto = funExt ve-re
|
|
||||||
; recto-verso = funExt re-ve
|
|
||||||
}
|
|
||||||
iso : (p ≡ q) ≈ (fst p ≡ fst q)
|
iso : (p ≡ q) ≈ (fst p ≡ fst q)
|
||||||
iso = f , g , inv
|
iso = f , g , inv
|
||||||
|
|
||||||
|
@ -120,11 +110,7 @@ module _ (ℓ : Level) where
|
||||||
ve-re : (x : isIso f) → (obv ∘ inv) x ≡ x
|
ve-re : (x : isIso f) → (obv ∘ inv) x ≡ x
|
||||||
ve-re = inverse-to-from-iso A B sA sB
|
ve-re = inverse-to-from-iso A B sA sB
|
||||||
iso : isEquiv A B f ≈ isIso f
|
iso : isEquiv A B f ≈ isIso f
|
||||||
iso = obv , inv ,
|
iso = obv , inv , funExt re-ve , funExt ve-re
|
||||||
record
|
|
||||||
{ verso-recto = funExt re-ve
|
|
||||||
; recto-verso = funExt ve-re
|
|
||||||
}
|
|
||||||
in fromIsomorphism _ _ iso
|
in fromIsomorphism _ _ iso
|
||||||
|
|
||||||
module _ {hA hB : Object} where
|
module _ {hA hB : Object} where
|
||||||
|
@ -139,20 +125,8 @@ module _ (ℓ : Level) where
|
||||||
step2 : (hA ≡ hB) ≃ (A ≡ B)
|
step2 : (hA ≡ hB) ≃ (A ≡ B)
|
||||||
step2 = lem2 (λ A → isSetIsProp) hA hB
|
step2 = lem2 (λ A → isSetIsProp) hA hB
|
||||||
|
|
||||||
-- Go from an isomorphism on sets to an isomorphism on homotopic sets
|
|
||||||
trivial? : (A ≈ B) ≃ (hA ≅ hB)
|
|
||||||
trivial? = fromIsomorphism _ _ res
|
|
||||||
where
|
|
||||||
fwd : Σ (A → B) isIso → hA ≅ hB
|
|
||||||
fwd (f , g , inv) = f , g , inv.toPair
|
|
||||||
where
|
|
||||||
module inv = AreInverses inv
|
|
||||||
bwd : hA ≅ hB → Σ (A → B) isIso
|
|
||||||
bwd (f , g , x , y) = f , g , record { verso-recto = x ; recto-verso = y }
|
|
||||||
res : Σ (A → B) isIso ≈ (hA ≅ hB)
|
|
||||||
res = fwd , bwd , record { verso-recto = refl ; recto-verso = refl }
|
|
||||||
univ≃ : (hA ≡ hB) ≃ (hA ≅ hB)
|
univ≃ : (hA ≡ hB) ≃ (hA ≅ hB)
|
||||||
univ≃ = step2 ⊙ univalence ⊙ step0 ⊙ trivial?
|
univ≃ = step2 ⊙ univalence ⊙ step0
|
||||||
|
|
||||||
univalent : Univalent
|
univalent : Univalent
|
||||||
univalent = from[Andrea] (λ _ _ → univ≃)
|
univalent = from[Andrea] (λ _ _ → univ≃)
|
||||||
|
|
|
@ -528,7 +528,7 @@ module Opposite {ℓa ℓb : Level} where
|
||||||
k : TypeIsomorphism (ℂ.idToIso A B)
|
k : TypeIsomorphism (ℂ.idToIso A B)
|
||||||
k = toIso _ _ ℂ.univalent
|
k = toIso _ _ ℂ.univalent
|
||||||
open Σ k renaming (fst to η ; snd to inv-η)
|
open Σ k renaming (fst to η ; snd to inv-η)
|
||||||
open AreInverses inv-η
|
open AreInverses {f = ℂ.idToIso A B} {η} inv-η
|
||||||
|
|
||||||
genericly : {ℓa ℓb ℓc : Level} {a : Set ℓa} {b : Set ℓb} {c : Set ℓc}
|
genericly : {ℓa ℓb ℓc : Level} {a : Set ℓa} {b : Set ℓb} {c : Set ℓc}
|
||||||
→ a × b × c → b × a × c
|
→ a × b × c → b × a × c
|
||||||
|
@ -561,13 +561,13 @@ module Opposite {ℓa ℓb : Level} where
|
||||||
inv-ζ : AreInverses (idToIso A B) ζ
|
inv-ζ : AreInverses (idToIso A B) ζ
|
||||||
-- recto-verso : ℂ.idToIso A B <<< f ≡ idFun (A ℂ.≅ B)
|
-- recto-verso : ℂ.idToIso A B <<< f ≡ idFun (A ℂ.≅ B)
|
||||||
inv-ζ = record
|
inv-ζ = record
|
||||||
{ verso-recto = funExt (λ x → begin
|
{ fst = funExt (λ x → begin
|
||||||
(ζ ∘ idToIso A B) x ≡⟨⟩
|
(ζ ∘ idToIso A B) x ≡⟨⟩
|
||||||
(η ∘ shuffle ∘ idToIso A B) x ≡⟨ cong (λ φ → φ x) (cong (λ φ → η ∘ shuffle ∘ φ) (funExt lem)) ⟩
|
(η ∘ shuffle ∘ idToIso A B) x ≡⟨ cong (λ φ → φ x) (cong (λ φ → η ∘ shuffle ∘ φ) (funExt lem)) ⟩
|
||||||
(η ∘ shuffle ∘ shuffle~ ∘ ℂ.idToIso A B) x ≡⟨⟩
|
(η ∘ shuffle ∘ shuffle~ ∘ ℂ.idToIso A B) x ≡⟨⟩
|
||||||
(η ∘ ℂ.idToIso A B) x ≡⟨ (λ i → verso-recto i x) ⟩
|
(η ∘ ℂ.idToIso A B) x ≡⟨ (λ i → verso-recto i x) ⟩
|
||||||
x ∎)
|
x ∎)
|
||||||
; recto-verso = funExt (λ x → begin
|
; snd = funExt (λ x → begin
|
||||||
(idToIso A B ∘ η ∘ shuffle) x ≡⟨ cong (λ φ → φ x) (cong (λ φ → φ ∘ η ∘ shuffle) (funExt lem)) ⟩
|
(idToIso A B ∘ η ∘ shuffle) x ≡⟨ cong (λ φ → φ x) (cong (λ φ → φ ∘ η ∘ shuffle) (funExt lem)) ⟩
|
||||||
(shuffle~ ∘ ℂ.idToIso A B ∘ η ∘ shuffle) x ≡⟨ cong (λ φ → φ x) (cong (λ φ → shuffle~ ∘ φ ∘ shuffle) recto-verso) ⟩
|
(shuffle~ ∘ ℂ.idToIso A B ∘ η ∘ shuffle) x ≡⟨ cong (λ φ → φ x) (cong (λ φ → shuffle~ ∘ φ ∘ shuffle) recto-verso) ⟩
|
||||||
(shuffle~ ∘ shuffle) x ≡⟨⟩
|
(shuffle~ ∘ shuffle) x ≡⟨⟩
|
||||||
|
|
|
@ -205,7 +205,7 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
|
||||||
open import Cat.Equivalence
|
open import Cat.Equivalence
|
||||||
|
|
||||||
Monoidal≅Kleisli : M.Monad ≅ K.Monad
|
Monoidal≅Kleisli : M.Monad ≅ K.Monad
|
||||||
Monoidal≅Kleisli = forth , (back , (record { verso-recto = funExt backeq ; recto-verso = funExt fortheq }))
|
Monoidal≅Kleisli = forth , back , funExt backeq , funExt fortheq
|
||||||
|
|
||||||
Monoidal≃Kleisli : M.Monad ≃ K.Monad
|
Monoidal≃Kleisli : M.Monad ≃ K.Monad
|
||||||
Monoidal≃Kleisli = forth , eqv
|
Monoidal≃Kleisli = forth , eqv
|
||||||
|
|
|
@ -123,7 +123,7 @@ module voe {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
|
||||||
-- | to talk about voevodsky's construction.
|
-- | to talk about voevodsky's construction.
|
||||||
module _ (omap : Omap ℂ ℂ) (pure : {X : Object} → Arrow X (omap X)) where
|
module _ (omap : Omap ℂ ℂ) (pure : {X : Object} → Arrow X (omap X)) where
|
||||||
private
|
private
|
||||||
module E = AreInverses (Monoidal≅Kleisli ℂ .snd .snd)
|
module E = AreInverses {f = (fst (Monoidal≅Kleisli ℂ))} {fst (snd (Monoidal≅Kleisli ℂ))}(Monoidal≅Kleisli ℂ .snd .snd)
|
||||||
|
|
||||||
Monoidal→Kleisli : M.Monad → K.Monad
|
Monoidal→Kleisli : M.Monad → K.Monad
|
||||||
Monoidal→Kleisli = E.obverse
|
Monoidal→Kleisli = E.obverse
|
||||||
|
|
|
@ -184,10 +184,8 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
|
||||||
= (λ p → cong fst p , cong-d (fst ∘ snd) p , cong-d (snd ∘ snd) p)
|
= (λ p → cong fst p , cong-d (fst ∘ snd) p , cong-d (snd ∘ snd) p)
|
||||||
-- , (λ x → λ i → fst x i , (fst (snd x) i) , (snd (snd x) i))
|
-- , (λ x → λ i → fst x i , (fst (snd x) i) , (snd (snd x) i))
|
||||||
, (λ{ (p , q , r) → Σ≡ p λ i → q i , r i})
|
, (λ{ (p , q , r) → Σ≡ p λ i → q i , r i})
|
||||||
, record
|
, funExt (λ{ p → refl})
|
||||||
{ verso-recto = funExt (λ{ p → refl})
|
, funExt (λ{ (p , q , r) → refl})
|
||||||
; recto-verso = funExt (λ{ (p , q , r) → refl})
|
|
||||||
}
|
|
||||||
|
|
||||||
-- Should follow from c being univalent
|
-- Should follow from c being univalent
|
||||||
iso-id-inv : {p : X ≡ Y} → p ≡ ℂ.isoToId (ℂ.idToIso X Y p)
|
iso-id-inv : {p : X ≡ Y} → p ≡ ℂ.isoToId (ℂ.idToIso X Y p)
|
||||||
|
@ -240,11 +238,8 @@ 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})
|
||||||
, record
|
, funExt (λ{ (p , q , r) → Σ≡ (sym iso-id-inv) (toPathP {A = λ i → {!!}} {!!})})
|
||||||
{ verso-recto = funExt (λ{ (p , q , r) → Σ≡ (sym iso-id-inv) (toPathP {A = λ i → {!!}} {!!})})
|
, funExt (λ x → Σ≡ (sym id-iso-inv) {!!})
|
||||||
-- { verso-recto = funExt (λ{ (p , q , r) → Σ≡ (sym iso-id-inv) {!!}})
|
|
||||||
; recto-verso = funExt (λ x → Σ≡ (sym id-iso-inv) {!!})
|
|
||||||
}
|
|
||||||
step2
|
step2
|
||||||
: Σ (X ℂ.≅ Y) (λ iso
|
: Σ (X ℂ.≅ Y) (λ iso
|
||||||
→ let p = ℂ.isoToId iso
|
→ let p = ℂ.isoToId iso
|
||||||
|
@ -270,11 +265,11 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
|
||||||
helper = {!!}
|
helper = {!!}
|
||||||
in iso , helper , {!!}})
|
in iso , helper , {!!}})
|
||||||
, record
|
, record
|
||||||
{ verso-recto = funExt (λ x → lemSig
|
{ fst = funExt (λ x → lemSig
|
||||||
(λ x → propSig prop0 (λ _ → prop1))
|
(λ x → propSig prop0 (λ _ → prop1))
|
||||||
_ _
|
_ _
|
||||||
(Σ≡ {!!} (ℂ.propIsomorphism _ _ _)))
|
(Σ≡ {!!} (ℂ.propIsomorphism _ _ _)))
|
||||||
; recto-verso = funExt (λ{ (f , _) → lemSig propIsomorphism _ _ {!refl!}})
|
; snd = funExt (λ{ (f , _) → lemSig propIsomorphism _ _ {!refl!}})
|
||||||
}
|
}
|
||||||
where
|
where
|
||||||
prop0 : ∀ {x} → isProp (PathP (λ i → ℂ.Arrow (ℂ.isoToId x i) A) xa ya)
|
prop0 : ∀ {x} → isProp (PathP (λ i → ℂ.Arrow (ℂ.isoToId x i) A) xa ya)
|
||||||
|
@ -386,10 +381,7 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
|
||||||
RawProduct.fst (e i) = p.fst
|
RawProduct.fst (e i) = p.fst
|
||||||
RawProduct.snd (e i) = p.snd
|
RawProduct.snd (e i) = p.snd
|
||||||
inv : AreInverses f g
|
inv : AreInverses f g
|
||||||
inv = record
|
inv = funExt ve-re , funExt re-ve
|
||||||
{ verso-recto = funExt ve-re
|
|
||||||
; recto-verso = funExt re-ve
|
|
||||||
}
|
|
||||||
|
|
||||||
propProduct : isProp (Product ℂ A B)
|
propProduct : isProp (Product ℂ A B)
|
||||||
propProduct = equivPreservesNType {n = ⟨-1⟩} lemma Propositionality.propTerminal
|
propProduct = equivPreservesNType {n = ⟨-1⟩} lemma Propositionality.propTerminal
|
||||||
|
|
|
@ -31,10 +31,12 @@ module _ {ℓa ℓb : Level} where
|
||||||
module _ {A : Set ℓa} {B : Set ℓb} where
|
module _ {A : Set ℓa} {B : Set ℓb} where
|
||||||
-- Quasi-inverse in [HoTT] §2.4.6
|
-- Quasi-inverse in [HoTT] §2.4.6
|
||||||
-- FIXME Maybe rename?
|
-- FIXME Maybe rename?
|
||||||
record AreInverses (f : A → B) (g : B → A) : Set ℓ where
|
AreInverses : (f : A → B) (g : B → A) → Set ℓ
|
||||||
field
|
AreInverses f g = g ∘ f ≡ idFun A × f ∘ g ≡ idFun B
|
||||||
verso-recto : g ∘ f ≡ idFun A
|
|
||||||
recto-verso : f ∘ g ≡ idFun B
|
module AreInverses {f : A → B} {g : B → A}
|
||||||
|
(inv : AreInverses f g) where
|
||||||
|
open Σ inv renaming (fst to verso-recto ; snd to recto-verso) public
|
||||||
obverse = f
|
obverse = f
|
||||||
reverse = g
|
reverse = g
|
||||||
inverse = reverse
|
inverse = reverse
|
||||||
|
@ -49,10 +51,7 @@ module _ {ℓa ℓb : Level} where
|
||||||
× (f ∘ g) ≡ idFun B) where
|
× (f ∘ g) ≡ idFun B) where
|
||||||
open Σ inv renaming (fst to ve-re ; snd to re-ve)
|
open Σ inv renaming (fst to ve-re ; snd to re-ve)
|
||||||
toAreInverses : AreInverses f g
|
toAreInverses : AreInverses f g
|
||||||
toAreInverses = record
|
toAreInverses = ve-re , re-ve
|
||||||
{ verso-recto = ve-re
|
|
||||||
; recto-verso = re-ve
|
|
||||||
}
|
|
||||||
|
|
||||||
_≅_ : Set ℓa → Set ℓb → Set _
|
_≅_ : Set ℓa → Set ℓb → Set _
|
||||||
A ≅ B = Σ (A → B) Isomorphism
|
A ≅ B = Σ (A → B) Isomorphism
|
||||||
|
@ -61,16 +60,12 @@ module _ {ℓ : Level} {A B : Set ℓ} {f : A → B}
|
||||||
(g : B → A) (s : {A B : Set ℓ} → isSet (A → B)) where
|
(g : B → A) (s : {A B : Set ℓ} → isSet (A → B)) where
|
||||||
|
|
||||||
propAreInverses : isProp (AreInverses {A = A} {B} f g)
|
propAreInverses : isProp (AreInverses {A = A} {B} f g)
|
||||||
propAreInverses x y i = record
|
propAreInverses x y i = ve-re , re-ve
|
||||||
{ verso-recto = ve-re
|
|
||||||
; recto-verso = re-ve
|
|
||||||
}
|
|
||||||
where
|
where
|
||||||
open AreInverses
|
|
||||||
ve-re : g ∘ f ≡ idFun A
|
ve-re : g ∘ f ≡ idFun A
|
||||||
ve-re = s (g ∘ f) (idFun A) (verso-recto x) (verso-recto y) i
|
ve-re = s (g ∘ f) (idFun A) (fst x) (fst y) i
|
||||||
re-ve : f ∘ g ≡ idFun B
|
re-ve : f ∘ g ≡ idFun B
|
||||||
re-ve = s (f ∘ g) (idFun B) (recto-verso x) (recto-verso y) i
|
re-ve = s (f ∘ g) (idFun B) (snd x) (snd y) i
|
||||||
|
|
||||||
module _ {ℓ : Level} {A B : Set ℓ} (f : A → B)
|
module _ {ℓ : Level} {A B : Set ℓ} (f : A → B)
|
||||||
(sA : isSet A) (sB : isSet B) where
|
(sA : isSet A) (sB : isSet B) where
|
||||||
|
@ -81,20 +76,17 @@ module _ {ℓ : Level} {A B : Set ℓ} (f : A → B)
|
||||||
module _ (x y : Isomorphism f) where
|
module _ (x y : Isomorphism f) where
|
||||||
module x = Σ x renaming (fst to inverse ; snd to areInverses)
|
module x = Σ x renaming (fst to inverse ; snd to areInverses)
|
||||||
module y = Σ y renaming (fst to inverse ; snd to areInverses)
|
module y = Σ y renaming (fst to inverse ; snd to areInverses)
|
||||||
module xA = AreInverses x.areInverses
|
module xA = AreInverses {f = f} {x.inverse} x.areInverses
|
||||||
module yA = AreInverses y.areInverses
|
module yA = AreInverses {f = f} {y.inverse} y.areInverses
|
||||||
-- I had a lot of difficulty using the corresponding proof where
|
-- I had a lot of difficulty using the corresponding proof where
|
||||||
-- AreInverses is defined. This is sadly a bit anti-modular. The
|
-- AreInverses is defined. This is sadly a bit anti-modular. The
|
||||||
-- reason for my troubles is probably related to the type of objects
|
-- reason for my troubles is probably related to the type of objects
|
||||||
-- being hSet's rather than sets.
|
-- being hSet's rather than sets.
|
||||||
p : ∀ {f} g → isProp (AreInverses {A = A} {B} f g)
|
p : ∀ {f} g → isProp (AreInverses {A = A} {B} f g)
|
||||||
p {f} g xx yy i = record
|
p {f} g xx yy i = ve-re , re-ve
|
||||||
{ verso-recto = ve-re
|
|
||||||
; recto-verso = re-ve
|
|
||||||
}
|
|
||||||
where
|
where
|
||||||
module xxA = AreInverses xx
|
module xxA = AreInverses {f = f} {g} xx
|
||||||
module yyA = AreInverses yy
|
module yyA = AreInverses {f = f} {g} yy
|
||||||
setPiB : ∀ {X : Set ℓ} → isSet (X → B)
|
setPiB : ∀ {X : Set ℓ} → isSet (X → B)
|
||||||
setPiB = setPi (λ _ → sB)
|
setPiB = setPi (λ _ → sB)
|
||||||
setPiA : ∀ {X : Set ℓ} → isSet (X → A)
|
setPiA : ∀ {X : Set ℓ} → isSet (X → A)
|
||||||
|
@ -141,33 +133,29 @@ module _ {ℓa ℓb ℓ : Level} (A : Set ℓa) (B : Set ℓb) where
|
||||||
module _ (iso-x iso-y : Isomorphism f) where
|
module _ (iso-x iso-y : Isomorphism f) where
|
||||||
open Σ iso-x renaming (fst to x ; snd to inv-x)
|
open Σ iso-x renaming (fst to x ; snd to inv-x)
|
||||||
open Σ iso-y renaming (fst to y ; snd to inv-y)
|
open Σ iso-y renaming (fst to y ; snd to inv-y)
|
||||||
module inv-x = AreInverses inv-x
|
|
||||||
module inv-y = AreInverses inv-y
|
|
||||||
|
|
||||||
fx≡fy : x ≡ y
|
fx≡fy : x ≡ y
|
||||||
fx≡fy = begin
|
fx≡fy = begin
|
||||||
x ≡⟨ cong (λ φ → x ∘ φ) (sym inv-y.recto-verso) ⟩
|
x ≡⟨ cong (λ φ → x ∘ φ) (sym (snd inv-y)) ⟩
|
||||||
x ∘ (f ∘ y) ≡⟨⟩
|
x ∘ (f ∘ y) ≡⟨⟩
|
||||||
(x ∘ f) ∘ y ≡⟨ cong (λ φ → φ ∘ y) inv-x.verso-recto ⟩
|
(x ∘ f) ∘ y ≡⟨ cong (λ φ → φ ∘ y) (fst inv-x) ⟩
|
||||||
y ∎
|
y ∎
|
||||||
|
|
||||||
propInv : ∀ g → isProp (AreInverses f g)
|
propInv : ∀ g → isProp (AreInverses f g)
|
||||||
propInv g t u i = record { verso-recto = a i ; recto-verso = b i }
|
propInv g t u i = a i , b i
|
||||||
where
|
where
|
||||||
module t = AreInverses t
|
a : (fst t) ≡ (fst u)
|
||||||
module u = AreInverses u
|
|
||||||
a : t.verso-recto ≡ u.verso-recto
|
|
||||||
a i = h
|
a i = h
|
||||||
where
|
where
|
||||||
hh : ∀ a → (g ∘ f) a ≡ a
|
hh : ∀ a → (g ∘ f) a ≡ a
|
||||||
hh a = sA ((g ∘ f) a) a (λ i → t.verso-recto i a) (λ i → u.verso-recto i a) i
|
hh a = sA ((g ∘ f) a) a (λ i → (fst t) i a) (λ i → (fst u) i a) i
|
||||||
h : g ∘ f ≡ idFun A
|
h : g ∘ f ≡ idFun A
|
||||||
h i a = hh a i
|
h i a = hh a i
|
||||||
b : t.recto-verso ≡ u.recto-verso
|
b : (snd t) ≡ (snd u)
|
||||||
b i = h
|
b i = h
|
||||||
where
|
where
|
||||||
hh : ∀ b → (f ∘ g) b ≡ b
|
hh : ∀ b → (f ∘ g) b ≡ b
|
||||||
hh b = sB _ _ (λ i → t.recto-verso i b) (λ i → u.recto-verso i b) i
|
hh b = sB _ _ (λ i → snd t i b) (λ i → snd u i b) i
|
||||||
h : f ∘ g ≡ idFun B
|
h : f ∘ g ≡ idFun B
|
||||||
h i b = hh b i
|
h i b = hh b i
|
||||||
|
|
||||||
|
@ -201,10 +189,7 @@ module _ {ℓa ℓb : Level} (A : Set ℓa) (B : Set ℓb) where
|
||||||
reverse = inverse
|
reverse = inverse
|
||||||
|
|
||||||
areInverses : AreInverses obverse inverse
|
areInverses : AreInverses obverse inverse
|
||||||
areInverses = record
|
areInverses = funExt verso-recto , funExt recto-verso
|
||||||
{ verso-recto = funExt verso-recto
|
|
||||||
; recto-verso = funExt recto-verso
|
|
||||||
}
|
|
||||||
where
|
where
|
||||||
recto-verso : ∀ b → (obverse ∘ inverse) b ≡ b
|
recto-verso : ∀ b → (obverse ∘ inverse) b ≡ b
|
||||||
recto-verso b = begin
|
recto-verso b = begin
|
||||||
|
@ -245,11 +230,10 @@ module _ {ℓa ℓb : Level} (A : Set ℓa) (B : Set ℓb) where
|
||||||
≃isEquiv : Equiv A B (isEquiv A B)
|
≃isEquiv : Equiv A B (isEquiv A B)
|
||||||
Equiv.fromIso ≃isEquiv {f} (f~ , iso) = gradLemma f f~ rv vr
|
Equiv.fromIso ≃isEquiv {f} (f~ , iso) = gradLemma f f~ rv vr
|
||||||
where
|
where
|
||||||
open AreInverses iso
|
|
||||||
rv : (b : B) → _ ≡ b
|
rv : (b : B) → _ ≡ b
|
||||||
rv b i = recto-verso i b
|
rv b i = snd iso i b
|
||||||
vr : (a : A) → _ ≡ a
|
vr : (a : A) → _ ≡ a
|
||||||
vr a i = verso-recto i a
|
vr a i = fst iso i a
|
||||||
Equiv.toIso ≃isEquiv = toIsomorphism
|
Equiv.toIso ≃isEquiv = toIsomorphism
|
||||||
Equiv.propIsEquiv ≃isEquiv = P.propIsEquiv
|
Equiv.propIsEquiv ≃isEquiv = P.propIsEquiv
|
||||||
where
|
where
|
||||||
|
@ -266,21 +250,19 @@ module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where
|
||||||
composeIsomorphism a b = f~ ∘ g~ , inv
|
composeIsomorphism a b = f~ ∘ g~ , inv
|
||||||
where
|
where
|
||||||
open Σ a renaming (fst to f~ ; snd to inv-a)
|
open Σ a renaming (fst to f~ ; snd to inv-a)
|
||||||
module A = AreInverses inv-a
|
|
||||||
open Σ b renaming (fst to g~ ; snd to inv-b)
|
open Σ b renaming (fst to g~ ; snd to inv-b)
|
||||||
module B = AreInverses inv-b
|
|
||||||
inv : AreInverses (g ∘ f) (f~ ∘ g~)
|
inv : AreInverses (g ∘ f) (f~ ∘ g~)
|
||||||
inv = record
|
inv = record
|
||||||
{ verso-recto = begin
|
{ fst = begin
|
||||||
(f~ ∘ g~) ∘ (g ∘ f) ≡⟨⟩
|
(f~ ∘ g~) ∘ (g ∘ f) ≡⟨⟩
|
||||||
f~ ∘ (g~ ∘ g) ∘ f ≡⟨ cong (λ φ → f~ ∘ φ ∘ f) B.verso-recto ⟩
|
f~ ∘ (g~ ∘ g) ∘ f ≡⟨ cong (λ φ → f~ ∘ φ ∘ f) (fst inv-b) ⟩
|
||||||
f~ ∘ idFun _ ∘ f ≡⟨⟩
|
f~ ∘ idFun _ ∘ f ≡⟨⟩
|
||||||
f~ ∘ f ≡⟨ A.verso-recto ⟩
|
f~ ∘ f ≡⟨ (fst inv-a) ⟩
|
||||||
idFun A ∎
|
idFun A ∎
|
||||||
; recto-verso = begin
|
; snd = begin
|
||||||
(g ∘ f) ∘ (f~ ∘ g~) ≡⟨⟩
|
(g ∘ f) ∘ (f~ ∘ g~) ≡⟨⟩
|
||||||
g ∘ (f ∘ f~) ∘ g~ ≡⟨ cong (λ φ → g ∘ φ ∘ g~) A.recto-verso ⟩
|
g ∘ (f ∘ f~) ∘ g~ ≡⟨ cong (λ φ → g ∘ φ ∘ g~) (snd inv-a) ⟩
|
||||||
g ∘ g~ ≡⟨ B.recto-verso ⟩
|
g ∘ g~ ≡⟨ (snd inv-b) ⟩
|
||||||
idFun C ∎
|
idFun C ∎
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -299,7 +281,7 @@ module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where
|
||||||
iso : Isomorphism (fst e)
|
iso : Isomorphism (fst e)
|
||||||
iso = snd (toIsomorphism _ _ e)
|
iso = snd (toIsomorphism _ _ e)
|
||||||
|
|
||||||
open AreInverses (snd iso) public
|
open AreInverses {f = fst e} {fst iso} (snd iso) public
|
||||||
|
|
||||||
compose : {ℓc : Level} {C : Set ℓc} → (B ≃ C) → A ≃ C
|
compose : {ℓc : Level} {C : Set ℓc} → (B ≃ C) → A ≃ C
|
||||||
compose (f , isEquiv) = f ∘ obverse , composeIsEquiv (snd e) isEquiv
|
compose (f , isEquiv) = f ∘ obverse , composeIsEquiv (snd e) isEquiv
|
||||||
|
@ -308,10 +290,8 @@ module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where
|
||||||
symmetryIso
|
symmetryIso
|
||||||
= inverse
|
= inverse
|
||||||
, obverse
|
, obverse
|
||||||
, record
|
, recto-verso
|
||||||
{ verso-recto = recto-verso
|
, verso-recto
|
||||||
; recto-verso = verso-recto
|
|
||||||
}
|
|
||||||
|
|
||||||
symmetry : B ≃ A
|
symmetry : B ≃ A
|
||||||
symmetry = fromIsomorphism _ _ symmetryIso
|
symmetry = fromIsomorphism _ _ symmetryIso
|
||||||
|
@ -325,13 +305,43 @@ preorder≅ ℓ = record
|
||||||
→ coe p
|
→ coe p
|
||||||
, coe (sym p)
|
, coe (sym p)
|
||||||
-- I believe I stashed the proof of this somewhere.
|
-- I believe I stashed the proof of this somewhere.
|
||||||
, record
|
, funExt (λ x → inv-coe p)
|
||||||
{ verso-recto = {!refl!}
|
, funExt (λ x → inv-coe' p)
|
||||||
; recto-verso = {!!}
|
|
||||||
}
|
|
||||||
; trans = composeIso
|
; trans = composeIso
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
where
|
||||||
|
module _ {ℓ : Level} {A : Set ℓ} {a : A} where
|
||||||
|
id-coe : coe refl a ≡ a
|
||||||
|
id-coe = begin
|
||||||
|
coe refl a ≡⟨⟩
|
||||||
|
pathJ (λ y x → A) _ A refl ≡⟨ pathJprop {x = a} (λ y x → A) _ ⟩
|
||||||
|
_ ≡⟨ pathJprop {x = a} (λ y x → A) _ ⟩
|
||||||
|
a ∎
|
||||||
|
|
||||||
|
module _ {ℓ : Level} {A B : Set ℓ} {a : A} where
|
||||||
|
inv-coe : (p : A ≡ B) → coe (sym p) (coe p a) ≡ a
|
||||||
|
inv-coe p =
|
||||||
|
let
|
||||||
|
D : (y : Set ℓ) → _ ≡ y → Set _
|
||||||
|
D _ q = coe (sym q) (coe q a) ≡ a
|
||||||
|
d : D A refl
|
||||||
|
d = begin
|
||||||
|
coe (sym refl) (coe refl a) ≡⟨⟩
|
||||||
|
coe refl (coe refl a) ≡⟨ id-coe ⟩
|
||||||
|
coe refl a ≡⟨ id-coe ⟩
|
||||||
|
a ∎
|
||||||
|
in pathJ D d B p
|
||||||
|
inv-coe' : (p : B ≡ A) → coe p (coe (sym p) a) ≡ a
|
||||||
|
inv-coe' p =
|
||||||
|
let
|
||||||
|
D : (y : Set ℓ) → _ ≡ y → Set _
|
||||||
|
D _ q = coe (sym q) (coe q a) ≡ a
|
||||||
|
k : coe p (coe (sym p) a) ≡ a
|
||||||
|
k = pathJ D (trans id-coe id-coe) B (sym p)
|
||||||
|
in k
|
||||||
|
|
||||||
|
|
||||||
module _ {ℓ : Level} {A B : Set ℓ} where
|
module _ {ℓ : Level} {A B : Set ℓ} where
|
||||||
univalence : (A ≡ B) ≃ (A ≃ B)
|
univalence : (A ≡ B) ≃ (A ≃ B)
|
||||||
univalence = Equivalence.compose u' aux
|
univalence = Equivalence.compose u' aux
|
||||||
|
@ -341,7 +351,7 @@ module _ {ℓ : Level} {A B : Set ℓ} where
|
||||||
u' : (A ≡ B) ≃ (A U.≃ B)
|
u' : (A ≡ B) ≃ (A U.≃ B)
|
||||||
u' = doEta u
|
u' = doEta u
|
||||||
aux : (A U.≃ B) ≃ (A ≃ B)
|
aux : (A U.≃ B) ≃ (A ≃ B)
|
||||||
aux = fromIsomorphism _ _ (doEta , deEta , record { verso-recto = funExt (λ{ (U.con _ _) → refl}) ; recto-verso = refl })
|
aux = fromIsomorphism _ _ (doEta , deEta , funExt (λ{ (U.con _ _) → refl}) , refl)
|
||||||
|
|
||||||
-- A few results that I have not generalized to work with both the eta and no-eta variable of ≃
|
-- A few results that I have not generalized to work with both the eta and no-eta variable of ≃
|
||||||
module _ {ℓa ℓb : Level} {A : Set ℓa} {P : A → Set ℓb} where
|
module _ {ℓa ℓb : Level} {A : Set ℓa} {P : A → Set ℓb} where
|
||||||
|
@ -361,10 +371,7 @@ module _ {ℓa ℓb : Level} {A : Set ℓa} {P : A → Set ℓb} where
|
||||||
re-ve : (e : fst p ≡ fst q) → (f {p} {q} ∘ g {p} {q}) e ≡ e
|
re-ve : (e : fst p ≡ fst q) → (f {p} {q} ∘ g {p} {q}) e ≡ e
|
||||||
re-ve e = refl
|
re-ve e = refl
|
||||||
inv : AreInverses (f {p} {q}) (g {p} {q})
|
inv : AreInverses (f {p} {q}) (g {p} {q})
|
||||||
inv = record
|
inv = funExt ve-re , funExt re-ve
|
||||||
{ verso-recto = funExt ve-re
|
|
||||||
; recto-verso = funExt re-ve
|
|
||||||
}
|
|
||||||
iso : (p ≡ q) ≅ (fst p ≡ fst q)
|
iso : (p ≡ q) ≅ (fst p ≡ fst q)
|
||||||
iso = f , g , inv
|
iso = f , g , inv
|
||||||
|
|
||||||
|
@ -396,28 +403,22 @@ module _ {ℓa ℓb : Level} {A : Set ℓa} {P : A → Set ℓb} where
|
||||||
k : Isomorphism _
|
k : Isomorphism _
|
||||||
k = toIso _ _ (snd (eA a))
|
k = toIso _ _ (snd (eA a))
|
||||||
open Σ k renaming (fst to g' ; snd to inv)
|
open Σ k renaming (fst to g' ; snd to inv)
|
||||||
module A = AreInverses inv
|
|
||||||
-- anti-funExt
|
|
||||||
lem : (g' ∘ (fst (eA a))) pA ≡ pA
|
lem : (g' ∘ (fst (eA a))) pA ≡ pA
|
||||||
lem i = A.verso-recto i pA
|
lem i = fst inv i pA
|
||||||
re-ve : (x : Σ A Q) → (f ∘ g) x ≡ x
|
re-ve : (x : Σ A Q) → (f ∘ g) x ≡ x
|
||||||
re-ve x i = fst x , eq i
|
re-ve x i = fst x , eq i
|
||||||
where
|
where
|
||||||
open Σ x renaming (fst to a ; snd to qA)
|
open Σ x renaming (fst to a ; snd to qA)
|
||||||
eq = begin
|
eq = begin
|
||||||
snd ((f ∘ g) x) ≡⟨⟩
|
snd ((f ∘ g) x) ≡⟨⟩
|
||||||
fst (eA a) (g' qA) ≡⟨ (λ i → A.recto-verso i qA) ⟩
|
fst (eA a) (g' qA) ≡⟨ (λ i → snd inv i qA) ⟩
|
||||||
qA ∎
|
qA ∎
|
||||||
where
|
where
|
||||||
k : Isomorphism _
|
k : Isomorphism _
|
||||||
k = toIso _ _ (snd (eA a))
|
k = toIso _ _ (snd (eA a))
|
||||||
open Σ k renaming (fst to g' ; snd to inv)
|
open Σ k renaming (fst to g' ; snd to inv)
|
||||||
module A = AreInverses inv
|
|
||||||
inv : AreInverses f g
|
inv : AreInverses f g
|
||||||
inv = record
|
inv = funExt ve-re , funExt re-ve
|
||||||
{ verso-recto = funExt ve-re
|
|
||||||
; recto-verso = funExt re-ve
|
|
||||||
}
|
|
||||||
iso : Σ A P ≅ Σ A Q
|
iso : Σ A P ≅ Σ A Q
|
||||||
iso = f , g , inv
|
iso = f , g , inv
|
||||||
res : Σ A P ≃ Σ A Q
|
res : Σ A P ≃ Σ A Q
|
||||||
|
@ -439,11 +440,7 @@ module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where
|
||||||
ve-re : (x : Isomorphism f) → (obv ∘ inv) x ≡ x
|
ve-re : (x : Isomorphism f) → (obv ∘ inv) x ≡ x
|
||||||
ve-re = inverse-to-from-iso A B sA sB
|
ve-re = inverse-to-from-iso A B sA sB
|
||||||
iso : isEquiv A B f ≅ Isomorphism f
|
iso : isEquiv A B f ≅ Isomorphism f
|
||||||
iso = obv , inv ,
|
iso = obv , inv , funExt re-ve , funExt ve-re
|
||||||
record
|
|
||||||
{ verso-recto = funExt re-ve
|
|
||||||
; recto-verso = funExt ve-re
|
|
||||||
}
|
|
||||||
in fromIsomorphism _ _ iso
|
in fromIsomorphism _ _ iso
|
||||||
|
|
||||||
module _ {ℓa ℓb : Level} {A : Set ℓa} {P : A → Set ℓb} where
|
module _ {ℓa ℓb : Level} {A : Set ℓa} {P : A → Set ℓb} where
|
||||||
|
@ -473,28 +470,23 @@ module _ {ℓa ℓb : Level} {A : Set ℓa} {P : A → Set ℓb} where
|
||||||
k : Isomorphism _
|
k : Isomorphism _
|
||||||
k = toIso _ _ (snd (eA a))
|
k = toIso _ _ (snd (eA a))
|
||||||
open Σ k renaming (fst to g' ; snd to inv)
|
open Σ k renaming (fst to g' ; snd to inv)
|
||||||
module A = AreInverses inv
|
|
||||||
-- anti-funExt
|
-- anti-funExt
|
||||||
lem : (g' ∘ (fst (eA a))) pA ≡ pA
|
lem : (g' ∘ (fst (eA a))) pA ≡ pA
|
||||||
lem i = A.verso-recto i pA
|
lem i = fst inv i pA
|
||||||
re-ve : (x : Σ A Q) → (f ∘ g) x ≡ x
|
re-ve : (x : Σ A Q) → (f ∘ g) x ≡ x
|
||||||
re-ve x i = fst x , eq i
|
re-ve x i = fst x , eq i
|
||||||
where
|
where
|
||||||
open Σ x renaming (fst to a ; snd to qA)
|
open Σ x renaming (fst to a ; snd to qA)
|
||||||
eq = begin
|
eq = begin
|
||||||
snd ((f ∘ g) x) ≡⟨⟩
|
snd ((f ∘ g) x) ≡⟨⟩
|
||||||
fst (eA a) (g' qA) ≡⟨ (λ i → A.recto-verso i qA) ⟩
|
fst (eA a) (g' qA) ≡⟨ (λ i → snd inv i qA) ⟩
|
||||||
qA ∎
|
qA ∎
|
||||||
where
|
where
|
||||||
k : Isomorphism _
|
k : Isomorphism _
|
||||||
k = toIso _ _ (snd (eA a))
|
k = toIso _ _ (snd (eA a))
|
||||||
open Σ k renaming (fst to g' ; snd to inv)
|
open Σ k renaming (fst to g' ; snd to inv)
|
||||||
module A = AreInverses inv
|
|
||||||
inv : AreInverses f g
|
inv : AreInverses f g
|
||||||
inv = record
|
inv = funExt ve-re , funExt re-ve
|
||||||
{ verso-recto = funExt ve-re
|
|
||||||
; recto-verso = funExt re-ve
|
|
||||||
}
|
|
||||||
iso : Σ A P ≅ Σ A Q
|
iso : Σ A P ≅ Σ A Q
|
||||||
iso = f , g , inv
|
iso = f , g , inv
|
||||||
res : Σ A P ≃ Σ A Q
|
res : Σ A P ≃ Σ A Q
|
||||||
|
|
Loading…
Reference in a new issue