text:
------------------------------------------------------------------------
-- Admissible rules are sometimes not "postulable"
------------------------------------------------------------------------

-- Even though a rule is admissible it may not be sound to postulate
-- it, i.e. add it as an inductive constructor. This was observed by
-- Edsko de Vries in a message to the Coq-club mailing list (Re:
-- [Coq-Club] Adding (inductive) transitivity to weak bisimilarity not
-- sound? (was: Need help with coinductive proof), 2009-08-28).

module AdmissibleButNotPostulable where

open import Codata.Musical.Notation using (∞; ♯_; ♭)
open import Data.Nat
open import Data.Product as Prod
open import Function
open import Relation.Binary.PropositionalEquality as P using (_≡_; [_])
open import Relation.Nullary using (¬_)

------------------------------------------------------------------------
-- The partiality monad

data _⊥ (A : Set) : Set where
  now   : (v : A) → A ⊥
  later : (x : ∞ (A ⊥)) → A ⊥

------------------------------------------------------------------------
-- Weak equality of computations in the partiality monad

module WeakEquality where

  infix 4 _≈_

  data _≈_ {A : Set} : A ⊥ → A ⊥ → Set where
    now    : ∀ {v}                         → now   v ≈ now   v
    later  : ∀ {x y} (x≈y : ∞ (♭ x ≈ ♭ y)) → later x ≈ later y
    laterʳ : ∀ {x y} (x≈y :      x ≈ ♭ y ) →       x ≈ later y
    laterˡ : ∀ {x y} (x≈y :    ♭ x ≈   y ) → later x ≈       y

  -- Some lemmas.

  laterʳ⁻¹ : ∀ {A : Set} {x : A ⊥} {y} → x ≈ later y → x ≈ ♭ y
  laterʳ⁻¹ (later  x≈y)  = laterˡ        (♭ x≈y)
  laterʳ⁻¹ (laterʳ x≈y)  = x≈y
  laterʳ⁻¹ (laterˡ x≈ly) = laterˡ (laterʳ⁻¹ x≈ly)

  laterˡ⁻¹ : ∀ {A : Set} {x} {y : A ⊥} → later x ≈ y → ♭ x ≈ y
  laterˡ⁻¹ (later  x≈y)  = laterʳ         (♭ x≈y)
  laterˡ⁻¹ (laterʳ lx≈y) = laterʳ (laterˡ⁻¹ lx≈y)
  laterˡ⁻¹ (laterˡ x≈y)  = x≈y

  -- Weak equality is an equivalence relation.

  refl : {A : Set} (x : A ⊥) → x ≈ x
  refl (now v)   = now
  refl (later x) = later (♯ refl (♭ x))

  sym : {A : Set} {x y : A ⊥} → x ≈ y → y ≈ x
  sym now          = now
  sym (later  x≈y) = later (♯ sym (♭ x≈y))
  sym (laterʳ x≈y) = laterˡ (sym x≈y)
  sym (laterˡ x≈y) = laterʳ (sym x≈y)

  trans : {A : Set} {x y z : A ⊥} → x ≈ y → y ≈ z → x ≈ z
  trans {x = now v} {z = z} p q = tr p q
    where
    tr : ∀ {y} → now v ≈ y → y ≈ z → now v ≈ z
    tr now          y≈z  = y≈z
    tr (laterʳ v≈y) ly≈z = tr v≈y (laterˡ⁻¹ ly≈z)
  trans {x = later x} lx≈y y≈z = tr lx≈y y≈z
    where
    tr : ∀ {y z} → later x ≈ y → y ≈ z → later x ≈ z
    tr         lx≈ly (later  y≈z) = later  (♯ trans (laterˡ⁻¹ lx≈ly) (laterˡ (♭ y≈z)))
    tr         lx≈y  (laterʳ y≈z) = later  (♯ trans (laterˡ⁻¹ lx≈y)             y≈z  )
    tr         lx≈ly (laterˡ y≈z) =           tr    (laterʳ⁻¹ lx≈ly)            y≈z
    tr (laterˡ  x≈y)         y≈z  = laterˡ (  trans            x≈y              y≈z  )

  -- Non-termination.

  never : {A : Set} → A ⊥
  never = later (♯ never)

  -- Weak equality is not trivial (assuming that the argument to _⊥ is
  -- non-empty).

  non-trivial : {A : Set} {v : A} → ¬ now v ≈ never
  non-trivial (laterʳ v≈⊥) = non-trivial v≈⊥

------------------------------------------------------------------------
-- Extended weak equality

module ExtendedWeakEquality where

  infix  4 _≈_
  infix  3 _∎
  infixr 2 _≈⟨_⟩_

  -- Let us try to postulate transitivity using an inductive rule.

  data _≈_ {A : Set} : A ⊥ → A ⊥ → Set where
    now    : ∀ {v}                         → now   v ≈ now   v
    later  : ∀ {x y} (x≈y : ∞ (♭ x ≈ ♭ y)) → later x ≈ later y
    laterʳ : ∀ {x y} (x≈y :      x ≈ ♭ y ) →       x ≈ later y
    laterˡ : ∀ {x y} (x≈y :    ♭ x ≈   y ) → later x ≈       y

    -- Transitivity.
    _≈⟨_⟩_ : ∀ x {y z} (x≈y : x ≈ y) (y≈z : y ≈ z) → x ≈ z

  -- Reflexivity.

  _∎ : {A : Set} (x : A ⊥) → x ≈ x
  now   v ∎ = now
  later x ∎ = later (♯ (♭ x ∎))

  -- Extended weak equality is trivial.

  trivial : {A : Set} (x y : A ⊥) → x ≈ y
  trivial x y =
    x           ≈⟨ laterʳ (x ∎)           ⟩
    later (♯ x) ≈⟨ later  (♯ trivial x y) ⟩
    later (♯ y) ≈⟨ laterˡ (y ∎)           ⟩
    y           ∎

  -- The problem is that there is no "contractive" proof of
  -- transitivity; the proof given above consumes the input
  -- certificate "faster" than it produces the output certificate.

