fredefox/cat
1
0
Fork 0
Code Issues Pull requests Releases Wiki Activity

[WIP] Finnish all intermediate steps for univalence of hSets

Browse source
This commit is contained in:
Frederik Hanghøj Iversen 2018-03-20 13:26:40 +01:00
parent 2188e690a0
commit 66cb5b363d
1 changed files with 14 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/Cat/Categories/Sets.agda
View file

@ -221,17 +221,25 @@ module _ (ℓ : Level) where
step0 = lem3 (λ f → sym≃ (lem4 sA sB f)) step0 = lem3 (λ f → sym≃ (lem4 sA sB f))
-- univalence -- univalence
step1 : Σ (A → B) (isEquiv A B) ≃ (A ≡ B) step1 : Σ (A → B) (isEquiv A B) ≃ (A ≡ B)
step1 = step1 = hh ⊙ h
let where
h : (A ≃ B) ≃ (A ≡ B) h : (A ≃ B) ≃ (A ≡ B)
h = sym≃ (univalence {A = A} {B}) h = sym≃ (univalence {A = A} {B})
k : Σ _ (isEquiv (A ≃ B) (A ≡ B)) obv : Σ (A → B) (isEquiv A B) → A ≃ B
k = Eqv.doEta h obv = Eqv.deEta
inv : A ≃ B → Σ (A → B) (isEquiv A B)
inv = Eqv.doEta
re-ve : (x : _) → (inv ∘ obv) x ≡ x
re-ve x = refl
-- Because _≃_ does not have eta equality!
ve-re : (x : _) → (obv ∘ inv) x ≡ x
ve-re (con eqv isEqv) i = con eqv isEqv
areInv : AreInverses obv inv
areInv = record { verso-recto = funExt re-ve ; recto-verso = funExt ve-re }
eqv : Σ (A → B) (isEquiv A B) Eqv.≅ (A ≃ B) eqv : Σ (A → B) (isEquiv A B) Eqv.≅ (A ≃ B)
eqv = {!!} , {!!} , {!!} eqv = obv , inv , areInv
hh : Σ (A → B) (isEquiv A B) ≃ (A ≃ B) hh : Σ (A → B) (isEquiv A B) ≃ (A ≃ B)
hh = Eeq.fromIsomorphism eqv hh = Eeq.fromIsomorphism eqv
in hh ⊙ h
-- lem2 with propIsSet -- lem2 with propIsSet
step2 : (A ≡ B) ≃ (hA ≡ hB) step2 : (A ≡ B) ≃ (hA ≡ hB)