open import Level
renaming ( zero to zeroL
; suc to sucL )
module Chapter2.IProp where
open import Data.Empty
open import Data.Unit
open import Data.Product
open import Data.Nat
open import Category.Applicative
open import Category.Applicative.Indexed
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.PropositionalEquality.TrustMe
infixr 1 ⊢_
data ⊢_ {ℓ : Level} (X : Set ℓ) : Set ℓ where
pf : .X → ⊢ X
postulate
extensionality : ∀{k ℓ}{A : Set k}{B : A → Set ℓ}{f g : (a : A) → B a} →
((x : A) → ⊢ (f x ≡ g x)) → ⊢ (f ≡ g)
module Applicative {ℓ : Level} where
Applicative⊢ : RawApplicative ⊢_
Applicative⊢ = record { pure = pf
; _⊛_ = _⊛_ }
where _⊛_ : {A B : Set ℓ} → ⊢ (A → B) → ⊢ A → ⊢ B
(pf f) ⊛ (pf a) = pf (f a)
open RawIApplicative Applicative⊢ public
pf-irrelevance : {A : Set ℓ}
(a : ⊢ A)(b : ⊢ A) → ⊢ (a ≡ b)
pf-irrelevance (pf _) (pf _) = pf refl
trans⊢ : {A : Set ℓ}{a b c : A} → ⊢ (a ≡ b) → ⊢ (b ≡ c) → ⊢ (a ≡ c)
trans⊢ (pf x) (pf y) = pf (trans x y)
subst⊢ : {A B : Set ℓ}(P : A → Set ℓ){x y : A} → ⊢ (x ≡ y) → ⊢ (P x) → ⊢ (P y)
subst⊢ f (pf x≡y) (pf Px) = pf (subst f x≡y Px)
cong⊢ : ∀ {A B : Set ℓ}
(f : A → B) {x y} → ⊢ (x ≡ y) → ⊢ (f x ≡ f y)
cong⊢ f (pf x≡y) = pf (cong f x≡y)
open Applicative public