module record1 where

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

open _∧_

ex1 : {A B : Set} → ( A ∧ B ) → A 
ex1 a∧b = {!!}

ex2 : {A B : Set} → ( A ∧ B ) → B 
ex2 a∧b = {!!}

ex3 : {A B : Set} → A → B → ( A ∧ B ) 
ex3 a b = {!!}

ex4 : {A B : Set} → A → ( A ∧ A ) 
ex4 a  = record { π1 = {!!} ;  π2 = {!!} }

ex5 : {A B C : Set} → ( A ∧ B ) ∧ C  →  A ∧ (B ∧ C) 
ex5 a∧b∧c = record { π1 = {!!} ; π2 = {!!} }

ex6 : {A B C : Set} → ( (A → B ) ∧ ( B →  C) )  → A → C
ex6  =  {!!}