Move lemmas about equivalences to that module
This commit is contained in:
parent
313c7593d1
commit
aa52bc8f07
|
|
@ -42,91 +42,16 @@ module _ (ℓ : Level) where
|
|||
IsPreCategory.isIdentity isPreCat {A} {B} = isIdentity {A} {B}
|
||||
IsPreCategory.arrowsAreSets isPreCat {A} {B} = arrowsAreSets {A} {B}
|
||||
|
||||
open IsPreCategory isPreCat hiding (_<<<_)
|
||||
|
||||
isIso = TypeIsomorphism
|
||||
module _ {hA hB : hSet ℓ} where
|
||||
open Σ hA renaming (fst to A ; snd to sA)
|
||||
open Σ hB renaming (fst to B ; snd to sB)
|
||||
lem1 : (f : A → B) → isSet A → isSet B → isProp (isIso f)
|
||||
lem1 f sA sB = res
|
||||
where
|
||||
module _ (x y : isIso f) where
|
||||
module x = Σ x renaming (fst to inverse ; snd to areInverses)
|
||||
module y = Σ y renaming (fst to inverse ; snd to areInverses)
|
||||
-- I had a lot of difficulty using the corresponding proof where
|
||||
-- AreInverses is defined. This is sadly a bit anti-modular. The
|
||||
-- reason for my troubles is probably related to the type of objects
|
||||
-- being hSet's rather than sets.
|
||||
p : ∀ {f} g → isProp (AreInverses {A = A} {B} f g)
|
||||
p {f} g xx yy i = ve-re , re-ve
|
||||
where
|
||||
ve-re : g ∘ f ≡ idFun _
|
||||
ve-re = arrowsAreSets {A = hA} {B = hA} _ _ (fst xx) (fst yy) i
|
||||
re-ve : f ∘ g ≡ idFun _
|
||||
re-ve = arrowsAreSets {A = hB} {B = hB} _ _ (snd xx) (snd yy) i
|
||||
1eq : x.inverse ≡ y.inverse
|
||||
1eq = begin
|
||||
x.inverse ≡⟨⟩
|
||||
x.inverse ∘ idFun _ ≡⟨ cong (λ φ → x.inverse ∘ φ) (sym (snd y.areInverses)) ⟩
|
||||
x.inverse ∘ (f ∘ y.inverse) ≡⟨⟩
|
||||
(x.inverse ∘ f) ∘ y.inverse ≡⟨ cong (λ φ → φ ∘ y.inverse) (fst x.areInverses) ⟩
|
||||
idFun _ ∘ y.inverse ≡⟨⟩
|
||||
y.inverse ∎
|
||||
2eq : (λ i → AreInverses f (1eq i)) [ x.areInverses ≡ y.areInverses ]
|
||||
2eq = lemPropF p 1eq
|
||||
res : x ≡ y
|
||||
res i = 1eq i , 2eq i
|
||||
module _ {ℓa ℓb : Level} {A : Set ℓa} {P : A → Set ℓb} where
|
||||
lem2 : ((x : A) → isProp (P x)) → (p q : Σ A P)
|
||||
→ (p ≡ q) ≃ (fst p ≡ fst q)
|
||||
lem2 pA p q = fromIsomorphism _ _ iso
|
||||
where
|
||||
f : ∀ {p q} → p ≡ q → fst p ≡ fst q
|
||||
f e i = fst (e i)
|
||||
g : ∀ {p q} → fst p ≡ fst q → p ≡ q
|
||||
g {p} {q} = lemSig pA p q
|
||||
ve-re : (e : p ≡ q) → (g ∘ f) e ≡ e
|
||||
ve-re = pathJ (\ q (e : p ≡ q) → (g ∘ f) e ≡ e)
|
||||
(\ i j → p .fst , propSet (pA (p .fst)) (p .snd) (p .snd) (λ i → (g {p} {p} ∘ f) (λ i₁ → p) i .snd) (λ i → p .snd) i j ) q
|
||||
re-ve : (e : fst p ≡ fst q) → (f {p} {q} ∘ g {p} {q}) e ≡ e
|
||||
re-ve e = refl
|
||||
inv : AreInverses (f {p} {q}) (g {p} {q})
|
||||
inv = funExt ve-re , funExt re-ve
|
||||
iso : (p ≡ q) ≅ (fst p ≡ fst q)
|
||||
iso = f , g , inv
|
||||
|
||||
module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where
|
||||
lem4 : isSet A → isSet B → (f : A → B)
|
||||
→ isEquiv A B f ≃ isIso f
|
||||
lem4 sA sB f =
|
||||
let
|
||||
obv : isEquiv A B f → isIso f
|
||||
obv = toIso A B
|
||||
inv : isIso f → isEquiv A B f
|
||||
inv = fromIso A B
|
||||
re-ve : (x : isEquiv A B f) → (inv ∘ obv) x ≡ x
|
||||
re-ve = inverse-from-to-iso A B
|
||||
ve-re : (x : isIso f) → (obv ∘ inv) x ≡ x
|
||||
ve-re = inverse-to-from-iso A B sA sB
|
||||
iso : isEquiv A B f ≅ isIso f
|
||||
iso = obv , inv , funExt re-ve , funExt ve-re
|
||||
in fromIsomorphism _ _ iso
|
||||
|
||||
open IsPreCategory isPreCat
|
||||
module _ {hA hB : Object} where
|
||||
open Σ hA renaming (fst to A ; snd to sA)
|
||||
open Σ hB renaming (fst to B ; snd to sB)
|
||||
|
||||
-- lem3 and the equivalence from lem4
|
||||
step0 : Σ (A → B) (isEquiv A B) ≃ Σ (A → B) isIso
|
||||
step0 = equivSig (lem4 sA sB)
|
||||
|
||||
-- lem2 with propIsSet
|
||||
step2 : (hA ≡ hB) ≃ (A ≡ B)
|
||||
step2 = lem2 (λ A → isSetIsProp) hA hB
|
||||
|
||||
univ≃ : (hA ≡ hB) ≃ (hA ≊ hB)
|
||||
univ≃ = step2 ⊙ univalence ⊙ step0
|
||||
univ≃
|
||||
= equivSigProp (λ A → isSetIsProp)
|
||||
⊙ univalence
|
||||
⊙ equivSig {P = isEquiv A B} {Q = TypeIsomorphism} (equiv≃iso sA sB)
|
||||
|
||||
univalent : Univalent
|
||||
univalent = univalenceFrom≃ univ≃
|
||||
|
|
|
|||
|
|
@ -119,7 +119,7 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
|
|||
--
|
||||
-- [HoTT §9.1.4]
|
||||
idToIso : (A B : Object) → A ≡ B → A ≊ B
|
||||
idToIso A B eq = transp (\ i → A ≊ eq i) (idIso A)
|
||||
idToIso A B eq = subst eq (idIso A)
|
||||
|
||||
Univalent : Set (ℓa ⊔ ℓb)
|
||||
Univalent = {A B : Object} → isEquiv (A ≡ B) (A ≊ B) (idToIso A B)
|
||||
|
|
@ -348,7 +348,7 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
|
|||
coe refl f ≡⟨ id-coe ⟩
|
||||
f ≡⟨ sym rightIdentity ⟩
|
||||
f <<< identity ≡⟨ cong (f <<<_) (sym subst-neutral) ⟩
|
||||
f <<< _ ∎) a' p
|
||||
f <<< _ ≡⟨ {!!} ⟩ _ ∎) a' p
|
||||
|
||||
module _ {b' : Object} (p : b ≡ b') where
|
||||
private
|
||||
|
|
@ -431,28 +431,17 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
|
|||
|
||||
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 ⟩
|
||||
coe p-dom f ≡⟨ 9-1-9-left f p ⟩
|
||||
f <<< fst (snd (idToIso _ _ (isoToId iso))) ≡⟨⟩
|
||||
f <<< fst (snd (idToIso _ _ p)) ≡⟨ cong (f <<<_) (cong (fst ∘ snd) lem) ⟩
|
||||
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 ⟩
|
||||
≡⟨ 9-1-9-right f p ⟩
|
||||
fst (idToIso _ _ p) <<< f
|
||||
≡⟨ cong (λ φ → φ <<< f) (cong fst lem) ⟩
|
||||
ι <<< f ∎
|
||||
|
||||
module _ {f : Arrow A X} {g : Arrow B X} (q : PathP (λ i → p-dom i) f g) where
|
||||
|
|
|
|||
|
|
@ -7,7 +7,6 @@ open import Cat.Equivalence
|
|||
open import Cat.Category
|
||||
|
||||
module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
|
||||
|
||||
open Category ℂ
|
||||
|
||||
module _ (A B : Object) where
|
||||
|
|
@ -18,8 +17,6 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
|
|||
fst : ℂ [ object , A ]
|
||||
snd : ℂ [ object , B ]
|
||||
|
||||
-- FIXME Not sure this is actually a proposition - so this name is
|
||||
-- misleading.
|
||||
record IsProduct (raw : RawProduct) : Set (ℓa ⊔ ℓb) where
|
||||
open RawProduct raw public
|
||||
field
|
||||
|
|
|
|||
|
|
@ -7,7 +7,10 @@ open import Cubical.PathPrelude hiding (inverse)
|
|||
open import Cubical.PathPrelude using (isEquiv ; isContr ; fiber) public
|
||||
open import Cubical.GradLemma hiding (isoToPath)
|
||||
|
||||
open import Cat.Prelude using (lemPropF ; setPi ; lemSig ; propSet ; Preorder ; equalityIsEquivalence ; propSig ; id-coe)
|
||||
open import Cat.Prelude using
|
||||
( lemPropF ; setPi ; lemSig ; propSet
|
||||
; Preorder ; equalityIsEquivalence ; propSig ; id-coe
|
||||
; Setoid )
|
||||
|
||||
import Cubical.Univalence as U
|
||||
|
||||
|
|
@ -327,6 +330,48 @@ preorder≅ ℓ = record
|
|||
k = pathJ D (trans id-coe id-coe) B (sym p)
|
||||
in k
|
||||
|
||||
setoid≅ : (ℓ : Level) → Setoid _ _
|
||||
setoid≅ ℓ = record
|
||||
{ Carrier = Set ℓ
|
||||
; _≈_ = _≅_
|
||||
; isEquivalence = record
|
||||
{ refl = idFun _ , idFun _ , (funExt λ _ → refl) , (funExt λ _ → refl)
|
||||
; sym = symmetryIso
|
||||
; trans = composeIso
|
||||
}
|
||||
}
|
||||
|
||||
setoid≃ : (ℓ : Level) → Setoid _ _
|
||||
setoid≃ ℓ = record
|
||||
{ Carrier = Set ℓ
|
||||
; _≈_ = _≃_
|
||||
; isEquivalence = record
|
||||
{ refl = idEquiv
|
||||
; sym = Equivalence.symmetry
|
||||
; trans = λ x x₁ → Equivalence.compose x x₁
|
||||
}
|
||||
}
|
||||
|
||||
-- If the second component of a pair is propositional, then equality of such
|
||||
-- pairs is equivalent to equality of their first components.
|
||||
module _ {ℓa ℓb : Level} {A : Set ℓa} {P : A → Set ℓb} where
|
||||
equivSigProp : ((x : A) → isProp (P x)) → {p q : Σ A P}
|
||||
→ (p ≡ q) ≃ (fst p ≡ fst q)
|
||||
equivSigProp pA {p} {q} = fromIsomorphism _ _ iso
|
||||
where
|
||||
f : ∀ {p q} → p ≡ q → fst p ≡ fst q
|
||||
f = cong fst
|
||||
g : ∀ {p q} → fst p ≡ fst q → p ≡ q
|
||||
g = lemSig pA _ _
|
||||
ve-re : (e : p ≡ q) → (g ∘ f) e ≡ e
|
||||
ve-re = pathJ (\ q (e : p ≡ q) → (g ∘ f) e ≡ e)
|
||||
(\ i j → p .fst , propSet (pA (p .fst)) (p .snd) (p .snd) (λ i → (g {p} {p} ∘ f) (λ i₁ → p) i .snd) (λ i → p .snd) i j ) q
|
||||
re-ve : (e : fst p ≡ fst q) → (f {p} {q} ∘ g {p} {q}) e ≡ e
|
||||
re-ve e = refl
|
||||
inv : AreInverses (f {p} {q}) (g {p} {q})
|
||||
inv = funExt ve-re , funExt re-ve
|
||||
iso : (p ≡ q) ≅ (fst p ≡ fst q)
|
||||
iso = f , g , inv
|
||||
|
||||
module _ {ℓ : Level} {A B : Set ℓ} where
|
||||
isoToPath : (A ≅ B) → (A ≡ B)
|
||||
|
|
@ -347,6 +392,24 @@ module _ {ℓ : Level} {A B : Set ℓ} where
|
|||
aux : (A U.≃ B) ≃ (A ≃ B)
|
||||
aux = fromIsomorphism _ _ (doEta , deEta , funExt (λ{ (U.con _ _) → refl}) , refl)
|
||||
|
||||
-- Equivalence is equivalent to isomorphism when the equivalence (resp.
|
||||
-- isomorphism) acts on sets.
|
||||
module _ (sA : isSet A) (sB : isSet B) where
|
||||
equiv≃iso : (f : A → B) → isEquiv A B f ≃ Isomorphism f
|
||||
equiv≃iso f =
|
||||
let
|
||||
obv : isEquiv A B f → Isomorphism f
|
||||
obv = toIso A B
|
||||
inv : Isomorphism f → isEquiv A B f
|
||||
inv = fromIso A B
|
||||
re-ve : (x : isEquiv A B f) → (inv ∘ obv) x ≡ x
|
||||
re-ve = inverse-from-to-iso A B
|
||||
ve-re : (x : Isomorphism f) → (obv ∘ inv) x ≡ x
|
||||
ve-re = inverse-to-from-iso A B sA sB
|
||||
iso : isEquiv A B f ≅ Isomorphism f
|
||||
iso = obv , inv , funExt re-ve , funExt ve-re
|
||||
in fromIsomorphism _ _ iso
|
||||
|
||||
-- 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
|
||||
-- Equality on sigma's whose second component is a proposition is equivalent
|
||||
|
|
@ -438,6 +501,8 @@ module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where
|
|||
in fromIsomorphism _ _ iso
|
||||
|
||||
module _ {ℓa ℓb : Level} {A : Set ℓa} {P : A → Set ℓb} where
|
||||
-- Equivalence of pairs whose first components are identitical can be obtained
|
||||
-- from an equivalence of their seecond components.
|
||||
equivSig : {ℓc : Level} {Q : A → Set ℓc}
|
||||
→ ((a : A) → P a ≃ Q a) → Σ A P ≃ Σ A Q
|
||||
equivSig {Q = Q} eA = res
|
||||
|
|
|
|||
|
|
@ -76,7 +76,9 @@ module _ {ℓa ℓb : Level} {A : Set ℓa} {B : A → Set ℓb} {a b : Σ A B}
|
|||
snd (Σ≡ i) = snd≡ i
|
||||
|
||||
import Relation.Binary
|
||||
open Relation.Binary public using (Preorder ; Transitive ; IsEquivalence ; Rel)
|
||||
open Relation.Binary public using
|
||||
( Preorder ; Transitive ; IsEquivalence ; Rel
|
||||
; Setoid )
|
||||
|
||||
equalityIsEquivalence : {ℓ : Level} {A : Set ℓ} → IsEquivalence {A = A} _≡_
|
||||
IsEquivalence.refl equalityIsEquivalence = refl
|
||||
|
|
|
|||
Loading…
Reference in a new issue