------------------------------------------------------------------------
-- Capretta's definition of equality coincides with weak equality

-- This is not really related to the problem discussed above, I just
-- want to ensure that the definition of weak equality is not too
-- strange.

module Capretta'sEquality where

  infix 4 _⇓_ _≈_

  -- x ⇓ v means that x terminates with the value v.

  data _⇓_ {A : Set} : A ⊥ → A → Set where
    now   : ∀ {v} → now v ⇓ v
    later : ∀ {x v} (x⇓v : ♭ x ⇓ v) → later x ⇓ v

  -- Equality as defined by Capretta in "General Recursion via
  -- Coinductive Types".

  data _≈_ {A : Set} : A ⊥ → A ⊥ → Set where
    now   : ∀ {x y v} (x⇓v : x ⇓ v) (y⇓v : y ⇓ v) → x ≈ y
    later : ∀ {x y} (x≈y : ∞ (♭ x ≈ ♭ y)) → later x ≈ later y

  -- Soundness.

  open WeakEquality using () renaming (_≈_ to _≋_)

  sound : {A : Set} {x y : A ⊥} → x ≈ y → x ≋ y
  sound (later x≈y)   = WeakEquality.later (♯ sound (♭ x≈y))
  sound (now x⇓v y⇓v) = nw x⇓v y⇓v
    where
    nw : ∀ {A : Set} {x y : A ⊥} {v} → x ⇓ v → y ⇓ v → x ≋ y
    nw now         now         = WeakEquality.now
    nw x⇓v         (later y⇓v) = WeakEquality.laterʳ (nw x⇓v y⇓v)
    nw (later x⇓v) y⇓v         = WeakEquality.laterˡ (nw x⇓v y⇓v)

  -- Completeness.

  data _≈P_ {A : Set} : A ⊥ → A ⊥ → Set where
    now    : ∀ {x y v} (x⇓v : x ⇓ v) (y⇓v : y ⇓ v) → x ≈P y
    later  : ∀ {x y} (x≈y : ∞ (♭ x ≈P ♭ y)) → later x ≈P later y
    laterʳ : ∀ {x y} (x≈y :      x ≈P ♭ y ) →       x ≈P later y
    laterˡ : ∀ {x y} (x≈y :    ♭ x ≈P   y ) → later x ≈P       y

  data _≈W_ {A : Set} : A ⊥ → A ⊥ → Set where
    now   : ∀ {x y v} (x⇓v : x ⇓ v) (y⇓v : y ⇓ v) → x ≈W y
    later : ∀ {x y} (x≈y : ♭ x ≈P ♭ y) → later x ≈W later y

  laterʳW : ∀ {A : Set} {x : A ⊥} {y} → x ≈W ♭ y → x ≈W later y
  laterʳW {y = y} x≈y with ♭ y | P.inspect ♭ y
  laterʳW x≈y | y′ | [ eq ] with x≈y
  laterʳW x≈y | y′ | [ eq ] | now {v = v} x⇓v y⇓v =
    now x⇓v (later (P.subst (λ y → y ⇓ v) (P.sym eq) y⇓v))
  laterʳW x≈y | later y′ | [ eq ] | later x′≈y′ =
    later (P.subst (_≈P_ _) (P.sym eq) (laterʳ x′≈y′))

  laterˡW : ∀ {A : Set} {x} {y : A ⊥} → ♭ x ≈W y → later x ≈W y
  laterˡW {x = x} x≈y with ♭ x | P.inspect ♭ x
  laterˡW x≈y | x′ | [ eq ] with x≈y
  laterˡW x≈y | x′ | [ eq ] | now {v = v} x⇓v y⇓v =
    now (later (P.subst (λ x → x ⇓ v) (P.sym eq) x⇓v)) y⇓v
  laterˡW x≈y | later x′ | [ eq ] | later {y = y′} x′≈y′ =
    later (P.subst (λ x → x ≈P ♭ y′) (P.sym eq) (laterˡ x′≈y′))

  whnf : {A : Set} {x y : A ⊥} → x ≈P y → x ≈W y
  whnf (now x⇓v y⇓v) = now x⇓v y⇓v
  whnf (later  x≈y)  = later (♭ x≈y)
  whnf (laterʳ x≈y)  = laterʳW (whnf x≈y)
  whnf (laterˡ x≈y)  = laterˡW (whnf x≈y)

  mutual

    ⟦_⟧W : {A : Set} {x y : A ⊥} → x ≈W y → x ≈ y
    ⟦ now x⇓v y⇓v ⟧W = now x⇓v y⇓v
    ⟦ later x≈y   ⟧W = later (♯ ⟦ x≈y ⟧P)

    ⟦_⟧P : {A : Set} {x y : A ⊥} → x ≈P y → x ≈ y
    ⟦ x≈y ⟧P = ⟦ whnf x≈y ⟧W

  complete : {A : Set} {x y : A ⊥} → x ≋ y → x ≈ y
  complete x≋y = ⟦ completeP x≋y ⟧P
    where
    completeP : {A : Set} {x y : A ⊥} → x ≋ y → x ≈P y
    completeP WeakEquality.now          = now now now
    completeP (WeakEquality.later x≈y)  = later (♯ completeP (♭ x≈y))
    completeP (WeakEquality.laterʳ x≈y) = laterʳ (completeP x≈y)
    completeP (WeakEquality.laterˡ x≈y) = laterˡ (completeP x≈y)

