diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index b006f69..135e1a7 100644 --- a/src/Cat/Category.agda +++ b/src/Cat/Category.agda @@ -127,67 +127,6 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where Univalent[Contr] : Set _ 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 -- Date: Wed, Mar 21, 2018 at 3:12 PM -- diff --git a/src/Cat/Category/Product.agda b/src/Cat/Category/Product.agda index c65adeb..ed49dac 100644 --- a/src/Cat/Category/Product.agda +++ b/src/Cat/Category/Product.agda @@ -198,103 +198,6 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} -- alt : isContr (Σ Object (X ≡_)) -- 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 {X , x} {Y , y} = {!res!} where