From 772e6778f3904fd1c12b79e07c5584c850e40e9b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Tue, 10 Apr 2018 17:17:04 +0200 Subject: [PATCH] [WIP] Univalence in ad-hoc category in product --- src/Cat/Category.agda | 34 ++++++++--- src/Cat/Category/Product.agda | 109 ++++++++++++++++++++++++---------- 2 files changed, 106 insertions(+), 37 deletions(-) diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index 776c92a..f95603f 100644 --- a/src/Cat/Category.agda +++ b/src/Cat/Category.agda @@ -136,12 +136,25 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where Univalent[Contr] : Set _ Univalent[Contr] = ∀ A → isContr (Σ[ X ∈ Object ] A ≅ X) + Univalent[Andrea] : Set _ + Univalent[Andrea] = ∀ A B → (A ≅ B) ≃ (A ≡ B) + -- From: Thierry Coquand -- Date: Wed, Mar 21, 2018 at 3:12 PM -- -- This is not so straight-forward so you can assume it postulate from[Contr] : Univalent[Contr] → Univalent + from[Andrea] : Univalent[Andrea] → Univalent + from[Andrea] = from[Contr] Function.∘ step + where + module _ (f : Univalent[Andrea]) (A : Object) where + aux : isContr (Σ[ B ∈ Object ] A ≡ B) + aux = ? + + step : isContr (Σ Object (A ≅_)) + step = {!subst {P = isContr} {!!} aux!} + propUnivalent : isProp Univalent propUnivalent a b i = propPi (λ iso → propIsContr) a b i @@ -205,9 +218,9 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where propIsInverseOf : ∀ {A B f g} → isProp (IsInverseOf {A} {B} f g) propIsInverseOf = propSig (arrowsAreSets _ _) (λ _ → arrowsAreSets _ _) - module _ {A B : Object} {f : Arrow A B} where - isoIsProp : isProp (Isomorphism f) - isoIsProp a@(g , η , ε) a'@(g' , η' , ε') = + module _ {A B : Object} (f : Arrow A B) where + propIsomorphism : isProp (Isomorphism f) + propIsomorphism a@(g , η , ε) a'@(g' , η' , ε') = lemSig (λ g → propIsInverseOf) a a' geq where geq : g ≡ g' @@ -303,12 +316,19 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where univalent≃ = _ , univalent module _ {A B : Object} where - iso-to-id : (A ≅ B) → (A ≡ B) - iso-to-id = fst (toIso _ _ univalent) + private + iso : TypeIsomorphism (idToIso A B) + iso = toIso _ _ univalent + + isoToId : (A ≅ B) → (A ≡ B) + isoToId = fst iso asTypeIso : TypeIsomorphism (idToIso A B) asTypeIso = toIso _ _ univalent + inverse-from-to-iso' : AreInverses (idToIso A B) isoToId + inverse-from-to-iso' = snd iso + -- | All projections are propositions. module Propositionality where -- | Terminal objects are propositional - a.k.a uniqueness of terminal @@ -338,7 +358,7 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where iso : X ≅ Y iso = X→Y , Y→X , left , right p0 : X ≡ Y - p0 = iso-to-id iso + p0 = isoToId iso p1 : (λ i → IsTerminal (p0 i)) [ Xit ≡ Yit ] p1 = lemPropF propIsTerminal p0 res : Xt ≡ Yt @@ -368,7 +388,7 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where iso : X ≅ Y iso = Y→X , X→Y , right , left res : Xi ≡ Yi - res = lemSig propIsInitial _ _ (iso-to-id iso) + res = lemSig propIsInitial _ _ (isoToId iso) module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where open RawCategory ℂ diff --git a/src/Cat/Category/Product.agda b/src/Cat/Category/Product.agda index 1985656..3aa73ba 100644 --- a/src/Cat/Category/Product.agda +++ b/src/Cat/Category/Product.agda @@ -1,4 +1,4 @@ -{-# OPTIONS --allow-unsolved-metas --cubical #-} +{-# OPTIONS --allow-unsolved-metas --cubical --caching #-} module Cat.Category.Product where open import Cat.Prelude as P hiding (_×_ ; fst ; snd) @@ -183,7 +183,7 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} -- ; _∎ to _∎! ) -- lawl -- : ((X , xa , xb) ≡ (Y , ya , yb)) - -- ≈ (Σ[ iso ∈ (X ℂ.≅ Y) ] let p = ℂ.iso-to-id iso in (PathP (λ i → ℂ.Arrow (p i) A) xa ya) × (PathP (λ i → ℂ.Arrow (p i) B) xb yb)) + -- ≈ (Σ[ iso ∈ (X ℂ.≅ Y) ] let p = ℂ.isoToId iso in (PathP (λ i → ℂ.Arrow (p i) A) xa ya) × (PathP (λ i → ℂ.Arrow (p i) B) xb yb)) -- lawl = {!begin! ? ≈⟨ ? ⟩ ? ∎!!} -- Problem with the above approach: Preorders only work for heterogeneous equaluties. @@ -192,7 +192,7 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} -- Σ[ p ∈ (X ≡ Y) ] (PathP (λ i → ℂ.Arrow (p i) A) xa ya) × (PathP (λ i → ℂ.Arrow (p i) B) xb yb) -- ≅ -- Σ (X ℂ.≅ Y) (λ iso - -- → let p = ℂ.iso-to-id iso + -- → let p = ℂ.isoToId iso -- in -- ( PathP (λ i → ℂ.Arrow (p i) A) xa ya) -- × PathP (λ i → ℂ.Arrow (p i) B) xb yb @@ -207,63 +207,104 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} -- , (λ x → λ i → fst x i , (fst (snd x) i) , (snd (snd x) i)) , (λ{ (p , q , r) → Σ≡ p λ i → q i , r i}) , record - { verso-recto = {!!} - ; recto-verso = {!!} + { verso-recto = funExt (λ{ p → refl}) + ; recto-verso = funExt (λ{ (p , q , r) → refl}) } where open import Function renaming (_∘_ to _⊙_) + + -- Should follow from c being univalent + iso-id-inv : {p : X ≡ Y} → p ≡ ℂ.isoToId (ℂ.idToIso X Y p) + iso-id-inv {p} = sym (λ i → AreInverses.verso-recto ℂ.inverse-from-to-iso' i p) + id-iso-inv : {iso : X ℂ.≅ Y} → iso ≡ ℂ.idToIso X Y (ℂ.isoToId iso) + id-iso-inv {iso} = sym (λ i → AreInverses.recto-verso ℂ.inverse-from-to-iso' i iso) + + lemA : {A B : Object} {f g : Arrow A B} → fst f ≡ fst g → f ≡ g + lemA {A} {B} {f = f} {g} p i = p i , h i + where + h : PathP (λ i → + (ℂ [ fst (snd B) ∘ p i ]) ≡ fst (snd A) × + (ℂ [ snd (snd B) ∘ p i ]) ≡ snd (snd A) + ) (snd f) (snd g) + h = lemPropF (λ a → propSig + (ℂ.arrowsAreSets (ℂ [ fst (snd B) ∘ a ]) (fst (snd A))) + λ _ → ℂ.arrowsAreSets (ℂ [ snd (snd B) ∘ a ]) (snd (snd A))) + p + step1 : (Σ[ p ∈ (X ≡ Y) ] (PathP (λ i → ℂ.Arrow (p i) A) xa ya) × (PathP (λ i → ℂ.Arrow (p i) B) xb yb)) ≈ Σ (X ℂ.≅ Y) (λ iso - → let p = ℂ.iso-to-id iso + → let p = ℂ.isoToId iso in ( PathP (λ i → ℂ.Arrow (p i) A) xa ya) × PathP (λ i → ℂ.Arrow (p i) B) xb yb ) step1 - = (λ{ (p , x) → (ℂ.idToIso _ _ p) , {!snd x!}}) + = (λ{ (p , x) + → (ℂ.idToIso _ _ p) + , let + P-l : (p : X ≡ Y) → Set _ + P-l φ = PathP (λ i → ℂ.Arrow (φ i) A) xa ya + P-r : (p : X ≡ Y) → Set _ + P-r φ = PathP (λ i → ℂ.Arrow (φ i) B) xb yb + left : P-l p + left = fst x + right : P-r p + right = snd x + in subst {P = P-l} iso-id-inv left , subst {P = P-r} iso-id-inv right + }) -- Goal is: -- -- φ x -- -- where `x` is -- - -- ℂ.iso-to-id (ℂ.idToIso _ _ p) + -- ℂ.isoToId (ℂ.idToIso _ _ p) -- -- I have `φ p` in scope, but surely `p` and `x` are the same - though -- perhaps not definitonally. - , (λ{ (iso , x) → ℂ.iso-to-id iso , x}) - , record { verso-recto = {!!} ; recto-verso = {!!} } - lemA : {A B : Object} {f g : Arrow A B} → fst f ≡ fst g → f ≡ g - lemA {A} {B} {f = f} {g} p i = p i , h i - where - h : PathP (λ i → - (ℂ [ fst (snd B) ∘ p i ]) ≡ fst (snd A) × - (ℂ [ snd (snd B) ∘ p i ]) ≡ snd (snd A) - ) (snd f) (snd g) - h = lemPropF (λ a → propSig - (ℂ.arrowsAreSets (ℂ [ fst (snd B) ∘ a ]) (fst (snd A))) - λ _ → ℂ.arrowsAreSets (ℂ [ snd (snd B) ∘ a ]) (snd (snd A))) - p + , (λ{ (iso , x) → ℂ.isoToId iso , x}) + , record + { verso-recto = funExt (λ{ (p , q , r) → Σ≡ (sym iso-id-inv) (toPathP {A = λ i → {!!}} {!!})}) + -- { verso-recto = funExt (λ{ (p , q , r) → Σ≡ (sym iso-id-inv) {!!}}) + ; recto-verso = funExt (λ x → Σ≡ (sym id-iso-inv) {!!}) + } step2 : Σ (X ℂ.≅ Y) (λ iso - → let p = ℂ.iso-to-id iso + → let p = ℂ.isoToId iso in ( PathP (λ i → ℂ.Arrow (p i) A) xa ya) × PathP (λ i → ℂ.Arrow (p i) B) xb yb ) ≈ ((X , xa , xb) ≅ (Y , ya , yb)) step2 - = ( λ{ ((f , f~ , inv-f) , x) - → ( f , {!!}) - , ( (f~ , {!!}) - , lemA {!!} - , lemA {!!} + = ( λ{ ((f , f~ , inv-f) , p , q) + → ( f , (let r = fromPathP p in {!r!}) , {!!}) + , ( (f~ , {!!} , {!!}) + , lemA (fst inv-f) + , lemA (snd inv-f) ) } ) - , (λ x → {!!}) - , {!!} + , (λ{ (f , f~ , inv-f , inv-f~) → + let + iso : X ℂ.≅ Y + iso = fst f , fst f~ , cong fst inv-f , cong fst inv-f~ + helper : PathP (λ i → ℂ.Arrow (ℂ.isoToId ? i) A) xa ya + helper = {!!} + in iso , helper , {!!}}) + , record + { verso-recto = funExt (λ x → lemSig + (λ x → propSig prop0 (λ _ → prop1)) + _ _ + (Σ≡ {!!} (ℂ.propIsomorphism _ _ _))) + ; recto-verso = funExt (λ{ (f , _) → lemSig propIsomorphism _ _ {!refl!}}) + } + where + prop0 : ∀ {x} → isProp (PathP (λ i → ℂ.Arrow (ℂ.isoToId x i) A) xa ya) + prop0 {x} = pathJ (λ y p → ∀ x → isProp (PathP (λ i → ℂ.Arrow (p i) A) xa x)) (λ x → ℂ.arrowsAreSets _ _) Y (ℂ.isoToId x) ya + prop1 : ∀ {x} → isProp (PathP (λ i → ℂ.Arrow (ℂ.isoToId x i) B) xb yb) + prop1 {x} = pathJ (λ y p → ∀ x → isProp (PathP (λ i → ℂ.Arrow (p i) B) xb x)) (λ x → ℂ.arrowsAreSets _ _) Y (ℂ.isoToId x) yb -- One thing to watch out for here is that the isomorphisms going forwards -- must compose to give idToIso iso @@ -273,8 +314,16 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where infixl 5 _⊙_ _⊙_ = composeIso + equiv1 + : ((X , xa , xb) ≡ (Y , ya , yb)) + ≃ ((X , xa , xb) ≅ (Y , ya , yb)) + equiv1 = _ , fromIso _ _ (snd iso) + res : TypeIsomorphism (idToIso (X , xa , xb) (Y , ya , yb)) - res = {!snd iso!} + res = {!snd equiv1!} + + univalent2 : ∀ X Y → (X ≅ Y) ≃ (X ≡ Y) + univalent2 = {!!} isCat : IsCategory raw IsCategory.isPreCategory isCat = isPreCat