------------------------------------------------------------------------
-- The weak equality above coincides with weak bisimilarity

module WeakBisimilarity {A : Set} where

  -- The function drop n drops n later constructors (if possible).

  drop : ℕ → A ⊥ → A ⊥
  drop zero    x         = x
  drop _       (now v)   = now v
  drop (suc n) (later x) = drop n (♭ x)

  -- Weak simulations and bisimulations. The removal of a later
  -- constructor is treated as a silent transition.

  record IsWeakSimulation (_R_ : A ⊥ → A ⊥ → Set) : Set where
    field
      match-later : ∀ {x y} → later x R y → ∃ λ n → ♭ x   R drop n y
      match-now   : ∀ {v y} → now v   R y → ∃ λ n → now v ≡ drop n y

  record IsWeakBisimulation (_R_ : A ⊥ → A ⊥ → Set) : Set where
    field
      left  : IsWeakSimulation _R_
      right : IsWeakSimulation (flip _R_)

  -- Weak bisimilarity.

  record _≈_ (x y : A ⊥) : Set₁ where
    field
      _R_   : A ⊥ → A ⊥ → Set
      xRy   : x R y
      bisim : IsWeakBisimulation _R_

  open WeakEquality hiding (module _≈_) renaming (_≈_ to _≋_)

  -- Completeness.

  complete : ∀ {x y} → x ≋ y → x ≈ y
  complete x≋y = record
    { _R_   = _≋_
    ; xRy   = x≋y
    ; bisim = record
      { left = record
        { match-later = λ lx≋y → (0 , laterˡ⁻¹ lx≋y)
        ; match-now   = match-now
        }
      ; right = record
        { match-later = λ x≋ly → (0 , laterʳ⁻¹ x≋ly)
        ; match-now   = match-now ∘ sym
        }
      }
    }
    where
    match-now : ∀ {v y} → now v ≋ y → ∃ λ n → now v ≡ drop n y
    match-now now          = (0 , P.refl)
    match-now (laterʳ v≋y) = Prod.map suc id (match-now v≋y)

  -- Soundness.

  module Sound {x y} (x≈y : x ≈ y) where

    open _≈_ x≈y
    open IsWeakBisimulation
    open IsWeakSimulation

    helper₁ : ∀ {x} y → (∃ λ n → now x ≡ drop n y) → now x ≋ y
    helper₁ (now y)   (zero  , P.refl) = now
    helper₁ (now y)   (suc n , P.refl) = now
    helper₁ (later y) (zero  , ())
    helper₁ (later y) (suc n , nx≡y-n) =
      laterʳ (helper₁ (♭ y) (n , nx≡y-n))

    mutual

      helper₂ : ∀ {x} y → (∃ λ n → x R drop n y) → x ≋ y
      helper₂ y         (zero  , xRy)   = sound _ _ xRy
      helper₂ (now y)   (suc n , xRny)  = sound _ _ xRny
      helper₂ (later y) (suc n , xRy-n) =
        laterʳ (helper₂ (♭ y) (n , xRy-n))

      helper₃ : ∀ x {y} → (∃ λ n → drop (suc n) x R y) → x ≋ y
      helper₃ (now x)   (n     , nxRy)  = sound _ _ nxRy
      helper₃ (later x) (zero  , xRy)   = laterˡ (sound _ _ xRy)
      helper₃ (later x) (suc n , x-nRy) =
        laterˡ (helper₃ (♭ x) (n , x-nRy))

      sound : ∀ x y → x R y → x ≋ y
      sound (now x) y nxRy = helper₁ y $ match-now (left bisim) nxRy
      sound (later x) (now y) lxRny =
        sym $ helper₁ (later x) $ match-now (right bisim) lxRny
      sound (later x) (later y) lxRly
        with match-later (left bisim) lxRly
      ... | (suc n , xRy-n) = later (♯ helper₂ (♭ y) (n , xRy-n))
      ... | (zero  , xRly)  with match-later (right bisim) xRly
      ...   | (zero  , xRy)     = later (♯ sound _ _ xRy)
      ...   | (suc n , x-1+nRy) =
        later (♯ helper₃ (♭ x) (n , x-1+nRy))

  sound : ∀ {x y} → x ≈ y → x ≋ y
  sound x≈y = Sound.sound x≈y _ _ (_≈_.xRy x≈y)

-- Note that the problem illustrated in ExtendedWeakEquality is
-- related to the problem of weak bisimulation up to weak
-- bisimilarity. Let R be a relation which is only inhabited for the
-- pair (later (♯ x), later (♯ y)). R is a weak bisimulation up to
-- weak bisimilarity (_≈_):
--
--   later (♯ x)         R later (♯ y)
--       ↓                     =
--       x ≈ later (♯ x) R later (♯ y)
--
--   later (♯ x) R           later (♯ y)
--       =                       ↓
--   later (♯ x) R later (♯ y) ≈ y
--
-- Weak bisimilarity is transitive, so if every relation which is a
-- weak bisimulation up to weak bisimilarity were contained in weak
-- bisimilarity we would have x ≈ y for all x and y.


