From d78965d73f0e73756fb30a2997021d1fe45c27f0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Wed, 4 Apr 2018 17:45:36 +0200 Subject: [PATCH] Try to use lemma for proving univalence of product-category thing --- src/Cat/Categories/Sets.agda | 30 --------- src/Cat/Category.agda | 14 +++-- src/Cat/Category/Product.agda | 115 ++++++++++++++++++++++++++++++++-- 3 files changed, 119 insertions(+), 40 deletions(-) diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index 8536870..ab094c9 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -27,36 +27,6 @@ sym≃ = Equivalence.symmetry infixl 10 _⊙_ -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) where private SetsRaw : RawCategory (lsuc ℓ) ℓ diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index 9c1ee7c..5c497b9 100644 --- a/src/Cat/Category.agda +++ b/src/Cat/Category.agda @@ -132,16 +132,16 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where Univalent[Contr] = ∀ A → isContr (Σ[ X ∈ Object ] A ≅ X) private - module _ (A : Object) where - postulate + 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 (proj₁ to Y) using ()) → A ≡ Y - need2 : (iso : A ≅ A) + (need0 : (s : Σ Object (A ≅_)) → (open Σ s renaming (proj₁ to Y) using ()) → A ≡ Y) + (need2 : (iso : A ≅ A) → (open Σ iso renaming (proj₁ to f ; proj₂ to iso-f)) → (open Σ iso-f renaming (proj₁ to f~ ; proj₂ to areInv)) → (identity , identity) ≡ (f , f~) + ) where c : Σ Object (A ≅_) c = A , idIso A @@ -186,6 +186,12 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where 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 -- Date: Wed, Mar 21, 2018 at 3:12 PM -- diff --git a/src/Cat/Category/Product.agda b/src/Cat/Category/Product.agda index a811ecd..44fb0ef 100644 --- a/src/Cat/Category/Product.agda +++ b/src/Cat/Category/Product.agda @@ -99,13 +99,13 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} raw : RawCategory _ _ raw = record { Object = Σ[ X ∈ ℂ.Object ] ℂ.Arrow X A × ℂ.Arrow X B - ; Arrow = λ{ (X , xa , xb) (Y , ya , yb) - → Σ[ xy ∈ ℂ.Arrow X Y ] - ( ℂ [ ya ∘ xy ] ≡ xa) - × ℂ [ yb ∘ xy ] ≡ xb + ; Arrow = λ{ (X , x0 , x1) (Y , y0 , y1) + → Σ[ f ∈ ℂ.Arrow X Y ] + ℂ [ y0 ∘ f ] ≡ x0 + × ℂ [ y1 ∘ f ] ≡ x1 } - ; identity = λ{ {A , f , g} → ℂ.identity {A} , ℂ.rightIdentity , ℂ.rightIdentity} - ; _∘_ = λ { {A , a0 , a1} {B , b0 , b1} {C , c0 , c1} (f , f0 , f1) (g , g0 , g1) + ; identity = λ{ {X , f , g} → ℂ.identity {X} , ℂ.rightIdentity , ℂ.rightIdentity} + ; _∘_ = λ { {_ , a0 , a1} {_ , b0 , b1} {_ , c0 , c1} (f , f0 , f1) (g , g0 , g1) → (f ℂ.∘ g) , (begin ℂ [ c0 ∘ ℂ [ f ∘ g ] ] ≡⟨ ℂ.isAssociative ⟩ @@ -165,6 +165,109 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} open Univalence isIdentity + module _ (A : Object) where + c : Σ Object (A ≅_) + c = A , {!!} + univalent[Contr] : isContr (Σ Object (A ≅_)) + univalent[Contr] = {!!} , {!!} + + univalent' : Univalent[Contr] + univalent' = univalence-lemma p q + where + module _ {𝕏 : Object} where + open Σ 𝕏 renaming (proj₁ to X ; proj₂ to x0x1) + open Σ x0x1 renaming (proj₁ to x0 ; proj₂ to x1) + -- x0 : X → A in ℂ + -- x1 : X → B in ℂ + module _ (𝕐-isoY : Σ Object (𝕏 ≅_)) where + open Σ 𝕐-isoY renaming (proj₁ to 𝕐  ; proj₂ to isoY) + open Σ 𝕐 renaming (proj₁ to Y ; proj₂ to y0y1) + open Σ y0y1  renaming (proj₁ to y0 ; proj₂ to y1) + open Σ isoY  renaming (proj₁ to 𝓯 ; proj₂ to iso-𝓯) + open Σ iso-𝓯  renaming (proj₁ to 𝓯~ ; proj₂ to inv-𝓯) + open Σ 𝓯  renaming (proj₁ to f ; proj₂ to inv-f) + open Σ 𝓯~  renaming (proj₁ to f~ ; proj₂ to inv-f~) + open Σ inv-𝓯  renaming (proj₁ to left ; proj₂ 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 → proj₁ (left i)) ⟩ + ℂ.identity ∎ + ) + , ( begin + ℂ [ f ∘ f~ ] ≡⟨ (λ i → proj₁ (right i)) ⟩ + ℂ.identity ∎ + ) + p0 : X ≡ Y + p0 = ℂ.iso-to-id isoℂ + -- I note `left2` and right2` here as a reminder. + left2 : PathP + (λ i → ℂ [ x0 ∘ proj₁ (left i) ] ≡ x0 × ℂ [ x1 ∘ proj₁ (left i) ] ≡ x1) + (proj₂ (𝓯~ ∘ 𝓯)) (proj₂ identity) + left2 i = proj₂ (left i) + right2 : PathP + (λ i → ℂ [ y0 ∘ proj₁ (right i) ] ≡ y0 × ℂ [ y1 ∘ proj₁ (right i) ] ≡ y1) + (proj₂ (𝓯 ∘ 𝓯~)) (proj₂ identity) + right2 i = proj₂ (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 (proj₁ to 𝓯 ; proj₂ to inv-𝓯) + open Σ inv-𝓯 renaming (proj₁ to 𝓯~) using () + open Σ 𝓯 renaming (proj₁ to f ; proj₂ to inv-f) + open Σ 𝓯~ renaming (proj₁ to f~ ; proj₂ 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) (proj₂ 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) (proj₂ 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 {X , x} {Y , y} = {!res!} where