module data1 where

data _∨_ (A B : Set) : Set where
  p1 : A → A ∨ B
  p2 : B → A ∨ B

ex1 : {A B : Set} → A → ( A ∨ B ) 
ex1 = {!!}

ex2 : {A B : Set} → B → ( A ∨ B ) 
ex2 = {!!}

ex3 : {A B : Set} → ( A ∨ A ) → A 
ex3 = {!!}

ex4 : {A B C : Set} →  A ∨ ( B ∨ C ) → ( A ∨  B ) ∨ C 
ex4 = {!!}

record _∧_ A B : Set where
  field
     π1 : A
     π2 : B

open _∧_

--- ex5 :  {A B C : Set} →  (( A → C ) ∨ ( B  → C ) ) → ( ( A ∨  B ) → C ) is wrong
ex5 :  {A B C : Set} →  (( A → C ) ∨ ( B  → C ) ) → ( ( A ∧  B ) → C )
ex5 = {!!}

data Three : Set where
  t1 : Three
  t2 : Three
  t3 : Three

open Three

infixl 110 _∨_ 


data 3Ring : (dom cod : Three) → Set where
   r1 : 3Ring t1 t2
   r2 : 3Ring t2 t3
   r3 : 3Ring t3 t1

data Nat : Set where
  zero : Nat
  suc  : Nat →  Nat

add : ( a b : Nat ) → Nat
add zero x = x
add (suc x) y = suc ( add x y )

mul : ( a b : Nat ) → Nat
mul zero x = {!!}
mul (suc x) y = {!!}

ex6 : Nat
ex6 = mul ( suc ( suc zero)) (suc ( suc ( suc zero)) )


data ⊥ : Set where

⊥-elim : {A : Set } -> ⊥ -> A
⊥-elim ()

¬_ : Set → Set
¬ A = A → ⊥


data connected { V : Set } ( E : V -> V -> Set ) ( x y : V ) : Set  where
   direct :   E x y -> connected E x y
   indirect :  { z : V  } -> E x z  ->  connected {V} E z y -> connected E x y

dag :  { V : Set } ( E : V -> V -> Set ) ->  Set
dag {V} E =  ∀ (n : V)  →  ¬ ( connected E n n )

lemma : ¬ (dag 3Ring )
lemma r = r t1 ( indirect r1 (indirect r2 (direct r3 )))