[Agda] formalization of category theory

[Thorsten Altenkirch]

P.S.
Actually, to partially answer my own question: This doesn't seem to be  
the case since the natural definition of Ar would be Ar = Σ (A B :  
Obj) Arrow A B (not official Agda Syntax) and then you can only define  
partial composition, if equality of objects is decidable.

Thorsten

On 20 Jun 2010, at 16:34, Thorsten Altenkirch wrote:

> 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
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda