| 123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960 |
- {-# OPTIONS --type-in-type #-}
- module Nested where
- record Σ₁ (A : Set)(B : A → Set) : Set where
- constructor _,_
- field fst : A
- snd : B fst
- infixr 2 _,_
- record Σ (A : Set)(B : A → Set) : Set where
- field p : Σ₁ A B
- open Σ₁ p public
- open Σ
- data ⊤ : Set where
- tt : ⊤
- ∃ : {A : Set}(B : A → Set) → Set
- ∃ B = Σ _ B
- infix 10 _≡_
- data _≡_ {A : Set}(a : A) : {B : Set} → B → Set where
- refl : a ≡ a
- Cat : Set
- Cat =
- ∃ λ (Obj : Set) →
- ∃ λ (Hom : Obj → Obj → Set) →
- ∃ λ (id : ∀ X → Hom X X) →
- ∃ λ (_○_ : ∀ {X Y Z} → Hom Y Z → Hom X Y → Hom X Z) →
- ∃ λ (idl : ∀ {X Y}{f : Hom X Y} → (id Y ○ f) ≡ f) →
- ∃ λ (idr : ∀ {X Y}{f : Hom X Y} → (f ○ id X) ≡ f) →
- ∃ λ (assoc : ∀ {W X Y Z}{f : Hom W X}{g : Hom X Y}{h : Hom Y Z} →
- ((h ○ g) ○ f) ≡ (h ○ (g ○ f))) →
- ⊤
- Obj : (C : Cat) → Set
- Obj C = fst C
- Hom : (C : Cat) → Obj C → Obj C → Set
- Hom C = fst (snd C)
- id : (C : Cat) → ∀ X → Hom C X X
- id C = fst (snd (snd C))
- comp : (C : Cat) → ∀ {X Y Z} → Hom C Y Z → Hom C X Y → Hom C X Z
- comp C = fst (snd (snd (snd C)))
- idl : (C : Cat) → ∀ {X Y}{f : Hom C X Y} → comp C (id C Y) f ≡ f
- idl C = fst (snd (snd (snd (snd C))))
- idr : (C : Cat) → ∀ {X Y}{f : Hom C X Y} → comp C f (id C X) ≡ f
- idr C = fst (snd (snd (snd (snd (snd C)))))
- assoc : (C : Cat) → ∀ {W X Y Z}{f : Hom C W X}{g : Hom C X Y}{h : Hom C Y Z} →
- comp C (comp C h g) f ≡ comp C h (comp C g f)
- assoc C = fst (snd (snd (snd (snd (snd (snd C))))))
|
