### view CCC.agda @ 787:ca5eba647990

...
author Shinji KONO Thu, 18 Apr 2019 20:07:22 +0900 a67959bcd44b 4e1e2f7199c8
line wrap: on
line source
```
open import Level
open import Category
module CCC where

open import HomReasoning
open import cat-utility
open  import  Relation.Binary.PropositionalEquality

open import HomReasoning

record IsCCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
( １ : Obj A )
( ○ : (a : Obj A ) → Hom A a １ )
( _∧_ : Obj A → Obj A → Obj A  )
( <_,_> : {a b c : Obj A } → Hom A c a → Hom A c b → Hom A c (a ∧ b)  )
( π : {a b : Obj A } → Hom A (a ∧ b) a )
( π' : {a b : Obj A } → Hom A (a ∧ b) b )
( _<=_ : (a b : Obj A ) → Obj A )
( _* : {a b c : Obj A } → Hom A (a ∧ b) c → Hom A a (c <= b) )
( ε : {a b : Obj A } → Hom A ((a <= b ) ∧ b) a )
:  Set ( c₁  ⊔  c₂ ⊔ ℓ ) where
field
-- cartesian
e2  : {a : Obj A} → ∀ ( f : Hom A a １ ) →  A [ f ≈ ○ a ]
e3a : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } →  A [ A [ π o < f , g > ] ≈ f ]
e3b : {a b c : Obj A} → { f : Hom A c a }{ g : Hom A c b } →  A [ A [ π' o < f , g > ] ≈ g ]
e3c : {a b c : Obj A} → { h : Hom A c (a ∧ b) } →  A [ < A [ π o h ] , A [ π' o h  ] >  ≈ h ]
π-cong :  {a b c : Obj A} → { f f' : Hom A c a }{ g g' : Hom A c b } → A [ f ≈ f' ]  → A [ g ≈ g' ]  →  A [ < f , g >  ≈ < f' , g' > ]
-- closed
e4a : {a b c : Obj A} → { h : Hom A (c ∧ b) a } →  A [ A [ ε o < A [ (h *) o π ]  ,  π' > ] ≈ h ]
e4b : {a b c : Obj A} → { k : Hom A c (a <= b ) } →  A [ ( A [ ε o < A [ k o  π ]  ,  π' > ] ) * ≈ k ]
*-cong :  {a b c : Obj A} → { f f' : Hom A (a ∧ b) c } → A [ f ≈ f' ]  → A [  f *  ≈  f' * ]

e'2 : A [ ○ １ ≈ id1 A １ ]
e'2 = let open  ≈-Reasoning A in begin
○ １
≈↑⟨ e2 (id1 A １ ) ⟩
id1 A １
∎
e''2 : {a b : Obj A} {f : Hom A a b } → A [ A [  ○ b o f ] ≈ ○ a ]
e''2 {a} {b} {f} = let open  ≈-Reasoning A in begin
○ b o f
≈⟨ e2 (○ b o f) ⟩
○ a
∎
distr : {a b c d : Obj A} {f : Hom A c a }{g : Hom A c b } {h : Hom A d c } → A [ A [ < f , g > o h ]  ≈  < A [ f o h ] , A [ g o h ] > ]
distr {a} {b} {c} {d} {f} {g} {h} = let open  ≈-Reasoning A in begin
< f , g > o h
≈↑⟨ e3c ⟩
< π o  < f , g > o h  , π' o  < f , g > o h  >
≈⟨ π-cong assoc assoc ⟩
< ( π o  < f , g > ) o h  , (π' o  < f , g > ) o h  >
≈⟨ π-cong (car e3a ) (car e3b) ⟩
< f o h ,  g o h  >
∎
_×_ :  {  a b c d e : Obj A } ( f : Hom A a d ) (g : Hom A b e ) ( h : Hom A c (a ∧ b) ) → Hom A c ( d ∧ e )
f × g  = λ h →  < A [ f o A [ π o h  ] ] , A [ g o A [ π' o h ] ] >

record CCC {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) :  Set ( c₁  ⊔  c₂ ⊔ ℓ ) where
field
１ : Obj A
○ : (a : Obj A ) → Hom A a １
_∧_ : Obj A → Obj A → Obj A
<_,_> : {a b c : Obj A } → Hom A c a → Hom A c b → Hom A c (a ∧ b)
π : {a b : Obj A } → Hom A (a ∧ b) a
π' : {a b : Obj A } → Hom A (a ∧ b) b
_<=_ : (a b : Obj A ) → Obj A
_* : {a b c : Obj A } → Hom A (a ∧ b) c → Hom A a (c <= b)
ε : {a b : Obj A } → Hom A ((a <= b ) ∧ b) a
isCCC : IsCCC A １ ○ _∧_ <_,_> π π' _<=_ _* ε

```