----------------------------------------------------------------------
-- This Agda code is designed to accompany the paper "Axioms for
-- Modelling Cubical Type Theory in a Topos". It is currently a work
-- in progress and still includes postulates/holes in certain places.
-- It also needs some tidying up and possibily reorganisation.
--
-- The idea for getting an impredicative universe of propositions Ω
-- comes from Martin Escardo, more details can be found at:
--
--          http://www.cs.bham.ac.uk/~mhe/impredicativity/          
----------------------------------------------------------------------

module prelude where

open import Agda.Primitive public

infix  1 Σ proof:_
infixr 2 _≡[_]≡_
infix  3 _qed
infixr 3 _,_
infixr 5  _×_ _∘_ _⊎_

----------------------------------------------------------------------
-- Identity function
----------------------------------------------------------------------
id : {A : Set}  A  A
id x = x

----------------------------------------------------------------------
-- Composition
----------------------------------------------------------------------
_∘_ :
  { m n : Level}
  {A : Set }
  {B : Set m}
  {C : Set n}
  (g : B  C)
  (f : A  B)
   -------------
  A  C
(g  f) x = g (f x)

----------------------------------------------------------------------
-- Propositional equality
----------------------------------------------------------------------
open import Agda.Builtin.Equality public

trans :
  { : Level}
  {A : Set }
  {x y z : A}
  (q : y  z)
  (p : x  y)
   ---------
  x  z
trans q refl = q

symm :
  { : Level}
  {A : Set }
  {x y : A}
  (p : x  y)
   ---------
  y  x
symm refl = refl

cong :
  { ℓ' : Level}
  {A : Set }
  {B : Set ℓ'}
  (f : A  B)
  {x y : A}
  (p : x  y)
   -----------
  f x  f y
cong _ refl = refl

cong₂ :
  { ℓ' : Level}
  {A A' : Set }
  {B : Set ℓ'}
  (f : A  A'  B)
  {x y  : A}
  {x' y' : A'}
  (p : x  y)
  (q : x'  y')
   --------------
  f x x'  f y y'
cong₂ _ refl refl = refl

subst :
  { ℓ' : Level}
  {A  : Set }
  (B : A  Set ℓ')
  {x y : A}
  (p : x  y)
   --------------
  B x  B y
subst _  refl = λ b  b

congdep :
  { ℓ' : Level}
  {A : Set }
  {B : A  Set ℓ'}
  (f : (a : A)  B a)
  {x y : A}
  (p : x  y)
   -----------
  subst B p (f x)  f y
congdep _ refl = refl

substconst :
  { ℓ' : Level}
  {A : Set }
  (B : Set ℓ')
  {x y : A}
  (p : x  y)
  (b : B)
   ------------------------
  (subst  _  B) p) b  b
substconst _ refl _ = refl

subst₂ :
  { ℓ' : Level}
  {A  A' : Set }
  (B : A  A'  Set ℓ')
  {x y  : A}
  {x' y' : A'}
  (p : x  y)
  (p' : x'  y')
   ------------------
  B x x'  B y y'
subst₂ _ refl refl = λ b  b

uip :
  { : Level}
  {A : Set }
  {x y : A}
  (p q : x  y)
   -----------
  p  q
uip refl refl = refl

uipImp :
  { : Level}
  {A : Set }
  {x y : A}
  {p q : x  y}
   -----------
  p  q
uipImp {p = refl} {q = refl} = refl

appCong :
  { ℓ' : Level}
  {A : Set }
  {B : Set ℓ'}
  {f g : A  B}
  {x : A}
  (p : f  g)
   -----------
  f x  g x
appCong refl = refl

----------------------------------------------------------------------
-- Equational reasoning
----------------------------------------------------------------------
proof:_ :
  { : Level}
  {A : Set }
  {x y : A}
   ---------------------
  x  y  x  y
proof: p = p

_≡[_]≡_ :
  { : Level}
  {A : Set }
  (x : A)
  {y z : A}
   -------------------
  x  y  y  z  x  z
_ ≡[ p ]≡ q = trans q p  

_qed :
  { : Level}
  {A : Set }
  (x : A)
   ---------
  x  x
_qed _ = refl

----------------------------------------------------------------------
-- Type coersion
----------------------------------------------------------------------
coe : {A B : Set}  A  B  A  B
coe refl = id

----------------------------------------------------------------------
-- Empty type
----------------------------------------------------------------------
data  : Set where

∅-elim :
  { : Level}
  {A : Set }
   ---------
    A
∅-elim ()

----------------------------------------------------------------------
-- One-element type
----------------------------------------------------------------------
open import Agda.Builtin.Unit renaming ( to Unit) public

----------------------------------------------------------------------
-- Booleans
----------------------------------------------------------------------
open import Agda.Builtin.Bool renaming (Bool to 𝔹) public

----------------------------------------------------------------------
-- Natural Numbers
----------------------------------------------------------------------
open import Agda.Builtin.Nat renaming (Nat to ) public

----------------------------------------------------------------------
-- Disjoint union
----------------------------------------------------------------------
data _⊎_ { m : Level}(A : Set )(B : Set m) : Set (  m) where
  inl : A  A  B
  inr : B  A  B

----------------------------------------------------------------------
-- Dependent products
----------------------------------------------------------------------
record Σ { m : Level} (A : Set ) (B : A  Set m) : Set (  m) where
  constructor _,_
  field
    fst : A
    snd : B fst

open Σ public

syntax Σ A  x  B) = Σ x ∈ A , B

_×_ : { m : Level}  Set   Set m  Set (  m)
A × B = Σ A  _  B)

Σext :
  { m : Level}
  {A : Set }
  {B : A  Set m}
  {x x' : A}
  {y : B x}
  {y' : B x'}
  (p : x  x')
  (q : subst B p y  y')
   --------------------
  (x , y)  (x' , y')
Σext refl refl = refl

Σeq₁ :
  { ℓ' : Level}
  {A  : Set }
  {B : A  Set ℓ'}
  {x y : Σ A B}
  (p : x  y)
   --------------
  fst x  fst y
Σeq₁ refl = refl

Σeq₂ :
  { ℓ' : Level}
  {A  : Set }
  {B : A  Set ℓ'}
  {x y : Σ A B}
  (p : x  y)
   --------------
  subst B (Σeq₁ p) (snd x)  snd y
Σeq₂ refl = refl