Categories.Fam generalized

Fam.agda

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 ℓ
-}