fredefox/cat
1
0
Fork 0
Code Issues Pull requests Releases Wiki Activity

Add type-synonym

Browse source
This commit is contained in:
Frederik Hanghøj Iversen 2018-05-29 15:14:46 +02:00
parent 392d656709
commit 6d362af88e
1 changed files with 16 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

35
src/Cat/Categories/Span.agda
View file

@ -71,9 +71,20 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb)
open Σ 𝕐 renaming (fst to Y ; snd to y) open Σ 𝕐 renaming (fst to Y ; snd to y)
open Σ y renaming (fst to ya ; snd to yb) open Σ y renaming (fst to ya ; snd to yb)
open import Cat.Equivalence using (composeIso) renaming (_≅_ to _≅_) open import Cat.Equivalence using (composeIso) renaming (_≅_ to _≅_)
step0
: ((X , xa , xb) ≡ (Y , ya , yb)) -- The proof will be a sequence of isomorphisms between the
≅ (Σ[ p ∈ (X ≡ Y) ] (PathP (λ i → ℂ.Arrow (p i) 𝒜) xa ya) × (PathP (λ i → ℂ.Arrow (p i) ℬ) xb yb)) -- following 4 types:
T0 = ((X , xa , xb) ≡ (Y , ya , yb))
T1 = (Σ[ p ∈ (X ≡ Y) ] (PathP (λ i → ℂ.Arrow (p i) 𝒜) xa ya) × (PathP (λ i → ℂ.Arrow (p i) ℬ) xb yb))
T2 = Σ (X ℂ.≊ Y) (λ iso
→ let p = ℂ.isoToId iso
in
( PathP (λ i → ℂ.Arrow (p i) 𝒜) xa ya)
× PathP (λ i → ℂ.Arrow (p i) ℬ) xb yb
)
T3 = ((X , xa , xb) ≊ (Y , ya , yb))
step0 : T0 ≅ T1
step0 step0
= (λ p → cong fst p , cong-d (fst ∘ snd) p , cong-d (snd ∘ snd) p) = (λ 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)) -- , (λ x → λ i → fst x i , (fst (snd x) i) , (snd (snd x) i))
@ -81,14 +92,7 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb)
, funExt (λ{ p → refl}) , funExt (λ{ p → refl})
, funExt (λ{ (p , q , r) → refl}) , funExt (λ{ (p , q , r) → refl})
step1 step1 : T1 ≅ T2
: (Σ[ 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) 𝒜) xa ya)
× PathP (λ i → ℂ.Arrow (p i) ℬ) xb yb
)
step1 step1
= symIso = symIso
(isoSigFst (isoSigFst
@ -100,14 +104,7 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb)
(symIso (_ , ℂ.asTypeIso {X} {Y}) .snd) (symIso (_ , ℂ.asTypeIso {X} {Y}) .snd)
) )
step2 step2 : T2 ≅ T3
: Σ (X ℂ.≊ Y) (λ iso
→ let p = ℂ.isoToId iso
in
( PathP (λ i → ℂ.Arrow (p i) 𝒜) xa ya)
× PathP (λ i → ℂ.Arrow (p i) ℬ) xb yb
)
≅ ((X , xa , xb) ≊ (Y , ya , yb))
step2 step2
= ( λ{ (iso@(f , f~ , inv-f) , p , q) = ( λ{ (iso@(f , f~ , inv-f) , p , q)
→ ( f , sym (ℂ.domain-twist-sym iso p) , sym (ℂ.domain-twist-sym iso q)) → ( f , sym (ℂ.domain-twist-sym iso p) , sym (ℂ.domain-twist-sym iso q))