Remove bad lemma for showing univalence
This commit is contained in:
parent
e69ace21a0
commit
be56027c37
|
|
@ -127,67 +127,6 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where
|
||||||
Univalent[Contr] : Set _
|
Univalent[Contr] : Set _
|
||||||
Univalent[Contr] = ∀ A → isContr (Σ[ X ∈ Object ] A ≅ X)
|
Univalent[Contr] = ∀ A → isContr (Σ[ X ∈ Object ] A ≅ X)
|
||||||
|
|
||||||
private
|
|
||||||
module _ (A : Object)
|
|
||||||
-- It may be that we need something weaker than this, in that there
|
|
||||||
-- may be some other lemmas available to us.
|
|
||||||
-- For instance, `need0` should be available to us when we prove `need1`.
|
|
||||||
(need0 : (s : Σ Object (A ≅_)) → (open Σ s renaming (fst to Y) using ()) → A ≡ Y)
|
|
||||||
(need2 : (iso : A ≅ A)
|
|
||||||
→ (open Σ iso renaming (fst to f ; snd to iso-f))
|
|
||||||
→ (open Σ iso-f renaming (fst to f~ ; snd to areInv))
|
|
||||||
→ (identity , identity) ≡ (f , f~)
|
|
||||||
) where
|
|
||||||
|
|
||||||
c : Σ Object (A ≅_)
|
|
||||||
c = A , idIso A
|
|
||||||
|
|
||||||
module _ (y : Σ Object (A ≅_)) where
|
|
||||||
open Σ y renaming (fst to Y ; snd to isoY)
|
|
||||||
q : A ≡ Y
|
|
||||||
q = need0 y
|
|
||||||
|
|
||||||
-- Some error with primComp
|
|
||||||
isoAY : A ≅ Y
|
|
||||||
isoAY = {!idToIso A Y q!}
|
|
||||||
|
|
||||||
lem : PathP (λ i → A ≅ q i) (idIso A) isoY
|
|
||||||
lem = d* isoAY
|
|
||||||
where
|
|
||||||
D : (Y : Object) → (A ≡ Y) → Set _
|
|
||||||
D Y p = (A≅Y : A ≅ Y) → PathP (λ i → A ≅ p i) (idIso A) A≅Y
|
|
||||||
d : D A refl
|
|
||||||
d A≅Y i = a0 i , a1 i , a2 i
|
|
||||||
where
|
|
||||||
open Σ A≅Y renaming (fst to f ; snd to iso-f)
|
|
||||||
open Σ iso-f renaming (fst to f~ ; snd to areInv)
|
|
||||||
aaa : (identity , identity) ≡ (f , f~)
|
|
||||||
aaa = need2 A≅Y
|
|
||||||
a0 : identity ≡ f
|
|
||||||
a0 i = fst (aaa i)
|
|
||||||
a1 : identity ≡ f~
|
|
||||||
a1 i = snd (aaa i)
|
|
||||||
-- we do have this!
|
|
||||||
-- I just need to rearrange the proofs a bit.
|
|
||||||
postulate
|
|
||||||
prop : ∀ {A B} (fg : Arrow A B × Arrow B A) → isProp (IsInverseOf (fst fg) (snd fg))
|
|
||||||
a2 : PathP (λ i → IsInverseOf (a0 i) (a1 i)) isIdentity areInv
|
|
||||||
a2 = lemPropF prop aaa
|
|
||||||
d* : D Y q
|
|
||||||
d* = pathJ D d Y q
|
|
||||||
|
|
||||||
p : (A , idIso A) ≡ (Y , isoY)
|
|
||||||
p i = q i , lem i
|
|
||||||
|
|
||||||
univ-lem : isContr (Σ Object (A ≅_))
|
|
||||||
univ-lem = c , p
|
|
||||||
|
|
||||||
univalence-lemma
|
|
||||||
: (∀ {A} → (s : Σ Object (_≅_ A)) → A ≡ fst s)
|
|
||||||
→ (∀ {A} → (iso : A ≅ A) → (identity , identity) ≡ (fst iso , fst (snd iso)))
|
|
||||||
→ Univalent[Contr]
|
|
||||||
univalence-lemma s u A = univ-lem A s u
|
|
||||||
|
|
||||||
-- From: Thierry Coquand <Thierry.Coquand@cse.gu.se>
|
-- From: Thierry Coquand <Thierry.Coquand@cse.gu.se>
|
||||||
-- Date: Wed, Mar 21, 2018 at 3:12 PM
|
-- Date: Wed, Mar 21, 2018 at 3:12 PM
|
||||||
--
|
--
|
||||||
|
|
|
||||||
|
|
@ -198,103 +198,6 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
|
||||||
-- alt : isContr (Σ Object (X ≡_))
|
-- alt : isContr (Σ Object (X ≡_))
|
||||||
-- alt = (X , refl) , alt'
|
-- alt = (X , refl) , alt'
|
||||||
|
|
||||||
univalent' : Univalent[Contr]
|
|
||||||
univalent' = univalence-lemma p q
|
|
||||||
where
|
|
||||||
module _ {𝕏 : Object} where
|
|
||||||
open Σ 𝕏 renaming (fst to X ; snd to x0x1)
|
|
||||||
open Σ x0x1 renaming (fst to x0 ; snd to x1)
|
|
||||||
-- x0 : X → A in ℂ
|
|
||||||
-- x1 : X → B in ℂ
|
|
||||||
module _ (𝕐-isoY : Σ Object (𝕏 ≅_)) where
|
|
||||||
open Σ 𝕐-isoY renaming (fst to 𝕐 ; snd to isoY)
|
|
||||||
open Σ 𝕐 renaming (fst to Y ; snd to y0y1)
|
|
||||||
open Σ y0y1 renaming (fst to y0 ; snd to y1)
|
|
||||||
open Σ isoY renaming (fst to 𝓯 ; snd to iso-𝓯)
|
|
||||||
open Σ iso-𝓯 renaming (fst to 𝓯~ ; snd to inv-𝓯)
|
|
||||||
open Σ 𝓯 renaming (fst to f ; snd to inv-f)
|
|
||||||
open Σ 𝓯~ renaming (fst to f~ ; snd to inv-f~)
|
|
||||||
open Σ inv-𝓯 renaming (fst to left ; snd to right)
|
|
||||||
-- y0 : Y → A in ℂ
|
|
||||||
-- y1 : Y → B in ℂ
|
|
||||||
-- f : X → Y in ℂ
|
|
||||||
-- inv-f : ℂ [ y0 ∘ f ] ≡ x0 × ℂ [ y1 ∘ f ] ≡ x1
|
|
||||||
-- left : 𝓯~ ∘ 𝓯 ≡ identity
|
|
||||||
-- left~ : 𝓯 ∘ 𝓯~ ≡ identity
|
|
||||||
isoℂ : X ℂ.≅ Y
|
|
||||||
isoℂ
|
|
||||||
= f
|
|
||||||
, f~
|
|
||||||
, ( begin
|
|
||||||
ℂ [ f~ ∘ f ] ≡⟨ (λ i → fst (left i)) ⟩
|
|
||||||
ℂ.identity ∎
|
|
||||||
)
|
|
||||||
, ( begin
|
|
||||||
ℂ [ f ∘ f~ ] ≡⟨ (λ i → fst (right i)) ⟩
|
|
||||||
ℂ.identity ∎
|
|
||||||
)
|
|
||||||
p0 : X ≡ Y
|
|
||||||
p0 = ℂ.iso-to-id isoℂ
|
|
||||||
-- I note `left2` and right2` here as a reminder.
|
|
||||||
left2 : PathP
|
|
||||||
(λ i → ℂ [ x0 ∘ fst (left i) ] ≡ x0 × ℂ [ x1 ∘ fst (left i) ] ≡ x1)
|
|
||||||
(snd (𝓯~ ∘ 𝓯)) (snd identity)
|
|
||||||
left2 i = snd (left i)
|
|
||||||
right2 : PathP
|
|
||||||
(λ i → ℂ [ y0 ∘ fst (right i) ] ≡ y0 × ℂ [ y1 ∘ fst (right i) ] ≡ y1)
|
|
||||||
(snd (𝓯 ∘ 𝓯~)) (snd identity)
|
|
||||||
right2 i = snd (right i)
|
|
||||||
-- My idea:
|
|
||||||
--
|
|
||||||
-- x0, x1 and y0 and y1 are product arrows as in the diagram
|
|
||||||
--
|
|
||||||
-- X
|
|
||||||
-- ↙ ↘
|
|
||||||
-- A ⇣ ⇡ B
|
|
||||||
-- ↖ ↗
|
|
||||||
-- Y (All hail unicode)
|
|
||||||
--
|
|
||||||
-- The dotted lines indicate the unique product arrows. Since they are
|
|
||||||
-- unique they necessarily be each others inverses. Alas, more than
|
|
||||||
-- this we must show that they are actually (heterogeneously)
|
|
||||||
-- identical as in `p1`:
|
|
||||||
p1 : PathP (λ i → ℂ.Arrow (p0 i) A × ℂ.Arrow (p0 i) B) x0x1 y0y1
|
|
||||||
p1 = {!!}
|
|
||||||
where
|
|
||||||
-- This, however, should probably somehow follow from them being
|
|
||||||
-- inverses on objects that are propositionally equal cf. `p0`.
|
|
||||||
helper : {A B : Object} {f : Arrow A B} {g : Arrow B A}
|
|
||||||
→ IsInverseOf f g
|
|
||||||
→ (p : A ≡ B)
|
|
||||||
→ PathP (λ i → Arrow (p i) (p (~ i))) f g
|
|
||||||
helper = {!!}
|
|
||||||
|
|
||||||
p : (X , x0x1) ≡ (Y , y0y1)
|
|
||||||
p i = p0 i , {!!}
|
|
||||||
module _ (iso : 𝕏 ≅ 𝕏) where
|
|
||||||
open Σ iso renaming (fst to 𝓯 ; snd to inv-𝓯)
|
|
||||||
open Σ inv-𝓯 renaming (fst to 𝓯~) using ()
|
|
||||||
open Σ 𝓯 renaming (fst to f ; snd to inv-f)
|
|
||||||
open Σ 𝓯~ renaming (fst to f~ ; snd to inv-f~)
|
|
||||||
q0' : ℂ.identity ≡ f
|
|
||||||
q0' i = {!!}
|
|
||||||
prop : ∀ x → isProp (ℂ [ x0 ∘ x ] ≡ x0 × ℂ [ x1 ∘ x ] ≡ x1)
|
|
||||||
prop x = propSig
|
|
||||||
( ℂ.arrowsAreSets (ℂ [ x0 ∘ x ]) x0)
|
|
||||||
(λ _ → ℂ.arrowsAreSets (ℂ [ x1 ∘ x ]) x1)
|
|
||||||
q0'' : PathP (λ i → ℂ [ x0 ∘ q0' i ] ≡ x0 × ℂ [ x1 ∘ q0' i ] ≡ x1) (snd identity) inv-f
|
|
||||||
q0'' = lemPropF prop q0'
|
|
||||||
q0 : identity ≡ 𝓯
|
|
||||||
q0 i = q0' i , q0'' i
|
|
||||||
q1' : ℂ.identity ≡ f~
|
|
||||||
q1' = {!!}
|
|
||||||
q1'' : PathP (λ i → (ℂ [ x0 ∘ q1' i ]) ≡ x0 × (ℂ [ x1 ∘ q1' i ]) ≡ x1) (snd identity) inv-f~
|
|
||||||
q1'' = lemPropF prop q1'
|
|
||||||
q1 : identity ≡ 𝓯~
|
|
||||||
q1 i = q1' i , {!!}
|
|
||||||
q : (identity , identity) ≡ (𝓯 , 𝓯~)
|
|
||||||
q i = q0 i , q1 i
|
|
||||||
|
|
||||||
univalent : Univalent
|
univalent : Univalent
|
||||||
univalent {X , x} {Y , y} = {!res!}
|
univalent {X , x} {Y , y} = {!res!}
|
||||||
where
|
where
|
||||||
|
|
|
||||||
Loading…
Reference in a new issue