RelIso.agda

{-# OPTIONS --cubical --safe --postfix-projections #-}

module Nominal where

  open import Cubical.Foundations.Everything
    renaming (isOfHLevel to IsOfHLevel; isProp to IsProp)
    hiding (_∘_)
  open import Cubical.HITs.PropositionalTruncation
  open import Data.Nat hiding (_⊔_)
  open import Function.Base
  open import Level renaming (suc to sucℓ)

  record HType (n : ℕ) a : Type (sucℓ a) where
    constructor htype
    field
      [_] : Type a
      hLevel : IsOfHLevel n [_]
  open HType public

  HProp = HType 1
  HSet = HType 2

  Rel : ∀ {a b} (A : Type a) (B : Type b) (r : Level) → Type (a ⊔ b ⊔ sucℓ r)
  Rel A B r = A → B → HProp r

  module _ {a b c r s} {A : Type a} {B : Type b} {C : Type c} where

    infix 6 _◆_ _◇_

    -- Relation composition
    record _◆_ (R : Rel A B r) (S : Rel B C s) (x : A) (z : C)
               : Type (b ⊔ r ⊔ s) where
      constructor _,_
      field
        {middle} : B
        left : [ R x middle ]
        right : [ S middle z ]
    open _◆_ public

    -- In general, the squashing is necessary, because there are many choices
    -- for `middle`.
    _◇_ : Rel A B r → Rel B C s → Rel A C (b ⊔ r ⊔ s)
    (R ◇ S) x z = htype ∥ (R ◆ S) x z ∥ squash

    ◆-ext : {R : Rel A B r} {S : Rel B C s} {x : A} {z : C} →
            {c d : (R ◆ S) x z} → c .middle ≡ d .middle → c ≡ d
    ◆-ext p i .middle = p i
    ◆-ext {R = R} {x = x} {c = c} {d} p i .left =
      isProp→PathP (λ i → R x (p i) .hLevel) (c .left) (d .left) i
    ◆-ext {S = S} {z = z} {c = c} {d} p i .right =
      isProp→PathP (λ i → S (p i) z .hLevel) (c .right) (d .right) i

  Id : ∀ {a} (A : HSet a) → Rel [ A ] [ A ] a
  Id A x y = htype (x ≡ y) (A .hLevel x y)

  record RelIso {ℓ} (A B : HSet ℓ) : Type (sucℓ ℓ) where
    field
      to : Rel [ A ] [ B ] ℓ
      from : Rel [ B ] [ A ] ℓ
      to-from : to ◇ from ≡ Id A
      from-to : from ◇ to ≡ Id B

  infixl 5 _>>_
  _>>_ : ∀ {a b c} {A : Type a} {B : Type b} {C : Type c} →
         (A → B) → (B → C) → (A → C)
  (f >> g) x = g (f x)

  record SetIso {ℓ} (A B : HSet ℓ) : Type (sucℓ ℓ) where
    field
      to : [ A ] → [ B ]
      from : [ B ] → [ A ]
      to-from : to >> from ≡ id
      from-to : from >> to ≡ id

  module _ where
    open RelIso
    open SetIso

    RelIso→SetIso : ∀ {ℓ} {A B : HSet ℓ} → RelIso A B → SetIso A B
    RelIso→SetIso i .to x =
      rec isProp id (subst (λ T → [ T x x ]) (sym (i .to-from)) refl) .middle
      module To where
      isProp : IsProp ((i .to ◆ i .from) x x)
      isProp c d = ◆-ext
        (subst (λ T → [ T (c .middle) (d .middle) ]) (i .from-to)
               ∣ c .right , d .left ∣)
    RelIso→SetIso i .from y =
      rec isProp id (subst (λ T → [ T y y ]) (sym (i .from-to)) refl) .middle
      module From where
      isProp : IsProp ((i .from ◆ i .to) y y)
      isProp c d = ◆-ext
        (subst (λ T → [ T (c .middle) (d .middle) ]) (i .to-from)
               ∣ c .right , d .left ∣)
    RelIso→SetIso {A = A} i .to-from = funExt λ x → elim
      {P = λ z → from-i (rec (To.isProp i x) id z .middle) ≡ x}
      (λ _ → A .hLevel _ _)
      (λ (_,_ {y} to-l to-r) → elim
        {P = λ z → rec (From.isProp i y) id z .middle ≡ x}
        (λ _ → A .hLevel _ _)
        (λ (_,_ {z} from-l from-r) →
          subst (λ T → [ T z x ]) (i .to-from) ∣ from-r , to-r ∣)
        (subst (λ T → [ T y y ]) (sym (i .from-to)) refl))
      (subst (λ T → [ T x x ]) (sym (i .to-from)) refl)
      where
      to-i = RelIso→SetIso i .to
      from-i = RelIso→SetIso i .from
    RelIso→SetIso {B = B} i .from-to = funExt λ x → elim
      {P = λ z → to-i (rec (From.isProp i x) id z .middle) ≡ x}
      (λ _ → B .hLevel _ _)
      (λ (_,_ {y} from-l from-r) → elim
        {P = λ z → rec (To.isProp i y) id z .middle ≡ x}
        (λ _ → B .hLevel _ _)
        (λ (_,_ {z} to-l to-r) →
          subst (λ T → [ T z x ]) (i .from-to) ∣ to-r , from-r ∣)
        (subst (λ T → [ T y y ]) (sym (i .to-from)) refl))
      (subst (λ T → [ T x x ]) (sym (i .from-to)) refl)
      where
      to-i = RelIso→SetIso i .to
      from-i = RelIso→SetIso i .from