{-# OPTIONS --without-K #-}

open import library.Basics hiding (Type ; Σ)
open import library.types.Sigma

module Sec2preliminaries where

-- is-prop, is-contr, is-set, has-dec-eq exist in library.Basicss

-- Let us redefine Type and Σ so that they only refer to the lowest universe.
Type = Type₀
Σ = library.Basics.Σ {lzero} {lzero} 

_+_ : Type  Type  Type
X + Y = Coprod X Y

const : {X Y : Type}  (f : X  Y)  Type
const {X} f = (x₁ x₂ : X)  (f x₁) == (f x₂)

coll : Type  Type
coll X = Σ (X  X) const

pathColl : Type  Type
pathColl X = (x₁ x₂ : X)  coll (x₁ == x₂)

LEM : Type₁
LEM = (P : Type)  is-prop P  P + (¬ P)

LEM∞ : Type₁
LEM∞ = (X : Type)  X + (¬ X)

Funext : {X Y : Type}  Type
Funext {X} {Y} = (f g : X  Y)  ((x : X)  (f x) == (g x))  f == g


-- In the rest of this file, we define several auxiliary notations or lemmata that are not mentioned 
-- explicitly in the article but are somewhat self-explaining.

-- for convenience, we also define ↔ to mean logical equivalence (maps in both directions)
_↔_ : Type  Type  Type
X  Y = (X  Y) × (Y  X)

-- we define it for types in the higher universe separately 
-- (because most of the time, we only need the lowest universe and do not want to carry around indices)
_↔₀₁_ : Type  Type₁  Type₁
A ↔₀₁ B = (A  B) × (B  A)

_↔₁₁_ : Type₁  Type₁  Type₁
X ↔₁₁ Y = (X  Y) × (Y  X)

-- composition of ↔
_◎_ : {X Y Z : Type}  (X  Y)  (Y  Z)  (X  Z) 
e₁  e₂ = fst e₂  fst e₁ , snd e₁  snd e₂

-- A trivial, but useful lemma. The only thing we do is hiding the arguments.
prop-eq-triv : {P : Type}  {p₁ p₂ : P}  is-prop P  p₁ == p₂
prop-eq-triv h = prop-has-all-paths h _ _

-- A second such useful lemma
second-comp-triv : {X : Type}  {P : X  Type}  ((x : X)  is-prop (P x))  (a b : Σ X P)  (fst a == fst b)  a == b
second-comp-triv {X} {P} h a b q = pair= q (from-transp P q (prop-eq-triv (h (fst b))))

open import library.types.Pi

-- Note that this lemma needs function extensionality (we use Π-level).
neutral-codomain : {X : Type}  {Y : X  Type}  ((x : X)  is-contr (Y x))  Π X Y  Unit
neutral-codomain = contr-equiv-Unit  Π-level

-- the following is the function which the univalence axiom postulates to be an equivalence
-- (we define it ourselves as we do not want to implicitly import the whole univalence library)
path-to-equiv : {X Y : Type}  X == Y  X  Y
path-to-equiv {X} idp = ide X

-- some rather silly lemmata

delete-idp : {X : Type}  {x₁ x₂ : X}  (p q : x₁ == x₂)  (p  idp == q)  (p == q)
delete-idp idp q = ide _

add-path : {X : Type}  {x₁ x₂ x₃ : X}  (p q : x₁ == x₂)  (r : x₂ == x₃)  (p == q) == (p  r == q  r)
add-path idp q idp = transport  q₁  (idp == q₁) == (idp == q  idp)) {x = q  idp} {y = q} (∙-unit-r _) idp

open import library.types.Paths

reverse-paths : {X : Type}  {x₁ x₂ : X}  (p : x₂ == x₁)  (q : x₁ == x₂)  (! p == q)  (p == ! q)
reverse-paths p idp = 
  ! p == idp   ≃⟨ path-to-equiv (add-path _ _ _) 
  ! p  p == p ≃⟨ path-to-equiv (transport  p₁  (! p  p == p) == (p₁ == p)) (!-inv-l p) idp) 
  idp == p     ≃⟨ !-equiv 
  p == idp     ≃∎

switch-args : {X Y : Type}  {Z : X  Y  Type}  ((x : X)  (y : Y)  Z x y)  ((y : Y)  (x : X)  Z x y)
switch-args = equiv f g h₁ h₂ where
  f = λ k y x  k x y
  g = λ i x y  i y x
  h₁ = λ _  idp
  h₂ = λ _  idp


-- another useful (but simple) lemma: if we have a proof of (x , y₁) == (x , y₂) and the type of x is a set, we get a proof of y₁ == y₂.
set-lemma : {X : Type}  (is-set X)  {Y : X  Type}  (x₀ : X)  (y₁ y₂ : Y x₀)  _==_ {A = Σ X Y} (x₀ , y₁) (x₀ , y₂)  y₁ == y₂
set-lemma {X} h {Y} x₀ y₁ y₂ p = 
  y₁ =⟨ idp 
  transport Y idp        y₁ =⟨ transport {A = x₀ == x₀}  q  y₁ == transport Y q y₁) 
                                 {x = idp} {y = ap fst p} 
                                 (prop-has-all-paths (h x₀ x₀) _ _) 
                                 idp 
  transport Y (ap fst p) y₁ =⟨ snd-of-p 
  y₂  where
    pairs :  {B = Y} (x₀ , y₁) (x₀ , y₂)
    pairs = <– (=Σ-eqv _ _) p

    paov : y₁ == y₂ [ Y  fst (pairs) ]
    paov = snd pairs

    snd-of-p : transport Y (ap fst p) y₁ == y₂
    snd-of-p = to-transp paov