[Agda] formalization of category theory

[Thorsten Altenkirch]

Hi Vag,

I am afraid I agree with Wolfgang. The indexed way is more in the  
spirit of Type Theory while using partial application seems to be the  
natural choice if you work in an algebraic framework.

Btw, can you show that both definitions are equivalent, i.e. give  
translations in both directions and show that there composites lead to  
equivalent categories in the appropriate sense.

Cheers,
Thorsten

On 17 Jun 2010, at 08:42, Vag Vagoff wrote:

> > record Cat (l : Level) : Set (S l) where
> >  field
> >   Ob     : Set l
> >   Arrow  : Ob → Ob → Set l
> >   id     : ∀ {o1} → (Arrow o1 o1)
> >   comp   : ∀ {o1 o2 o3} → (Arrow o2 o3) → (Arrow o1 o2) →  
> (Arrow o1 o3)
>
> It is more convenient to define category without mentioning objects:
>
> record CategoryWO (Ar : Set) : Set where
>    field
>        _∘_ : Ar → Ar → Maybe Ar
>    infix 90 _∘_
>    field
>        idR : ∀ f → ∃ λ g → f ∘ g ≡ just f
>        idL : ∀ f → ∃ λ g → g ∘ f ≡ just f
>        identity : ∀ {f g} → Ex f ∘ g → un∃ (idL g) ≡  
> un∃ (idR f)
>        composition : ∀ {f g h} → Ex f ∘ g → Ex g ∘ h → Ex  
> f ∘ h
>        associativity : ∀ {f g h fg gh} → f ∘ g ≡ just fg →  
> g ∘ h ≡ just gh → fg ∘ h ≡ f ∘ gh
>
> -- or --
>
> record CategoryWO' (Ar : Set) : Set where
>    field
>        _∘_ : Maybe Ar → Maybe Ar → Maybe Ar
>        undefR : ∀ {f} → f ∘ nothing ≡ nothing
>        undefL : ∀ {f} → nothing ∘ f ≡ nothing
>    infix 90 _∘_
>    field
>        idR : ∀ f → ∃ λ g → f ∘ g ≡ f
>        idL : ∀ f → ∃ λ g → g ∘ f ≡ f
>        identity : ∀ {f g} → Ex f ∘ g → un∃ (idL g) ≡  
> un∃ (idR f)
>        composition : ∀ {f g h} → Ex f ∘ g → Ex g ∘ h → Ex  
> f ∘ h
>        associativity : ∀ {f g h} → (f ∘ g) ∘ h ≡ f ∘ (g  
> ∘ h)
>
>
> Isn't it?
> <Pub.agda>_______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda