module PLFA.Connectives where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open Eq.≡-Reasoning
open import Data.Nat using (ℕ)
open import Function using (_∘_)
open import PLFA.Isomorphism using (_≃_; _≲_; extensionality)
open PLFA.Isomorphism.≃-Reasoning








-- * -- Important principle: Propositions as Types

--  conjunction <-> product
--  disjunction <-> sum
--  truth       <-> unit type
--  falsity     <-> empty type
--  implication <-> function space




















-- * -- conjunction <-> product
-- _×_; <_,_> ; proj₁ ; proj₂ ; η-×

data _×_ (A B : Set) : Set where
  <_,_> :
    A → 
    B → 
    ----------
    A × B

-- in type theory, this rule is called
-- "product introduction" or "×-I"

_ : ℕ × ℕ
_ = < 17 , 4 >

-- the dual operation i s"elimination"

proj₁ : ∀ {A B} →
  A × B →
  ----------
  A
proj₁ < a , b > = a

proj₂ : ∀ {A B} →
  A × B →
  ----------
  B
proj₂ < a , b > = b

-- these (derived) rules are the elimination rules, called "×-E₁" and "×-E₂"

η-× : ∀ {A B} → (w : A × B) → w ≡ < proj₁ w , proj₂ w >
η-× < a , b > = refl

-- Cartesian product
-- ×-comm ; ×-assoc

data Bool : Set where
  True False : Bool

data Tri : Set where
  aa bb cc : Tri

_ : Bool × Tri
_ = < False , cc >

-- there 2 * 3 elements in Bool × Tri

×-comm : ∀ {A B} → (A × B) ≃ (B × A)
×-comm = record {
  to      = λ{ < a , b > → < b , a > };
  from    = λ{ < b , a > → < a , b > };
  from∘to = λ{ < a , b > → refl };
  to∘from = λ{ < b , a > → refl }
  }

×-assoc : ∀ {A B C} → (A × (B × C)) ≃ ((A × B) × C)
×-assoc = record {
  to = λ{ < a , < b , c > > → < < a , b > , c > };
  from = λ{ < < a , b > , c > →  < a , < b , c > > };
  from∘to = λ{ < a , < b , c > > → refl };
  to∘from = λ{ < < a , b > , c > → refl }
  }

infixr 2 _×_





















-- * -- truth       <-> unit type
-- ⊤ ; η-⊤; ⊤-identityˡ ; ⊤-identityʳ 

-- truth introduction

data ⊤ : Set where
  tt : ⊤


η-⊤ : (w : ⊤) → w ≡ tt
η-⊤ tt = refl

-- type ⊤ behaves like a unit with respect to product (just like 1 for multiplication)

⊤-identityʳ : ∀ {A} → A × ⊤ ≃ A
⊤-identityʳ = record {
  to = proj₁ ;
  from = λ a → < a , tt > ;
  from∘to = λ{ < a , tt > → refl };
  to∘from = λ a → refl
  }

⊤-identityˡ : ∀ {A} → ⊤ × A ≃ A
⊤-identityˡ {A} = ≃-begin
              ((⊤ × A)
              ≃⟨ ×-comm ⟩
              (A × ⊤)
              ≃⟨ ⊤-identityʳ ⟩
              (A 
              ≃-∎))












-- * -- disjunction <-> sum
-- _⊎_ ; inj₁ ; inj₂ ; case-⊎ ; η-⊎

data _⊎_ (A B : Set) : Set where

  inj₁ :
    A →
    ----------
    A ⊎ B

  inj₂ :
    B →
    ----------
    A ⊎ B

-- these are the introduction rules for sum types, sometimes called "⊎-IL" "⊎-IR"
-- we also need elimination

case-⊎ : ∀ {A B C : Set} → (A → C) → (B → C) → (A ⊎ B) → C
case-⊎ f g (inj₁ a) = f a
case-⊎ f g (inj₂ b) = g b

-- the eta principle for sums:
η-⊎ : ∀ {A B : Set} → (w : A ⊎ B) → (case-⊎ inj₁ inj₂ w ≡ w)
η-⊎ (inj₁ a) = refl
η-⊎ (inj₂ b) = refl

infixr 1 _⊎_

-- ⊎-comm ; ⊎-assoc
postulate
  ⊎-comm : ∀ {A B} → A ⊎ B ≃ B ⊎ A
  ⊎-assoc : ∀ {A B C} → A ⊎ B ⊎ C ≃ (A ⊎ B) ⊎ C









{-
Q: So you can always get two different A⊎B from A x B?
A: A × B is the set of pairs { < a , b > | a ∈ A, b ∈ B }
   A ⊎ B is { inj₁ a | a ∈ A } ∪ { inj₂ b | b ∈ B }
Q: And A⊎B is never A and B simultaneously?
A:YES!
-}












-- * -- falsity     <-> empty type
-- ⊥ ; ⊥-elim

data ⊥ : Set where

-- also called "bottom"
-- "ex falso quolibet"
⊥-elim : ∀ {A : Set} →
  ⊥ →
  -----
  A
⊥-elim ()

-- this is called an "absurd pattern"

postulate
  ext : ∀ {A B : Set}{f g : A → B} → (∀ x → f x ≡ g x) → f ≡ g

unit-⊥ : ∀ {A : Set} → (f : ⊥ → A) → f ≡ ⊥-elim
unit-⊥ f = ext (λ{ () })

-- further:  ⊥-identityˡ ; ⊥-identityʳ

⊥-identityˡ : ∀ {A} → ⊥ ⊎ A ≃ A
⊥-identityˡ = record {
  to = λ{ (inj₂ a) → a };
  from = inj₂ ;
  from∘to = λ{ (inj₂ a) → refl };
  to∘from = λ a → refl
  }

⊥-identityʳ : ∀ {A} → A ⊎ ⊥ ≃ A
⊥-identityʳ = record {
  to = case-⊎ (λ a → a) ⊥-elim ;
  from = inj₁ ;
  from∘to = λ{ (inj₁ a) → refl } ;
  to∘from = λ a → refl
  }


















-- * -- implication <-> function space
-- →-elim ; η-→

→-elim : ∀ {A B : Set} →
  (A → B) →
  A → 
  ----------
  B
-- this is "modus ponens"

→-elim f a = f a

-- →-introduction corresponds to λ abstaction
-- (x : A) B
-- --------------------
-- λ (x : A) e : A → B

η-→ : ∀ {A B : Set} → (w : A → B) → w ≡ λ (x : A) → w x
η-→ w = refl

-- in terms of number of elements in a finite set, | A -> B | = | B | ^ | A |

bt0 : Bool → Tri
bt0 True = aa                 -- three choices here
bt0 False = aa                -- three choices here
-- total of 3 * 3 = 3^2 choices

tb0 : Tri → Bool
tb0 aa = True                   -- two choices here
tb0 bb = True                   -- two choices here
tb0 cc = True                   -- two choices here
-- total of 2 * 2 * 2 = 2^3 choices

-- currying ; →-distrib-⊎ ; →-distrib-×

-- currying
-- (A × B) → C  ≃   A → (B → C)

-- in terms of number of elements:

-- c ^ (a * b)  =  (c ^ b) ^ a

currying : ∀ {A B C} → ((A × B) → C)  ≃ (A → (B → C))
currying = record {
  to = λ f a b → f < a , b > ;
  from = λ{ f < a , b > → f a b };
  from∘to = λ f → ext (λ{ < a , b > → refl }) ;
  to∘from = λ f → ext (λ x → refl)
  }

-- c ^ (a + b) = c^a * c^b
-- (A ⊎ B) → C ≃ (A → C) × (B → C)

















-- * -- further laws
-- ×-distrib-⊎ ; ⊎-distrib-× (embedding)