Rename variable
This commit is contained in:
parent
129eef1150
commit
6b6e6672e0
|
|
@ -87,18 +87,18 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} {A B : Category.Object
|
|||
q = lemPropF propIsProduct p
|
||||
|
||||
module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
|
||||
(let module ℂ = Category ℂ) {A B : ℂ.Object} where
|
||||
(let module ℂ = Category ℂ) {𝓐 𝓑 : ℂ.Object} where
|
||||
|
||||
open P
|
||||
|
||||
module _ where
|
||||
raw : RawCategory _ _
|
||||
raw = record
|
||||
{ Object = Σ[ X ∈ ℂ.Object ] ℂ.Arrow X A × ℂ.Arrow X B
|
||||
; Arrow = λ{ (X , x0 , x1) (Y , y0 , y1)
|
||||
→ Σ[ f ∈ ℂ.Arrow X Y ]
|
||||
ℂ [ y0 ∘ f ] ≡ x0
|
||||
× ℂ [ y1 ∘ f ] ≡ x1
|
||||
{ Object = Σ[ X ∈ ℂ.Object ] ℂ.Arrow X 𝓐 × ℂ.Arrow X 𝓑
|
||||
; Arrow = λ{ (A , a0 , a1) (B , b0 , b1)
|
||||
→ Σ[ f ∈ ℂ.Arrow A B ]
|
||||
ℂ [ b0 ∘ f ] ≡ a0
|
||||
× ℂ [ b1 ∘ f ] ≡ a1
|
||||
}
|
||||
; identity = λ{ {X , f , g} → ℂ.identity {X} , ℂ.rightIdentity , ℂ.rightIdentity}
|
||||
; _<<<_ = λ { {_ , a0 , a1} {_ , b0 , b1} {_ , c0 , c1} (f , f0 , f1) (g , g0 , g1)
|
||||
|
|
@ -176,7 +176,7 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
|
|||
open import Cat.Equivalence using (composeIso) renaming (_≅_ to _≅_)
|
||||
step0
|
||||
: ((X , xa , xb) ≡ (Y , ya , yb))
|
||||
≅ (Σ[ p ∈ (X ≡ Y) ] (PathP (λ i → ℂ.Arrow (p i) A) xa ya) × (PathP (λ i → ℂ.Arrow (p i) B) xb yb))
|
||||
≅ (Σ[ p ∈ (X ≡ Y) ] (PathP (λ i → ℂ.Arrow (p i) 𝓐) xa ya) × (PathP (λ i → ℂ.Arrow (p i) 𝓑) xb yb))
|
||||
step0
|
||||
= (λ p → cong fst p , cong-d (fst ∘ snd) p , cong-d (snd ∘ snd) p)
|
||||
-- , (λ x → λ i → fst x i , (fst (snd x) i) , (snd (snd x) i))
|
||||
|
|
@ -203,12 +203,12 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
|
|||
p
|
||||
|
||||
step1
|
||||
: (Σ[ p ∈ (X ≡ Y) ] (PathP (λ i → ℂ.Arrow (p i) A) xa ya) × (PathP (λ i → ℂ.Arrow (p i) B) xb yb))
|
||||
: (Σ[ p ∈ (X ≡ Y) ] (PathP (λ i → ℂ.Arrow (p i) 𝓐) xa ya) × (PathP (λ i → ℂ.Arrow (p i) 𝓑) xb yb))
|
||||
≅ Σ (X ℂ.≊ Y) (λ iso
|
||||
→ let p = ℂ.isoToId iso
|
||||
in
|
||||
( PathP (λ i → ℂ.Arrow (p i) A) xa ya)
|
||||
× PathP (λ i → ℂ.Arrow (p i) B) xb yb
|
||||
( PathP (λ i → ℂ.Arrow (p i) 𝓐) xa ya)
|
||||
× PathP (λ i → ℂ.Arrow (p i) 𝓑) xb yb
|
||||
)
|
||||
step1
|
||||
= symIso
|
||||
|
|
@ -216,7 +216,7 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
|
|||
{A = (X ℂ.≊ Y)}
|
||||
{B = (X ≡ Y)}
|
||||
(ℂ.groupoidObject _ _)
|
||||
{Q = \ p → (PathP (λ i → ℂ.Arrow (p i) A) xa ya) × (PathP (λ i → ℂ.Arrow (p i) B) xb yb)}
|
||||
{Q = \ p → (PathP (λ i → ℂ.Arrow (p i) 𝓐) xa ya) × (PathP (λ i → ℂ.Arrow (p i) 𝓑) xb yb)}
|
||||
ℂ.isoToId
|
||||
(symIso (_ , ℂ.asTypeIso {X} {Y}) .snd)
|
||||
)
|
||||
|
|
@ -225,8 +225,8 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
|
|||
: Σ (X ℂ.≊ Y) (λ iso
|
||||
→ let p = ℂ.isoToId iso
|
||||
in
|
||||
( PathP (λ i → ℂ.Arrow (p i) A) xa ya)
|
||||
× PathP (λ i → ℂ.Arrow (p i) B) xb yb
|
||||
( PathP (λ i → ℂ.Arrow (p i) 𝓐) xa ya)
|
||||
× PathP (λ i → ℂ.Arrow (p i) 𝓑) xb yb
|
||||
)
|
||||
≅ ((X , xa , xb) ≊ (Y , ya , yb))
|
||||
step2
|
||||
|
|
@ -243,10 +243,10 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
|
|||
iso = fst f , fst f~ , cong fst inv-f , cong fst inv-f~
|
||||
p : X ≡ Y
|
||||
p = ℂ.isoToId iso
|
||||
pA : ℂ.Arrow X A ≡ ℂ.Arrow Y A
|
||||
pA = cong (λ x → ℂ.Arrow x A) p
|
||||
pB : ℂ.Arrow X B ≡ ℂ.Arrow Y B
|
||||
pB = cong (λ x → ℂ.Arrow x B) p
|
||||
pA : ℂ.Arrow X 𝓐 ≡ ℂ.Arrow Y 𝓐
|
||||
pA = cong (λ x → ℂ.Arrow x 𝓐) p
|
||||
pB : ℂ.Arrow X 𝓑 ≡ ℂ.Arrow Y 𝓑
|
||||
pB = cong (λ x → ℂ.Arrow x 𝓑) p
|
||||
k0 = begin
|
||||
coe pB xb ≡⟨ ℂ.coe-dom iso ⟩
|
||||
xb ℂ.<<< fst f~ ≡⟨ snd (snd f~) ⟩
|
||||
|
|
@ -264,10 +264,10 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
|
|||
(Σ≡ refl (ℂ.propIsomorphism _ _ _)))
|
||||
, funExt (λ{ (f , _) → lemSig propIsomorphism _ _ (Σ≡ refl (propEqs _ _ _))})
|
||||
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
|
||||
prop0 : ∀ {x} → isProp (PathP (λ i → ℂ.Arrow (ℂ.isoToId x i) 𝓐) xa ya)
|
||||
prop0 {x} = pathJ (λ y p → ∀ x → isProp (PathP (λ i → ℂ.Arrow (p i) 𝓐) xa x)) (λ x → ℂ.arrowsAreSets _ _) Y (ℂ.isoToId x) ya
|
||||
prop1 : ∀ {x} → isProp (PathP (λ i → ℂ.Arrow (ℂ.isoToId x i) 𝓑) xb yb)
|
||||
prop1 {x} = pathJ (λ y p → ∀ x → isProp (PathP (λ i → ℂ.Arrow (p i) 𝓑) 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
|
||||
|
|
@ -297,34 +297,34 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
|
|||
|
||||
open Category cat
|
||||
|
||||
lemma : Terminal ≃ Product ℂ A B
|
||||
lemma = fromIsomorphism Terminal (Product ℂ A B) (f , g , inv)
|
||||
lemma : Terminal ≃ Product ℂ 𝓐 𝓑
|
||||
lemma = fromIsomorphism Terminal (Product ℂ 𝓐 𝓑) (f , g , inv)
|
||||
where
|
||||
f : Terminal → Product ℂ A B
|
||||
f : Terminal → Product ℂ 𝓐 𝓑
|
||||
f ((X , x0 , x1) , uniq) = p
|
||||
where
|
||||
rawP : RawProduct ℂ A B
|
||||
rawP : RawProduct ℂ 𝓐 𝓑
|
||||
rawP = record
|
||||
{ object = X
|
||||
; fst = x0
|
||||
; snd = x1
|
||||
}
|
||||
-- open RawProduct rawP renaming (fst to x0 ; snd to x1)
|
||||
module _ {Y : ℂ.Object} (p0 : ℂ [ Y , A ]) (p1 : ℂ [ Y , B ]) where
|
||||
module _ {Y : ℂ.Object} (p0 : ℂ [ Y , 𝓐 ]) (p1 : ℂ [ Y , 𝓑 ]) where
|
||||
uy : isContr (Arrow (Y , p0 , p1) (X , x0 , x1))
|
||||
uy = uniq {Y , p0 , p1}
|
||||
open Σ uy renaming (fst to Y→X ; snd to contractible)
|
||||
open Σ Y→X renaming (fst to p0×p1 ; snd to cond)
|
||||
ump : ∃![ f×g ] (ℂ [ x0 ∘ f×g ] ≡ p0 P.× ℂ [ x1 ∘ f×g ] ≡ p1)
|
||||
ump = p0×p1 , cond , λ {y} x → let k = contractible (y , x) in λ i → fst (k i)
|
||||
isP : IsProduct ℂ A B rawP
|
||||
isP : IsProduct ℂ 𝓐 𝓑 rawP
|
||||
isP = record { ump = ump }
|
||||
p : Product ℂ A B
|
||||
p : Product ℂ 𝓐 𝓑
|
||||
p = record
|
||||
{ raw = rawP
|
||||
; isProduct = isP
|
||||
}
|
||||
g : Product ℂ A B → Terminal
|
||||
g : Product ℂ 𝓐 𝓑 → Terminal
|
||||
g p = o , t
|
||||
where
|
||||
module p = Product p
|
||||
|
|
@ -375,7 +375,7 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
|
|||
inv : AreInverses f g
|
||||
inv = funExt ve-re , funExt re-ve
|
||||
|
||||
propProduct : isProp (Product ℂ A B)
|
||||
propProduct : isProp (Product ℂ 𝓐 𝓑)
|
||||
propProduct = equivPreservesNType {n = ⟨-1⟩} lemma Propositionality.propTerminal
|
||||
|
||||
module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} {A B : Category.Object ℂ} where
|
||||
|
|
|
|||
Loading…
Reference in a new issue