Skip to content

Instantly share code, notes, and snippets.

@gallais
Last active Aug 29, 2015
Embed
What would you like to do?
Categories.Fam generalized
module Categories.Fam where
open import Level
import Function as Fun
open import Data.Product
open import Relation.Binary
open import Categories.Category
open import Categories.Support.EqReasoning
open import Categories.Support.PropositionalEquality
module Fam {o m e : Level} (ℂ : Category o m e) {ℓ : Level} where
module C = Category ℂ
record Fam : Set (suc ℓ ⊔ o) where
constructor _,_
field
U : Set
T : U C.Obj
open Fam public
record Hom (A B : Fam) : Set (ℓ ⊔ m) where
constructor _,_
field
f : U A U B
φ : (x : U A) T A x C.⇒ T B (f x)
ΣFam : (A : Set ℓ) (B : A Fam) -> Fam
ΣFam A B = Σ A (U Fun.∘ B) , uncurry (T Fun.∘ B)
inΣ : {A : Set ℓ} {B : A Fam} (a : A) Hom (B a) (ΣFam A B)
inΣ a = _,_ a , λ _ C.id
outΣ : (A : Set ℓ) {B : A Fam} {C : Fam}
(p : (a : A) Hom (B a) C) Hom (ΣFam A B) C
outΣ A p = uncurry (Hom.f Fun.∘ p) , uncurry (Hom.φ Fun.∘ p)
syntax outΣ A (λ a p) = [ p ][ a ∈ A ]
record _≡Fam_ {X Y} (f g : (Hom X Y)) : Set (ℓ ⊔ e ⊔ m) where
constructor _,_
field
f≡g : {x : U X} Hom.f f x ≣ Hom.f g x
φ≡γ : {x : U X}
let rew = ≣-subst (λ y T X x C.⇒ T Y y) f≡g
in rew (Hom.φ f x) C.≡ Hom.φ g x
module Eq = _≡Fam_
cong : {ℓ m e} {A : Set ℓ} {x y₁ y₂ : A} (P : A Set m)
(R : {y₁ y₂} P y₁ P y₂ Set e) (eq : y₁ ≣ y₂) {γ₁ : P y₁} {γ₂}
R γ₁ γ₂ R (≣-subst P eq γ₁) (≣-subst P eq γ₂)
cong P R ≣-refl pr = pr
switch : {ℓ m o} {A : Set ℓ} (P : A Set o) (R : {x} P x P x Set m)
{x y : A} (eq : y ≣ x) {γ : P x} {ρ : P y}
R γ (≣-subst P eq ρ) R (≣-subst P (≣-sym eq) γ) ρ
switch P R ≣-refl rel = rel
switch⁻¹ : {ℓ m o} {A : Set ℓ} (P : A Set o) (R : {x} P x P x Set m)
{x y : A} (eq : x ≣ y) {γ : P x} {ρ : P y}
R (≣-subst P eq γ) ρ R γ (≣-subst P (≣-sym eq) ρ)
switch⁻¹ P R ≣-refl rel = rel
fuse : {ℓ m o} {A : Set ℓ} (P : A Set o) (R : {x} P x P x Set m)
{x y z : A} (eq₁ : x ≣ y) (eq₂ : y ≣ z) {γ : P x} {ρ : P z}
R (≣-subst P eq₂ (≣-subst P eq₁ γ)) ρ
R (≣-subst P (≣-trans eq₁ eq₂) γ) ρ
fuse P R ≣-refl ≣-refl rel = rel
skip : {ℓ m o} {A : Set ℓ} (P : A Set o) (R : {x} P x P x Set m)
{x y : A} (eq : x ≣ y) {γ ρ : P x}
R γ ρ R (≣-subst P eq γ) (≣-subst P eq ρ)
skip P R ≣-refl rel = rel
Cat : Category (suc ℓ ⊔ o) (ℓ ⊔ m) (ℓ ⊔ e ⊔ m)
Cat = record { Obj = Fam
; _⇒_ = Hom
; _≡_ = _≡Fam_
; id = id′
; _∘_ = _∘′_
; assoc = ≣-refl , C.assoc
; identityˡ = ≣-refl , C.identityˡ
; identityʳ = ≣-refl , C.identityʳ
; equiv = record { refl = refl′
; sym = sym′
; trans = trans′ }
; ∘-resp-≡ = ∘-resp-≡′ }
where
id′ : {A : Fam} Hom A A
id′ = Fun.id , λ x C.id
_∘′_ : {A B C : Fam} (g : Hom B C) (f : Hom A B) Hom A C
(U₂ , T₂) ∘′ (U₁ , T₁) = (U₂ Fun.∘ U₁) , λ x T₂ (U₁ x) C.∘ T₁ x
.refl′ : {A B} Reflexive (_≡Fam_ {A} {B})
refl′ = ≣-refl , IsEquivalence.refl C.equiv
.sym′ : {A B} Symmetric (_≡Fam_ {A} {B})
sym′ {U₁ , T₁} {U₂ , T₂} {f , φ} {g , γ} (f≡g , φ≡γ) =
≣-sym f≡g , λ {x}
switch (λ y T₁ x C.⇒ T₂ y) C._≡_ f≡g Fun.$ IsEquivalence.sym C.equiv φ≡γ
.trans′ : {A B} Transitive (_≡Fam_ {A} {B})
trans′ {U₁ , T₁} {U₂ , T₂} {f , φ} {g , γ} {h , δ} (f≡g , φ≡γ) (g≡h , γ≡δ) =
≣-trans f≡g g≡h , λ {x}
fuse (λ y T₁ x C.⇒ T₂ y) C._≡_ f≡g g≡h Fun.$
IsEquivalence.trans C.equiv (skip (λ y T₁ x C.⇒ T₂ y) C._≡_ g≡h φ≡γ) γ≡δ
.∘-resp-≡′ : {A B C : Fam} {f h : Hom B C} {g i : Hom A B}
f ≡Fam h g ≡Fam i (f ∘′ g) ≡Fam (h ∘′ i)
∘-resp-≡′ {U₁ , T₁} {U₂ , T₂} {U₃ , T₃} {f , φ} {g , γ} {h , η} {i , ι}
(f≡g , φ≡γ) (h≡i , η≡ι) =
≣-trans f≡g (≣-cong g h≡i) , λ {x}
IsEquivalence.trans C.equiv
(IsEquivalence.trans C.equiv
(skip (λ y T₁ x C.⇒ T₃ y) C._≡_ (≣-trans f≡g (≣-cong g h≡i))
(C.∘-resp-≡
(switch⁻¹ (λ y T₂ (h x) C.⇒ T₃ y) C._≡_ f≡g φ≡γ)
(switch⁻¹ (λ y T₁ x C.⇒ T₂ y) C._≡_ h≡i η≡ι))) {!!})
(C.∘-resp-≡ φ≡γ η≡ι)
{-
open Category Cat public
Fam : {o m e : Level} (a : Level) (ℂ : Category o m e) → Category _ _ _
Fam a ℂ = Fam.Cat ℂ {a}
open import Categories.Agda
FamSet : (ℓ : Level) → Category _ _ _
FamSet ℓ = Fam ℓ Fun.$ Sets ℓ
-}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment