5f.agda

module 5f where

postulate
  A : Set
  B : Set

postulate
  a′ : A
  b′ : B

module r where
  record AB : Set where
    field
      a : A
      b : B

  t₀ : AB
  t₀ = record { a = a′ ; b = b′ }

  postulate
    ab : AB

  t₁ : A
  t₁ = AB.a ab

  t₂ : B
  t₂ = AB.b ab

module d where
  data AB : Set where
    prod : (a′ : A) → B → AB

  t₀ : AB
  t₀ = prod a′ b′

data Gender : Set where
  female : Gender
  male   : Gender

data FemaleName : Set where
  jill : FemaleName
  sara : FemaleName

data MaleName : Set where
  tom : MaleName
  jim : MaleName

Name : Gender → Set
Name male   = MaleName
Name female = FemaleName

record NameWithGender : Set where
  field
    gender : Gender
    name   : Name gender

t₀ : NameWithGender
t₀ = record { gender = male; name = tom }

t₁ : NameWithGender
t₁ = record { gender = male; name = {!!} }

record ∃r (A : Set) (B : A → Set) : Set where
  field
    a : A
    b : B a

data ∃d (A : Set) (B : A → Set) : Set where
  exists : (a : A) → B a → ∃d A B

---------------------------- Example ----------------------------

open import Data.Bool                             using (Bool; not; true; false)
open import Data.Product                          using (∃; _,_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; cong; inspect; [_])

lem₁ : ∀ (a : Bool) → ∃ λ (b : Bool) → a ≡ not b
lem₁ = {!!}

open import Relation.Binary.Core              using (Symmetric)
open import Relation.Binary.Product.Pointwise using (_×-Rel_)

sym-≡ : {A : Set} → Symmetric (_≡_ {A = A})
sym-≡ {i = x} {j = y} x≡y = sym x≡y

lem₂ : {A B : Set} {_~A_ : A → A → Set} {_~B_ : B → B → Set}
       → Symmetric _~A_
       → Symmetric _~B_
       → Symmetric (_~A_ ×-Rel _~B_)
lem₂ symA symB = {!!}

---------------------------- Exercise ----------------------------

Injective : {A B : Set} → (A → B) → Set
Injective f = ∀ x y → f x ≡ f y → x ≡ y

_LeftInverseOf_ : {A B : Set} → (B → A) → (A → B) → Set
_LeftInverseOf_ g f = ∀ x → g (f x) ≡ x 

ex₁ : ∀ (f : Bool → Bool)
      → Injective f
      → ∃ (λ g → g LeftInverseOf f)
ex₁ = {!!}