{-# OPTIONS --universe-polymorphism #-}
module IProp where
open import Level
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 ⊢_ {l : Level}(X : Set l) : Set l where
pf : .X → ⊢ X
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
postulate
extensionality : {A : Set}{B : A → Set}{f g : (a : A) → B a} →
((x : A) → ⊢ (f x ≡ g x)) → ⊢ (f ≡ g)
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} {A : Set a} {B : Set b}
(f : A → B) {x y} → ⊢ (x ≡ y) → ⊢ (f x ≡ f y)
cong⊢ f (pf x≡y) = pf (cong f x≡y)
open import Data.Bool