text:
{-# OPTIONS --universe-polymorphism #-}
open import Categories.Category
open import Categories.Object.BinaryProducts

module Categories.Object.Exponentiating {o ℓ e}
    (C : Category o ℓ e)
    (binary : BinaryProducts C)  where

open Category C
open BinaryProducts binary

import Categories.Object.Product
open Categories.Object.Product C

import Categories.Object.Product.Morphisms
open Categories.Object.Product.Morphisms C

open import Categories.Square
open GlueSquares C

import Categories.Object.Exponential
open   Categories.Object.Exponential C
  hiding (repack)
  renaming (λ-distrib to λ-distrib′)

open import Level

record Exponentiating Σ : Set (o ⊔ ℓ ⊔ e) where
    field
        exponential : ∀{A} → Exponential A Σ
    module Σ↑ (X : Obj) = Exponential (exponential {X})

    infixr 6 Σ↑_ Σ²_

    Σ↑_ : Obj → Obj
    Σ↑_ X = Σ↑.B^A X

    {-
      Γ ; x : A   ⊢ f x : Σ
      ──────────────────────────────────────   λ-abs A f
      Γ           ⊢ (λ (x : A) → f x) : Σ↑ A
     -}
    λ-abs : ∀ {Γ} A → (Γ × A) ⇒ Σ → Γ ⇒ Σ↑ A
    λ-abs {Γ} A f = Σ↑.λg A product f

    {-
      ─────────────────────────────   eval
      f : Σ↑ A ; x : A  ⊢ (f x) : Σ
     -}
    eval : {A : Obj} → (Σ↑ A × A) ⇒ Σ
    eval {A} = Σ↑.eval A ∘ repack product (Σ↑.product A)

    {-
      x : A     ⊢  f x : B
      ─────────────────────────────────────────   [Σ↑_]
      k : Σ↑ B  ⊢  (λ (x : A) → k (f x)) : Σ↑ A
    -}
    [Σ↑_] : ∀ {A B} → A ⇒ B → Σ↑ B ⇒ Σ↑ A
    [Σ↑_] {A}{B} f = λ-abs A (eval {B} ∘ second f)

    Σ²_ : Obj → Obj
    Σ²_ X = Σ↑ (Σ↑ X)

    [Σ²_] : ∀ {X Y} → X ⇒ Y → Σ² X ⇒ Σ² Y
    [Σ² f ] = [Σ↑ [Σ↑ f ] ]

    flip : ∀ {A B} → A ⇒ Σ↑ B → B ⇒ Σ↑ A
    flip {A}{B} f = λ-abs {B} A (eval {B} ∘ swap ∘ second f)

    -- not sure this is the best name... "partial-apply" might be better
    curry : ∀ {X Y} → (Σ↑ (X × Y) × X) ⇒ Σ↑ Y
    curry {X}{Y} = λ-abs Y (eval {X × Y} ∘ assocˡ)

    -- some lemmas from Exponential specialized to C's chosen products
    open Equiv
    open HomReasoning

    private
      .repack∘first : ∀ {A X}{f : X ⇒ Σ↑ A}
          → repack product (Σ↑.product A) ∘ first f
          ≡ [ product ⇒ Σ↑.product A ]first f
      repack∘first {A} = [ product ⇒ product ⇒ Σ↑.product A ]repack∘⁂

    .β : ∀{A X} {g : (X × A) ⇒ Σ}
        → eval {A} ∘ first (λ-abs A g) ≡ g
    β {A}{X}{g} =
      begin
        (Σ↑.eval A ∘ repack product (Σ↑.product A)) ∘ first (Σ↑.λg A product g)
      ↓⟨ pullʳ repack∘first ⟩
        Σ↑.eval A ∘ [ product ⇒ Σ↑.product A ]first (Σ↑.λg A product g)
      ↓⟨ Σ↑.β A product ⟩
        g
      ∎

    .λ-unique : ∀{A X} {g : (X × A) ⇒ Σ} {h : X ⇒ Σ↑ A}
        → (eval ∘ first h ≡ g)
        → (h ≡ λ-abs A g)
    λ-unique {A}{X}{g}{h} commutes
      = Σ↑.λ-unique A product commutes′
      where
      commutes′ : Σ↑.eval A ∘ [ product ⇒ Σ↑.product A ]first h ≡ g
      commutes′ =
        begin
          Σ↑.eval A ∘ [ product ⇒ Σ↑.product A ]first h
        ↑⟨ pullʳ repack∘first ⟩
          (Σ↑.eval A ∘ repack product (Σ↑.product A)) ∘ first h
        ↓⟨ commutes ⟩
          g
        ∎
    .λ-η : ∀ {A X}{f : X ⇒ Σ↑ A }
        → λ-abs A (eval ∘ first f) ≡ f
    λ-η {A}{X}{f} = sym (λ-unique refl)

    .λ-cong : ∀{A B : Obj}{f g : (B × A) ⇒ Σ}
        → (f ≡ g)
        → (λ-abs A f ≡ λ-abs A g)
    λ-cong {A} f≡g = Σ↑.λ-cong A product f≡g

    .subst : ∀ {A C D} {f : (D × A) ⇒ Σ} {g : C ⇒ D}
      → λ-abs {D} A f ∘ g
      ≡ λ-abs {C} A (f ∘ first g)
    subst {A} = Σ↑.subst A product product

    .λ-η-id : ∀ {A} → λ-abs A eval ≡ id
    λ-η-id {A} =
      begin
        Σ↑.λg A product (Σ↑.eval A ∘ repack product (Σ↑.product A))
      ↓⟨ Σ↑.λ-cong A product (∘-resp-≡ʳ (repack≡id⁂id product (Σ↑.product A))) ⟩
        Σ↑.λg A product (Σ↑.eval A ∘ [ product ⇒ Σ↑.product A ]first id)
      ↓⟨ Σ↑.η A product ⟩
        id
      ∎

    .λ-distrib : ∀ {A B C}{f : A ⇒ B}{g : (C × B) ⇒ Σ}
        → λ-abs A (g ∘ second f)
        ≡ [Σ↑ f ] ∘ λ-abs B g
    λ-distrib {A}{B}{C}{f}{g} =
      begin
        Σ↑.λg A product (g ∘ second f)
      ↓⟨ λ-distrib′ exponential exponential product product product ⟩
          Σ↑.λg A product (Σ↑.eval B ∘ [ product ⇒ Σ↑.product B ]second f)
        ∘ Σ↑.λg B product g
      ↑⟨ λ-cong (pullʳ [ product ⇒ product ⇒ Σ↑.product B ]repack∘⁂) ⟩∘⟨ refl ⟩
          Σ↑.λg A product ((Σ↑.eval B ∘ repack product (Σ↑.product B)) ∘ second f)
        ∘ Σ↑.λg B product g
      ∎

    .flip² : ∀{A B}{f : A ⇒ Σ↑ B} → flip (flip f) ≡ f
    flip² {A}{B}{f} =
      begin
        λ-abs {A} B (eval {A} ∘ swap ∘ second (flip f))
      ↓⟨ λ-cong lem₁ ⟩
        λ-abs {A} B (eval {B} ∘ first f)
      ↓⟨ λ-η ⟩
        f
      ∎
      where
      lem₁ : eval {A} ∘ swap ∘ second (flip f) ≡ eval {B} ∘ first f
      lem₁ =
        begin
          eval {A} ∘ swap ∘ second (flip f)
        ↑⟨ assoc ⟩
          (eval {A} ∘ swap) ∘ second (flip f)
        ↓⟨ glue β swap∘⁂ ⟩
          eval {B} ∘ (swap ∘ second f) ∘ swap
        ↓⟨ refl ⟩∘⟨ swap∘⁂ ⟩∘⟨ refl ⟩
          eval {B} ∘ (first f ∘ swap) ∘ swap
        ↓⟨ refl ⟩∘⟨ cancelRight swap∘swap ⟩
          eval {B} ∘ first f
        ∎

ext: agda

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
{-# OPTIONS --safe #-}
module Cubical.Data.FinData.Properties where

open import Cubical.Foundations.Function
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Powerset
open import Cubical.Foundations.Isomorphism

open import Cubical.Data.Sum
open import Cubical.Data.Sigma
open import Cubical.Data.FinData.Base as Fin
open import Cubical.Data.Nat renaming (zero to ℕzero ; suc to ℕsuc
                                      ;znots to ℕznots ; snotz to  ℕsnotz)
open import Cubical.Data.Nat.Order
open import Cubical.Data.Empty as Empty
open import Cubical.Relation.Nullary

private
 variable
   ℓ ℓ' : Level
   A : Type ℓ
   m n k : ℕ

znots : ∀{k} {m : Fin k} → ¬ (zero ≡ (suc m))
znots {k} {m} x = subst (Fin.rec (Fin k) ⊥) x m

snotz : ∀{k} {m : Fin k} → ¬ ((suc m) ≡ zero)
snotz {k} {m} x = subst (Fin.rec ⊥ (Fin k)) x m

isPropFin0 : isProp (Fin 0)
isPropFin0 = Empty.rec ∘ ¬Fin0

isContrFin1 : isContr (Fin 1)
isContrFin1 .fst = zero
isContrFin1 .snd zero = refl

injSucFin : ∀ {n} {p q : Fin n} → suc p ≡ suc q → p ≡ q
injSucFin {ℕsuc ℕzero} {zero} {zero} pf = refl
injSucFin {ℕsuc (ℕsuc n)} pf = cong predFin pf

discreteFin : ∀{k} → Discrete (Fin k)
discreteFin zero zero = yes refl
discreteFin zero (suc y) = no znots
discreteFin (suc x) zero = no snotz
discreteFin (suc x) (suc y) with discreteFin x y
... | yes p = yes (cong suc p)
... | no ¬p = no (λ q → ¬p (injSucFin q))

isSetFin : ∀{k} → isSet (Fin k)
isSetFin = Discrete→isSet discreteFin

data biEq {n : ℕ} (i j : Fin n) : Type where
  eq  :   i ≡ j → biEq i j
  ¬eq : ¬ i ≡ j → biEq i j

data triEq {n : ℕ} (i j a : Fin n) : Type where
  leq : a ≡ i → triEq i j a
  req : a ≡ j → triEq i j a
  ¬eq : (¬ a ≡ i) × (¬ a ≡ j) → triEq i j a

biEq? : (i j : Fin n) → biEq i j
biEq? i j = case (discreteFin i j) return (λ _ → biEq i j)
              of λ { (yes p) → eq p ; (no ¬p) → ¬eq ¬p }

triEq? : (i j a : Fin n) → triEq i j a
triEq? i j a =
  case (discreteFin a i) return (λ _ → triEq i j a) of
    λ { (yes p) → leq p
      ; (no ¬p) →
          case (discreteFin a j) return (λ _ → triEq i j a) of
            λ { (yes q) → req q
              ; (no ¬q) → ¬eq (¬p , ¬q) }}

weakenRespToℕ : ∀ {n} (i : Fin n) → toℕ (weakenFin i) ≡ toℕ i
weakenRespToℕ zero = refl
weakenRespToℕ (suc i) = cong ℕsuc (weakenRespToℕ i)

toℕ<n : ∀ {n} (i : Fin n) → toℕ i < n
toℕ<n {n = ℕsuc n} zero = n , +-comm n 1
toℕ<n {n = ℕsuc n} (suc i) = toℕ<n i .fst , +-suc _ _ ∙ cong ℕsuc (toℕ<n i .snd)

toFin : {n : ℕ} (m : ℕ) → m < n → Fin n
toFin {n = ℕzero} _ m<0 = Empty.rec (¬-<-zero m<0)
toFin {n = ℕsuc n} _ (ℕzero , _) = fromℕ n --in this case we have m≡n
toFin {n = ℕsuc n} m (ℕsuc k , p) = weakenFin (toFin m (k , cong predℕ p))

toFin0≡0 : {n : ℕ} (p : 0 < ℕsuc n) → toFin 0 p ≡ zero
toFin0≡0 (ℕzero , p) = subst (λ x → fromℕ x ≡ zero) (cong predℕ p) refl
toFin0≡0 {ℕzero} (ℕsuc k , p) = Empty.rec (ℕsnotz (+-comm 1 k ∙ (cong predℕ p)))
toFin0≡0 {ℕsuc n} (ℕsuc k , p) =
         subst (λ x → weakenFin x ≡ zero) (sym (toFin0≡0 (k , cong predℕ p))) refl

-- doing induction on toFin is awkward, so the following alternative
enum : (m : ℕ) → m < n → Fin n
enum {n = ℕzero} _ m<0 = Empty.rec (¬-<-zero m<0)
enum {n = ℕsuc n} 0 _ = zero
enum {n = ℕsuc n} (ℕsuc m) p = suc (enum m (pred-≤-pred p))

enum∘toℕ : (i : Fin n)(p : toℕ i < n) → enum (toℕ i) p ≡ i
enum∘toℕ {n = ℕsuc n} zero _ = refl
enum∘toℕ {n = ℕsuc n} (suc i) p t = suc (enum∘toℕ i (pred-≤-pred p) t)

toℕ∘enum : (m : ℕ)(p : m < n) → toℕ (enum m p) ≡ m
toℕ∘enum {n = ℕzero} _ m<0 = Empty.rec (¬-<-zero m<0)
toℕ∘enum {n = ℕsuc n} 0 _ = refl
toℕ∘enum {n = ℕsuc n} (ℕsuc m) p i = ℕsuc (toℕ∘enum m (pred-≤-pred p) i)

enumExt : {m m' : ℕ}(p : m < n)(p' : m' < n) → m ≡ m' → enum m p ≡ enum m' p'
enumExt p p' q i = enum (q i) (isProp→PathP (λ i → m≤n-isProp {m = ℕsuc (q i)}) p p' i)

enumInj : {p : m < k}{q : n < k} → enum m p ≡ enum n q → m ≡ n
enumInj p = sym (toℕ∘enum _ _) ∙ cong toℕ p ∙ toℕ∘enum _ _

enumIndStep :
    (P : Fin n → Type ℓ)
  → (k : ℕ)(p : ℕsuc k < n)
  → ((m : ℕ)(q : m < n)(q' : m ≤ k )     → P (enum m q))
  → P (enum (ℕsuc k) p)
  → ((m : ℕ)(q : m < n)(q' : m ≤ ℕsuc k) → P (enum m q))
enumIndStep P k p f x m q q' =
  case (≤-split q') return (λ _ → P (enum m q)) of
    λ { (inl r') → f m q (pred-≤-pred r')
      ; (inr r') → subst P (enumExt p q (sym r')) x }

enumElim :
    (P : Fin n → Type ℓ)
  → (k : ℕ)(p : k < n)(h : ℕsuc k ≡ n)
  → ((m : ℕ)(q : m < n)(q' : m ≤ k) → P (enum m q))
  → (i : Fin n) → P i
enumElim P k p h f i =
  subst P (enum∘toℕ i (toℕ<n i)) (f (toℕ i) (toℕ<n i)
    (pred-≤-pred (subst (λ a → toℕ i < a) (sym h) (toℕ<n i))))

++FinAssoc : {n m k : ℕ} (U : FinVec A n) (V : FinVec A m) (W : FinVec A k)
           → PathP (λ i → FinVec A (+-assoc n m k i)) (U ++Fin (V ++Fin W)) ((U ++Fin V) ++Fin W)
++FinAssoc {n = ℕzero} _ _ _ = refl
++FinAssoc {n = ℕsuc n} U V W i zero = U zero
++FinAssoc {n = ℕsuc n} U V W i (suc ind) = ++FinAssoc (U ∘ suc) V W i ind

++FinRid : {n : ℕ} (U : FinVec A n) (V : FinVec A 0)
         → PathP (λ i → FinVec A (+-zero n i)) (U ++Fin V) U
++FinRid {n = ℕzero} U V = funExt λ i → Empty.rec (¬Fin0 i)
++FinRid {n = ℕsuc n} U V i zero = U zero
++FinRid {n = ℕsuc n} U V i (suc ind) = ++FinRid (U ∘ suc) V i ind

++FinElim : {P : A → Type ℓ'} {n m : ℕ} (U : FinVec A n) (V : FinVec A m)
          → (∀ i → P (U i)) → (∀ i → P (V i)) → ∀ i → P ((U ++Fin V) i)
++FinElim {n = ℕzero} _ _ _ PVHyp i = PVHyp i
++FinElim {n = ℕsuc n} _ _ PUHyp _ zero = PUHyp zero
++FinElim {P = P} {n = ℕsuc n} U V PUHyp PVHyp (suc i) =
          ++FinElim {P = P} (U ∘ suc) V (λ i → PUHyp (suc i)) PVHyp i

++FinPres∈ : {n m : ℕ} {α : FinVec A n} {β : FinVec A m} (S : ℙ A)
           → (∀ i → α i ∈ S) → (∀ i → β i ∈ S) → ∀ i → (α ++Fin β) i ∈ S
++FinPres∈ {n = ℕzero} S hα hβ i = hβ i
++FinPres∈ {n = ℕsuc n} S hα hβ zero = hα zero
++FinPres∈ {n = ℕsuc n} S hα hβ (suc i) = ++FinPres∈ S (hα ∘ suc) hβ i

-- sends i to n+i if toℕ i < m and to i∸n otherwise
-- then +Shuffle²≡id and over the induced path (i.e. in PathP (ua +ShuffleEquiv))
-- ++Fin is commutative, but how to go from there?
+Shuffle : (m n : ℕ) → Fin (m + n) → Fin (n + m)
+Shuffle m n i with <Dec (toℕ i) m
... | yes i<m = toFin (n + (toℕ i)) (<-k+ i<m)
... | no ¬i<m = toFin (toℕ i ∸ m)
                  (subst (λ x → toℕ i ∸ m < x) (+-comm m n) (≤<-trans (∸-≤ (toℕ i) m) (toℕ<n i)))

-- Proof that Fin n ⊎ Fin m ≃ Fin (n+m)
module FinSumChar where

 fun : (n m : ℕ) → Fin n ⊎ Fin m → Fin (n + m)
 fun ℕzero m (inr i) = i
 fun (ℕsuc n) m (inl zero) = zero
 fun (ℕsuc n) m (inl (suc i)) = suc (fun n m (inl i))
 fun (ℕsuc n) m (inr i) = suc (fun n m (inr i))

 invSucAux : (n m : ℕ) → Fin n ⊎ Fin m → Fin (ℕsuc n) ⊎ Fin m
 invSucAux n m (inl i) = inl (suc i)
 invSucAux n m (inr i) = inr i

 inv : (n m : ℕ) → Fin (n + m) → Fin n ⊎ Fin m
 inv ℕzero m i = inr i
 inv (ℕsuc n) m zero = inl zero
 inv (ℕsuc n) m (suc i) = invSucAux n m (inv n m i)

 ret : (n m : ℕ) (i : Fin n ⊎ Fin m) → inv n m (fun n m i) ≡ i
 ret ℕzero m (inr i) = refl
 ret (ℕsuc n) m (inl zero) = refl
 ret (ℕsuc n) m (inl (suc i)) = subst (λ x → invSucAux n m x ≡ inl (suc i))
                                       (sym (ret n m (inl i))) refl
 ret (ℕsuc n) m (inr i) = subst (λ x → invSucAux n m x ≡ inr i) (sym (ret n m (inr i))) refl

 sec : (n m : ℕ) (i : Fin (n + m)) → fun n m (inv n m i) ≡ i
 sec ℕzero m i = refl
 sec (ℕsuc n) m zero = refl
 sec (ℕsuc n) m (suc i) = helperPath (inv n m i) ∙ cong suc (sec n m i)
  where
  helperPath : ∀ x → fun (ℕsuc n) m (invSucAux n m x) ≡ suc (fun n m x)
  helperPath (inl _) = refl
  helperPath (inr _) = refl

 Equiv : (n m : ℕ) → Fin n ⊎ Fin m ≃ Fin (n + m)
 Equiv n m = isoToEquiv (iso (fun n m) (inv n m) (sec n m) (ret n m))

 ++FinInl : (n m : ℕ) (U : FinVec A n) (W : FinVec A m) (i : Fin n)
          → U i ≡ (U ++Fin W) (fun n m (inl i))
 ++FinInl (ℕsuc n) m U W zero = refl
 ++FinInl (ℕsuc n) m U W (suc i) = ++FinInl n m (U ∘ suc) W i

 ++FinInr : (n m : ℕ) (U : FinVec A n) (W : FinVec A m) (i : Fin m)
          → W i ≡ (U ++Fin W) (fun n m (inr i))
 ++FinInr ℕzero (ℕsuc m) U W i = refl
 ++FinInr (ℕsuc n) m U W i = ++FinInr n m (U ∘ suc) W i

-- Proof that Fin n × Fin m ≃ Fin nm
module FinProdChar where

 open Iso
 sucProdToSumIso : (n m : ℕ) → Iso (Fin (ℕsuc n) × Fin m) (Fin m ⊎ (Fin n × Fin m))
 fun (sucProdToSumIso n m) (zero , j) = inl j
 fun (sucProdToSumIso n m) (suc i , j) = inr (i , j)
 inv (sucProdToSumIso n m) (inl j) = zero , j
 inv (sucProdToSumIso n m) (inr (i , j)) = suc i , j
 rightInv (sucProdToSumIso n m) (inl j) = refl
 rightInv (sucProdToSumIso n m) (inr (i , j)) = refl
 leftInv (sucProdToSumIso n m) (zero , j) = refl
 leftInv (sucProdToSumIso n m) (suc i , j) = refl

 Equiv : (n m : ℕ) → (Fin n × Fin m) ≃ Fin (n · m)
 Equiv ℕzero m = uninhabEquiv (λ x → ¬Fin0 (fst x)) ¬Fin0
 Equiv (ℕsuc n) m = Fin (ℕsuc n) × Fin m    ≃⟨ isoToEquiv (sucProdToSumIso n m) ⟩
                    Fin m ⊎ (Fin n × Fin m) ≃⟨ isoToEquiv (⊎Iso idIso (equivToIso (Equiv n m))) ⟩
                    Fin m ⊎ Fin (n · m)     ≃⟨ FinSumChar.Equiv m (n · m) ⟩
                    Fin (m + n · m)         ■

-- Exhaustion of decidable predicate

∀Dec :
    (P : Fin m → Type ℓ)
  → (dec : (i : Fin m) → Dec (P i))
  → ((i : Fin m) → P i) ⊎ (Σ[ i ∈ Fin m ] ¬ P i)
∀Dec {m = 0} _ _ = inl λ ()
∀Dec {m = ℕsuc m} P dec = helper (dec zero) (∀Dec _ (dec ∘ suc))
  where
    helper :
        Dec (P zero)
      → ((i : Fin m) → P (suc i))  ⊎ (Σ[ i ∈ Fin m ] ¬ P (suc i))
      → ((i : Fin (ℕsuc m)) → P i) ⊎ (Σ[ i ∈ Fin (ℕsuc m) ] ¬ P i)
    helper (yes p) (inl q) = inl λ { zero → p ; (suc i) → q i }
    helper (yes _) (inr q) = inr (suc (q .fst) , q .snd)
    helper (no ¬p) _ = inr (zero , ¬p)

∀Dec2 :
    (P : Fin m → Fin n → Type ℓ)
  → (dec : (i : Fin m)(j : Fin n) → Dec (P i j))
  → ((i : Fin m)(j : Fin n) → P i j) ⊎ (Σ[ i ∈ Fin m ] Σ[ j ∈ Fin n ] ¬ P i j)
∀Dec2 {m = 0} {n = n} _ _ = inl λ ()
∀Dec2 {m = ℕsuc m} {n = n} P dec = helper (∀Dec (P zero) (dec zero)) (∀Dec2 (P ∘ suc) (dec ∘ suc))
  where
    helper :
        ((j : Fin n) → P zero j) ⊎ (Σ[ j ∈ Fin n ] ¬ P zero j)
      → ((i : Fin m)(j : Fin n) → P (suc i) j)  ⊎ (Σ[ i ∈ Fin m ] Σ[ j ∈ Fin n ] ¬ P (suc i) j)
      → ((i : Fin (ℕsuc m))(j : Fin n) → P i j) ⊎ (Σ[ i ∈ Fin (ℕsuc m) ] Σ[ j ∈ Fin n ] ¬ P i j)
    helper (inl p) (inl q) = inl λ { zero j → p j ; (suc i) j → q i j }
    helper (inl _) (inr q) = inr (suc (q .fst) , q .snd .fst , q .snd .snd)
    helper (inr p) _ = inr (zero , p)

max_stars_repo_name: howsiyu/cubical

max_issues_repo_name: howsiyu/cubical

max_forks_repo_name: howsiyu/cubical


text:
-- Currently imports are not allowed in mutual blocks.
-- This might change.
module ImportInMutual where

mutual
  import Fake.Module
  T : Set -> Set
  T A = A

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


text:
{-

A parameterized family of structures S can be combined into a single structure:
X ↦ (a : A) → S a X

This is more general than Structures.Function in that S can vary in A.

-}
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Structures.Parameterized where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Functions.FunExtEquiv
open import Cubical.Foundations.SIP
open import Cubical.Foundations.Univalence

private
  variable
    ℓ ℓ₁ ℓ₁' : Level

module _ {ℓ₀} (A : Type ℓ₀) where

  ParamStructure : (S : A → Type ℓ → Type ℓ₁)
    → Type ℓ → Type (ℓ-max ℓ₀ ℓ₁)
  ParamStructure S X = (a : A) → S a X

  ParamEquivStr : {S : A → Type ℓ → Type ℓ₁}
    → (∀ a → StrEquiv (S a) ℓ₁') → StrEquiv (ParamStructure S) (ℓ-max ℓ₀ ℓ₁')
  ParamEquivStr ι (X , l) (Y , m) e = ∀ a → ι a (X , l a) (Y , m a) e

  paramUnivalentStr : {S : A → Type ℓ → Type ℓ₁}
    (ι : ∀ a → StrEquiv (S a) ℓ₁') (θ : ∀ a → UnivalentStr (S a) (ι a))
    → UnivalentStr (ParamStructure S) (ParamEquivStr ι)
  paramUnivalentStr ι θ e = compEquiv (equivΠCod λ a → θ a e) funExtEquiv

  paramEquivAction : {S : A → Type ℓ → Type ℓ₁}
    → (∀ a → EquivAction (S a)) → EquivAction (ParamStructure S)
  paramEquivAction α e = equivΠCod (λ a → α a e)

  paramTransportStr : {S : A → Type ℓ → Type ℓ₁}
    (α : ∀ a → EquivAction (S a)) (τ : ∀ a → TransportStr (α a))
    → TransportStr (paramEquivAction α)
  paramTransportStr {S = S} α τ e f =
    funExt λ a →
    τ a e (f a)
    ∙ cong (λ fib → transport (λ i → S (fib .snd (~ i)) (ua e i)) (f (fib .snd i1)))
      (isContrSingl a .snd (_ , sym (transportRefl a)))

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
module Haskell.Prim.Bool where

open import Agda.Primitive
open import Agda.Builtin.Bool public

private
  variable
    ℓ : Level

--------------------------------------------------
-- Booleans

infixr 3 _&&_
_&&_ : Bool → Bool → Bool
false && _ = false
true  && x = x

infixr 2 _||_
_||_ : Bool → Bool → Bool
false || x = x
true  || _ = true

not : Bool → Bool
not false = true
not true  = false

otherwise : Bool
otherwise = true


text:
------------------------------------------------------------------------------
-- Testing the η-expansion
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

module Eta5 where

postulate
  D   : Set
  _≈_ : D → D → Set

data ∃ (A : D → Set) : Set where
  _,_ : (t : D) → A t → ∃ A

P : D → Set
P ws = ∃ (λ zs → ws ≈ zs)
{-# ATP definition P #-}

postulate foo : ∀ ws → P ws → ∃ (λ zs → ws ≈ zs)
{-# ATP prove foo #-}

max_stars_repo_name: asr/apia

max_issues_repo_name: asr/apia

max_forks_repo_name: asr/apia