text:
open import Nat
open import Prelude
open import core

module lemmas-progress-checks where
  -- boxed values don't have an instruction transition
  boxedval-not-trans : ∀{d d'} → d boxedval → d →> d' → ⊥
  boxedval-not-trans (BVVal VConst) ()
  boxedval-not-trans (BVVal VLam) ()
  boxedval-not-trans (BVArrCast x bv) (ITCastID) = x refl
  boxedval-not-trans (BVHoleCast () bv) (ITCastID)
  boxedval-not-trans (BVHoleCast () bv) (ITCastSucceed x₁)
  boxedval-not-trans (BVHoleCast GHole bv) (ITGround (MGArr x)) = x refl
  boxedval-not-trans (BVHoleCast x a) (ITExpand ())
  boxedval-not-trans (BVHoleCast x x₁) (ITCastFail x₂ () x₄)

  -- indets don't have an instruction transition
  indet-not-trans : ∀{d d'} → d indet → d →> d' → ⊥
  indet-not-trans IEHole ()
  indet-not-trans (INEHole x) ()
  indet-not-trans (IAp x₁ () x₂) (ITLam)
  indet-not-trans (IAp x (ICastArr x₁ ind) x₂) (ITApCast ) = x _ _ _ _ _ refl
  indet-not-trans (ICastArr x ind) (ITCastID) = x refl
  indet-not-trans (ICastGroundHole () ind) (ITCastID)
  indet-not-trans (ICastGroundHole x ind) (ITCastSucceed ())
  indet-not-trans (ICastGroundHole GHole ind) (ITGround (MGArr x)) = x refl
  indet-not-trans (ICastHoleGround x ind ()) (ITCastID)
  indet-not-trans (ICastHoleGround x ind x₁) (ITCastSucceed x₂) = x _ _ refl
  indet-not-trans (ICastHoleGround x ind GHole) (ITExpand (MGArr x₂)) = x₂ refl
  indet-not-trans (ICastGroundHole x a) (ITExpand ())
  indet-not-trans (ICastHoleGround x a x₁) (ITGround ())
  indet-not-trans (ICastGroundHole x x₁) (ITCastFail x₂ () x₄)
  indet-not-trans (ICastHoleGround x x₁ x₂) (ITCastFail x₃ x₄ x₅) = x _ _ refl
  indet-not-trans (IFailedCast x x₁ x₂ x₃) ()

  -- finals don't have an instruction transition
  final-not-trans : ∀{d d'} → d final → d →> d' → ⊥
  final-not-trans (FBoxedVal x) = boxedval-not-trans x
  final-not-trans (FIndet x) = indet-not-trans x

  -- finals cast from a ground are still final
  final-gnd-cast : ∀{ d τ } → d final → τ ground → (d ⟨ τ ⇒ ⦇-⦈ ⟩) final
  final-gnd-cast (FBoxedVal x) gnd = FBoxedVal (BVHoleCast gnd x)
  final-gnd-cast (FIndet x) gnd = FIndet (ICastGroundHole gnd x)

  -- if an expression results from filling a hole in an evaluation context,
  -- the hole-filler must have been final
  final-sub-final : ∀{d ε x} → d final → d == ε ⟦ x ⟧ → x final
  final-sub-final x FHOuter = x
  final-sub-final (FBoxedVal (BVVal ())) (FHAp1 eps)
  final-sub-final (FBoxedVal (BVVal ())) (FHAp2 eps)
  final-sub-final (FBoxedVal (BVVal ())) (FHNEHole eps)
  final-sub-final (FBoxedVal (BVVal ())) (FHCast eps)
  final-sub-final (FBoxedVal (BVVal ())) (FHFailedCast y)
  final-sub-final (FBoxedVal (BVArrCast x₁ x₂)) (FHCast eps) = final-sub-final (FBoxedVal x₂) eps
  final-sub-final (FBoxedVal (BVHoleCast x₁ x₂)) (FHCast eps) = final-sub-final (FBoxedVal x₂) eps
  final-sub-final (FIndet (IAp x₁ x₂ x₃)) (FHAp1 eps) = final-sub-final (FIndet x₂) eps
  final-sub-final (FIndet (IAp x₁ x₂ x₃)) (FHAp2 eps) = final-sub-final x₃ eps
  final-sub-final (FIndet (INEHole x₁)) (FHNEHole eps) = final-sub-final x₁ eps
  final-sub-final (FIndet (ICastArr x₁ x₂)) (FHCast eps) = final-sub-final (FIndet x₂) eps
  final-sub-final (FIndet (ICastGroundHole x₁ x₂)) (FHCast eps) = final-sub-final (FIndet x₂) eps
  final-sub-final (FIndet (ICastHoleGround x₁ x₂ x₃)) (FHCast eps) = final-sub-final (FIndet x₂) eps
  final-sub-final (FIndet (IFailedCast x₁ x₂ x₃ x₄)) (FHFailedCast y) = final-sub-final x₁ y

  final-sub-not-trans : ∀{d d' d'' ε} →  d final → d == ε ⟦ d' ⟧ → d' →> d'' → ⊥
  final-sub-not-trans f sub step = final-not-trans (final-sub-final f sub) step

max_stars_repo_name: hazelgrove/hazelnut-dynamics-agda

max_issues_repo_name: hazelgrove/hazelnut-dynamics-agda

max_forks_repo_name: hazelgrove/hazelnut-dynamics-agda


text:
module UnderscoresAsDataParam where

data List (A : Set) : Set where
  nil  : List _
  cons : A -> List A -> List _

ext: agda

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
module PartialOrder where

open import Prelude

record PartialOrder (A : Set) : Set1 where
  field
    _==_    : A -> A -> Set
    _≤_     : A -> A -> Set
    ==-def  : forall {x y} -> (x == y) ⇐⇒ (x ≤ y) ∧ (y ≤ x)
    ≤-refl  : forall {x} -> x ≤ x
    ≤-trans : forall {x y z} -> x ≤ y -> y ≤ z -> x ≤ z

module POrder {A : Set}(ord : PartialOrder A) where

  private module POrd = PartialOrder ord
  open POrd public

  infix 60 _≤_ _==_

  Monotone : (A -> A) -> Set
  Monotone f = forall {x y} -> x ≤ y -> f x ≤ f y

  Antitone : (A -> A) -> Set
  Antitone f = forall {x y} -> x ≤ y -> f y ≤ f x

  ≤-antisym : forall {x y} -> x ≤ y -> y ≤ x -> x == y
  ≤-antisym p q = snd ==-def (p , q)

  ==≤-L : forall {x y} -> x == y -> x ≤ y
  ==≤-L x=y = fst (fst ==-def x=y)

  ==≤-R : forall {x y} -> x == y -> y ≤ x
  ==≤-R x=y = snd (fst ==-def x=y)

  ==-refl : forall {x} -> x == x
  ==-refl = ≤-antisym ≤-refl ≤-refl

  ==-sym : forall {x y} -> x == y -> y == x
  ==-sym xy = snd ==-def (swap (fst ==-def xy))

  ==-trans : forall {x y z} -> x == y -> y == z -> x == z
  ==-trans xy yz = ≤-antisym
                           (≤-trans x≤y y≤z)
                           (≤-trans z≤y y≤x)
    where
      x≤y = ==≤-L xy
      y≤z = ==≤-L yz
      y≤x = ==≤-R xy
      z≤y = ==≤-R yz

  Dual : PartialOrder A
  Dual = record
    { _==_    = _==_
    ; _≤_     = \x y -> y ≤ x
    ; ==-def  = (swap ∘ fst ==-def , snd ==-def ∘ swap)
    ; ≤-refl  = ≤-refl
    ; ≤-trans = \yx zy -> ≤-trans zy yx
    }

max_stars_repo_name: asr/agda-kanso


text:
------------------------------------------------------------------------
-- Type checing of polymorphic and iso-recursive lambda terms
------------------------------------------------------------------------

module SystemF.TypeCheck where

open import Data.Fin using (Fin; suc; zero; pred)
open import Data.Nat as Nat using (ℕ; _+_)
open import Data.Product
open import Data.Vec using (_∷_; []; lookup)
open import Function hiding (typeOf)
open import Relation.Nullary
open import Relation.Nullary.Negation
open import Relation.Binary using (Decidable)
open import Relation.Binary.PropositionalEquality hiding ([_])
open ≡-Reasoning

open import SystemF.Type
open import SystemF.Term
open import SystemF.WtTerm

open TypeSubst using () renaming (_[/_]  to _[/tp_])
open CtxSubst  using () renaming (weaken to weakenCtx)

------------------------------------------------------------------------
-- Decision procedures for equality of variable names and types

-- This module contains two decision procedures for type checking:
--
--  * the function typeOf synthesizes a type a for a given (untyped)
--    term t and typing environment Γ, if possible;
--
--  * the function check_⊢_∈_ checks whether a given triple Γ, t, a is
--    in the well-typedness relation.
--
-- The two functions correspond to a synthetic resp. analytic view of
-- type-checking.  Both produce evidence in the form of a typing
-- derivation if type checking succeeds or a proof that no such
-- derivation exists otherwise.

infix 4 _≟n_ _≡tp_ _≟_

-- Equal successors have equal predecessors.
≡suc : ∀ {n} {x y : Fin n} → suc x ≡ suc y → x ≡ y
≡suc refl = refl

-- A decision procedure for equality of variable names.
_≟n_ : ∀ {n} → Decidable {A = Fin n} _≡_
zero  ≟n zero   = yes refl
suc x ≟n suc y  with x ≟n y
... | yes x≡y   = yes (cong suc x≡y)
... | no  x≢y   = no (x≢y ∘ ≡suc)
zero  ≟n suc y  = no λ()
suc x ≟n zero   = no λ()

-- A shorthand for (syntactic) type equality.
_≡tp_ : ∀ {n} → Type n → Type n → Set
a ≡tp b = a ≡ b

-- Equal type variables have equal names.
≡var : ∀ {n} {x y : Fin n} → var x ≡tp var y → x ≡ y
≡var refl = refl

-- Equal function types have equal domains.
≡dom→ : ∀ {n} {a a′ b b′ : Type n} → a →' b ≡tp a′ →' b′ → a ≡ a′
≡dom→ refl = refl

-- Equal function types have equal codomains.
≡cod→ : ∀ {n} {a a′ b b′ : Type n} → a →' b ≡tp a′ →' b′ → b ≡ b′
≡cod→ refl = refl

-- Equal univeral types have equal bodies.
≡∀ : ∀ {n} {a a′ : Type (1 + n)} → ∀' a ≡tp ∀' a′ → a ≡ a′
≡∀ refl = refl

-- Equal recursive types have equal bodies.
≡μ : ∀ {n} {a a′ : Type (1 + n)} → μ a ≡tp μ a′ → a ≡ a′
≡μ refl = refl

-- A decision procedure for (syntactic) type equality
_≟_ : ∀ {n} → Decidable {A = Type n} _≡_
var x  ≟ var  y    with x ≟n y
var x  ≟ var .x    | yes refl = yes refl
var x  ≟ var  y    | no  x≢y  = no (x≢y ∘ ≡var)
var _  ≟ _ →' _    = no λ()
var _  ≟ ∀' _      = no λ()
var _  ≟ μ _       = no λ()
a →' b ≟ var x     = no λ()
a →' b ≟  a′ →' b′ with a ≟ a′ | b ≟ b′
a →' b ≟ .a →' .b  | yes refl  | yes refl = yes refl
a →' b ≟  a′ →' b′ | yes _     | no  b≢b′ = no (b≢b′ ∘ ≡cod→)
a →' b ≟  a′ →' b′ | no  a≢a′  | _        = no (a≢a′ ∘ ≡dom→)
a →' b ≟ ∀' _      = no λ()
a →' b ≟ μ _       = no λ()
∀' _   ≟ var _     = no λ()
∀' _   ≟ _ →' _    = no λ()
∀' a   ≟ ∀'  a′    with a ≟ a′
∀' a   ≟ ∀' .a     | yes refl = yes refl
∀' a   ≟ ∀'  a′    | no  a≢a′ = no (a≢a′ ∘ ≡∀)
∀' _   ≟ μ _       = no λ()
μ _    ≟ var _     = no λ()
μ _    ≟ _ →' _    = no λ()
μ _    ≟ ∀' _      = no λ()
μ a    ≟ μ  a′     with a ≟ a′
μ a    ≟ μ .a      | yes refl = yes refl
μ a    ≟ μ  a′     | no  a≢a′ = no (a≢a′ ∘ ≡μ)

------------------------------------------------------------------------
-- Inversion and functionality of the well-typedness relation

-- Inversion of type application typing.
Λ-inversion : ∀ {m n} {Γ : Ctx m n} {t a} →
              Γ ⊢ Λ t ∈ a → ∃ λ a′ → (a ≡ ∀' a′) × (weakenCtx Γ ⊢ t ∈ a′)
Λ-inversion {a = ∀' a′} (Λ t∈a) = a′ , (refl , t∈a)

-- Inversion of term application typing.
λ'-inversion : ∀ {m n} {Γ : Ctx m n} {t a a→b} →
               Γ ⊢ λ' a t ∈ a→b → ∃ λ b → (a→b ≡ a →' b) × (a ∷ Γ ⊢ t ∈ b)
λ'-inversion {a→b = a →' b} (λ' .a t∈b) = b , (refl , t∈b)

-- Inversion of recursive term typing.
μ-inversion : ∀ {m n} {Γ : Ctx m n} {t a a′} →
              Γ ⊢ μ a t ∈ a′ → (a ≡ a′) × (a ∷ Γ ⊢ t ∈ a)
μ-inversion (μ a t∈b) = refl , t∈b

-- Inversion of type application.
[]-inversion : ∀ {m n} {Γ : Ctx m n} {t b a[/b]} → Γ ⊢ t [ b ] ∈ a[/b] →
               ∃ λ a → (a[/b] ≡ a [/tp b ]) × (Γ ⊢ t ∈ ∀' a)
[]-inversion (_[_] {a = a} t∈∀a b) = a , (refl , t∈∀a)

-- Inversion of term application.
·-inversion : ∀ {m n} {Γ : Ctx m n} {s t b} → Γ ⊢ s · t ∈ b →
              ∃ λ a → (Γ ⊢ s ∈ a →' b) × (Γ ⊢ t ∈ a)
·-inversion (_·_ {a = a} s∈a→b t∈a) = a , (s∈a→b , t∈a)

-- Inversion of recursive type folding.
fold-inversion : ∀ {m n} {Γ : Ctx m n} {t a μa} → Γ ⊢ fold a t ∈ μa →
                 (μa ≡ μ a) × (Γ ⊢ t ∈ a [/tp μ a ])
fold-inversion (fold a t∈a[/μa]) = refl , t∈a[/μa]

-- Inversion of recursive type unfolding.
unfold-inversion : ∀ {m n} {Γ : Ctx m n} {t a a[/μa]} →
                   Γ ⊢ unfold a t ∈ a[/μa] →
                   (a[/μa] ≡ a [/tp μ a ]) × (Γ ⊢ t ∈ μ a)
unfold-inversion (unfold a t∈μa) = refl , t∈μa

-- The relation _⊢_∈_ is functional in its last argument.
functional : ∀ {m n} {Γ : Ctx m n} {t a a′} → Γ ⊢ t ∈ a → Γ ⊢ t ∈ a′ → a ≡ a′
functional (var x)       (var .x)        = refl
functional (Λ t∈a)       (Λ t∈a′)        = cong ∀' (functional t∈a t∈a′)
functional (λ' a t∈b)    (λ' .a t∈b′)    = cong (_→'_ a) (functional t∈b t∈b′)
functional (μ a t∈a)     (μ .a t∈a′)     = functional t∈a t∈a′
functional (t∈∀a [ b ])  (t∈∀a′ [ .b ])  =
  cong (λ{ (∀' a)   → a [/tp b ] ; a → a }) (functional t∈∀a t∈∀a′)
functional (s∈a→b · _)   (s∈a→b′ · _)    =
  cong (λ{ (a →' b) → b          ; a → a }) (functional s∈a→b s∈a→b′)
functional (fold a t∈)   (fold .a t∈′)   = refl
functional (unfold a t∈) (unfold .a t∈′) = refl

-- A variant of functionality.
functional′ : ∀ {m n} {Γ : Ctx m n} {t a a′} → Γ ⊢ t ∈ a → a ≢ a′ → Γ ⊢ t ∉ a′
functional′ t∈a = contraposition (functional t∈a)

------------------------------------------------------------------------
-- Type checking

infix 5 check_⊢_∈_

-- A predicate for typable terms
HasType : ∀ {m n} → Ctx m n → Term m n → Set
HasType Γ t = ∃ λ a → Γ ⊢ t ∈ a

-- Type checking viewed as a decision procedure for the existence of
-- typings (i.e. type synthesis).  Note that together with
-- functionality, this proves that the well-typedness relation is a
-- decidable partial function.
typeOf : ∀ {m n} (Γ : Ctx m n) t → Dec (HasType Γ t)
typeOf Γ (var x)      = yes (lookup Γ x , var x)
typeOf Γ (Λ t)        with typeOf (weakenCtx Γ) t
... | yes (a , t∈a)   = yes (∀' a , Λ t∈a)
... | no ∄a           = no (∄a ∘ map id proj₂ ∘ Λ-inversion ∘ proj₂)
typeOf Γ (λ' a t)     with typeOf (a ∷ Γ) t
... | yes (b , t∈b)   = yes (a →' b , λ' a t∈b)
... | no ∄b           = no (∄b ∘ map id proj₂ ∘ λ'-inversion ∘ proj₂)
typeOf Γ (μ a t)      with typeOf (a ∷ Γ) t
typeOf Γ (μ a t)      | yes ( a′ , t∈a′) with a′ ≟ a
typeOf Γ (μ a t)      | yes (.a  , t∈a′) | yes refl = yes (a , μ a t∈a′)
... | no  a′≢a = no (a′≢a ∘ functional t∈a′ ∘ proj₂ ∘ μ-inversion ∘ proj₂)
typeOf Γ (μ a t)      | no ∄a′ =
  no (∄a′ ∘ map id (uncurry ⊢substTp ∘ μ-inversion))
typeOf Γ (t [ b ])    with typeOf Γ t
typeOf Γ (t [ b ])    | yes (var _  , t∈x   ) =
  no ((functional′ t∈x λ()) ∘ proj₂ ∘ proj₂ ∘ []-inversion ∘ proj₂)
typeOf Γ (t [ b ])    | yes (_ →' _ , t∈a→b ) =
  no ((functional′ t∈a→b λ()) ∘ proj₂ ∘ proj₂ ∘ []-inversion ∘ proj₂)
typeOf Γ (t [ b ])    | yes (∀' a   , t∈∀a  ) = yes (a [/tp b ] , t∈∀a [ b ])
typeOf Γ (t [ b ])    | yes (μ _    , t∈μa  ) =
  no ((functional′ t∈μa λ()) ∘ proj₂ ∘ proj₂ ∘ []-inversion ∘ proj₂)
typeOf Γ (t [ b ])    | no  ∄a = no (∄a ∘ map ∀' proj₂ ∘ []-inversion ∘ proj₂)
typeOf Γ (s · t)      with typeOf Γ s | typeOf Γ t
typeOf Γ (s · t)      | yes (var _  , s∈x  ) | _ =
  no ((functional′ s∈x λ()) ∘ proj₁ ∘ proj₂ ∘ ·-inversion ∘ proj₂)
typeOf Γ (s · t) | yes (a →' b , s∈a→b) | yes ( a′ , t∈a) with a′ ≟ a
typeOf Γ (s · t) | yes (a →' b , s∈a→b) | yes (.a  , t∈a) | yes refl =
  yes (b , s∈a→b · t∈a)
typeOf Γ (s · t) | yes (a →' b , s∈a→b) | yes ( a′ , t∈a) | no  a′≢a =
  no (a′≢a ∘ helper)
  where
    helper : HasType Γ (s · t) → a′ ≡ a
    helper (b , s·t∈b) with ·-inversion s·t∈b
    ... | c , s∈c→b , t∈c = begin
      a′ ≡⟨ functional t∈a t∈c ⟩
      c  ≡⟨ ≡dom→ (functional s∈c→b s∈a→b) ⟩
      a  ∎
typeOf Γ (s · t) | yes (a →' b , s∈a→b) | no  ∄a′ =
  no (∄a′ ∘ map id proj₂ ∘ ·-inversion ∘ proj₂)
typeOf Γ (s · t) | yes (∀' _   , s∈∀a ) | _ =
  no ((functional′ s∈∀a λ()) ∘ proj₁ ∘ proj₂ ∘ ·-inversion ∘ proj₂)
typeOf Γ (s · t) | yes (μ  _   , s∈μa ) | _ =
  no ((functional′ s∈μa λ()) ∘ proj₁ ∘ proj₂ ∘ ·-inversion ∘ proj₂)
typeOf Γ (s · t) | no  ∄a               | _ = no (∄a ∘ helper)
  where
    helper : HasType Γ (s · t) → HasType Γ s
    helper (b , s·t∈b) with ·-inversion s·t∈b
    ... | a , s∈a→b , _ = a →' b , s∈a→b
typeOf Γ (fold a t)   with typeOf Γ t
typeOf Γ (fold a t)   | yes (a′ , t∈a′) with a′ ≟ a [/tp μ a ]
typeOf Γ (fold a t)   | yes (._ , t∈a′) | yes refl = yes (μ a , fold a t∈a′)
typeOf Γ (fold a t)   | yes (a′ , t∈a′) | no a′≢a[/μa] =
  no (a′≢a[/μa] ∘ functional t∈a′ ∘ proj₂ ∘ fold-inversion ∘ proj₂)
typeOf Γ (fold a t)   | no  ∄a′ =
  no (∄a′ ∘ map (const (a [/tp μ a ])) id ∘ fold-inversion ∘ proj₂)
typeOf Γ (unfold a t) with typeOf Γ t
typeOf Γ (unfold a t) | yes (a′ , t∈a′) with a′ ≟ μ a
typeOf Γ (unfold a t) | yes (._ , t∈a′) | yes refl =
  yes (a [/tp μ a ] , unfold a t∈a′)
typeOf Γ (unfold a t) | yes (a′ , t∈a′) | no a′≢μa =
  no (a′≢μa ∘ functional t∈a′ ∘ proj₂ ∘ unfold-inversion ∘ proj₂)
typeOf Γ (unfold a t) | no  ∄a′ =
  no (∄a′ ∘ map (const (μ a)) id ∘ unfold-inversion ∘ proj₂)

-- Type checking as a decision procedure for the well-typedness
-- relation.
check_⊢_∈_ : ∀ {m n} (Γ : Ctx m n) t a → Dec (Γ ⊢ t ∈ a)
check Γ ⊢ t ∈ a with typeOf Γ t
check Γ ⊢ t ∈ a | yes ( a′ , t∈a′) with a′ ≟ a
check Γ ⊢ t ∈ a | yes (.a  , t∈a ) | yes refl = yes t∈a
check Γ ⊢ t ∈ a | yes ( a′ , t∈a′) | no  a′≢a = no (a′≢a ∘ functional t∈a′)
check Γ ⊢ t ∈ a | no   ∄a′                    = no (∄a′ ∘ helper)
  where
    helper : ∀ {m n} {Γ : Ctx m n} {t a} → Γ ⊢ t ∈ a → HasType Γ t
    helper {a = a} t∈a = a , t∈a

------------------------------------------------------------------------
-- Some simple test cases

private
  module TpOp = TypeOperators
  module TmOp = TermOperators
  module WtOp = WtTermOperators

-- Test: synthesize the type of the polymorphic identity.
test-typeOf-id : typeOf [] (TmOp.id {n = 0}) ≡ yes (TpOp.id , WtOp.id)
test-typeOf-id = refl

-- Test: check the type of the polymorphic identity.
test-check-id : check [] ⊢ TmOp.id {n = 0} ∈ TpOp.id ≡ yes WtOp.id
test-check-id = refl

-- Using the agda2-mode one can also run the above decision procedures
-- interactively in GNU/Emacs by typing C-x C-n <expression>.
-- E.g. typing
--
--   C-x C-n typeOf [] (Λ (λ' (var zero) (var zero)))
--
-- should return
--
--   yes (∀' (var zero →' var zero) , Λ (λ' (var zero) (var zero)))

------------------------------------------------------------------------
-- Uniqueness of typing derivations

-- There is at most one typing derivation for each triple Γ, t, a.
-- I.e. if there is an x : Γ ⊢ t ∈ a, it is unique.
unique : ∀ {m n} {Γ : Ctx m n} {t a} (t∈a t∈a′ : Γ ⊢ t ∈ a) → t∈a ≡ t∈a′
unique (var x)    (var .x)     = refl
unique (Λ t∈a)    (Λ t∈a′)     = cong Λ (unique t∈a t∈a′)
unique (λ' a t∈a) (λ' .a t∈a′) = cong (λ' a) (unique t∈a t∈a′)
unique (μ  a t∈a) (μ  .a t∈a′) = cong (μ  a) (unique t∈a t∈a′)
unique {Γ = Γ} {t [ b ]} (_[_] {a = a } t∈a .b) t∈a′[b] = helper t∈a′[b] refl
  where
    helper : ∀ {a′[/b]} (t∈a′[b] : Γ ⊢ t [ b ] ∈ a′[/b])
             (a[/b]≡a′[/b] : a [/tp b ] ≡ a′[/b]) →
             ⊢substTp a[/b]≡a′[/b] (t∈a [ b ]) ≡ t∈a′[b]
    helper (_[_] {a = a′} t∈a′ .b) _ with functional t∈a t∈a′
    helper (t∈a′ [ .b ]) refl | refl = cong _ (unique t∈a t∈a′)
unique (_·_ {a = a} s∈a→b t∈a) (_·_ {a = a′} s∈a′→b t∈a′) with
  functional s∈a→b s∈a′→b
unique (s∈a→b · t∈a) (s∈a′→b · t∈a′) | refl =
  cong₂ _·_ (unique s∈a→b s∈a′→b) (unique t∈a t∈a′)
unique (fold   a t∈a) (fold   .a t∈a′) = cong (fold   a) (unique t∈a t∈a′)
unique (unfold a t∈a) (unfold .a t∈a′) = cong (unfold a) (unique t∈a t∈a′)

max_stars_repo_name: sstucki/system-f-agda

max_issues_repo_name: sstucki/system-f-agda

max_forks_repo_name: sstucki/system-f-agda


text:
{-# OPTIONS --without-K --safe #-}

open import Polynomial.Parameters
open import Algebra

module Polynomial.NormalForm.Operations
  {a ℓ}
  (coeffs : RawCoeff a ℓ)
  where

open import Polynomial.Exponentiation (RawCoeff.coeffs coeffs)

open import Data.Nat as ℕ          using (ℕ; suc; zero; compare)
open import Data.Nat.Properties    using (z≤′n)
open import Data.List              using (_∷_; [])
open import Data.Fin               using (Fin)
open import Data.Product           using (_,_; map₁)
open import Induction.WellFounded  using (Acc; acc)
open import Induction.Nat          using (<′-wellFounded)

open import Polynomial.NormalForm.InjectionIndex
open import Polynomial.NormalForm.Definition coeffs
open import Polynomial.NormalForm.Construction coeffs

open RawCoeff coeffs

----------------------------------------------------------------------
-- Addition
----------------------------------------------------------------------
-- The reason the following code is so verbose is termination
-- checking. For instance, in the third case for ⊞-coeffs, we call a
-- helper function. Instead, you could conceivably use a with-block
-- (on ℕ.compare p q):
--
-- ⊞-coeffs ((x , p) ∷ xs) ((y , q) ∷ ys) with (ℕ.compare p q)
-- ... | ℕ.less    p k = (x , p) ∷ ⊞-coeffs xs ((y , k) ∷ ys)
-- ... | ℕ.equal   p   = (fst~ x ⊞ fst~ y , p) ∷↓ ⊞-coeffs xs ys
-- ... | ℕ.greater q k = (y , q) ∷ ⊞-coeffs ((x , k) ∷ xs) ys
--
-- However, because the first and third recursive calls each rewrap
-- a list that was already pattern-matched on, the recursive call
-- does not strictly decrease the size of its argument.
--
-- Interestingly, if --without-K is turned off, we don't need the
-- helper function ⊞-coeffs; we could pattern match on _⊞_ directly.
--
-- _⊞_ {zero} (lift x) (lift y) = lift (x + y)
-- _⊞_ {suc n} [] ys = ys
-- _⊞_ {suc n} (x ∷ xs) [] = x ∷ xs
-- _⊞_ {suc n} ((x , p) ∷ xs) ((y , q) ∷ ys) =
--   ⊞-zip (ℕ.compare p q) x xs y ys
mutual
  infixl 6 _⊞_
  _⊞_ : ∀ {n} → Poly n → Poly n → Poly n
  (xs Π i≤n) ⊞ (ys Π j≤n) = ⊞-match (inj-compare i≤n j≤n) xs ys

  ⊞-match : ∀ {i j n}
        → {i≤n : i ≤′ n}
        → {j≤n : j ≤′ n}
        → InjectionOrdering i≤n j≤n
        → FlatPoly i
        → FlatPoly j
        → Poly n
  ⊞-match (inj-eq i&j≤n)     (Κ x)  (Κ y)  = Κ (x + y)         Π  i&j≤n
  ⊞-match (inj-eq i&j≤n)     (Σ (x Δ i & xs)) (Σ (y Δ j & ys)) = ⊞-zip (compare i j) x xs y ys Π↓ i&j≤n
  ⊞-match (inj-lt i≤j-1 j≤n)  xs    (Σ ys) = ⊞-inj i≤j-1 xs ys Π↓ j≤n
  ⊞-match (inj-gt i≤n j≤i-1) (Σ xs)  ys    = ⊞-inj j≤i-1 ys xs Π↓ i≤n

  ⊞-inj : ∀ {i k}
        → (i ≤′ k)
        → FlatPoly i
        → Coeff k +
        → Coeff k *
  ⊞-inj i≤k xs (y Π j≤k ≠0 Δ zero & ys) = ⊞-match (inj-compare j≤k i≤k) y xs Δ zero ∷↓ ys
  ⊞-inj i≤k xs (y Δ suc j & ys) = xs Π i≤k Δ zero ∷↓ ∹ y Δ j & ys

  ⊞-coeffs : ∀ {n} → Coeff n * → Coeff n * → Coeff n *
  ⊞-coeffs (∹ x Δ i & xs) ys = ⊞-zip-r x i xs ys
  ⊞-coeffs [] ys = ys

  ⊞-zip : ∀ {p q n}
        → ℕ.Ordering p q
        → NonZero n
        → Coeff n *
        → NonZero n
        → Coeff n *
        → Coeff n *
  ⊞-zip (ℕ.less    i k) x xs y ys = (∹ x Δ i & ⊞-zip-r y k ys xs)
  ⊞-zip (ℕ.greater j k) x xs y ys = (∹ y Δ j & ⊞-zip-r x k xs ys)
  ⊞-zip (ℕ.equal   i  ) x xs y ys = (x .poly ⊞ y .poly) Δ i ∷↓ ⊞-coeffs xs ys

  ⊞-zip-r : ∀ {n} → NonZero n → ℕ → Coeff n * → Coeff n * → Coeff n *
  ⊞-zip-r x i xs [] = ∹ x Δ i & xs
  ⊞-zip-r x i xs (∹ y Δ j & ys) = ⊞-zip (compare i j) x xs y ys
{-# INLINE ⊞-zip #-}

----------------------------------------------------------------------
-- Negation
----------------------------------------------------------------------

-- recurse on acc directly
-- https://github.com/agda/agda/issues/3190#issuecomment-416900716

⊟-step : ∀ {n} → Acc _<′_ n → Poly n → Poly n
⊟-step (acc wf) (Κ x  Π i≤n) = Κ (- x) Π i≤n
⊟-step (acc wf) (Σ xs Π i≤n) = poly-map (⊟-step (wf _ i≤n)) xs Π↓ i≤n

⊟_ : ∀ {n} → Poly n → Poly n
⊟_ = ⊟-step (<′-wellFounded _)
{-# INLINE ⊟_ #-}

----------------------------------------------------------------------
-- Multiplication
----------------------------------------------------------------------
mutual
  ⊠-step′ : ∀ {n} → Acc _<′_ n → Poly n → Poly n → Poly n
  ⊠-step′ a (x Π i≤n) = ⊠-step a x i≤n

  ⊠-step : ∀ {i n} → Acc _<′_ n → FlatPoly i → i ≤′ n → Poly n → Poly n
  ⊠-step a (Κ x) _ = ⊠-Κ a x
  ⊠-step a (Σ xs)  = ⊠-Σ a xs

  ⊠-Κ : ∀ {n} → Acc _<′_ n → Carrier → Poly n → Poly n
  ⊠-Κ (acc _ ) x (Κ y  Π i≤n) = Κ (x * y) Π i≤n
  ⊠-Κ (acc wf) x (Σ xs Π i≤n) = ⊠-Κ-inj (wf _ i≤n) x xs Π↓ i≤n

  ⊠-Σ : ∀ {i n} → Acc _<′_ n → Coeff i + → i <′ n → Poly n → Poly n
  ⊠-Σ (acc wf) xs i≤n (Σ ys Π j≤n) = ⊠-match  (acc wf) (inj-compare i≤n j≤n) xs ys
  ⊠-Σ (acc wf) xs i≤n (Κ y Π _) = ⊠-Κ-inj (wf _ i≤n) y xs Π↓ i≤n

  ⊠-Κ-inj : ∀ {i}  → Acc _<′_ i → Carrier → Coeff i + → Coeff i *
  ⊠-Κ-inj a x xs = poly-map (⊠-Κ a x) (xs)

  ⊠-Σ-inj : ∀ {i k}
          → Acc _<′_ k
          → i <′ k
          → Coeff i +
          → Poly k
          → Poly k
  ⊠-Σ-inj (acc wf) i≤k x (Σ y Π j≤k) = ⊠-match (acc wf) (inj-compare i≤k j≤k) x y
  ⊠-Σ-inj (acc wf) i≤k x (Κ y Π j≤k) = ⊠-Κ-inj (wf _ i≤k) y x Π↓ i≤k

  ⊠-match : ∀ {i j n}
          → Acc _<′_ n
          → {i≤n : i <′ n}
          → {j≤n : j <′ n}
          → InjectionOrdering i≤n j≤n
          → Coeff i +
          → Coeff j +
          → Poly n
  ⊠-match (acc wf) (inj-eq i&j≤n)     xs ys = ⊠-coeffs (wf _ i&j≤n) xs ys               Π↓ i&j≤n
  ⊠-match (acc wf) (inj-lt i≤j-1 j≤n) xs ys = poly-map (⊠-Σ-inj (wf _ j≤n) i≤j-1 xs) (ys) Π↓ j≤n
  ⊠-match (acc wf) (inj-gt i≤n j≤i-1) xs ys = poly-map (⊠-Σ-inj (wf _ i≤n) j≤i-1 ys) (xs) Π↓ i≤n

  ⊠-coeffs : ∀ {n} → Acc _<′_ n → Coeff n + → Coeff n + → Coeff n *
  ⊠-coeffs a xs (y ≠0 Δ j & []) = poly-map (⊠-step′ a y) xs ⍓* j
  ⊠-coeffs a xs (y ≠0 Δ j & ∹ ys) = para (⊠-cons a y ys) xs ⍓* j

  ⊠-cons : ∀ {n}
          → Acc _<′_ n
          → Poly n
          → Coeff n +
          → Fold n
  -- ⊠-cons a y [] (x Π j≤n , xs) = ⊠-step a x j≤n y , xs
  ⊠-cons a y ys (x Π j≤n , xs) =
    ⊠-step a x j≤n y , ⊞-coeffs (poly-map (⊠-step a x j≤n) ys) xs
{-# INLINE ⊠-Κ #-}
{-# INLINE ⊠-coeffs #-}
{-# INLINE ⊠-cons #-}

infixl 7 _⊠_
_⊠_ : ∀ {n} → Poly n → Poly n → Poly n
_⊠_ = ⊠-step′ (<′-wellFounded _)
{-# INLINE _⊠_ #-}

----------------------------------------------------------------------
-- Constants and Variables
----------------------------------------------------------------------

-- The constant polynomial
κ : ∀ {n} → Carrier → Poly n
κ x = Κ x Π z≤′n
{-# INLINE κ #-}

-- A variable
ι : ∀ {n} → Fin n → Poly n
ι i = (κ 1# Δ 1 ∷↓ []) Π↓ Fin⇒≤ i
{-# INLINE ι #-}

----------------------------------------------------------------------
-- Exponentiation
----------------------------------------------------------------------
-- We try very hard to never do things like multiply by 1
-- unnecessarily. That's what all the weirdness here is for.
⊡-mult : ∀ {n} → ℕ → Poly n → Poly n
⊡-mult zero xs = xs
⊡-mult (suc n) xs = ⊡-mult n xs ⊠ xs

_⊡_+1 : ∀ {n} → Poly n → ℕ → Poly n
(Κ x  Π i≤n) ⊡ i +1  = Κ (x ^ i +1) Π i≤n
(Σ (x Δ j & []) Π i≤n) ⊡ i +1  = x .poly ⊡ i +1 Δ (j ℕ.+ i ℕ.* j) ∷↓ [] Π↓ i≤n
xs@(Σ (_ & ∹ _) Π i≤n) ⊡ i +1  = ⊡-mult i xs

infixr 8 _⊡_
_⊡_ : ∀ {n} → Poly n → ℕ → Poly n
_ ⊡ zero = κ 1#
xs ⊡ suc i = xs ⊡ i +1
{-# INLINE _⊡_ #-}

max_stars_repo_name: mckeankylej/agda-ring-solver

max_issues_repo_name: mckeankylej/agda-ring-solver

max_forks_repo_name: mckeankylej/agda-ring-solver


text:
{-

Constructing List ErrorPart from format strings. Supported formats

  %s : String
  %d : Nat
  %t : Term
  %n : Name
  %e : List ErrorPart

 Examples at the bottom.

-}
module Tactic.Reflection.Printf where

open import Prelude
open import Prelude.Variables
open import Builtin.Reflection

private

  data Format (A : Set) : Set where
    fmtLit  : A → Format A
    fmtStr  : Format A
    fmtNat  : Format A
    fmtTerm : Format A
    fmtName : Format A
    fmtErrs : Format A

  instance
    FunctorFormat : Functor Format
    FunctorFormat .fmap f (fmtLit x) = fmtLit (f x)
    FunctorFormat .fmap f fmtStr = fmtStr
    FunctorFormat .fmap f fmtNat = fmtNat
    FunctorFormat .fmap f fmtTerm = fmtTerm
    FunctorFormat .fmap f fmtName = fmtName
    FunctorFormat .fmap f fmtErrs = fmtErrs

  parseFormat : String → List (Format String)
  parseFormat = map (fmap packString) ∘ parse ∘ unpackString
    where
      cons : Char → List (Format (List Char)) → List (Format (List Char))
      cons c (fmtLit cs ∷ fs) = fmtLit (c ∷ cs) ∷ fs
      cons c fs = fmtLit [ c ] ∷ fs

      parse : List Char → List (Format (List Char))
      parse ('%' ∷ 's' ∷ fmt) = fmtStr  ∷ parse fmt
      parse ('%' ∷ 'd' ∷ fmt) = fmtNat  ∷ parse fmt
      parse ('%' ∷ 't' ∷ fmt) = fmtTerm ∷ parse fmt
      parse ('%' ∷ 'n' ∷ fmt) = fmtName ∷ parse fmt
      parse ('%' ∷ 'e' ∷ fmt) = fmtErrs ∷ parse fmt
      parse ('%' ∷ '%' ∷ fmt) = cons '%' (parse fmt)
      parse (c ∷ fmt)         = cons c (parse fmt)
      parse []                = []

  FormatErrorType : List (Format String) → Set ℓ → Set ℓ
  FormatErrorType [] Res = Res
  FormatErrorType (fmtLit _ ∷ fs) Res = FormatErrorType fs Res
  FormatErrorType (fmtStr   ∷ fs) Res = String         → FormatErrorType fs Res
  FormatErrorType (fmtNat   ∷ fs) Res = Nat            → FormatErrorType fs Res
  FormatErrorType (fmtTerm  ∷ fs) Res = Term           → FormatErrorType fs Res
  FormatErrorType (fmtName  ∷ fs) Res = Name           → FormatErrorType fs Res
  FormatErrorType (fmtErrs  ∷ fs) Res = List ErrorPart → FormatErrorType fs Res

-- Exported for library writers
formatError : (List ErrorPart → A) → (fmt : String) → FormatErrorType (parseFormat fmt) A
formatError {A = A} k = format [] ∘ parseFormat
  where
    format : List ErrorPart → (fmt : List (Format String)) → FormatErrorType fmt A
    format acc [] = k (reverse acc)
    format acc (fmtLit s ∷ fmt)   = format (strErr s        ∷ acc) fmt
    format acc (fmtStr   ∷ fmt) s = format (strErr s        ∷ acc) fmt
    format acc (fmtNat   ∷ fmt) n = format (strErr (show n) ∷ acc) fmt
    format acc (fmtTerm  ∷ fmt) t = format (termErr t       ∷ acc) fmt
    format acc (fmtName  ∷ fmt) x = format (nameErr x       ∷ acc) fmt
    format acc (fmtErrs  ∷ fmt) e = format (reverse e      ++ acc) fmt

-- Public API --

errorPartsFmt : (fmt : String) → FormatErrorType (parseFormat fmt) (List ErrorPart)
errorPartsFmt = formatError id

typeErrorFmt : (fmt : String) → FormatErrorType (parseFormat fmt) (TC A)
typeErrorFmt = formatError typeError

debugPrintFmt : String → Nat → (fmt : String) → FormatErrorType (parseFormat fmt) (TC ⊤)
debugPrintFmt tag lvl = formatError (debugPrint tag lvl)

-- Examples --

private

  _ : Name → Term → List ErrorPart
  _ = errorPartsFmt "%n : %t"

  _ : Name → Nat → Nat → TC A
  _ = typeErrorFmt "%n applied to %d arguments, expected %d"

  _ : Term → String → TC ⊤
  _ = debugPrintFmt "tactic.foo" 10 "solving %t with %s"

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Bundles for homogeneous binary relations
------------------------------------------------------------------------

-- The contents of this module should be accessed via `Relation.Binary`.

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

module Relation.Binary.Bundles where

open import Level
open import Relation.Nullary using (¬_)
open import Relation.Binary.Core
open import Relation.Binary.Definitions
open import Relation.Binary.Structures

------------------------------------------------------------------------
-- Setoids
------------------------------------------------------------------------

record PartialSetoid a ℓ : Set (suc (a ⊔ ℓ)) where
  field
    Carrier              : Set a
    _≈_                  : Rel Carrier ℓ
    isPartialEquivalence : IsPartialEquivalence _≈_

  open IsPartialEquivalence isPartialEquivalence public

  _≉_ : Rel Carrier _
  x ≉ y = ¬ (x ≈ y)

record Setoid c ℓ : Set (suc (c ⊔ ℓ)) where
  infix 4 _≈_
  field
    Carrier       : Set c
    _≈_           : Rel Carrier ℓ
    isEquivalence : IsEquivalence _≈_

  open IsEquivalence isEquivalence public

  partialSetoid : PartialSetoid c ℓ
  partialSetoid = record
    { isPartialEquivalence = isPartialEquivalence
    }

  open PartialSetoid partialSetoid public using (_≉_)

record DecSetoid c ℓ : Set (suc (c ⊔ ℓ)) where
  infix 4 _≈_
  field
    Carrier          : Set c
    _≈_              : Rel Carrier ℓ
    isDecEquivalence : IsDecEquivalence _≈_

  open IsDecEquivalence isDecEquivalence public

  setoid : Setoid c ℓ
  setoid = record
    { isEquivalence = isEquivalence
    }

  open Setoid setoid public using (partialSetoid; _≉_)

------------------------------------------------------------------------
-- Preorders
------------------------------------------------------------------------

record Preorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix 4 _≈_ _∼_
  field
    Carrier    : Set c
    _≈_        : Rel Carrier ℓ₁  -- The underlying equality.
    _∼_        : Rel Carrier ℓ₂  -- The relation.
    isPreorder : IsPreorder _≈_ _∼_

  open IsPreorder isPreorder public
    hiding (module Eq)

  module Eq where
    setoid : Setoid c ℓ₁
    setoid = record
      { isEquivalence = isEquivalence
      }

    open Setoid setoid public

------------------------------------------------------------------------
-- Partial orders
------------------------------------------------------------------------

record Poset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix 4 _≈_ _≤_
  field
    Carrier        : Set c
    _≈_            : Rel Carrier ℓ₁
    _≤_            : Rel Carrier ℓ₂
    isPartialOrder : IsPartialOrder _≈_ _≤_

  open IsPartialOrder isPartialOrder public
    hiding (module Eq)

  preorder : Preorder c ℓ₁ ℓ₂
  preorder = record
    { isPreorder = isPreorder
    }

  open Preorder preorder public
    using (module Eq)

record DecPoset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix 4 _≈_ _≤_
  field
    Carrier           : Set c
    _≈_               : Rel Carrier ℓ₁
    _≤_               : Rel Carrier ℓ₂
    isDecPartialOrder : IsDecPartialOrder _≈_ _≤_

  private
    module DPO = IsDecPartialOrder isDecPartialOrder
  open DPO public hiding (module Eq)

  poset : Poset c ℓ₁ ℓ₂
  poset = record
    { isPartialOrder = isPartialOrder
    }

  open Poset poset public
    using (preorder)

  module Eq where
    decSetoid : DecSetoid c ℓ₁
    decSetoid = record
      { isDecEquivalence = DPO.Eq.isDecEquivalence
      }

    open DecSetoid decSetoid public

record StrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix 4 _≈_ _<_
  field
    Carrier              : Set c
    _≈_                  : Rel Carrier ℓ₁
    _<_                  : Rel Carrier ℓ₂
    isStrictPartialOrder : IsStrictPartialOrder _≈_ _<_

  open IsStrictPartialOrder isStrictPartialOrder public
    hiding (module Eq)

  module Eq where
    setoid : Setoid c ℓ₁
    setoid = record
      { isEquivalence = isEquivalence
      }

    open Setoid setoid public

record DecStrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix 4 _≈_ _<_
  field
    Carrier                 : Set c
    _≈_                     : Rel Carrier ℓ₁
    _<_                     : Rel Carrier ℓ₂
    isDecStrictPartialOrder : IsDecStrictPartialOrder _≈_ _<_

  private
    module DSPO = IsDecStrictPartialOrder isDecStrictPartialOrder
  open DSPO public hiding (module Eq)

  strictPartialOrder : StrictPartialOrder c ℓ₁ ℓ₂
  strictPartialOrder = record
    { isStrictPartialOrder = isStrictPartialOrder
    }

  module Eq where

    decSetoid : DecSetoid c ℓ₁
    decSetoid = record
      { isDecEquivalence = DSPO.Eq.isDecEquivalence
      }

    open DecSetoid decSetoid public

------------------------------------------------------------------------
-- Total orders
------------------------------------------------------------------------

record TotalOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix 4 _≈_ _≤_
  field
    Carrier      : Set c
    _≈_          : Rel Carrier ℓ₁
    _≤_          : Rel Carrier ℓ₂
    isTotalOrder : IsTotalOrder _≈_ _≤_

  open IsTotalOrder isTotalOrder public
    hiding (module Eq)

  poset : Poset c ℓ₁ ℓ₂
  poset = record
    { isPartialOrder = isPartialOrder
    }

  open Poset poset public
    using (module Eq; preorder)

record DecTotalOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix 4 _≈_ _≤_
  field
    Carrier         : Set c
    _≈_             : Rel Carrier ℓ₁
    _≤_             : Rel Carrier ℓ₂
    isDecTotalOrder : IsDecTotalOrder _≈_ _≤_

  private
    module DTO = IsDecTotalOrder isDecTotalOrder
  open DTO public hiding (module Eq)

  totalOrder : TotalOrder c ℓ₁ ℓ₂
  totalOrder = record
    { isTotalOrder = isTotalOrder
    }

  open TotalOrder totalOrder public using (poset; preorder)

  decPoset : DecPoset c ℓ₁ ℓ₂
  decPoset = record
    { isDecPartialOrder = isDecPartialOrder
    }

  open DecPoset decPoset public using (module Eq)

-- Note that these orders are decidable. The current implementation
-- of `Trichotomous` subsumes irreflexivity and asymmetry. Any reasonable
-- definition capturing these three properties implies decidability
-- as `Trichotomous` necessarily separates out the equality case.

record StrictTotalOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
  infix 4 _≈_ _<_
  field
    Carrier            : Set c
    _≈_                : Rel Carrier ℓ₁
    _<_                : Rel Carrier ℓ₂
    isStrictTotalOrder : IsStrictTotalOrder _≈_ _<_

  open IsStrictTotalOrder isStrictTotalOrder public
    hiding (module Eq)

  strictPartialOrder : StrictPartialOrder c ℓ₁ ℓ₂
  strictPartialOrder = record
    { isStrictPartialOrder = isStrictPartialOrder
    }

  open StrictPartialOrder strictPartialOrder public
    using (module Eq)

  decSetoid : DecSetoid c ℓ₁
  decSetoid = record
    { isDecEquivalence = isDecEquivalence
    }
  {-# WARNING_ON_USAGE decSetoid
  "Warning: decSetoid was deprecated in v1.3.
  Please use Eq.decSetoid instead."
  #-}


text:
------------------------------------------------------------------------
-- Indexed containers
------------------------------------------------------------------------

-- Some parts are based on "Indexed containers" by Altenkirch, Ghani,
-- Hancock, McBride and Morris (JFP, 2015).

{-# OPTIONS --sized-types #-}

module Indexed-container where

open import Equality.Propositional
open import Logical-equivalence using (_⇔_)
open import Prelude
open import Prelude.Size

open import Bijection equality-with-J as Bijection using (_↔_)
import Equivalence equality-with-J as Eq
open import Function-universe equality-with-J hiding (id; _∘_)
open import H-level.Closure equality-with-J
open import Surjection equality-with-J using (_↠_)
open import Univalence-axiom equality-with-J

open import Relation

------------------------------------------------------------------------
-- Containers

-- Doubly indexed containers.

record Container {ℓ} (I O : Type ℓ) : Type (lsuc ℓ) where
  constructor _◁_
  field
    Shape    : Rel ℓ O
    Position : ∀ {o} → Shape o → Rel ℓ I

-- Interpretation of containers.

⟦_⟧ : ∀ {ℓ₁ ℓ₂} {I O : Type ℓ₁} →
      Container I O → Rel ℓ₂ I → Rel (ℓ₁ ⊔ ℓ₂) O
⟦ S ◁ P ⟧ A = λ o → ∃ λ (s : S o) → P s ⊆ A

-- A map function.

map : ∀ {ℓ₁ ℓ₂ ℓ₃} {I O : Type ℓ₁} (C : Container I O)
        {A : Rel ℓ₂ I} {B : Rel ℓ₃ I} →
      A ⊆ B → ⟦ C ⟧ A ⊆ ⟦ C ⟧ B
map _ f (s , g) = (s , f ∘ g)

-- Functor laws.

map-id : ∀ {ℓ₁ ℓ₂} {I O : Type ℓ₁} {C : Container I O} {A : Rel ℓ₂ I} →
         _≡_ {A = ⟦ C ⟧ A ⊆ _} (map C id) id
map-id = refl

map-∘ : ∀ {ℓ₁ ℓ₂ ℓ₃ ℓ₄} {I O : Type ℓ₁} {C : Container I O}
          {D : Rel ℓ₂ I} {E : Rel ℓ₃ I} {F : Rel ℓ₄ I}
        (f : E ⊆ F) (g : D ⊆ E) →
        _≡_ {A = ⟦ C ⟧ D ⊆ _} (map C (f ∘ g)) (map C f ∘ map C g)
map-∘ _ _ = refl

-- A preservation lemma.

⟦⟧-cong : ∀ {k ℓ₁ ℓ₂ ℓ₃} {I O : Type ℓ₁} →
          Extensionality? k ℓ₁ (ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃) →
          (C : Container I O) {A : Rel ℓ₂ I} {B : Rel ℓ₃ I} →
          (∀ {i} → A i ↝[ k ] B i) →
          (∀ {o} → ⟦ C ⟧ A o ↝[ k ] ⟦ C ⟧ B o)
⟦⟧-cong ext (S ◁ P) {A} {B} A↝B {o} =
  (∃ λ (s : S o) → P s ⊆ A)  ↝⟨ (∃-cong λ _ → ⊆-congʳ ext A↝B) ⟩□
  (∃ λ (s : S o) → P s ⊆ B)  □

-- The shapes of a container are in pointwise bijective correspondence
-- with the interpretation of the container applied to the constant
-- function yielding the unit type.
--
-- (This lemma was suggested to me by an anonymous reviewer of another
-- paper.)

Shape↔⟦⟧⊤ : ∀ {ℓ} {I O : Type ℓ} (C : Container I O) {o} →
            Container.Shape C o ↔ ⟦ C ⟧ (λ _ → ⊤) o
Shape↔⟦⟧⊤ C {o} =
  Shape C o                                         ↝⟨ inverse $ drop-⊤-right (λ _ → →-right-zero) ⟩
  (∃ λ (s : Shape C o) → ∃ (Position C s) → ⊤)      ↝⟨ ∃-cong (λ _ → currying) ⟩
  (∃ λ (s : Shape C o) → ∀ i → Position C s i → ⊤)  ↝⟨ ∃-cong (λ _ → inverse Bijection.implicit-Π↔Π) ⟩□
  (∃ λ (s : Shape C o) → Position C s ⊆ (λ _ → ⊤))  □
  where
  open Container

------------------------------------------------------------------------
-- Least fixpoints

mutual

  -- The least fixpoint of an indexed "endocontainer", expressed using
  -- sized types.

  μ : ∀ {ℓ} {X : Type ℓ} → Container X X → Size → Rel ℓ X
  μ C i = ⟦ C ⟧ (μ′ C i)

  data μ′ {ℓ} {X : Type ℓ}
          (C : Container X X) (i : Size) (x : X) : Type ℓ where
    ⟨_⟩ : {j : Size< i} → μ C j x → μ′ C i x

-- The least fixpoint μ C ∞ is pointwise logically equivalent to
-- μ′ C ∞.

μ⇔μ′ :
  ∀ {ℓ} {X : Type ℓ} {C : Container X X} {x : X} →
  μ C ∞ x ⇔ μ′ C ∞ x
μ⇔μ′ = record
  { to   = ⟨_⟩
  ; from = λ { ⟨ x ⟩ → x }
  }

-- The least fixpoint is a post-fixpoint.

μ-out :
  ∀ {ℓ} {X : Type ℓ} {C : Container X X} →
  μ C ∞ ⊆ ⟦ C ⟧ (μ C ∞)
μ-out {C = C} = map C (_⇔_.from μ⇔μ′)

-- The least fixpoint is a pre-fixpoint.

μ-in :
  ∀ {ℓ} {X : Type ℓ} {C : Container X X} →
  ⟦ C ⟧ (μ C ∞) ⊆ μ C ∞
μ-in {C = C} = map C (_⇔_.to μ⇔μ′)

-- The least fixpoint is smaller than or equal to every
-- pre-fixpoint.

fold :
  ∀ {ℓ₁ ℓ₂} {X : Type ℓ₁} (C : Container X X) {A : Rel ℓ₂ X} →
  ⟦ C ⟧ A ⊆ A →
  ∀ {i} → μ C i ⊆ A
fold C f a = f (map C (λ { ⟨ a ⟩ → fold C f a }) a)

------------------------------------------------------------------------
-- Greatest fixpoints

mutual

  -- The greatest fixpoint of an indexed "endocontainer", expressed
  -- using sized types.

  ν : ∀ {ℓ} {X : Type ℓ} → Container X X → Size → Rel ℓ X
  ν C i = ⟦ C ⟧ (ν′ C i)

  record ν′ {ℓ} {X : Type ℓ}
            (C : Container X X) (i : Size) (x : X) : Type ℓ where
    coinductive
    field
      force : {j : Size< i} → ν C j x

open ν′ public

-- The greatest fixpoint ν C ∞ is pointwise logically equivalent to
-- ν′ C ∞.

ν⇔ν′ :
  ∀ {ℓ} {X : Type ℓ} {C : Container X X} {x : X} →
  ν C ∞ x ⇔ ν′ C ∞ x
ν⇔ν′ = record
  { to   = λ { x .force → x }
  ; from = λ x → force x
  }

-- The greatest fixpoint ν C ∞ is a post-fixpoint.

ν-out :
  ∀ {ℓ} {X : Type ℓ} {i} {j : Size< i} (C : Container X X) →
  ν C i ⊆ ⟦ C ⟧ (ν C j)
ν-out C = map C (λ x → force x)

private

  ν-out-∞ :
    ∀ {ℓ} {X : Type ℓ} (C : Container X X) →
    ν C ∞ ⊆ ⟦ C ⟧ (ν C ∞)
  ν-out-∞ = ν-out

-- The greatest fixpoint is a pre-fixpoint.

ν-in :
  ∀ {ℓ} {X : Type ℓ} {i} (C : Container X X) →
  ⟦ C ⟧ (ν C i) ⊆ ν C i
ν-in C = map C (λ x → λ { .force → x })

-- The greatest fixpoint is greater than or equal to every
-- post-fixpoint.

unfold :
  ∀ {ℓ₁ ℓ₂} {X : Type ℓ₁} {A : Rel ℓ₂ X} {i} (C : Container X X) →
  A ⊆ ⟦ C ⟧ A → A ⊆ ν C i
unfold C f = map C (λ a → λ { .force → unfold C f a }) ∘ f

-- A generalisation of unfold with more sized types.

sized-unfold :
  ∀ {ℓ₁ ℓ₂} {X : Type ℓ₁} (C : Container X X) (A : Size → Rel ℓ₂ X) →
  (∀ {i} {j : Size< i} → A i ⊆ ⟦ C ⟧ (A j)) →
  ∀ {i} {j : Size< i} → A i ⊆ ν C j
sized-unfold C A f =
  map C (λ a → λ { .force → sized-unfold C A f a }) ∘ f

------------------------------------------------------------------------
-- Bisimilarity

-- A container corresponding to bisimilarity for a given container.

Bisimilarity :
  ∀ {ℓ} {X : Type ℓ} {C : Container X X} →
  let P = ∃ λ x → ν C ∞ x × ν C ∞ x in
  Container P P
Bisimilarity {C = C} =
  (λ { (_ , (s₁ , _) , (s₂ , _)) → s₁ ≡ s₂ })
    ◁
  (λ { {o = _ , (s₁ , f₁) , (s₂ , f₂)} eq (x , x₁ , x₂) →
       ∃ λ (p : Container.Position C s₁ x) →
       x₁ ≡ force (f₁ p)
         ×
       x₂ ≡ force (f₂ (subst (λ s → Container.Position C s x) eq p)) })

-- Bisimilarity for ν.

ν-bisimilar :
  ∀ {ℓ} {X : Type ℓ} {C : Container X X} {x} →
  Size → Rel₂ ℓ (ν C ∞ x)
ν-bisimilar i p = ν Bisimilarity i (_ , p)

ν′-bisimilar :
  ∀ {ℓ} {X : Type ℓ} {C : Container X X} {x} →
  Size → Rel₂ ℓ (ν′ C ∞ x)
ν′-bisimilar i (x , y) = ν′ Bisimilarity i (_ , force x , force y)

-- Lifts a family of binary relations from X to ⟦ C ⟧ X.

⟦_⟧₂ :
  ∀ {ℓ₁ ℓ₂} {I O : Type ℓ₁} {A : Rel ℓ₂ I} (C : Container I O) →
  (∀ {i} → Rel₂ ℓ₁ (A i)) →
  ∀ {o} → Rel₂ ℓ₁ (⟦ C ⟧ A o)
⟦ C ⟧₂ R ((s , f) , (t , g)) =
  ∃ λ (eq : s ≡ t) →
  ∀ {o} (p : Position C s o) →
  R (f p , g (subst (λ s → Position C s o) eq p))
  where
  open Container

-- An alternative characterisation of bisimilarity.

ν-bisimilar↔ :
  ∀ {k ℓ} {X : Type ℓ} {C : Container X X} {x i} →
  Extensionality? k ℓ ℓ →
  (x y : ν C ∞ x) →
  ν-bisimilar i (x , y) ↝[ k ] ⟦ C ⟧₂ (ν′-bisimilar i) (x , y)
ν-bisimilar↔ {C = C} {i = i} ext (s₁ , f₁) (s₂ , f₂) =

  ν-bisimilar i ((s₁ , f₁) , (s₂ , f₂))                             ↔⟨⟩

  (∃ λ (eq : s₁ ≡ s₂) →
   ∀ {x} →
   (∃ λ (p : Position C s₁ (proj₁ x)) →
      proj₁ (proj₂ x) ≡ force (f₁ p) ×
      proj₂ (proj₂ x) ≡
        force (f₂ (subst (λ s → Position C s (proj₁ x)) eq p))) →
   ν′ Bisimilarity i x)                                             ↝⟨ ∃-cong lemma ⟩

  (∃ λ (eq : s₁ ≡ s₂) →
   ∀ {x} (p : Position C s₁ x) →
   ν′-bisimilar i (f₁ p , f₂ (subst (λ s → Position C s x) eq p)))  ↔⟨⟩

  ⟦ C ⟧₂ (ν′-bisimilar i) ((s₁ , f₁) , (s₂ , f₂))                   □

  where
  open Container

  lemma = λ eq →

    (∀ {x} →
     (∃ λ (p : Position C s₁ (proj₁ x)) →
      proj₁ (proj₂ x) ≡ force (f₁ p) ×
      proj₂ (proj₂ x) ≡
        force (f₂ (subst (λ s → Position C s (proj₁ x)) eq p))) →
     ν′ Bisimilarity i x)                                                 ↔⟨ Bijection.implicit-Π↔Π ⟩

    (∀ x →
     (∃ λ (p : Position C s₁ (proj₁ x)) →
      proj₁ (proj₂ x) ≡ force (f₁ p) ×
      proj₂ (proj₂ x) ≡
        force (f₂ (subst (λ s → Position C s (proj₁ x)) eq p))) →
     ν′ Bisimilarity i x)                                                 ↝⟨ (∀-cong ext λ _ → from-isomorphism currying) ⟩

    (∀ x (p : Position C s₁ (proj₁ x)) →
     proj₁ (proj₂ x) ≡ force (f₁ p) ×
     proj₂ (proj₂ x) ≡
       force (f₂ (subst (λ s → Position C s (proj₁ x)) eq p)) →
     ν′ Bisimilarity i x)                                                 ↝⟨ (∀-cong ext λ _ → ∀-cong ext λ _ → from-isomorphism currying) ⟩

    (∀ x (p : Position C s₁ (proj₁ x)) →
     proj₁ (proj₂ x) ≡ force (f₁ p) →
     proj₂ (proj₂ x) ≡
       force (f₂ (subst (λ s → Position C s (proj₁ x)) eq p)) →
     ν′ Bisimilarity i x)                                                 ↔⟨ currying ⟩

    (∀ x yz (p : Position C s₁ x) →
     proj₁ yz ≡ force (f₁ p) →
     proj₂ yz ≡ force (f₂ (subst (λ s → Position C s x) eq p)) →
     ν′ Bisimilarity i (x , yz))                                          ↝⟨ (∀-cong ext λ _ → from-isomorphism Π-comm) ⟩

    (∀ x (p : Position C s₁ x) yz →
     proj₁ yz ≡ force (f₁ p) →
     proj₂ yz ≡ force (f₂ (subst (λ s → Position C s x) eq p)) →
     ν′ Bisimilarity i (x , yz))                                          ↝⟨ (∀-cong ext λ _ → ∀-cong ext λ _ → from-isomorphism currying) ⟩

    (∀ x (p : Position C s₁ x) y z →
     y ≡ force (f₁ p) →
     z ≡ force (f₂ (subst (λ s → Position C s x) eq p)) →
     ν′ Bisimilarity i (x , y , z))                                       ↝⟨ (∀-cong ext λ _ → ∀-cong ext λ _ → ∀-cong ext λ _ →
                                                                              from-isomorphism Π-comm) ⟩
    (∀ x (p : Position C s₁ x) →
     ∀ y → y ≡ force (f₁ p) →
     ∀ z → z ≡ force (f₂ (subst (λ s → Position C s x) eq p)) →
     ν′ Bisimilarity i (x , y , z))                                       ↝⟨ (∀-cong ext λ _ → ∀-cong ext λ _ →
                                                                              from-isomorphism $ inverse currying) ⟩
    (∀ x (p : Position C s₁ x) →
     (y : ∃ λ y → y ≡ force (f₁ p)) →
     ∀ z → z ≡ force (f₂ (subst (λ s → Position C s x) eq p)) →
     ν′ Bisimilarity i (x , proj₁ y , z))                                 ↝⟨ (∀-cong ext λ _ → ∀-cong ext λ _ → drop-⊤-left-Π ext (
                                                                              _⇔_.to contractible⇔↔⊤ $ singleton-contractible _)) ⟩
    (∀ x (p : Position C s₁ x) →
     ∀ z → z ≡ force (f₂ (subst (λ s → Position C s x) eq p)) →
     ν′ Bisimilarity i (x , force (f₁ p) , z))                            ↝⟨ (∀-cong ext λ _ → ∀-cong ext λ _ →
                                                                              from-isomorphism $ inverse currying) ⟩
    (∀ x (p : Position C s₁ x) →
     (z : ∃ λ z → z ≡ force (f₂ (subst (λ s → Position C s x) eq p))) →
     ν′ Bisimilarity i (x , force (f₁ p) , proj₁ z))                      ↝⟨ (∀-cong ext λ _ → ∀-cong ext λ _ → drop-⊤-left-Π ext (
                                                                              _⇔_.to contractible⇔↔⊤ $ singleton-contractible _)) ⟩
    (∀ x (p : Position C s₁ x) →
     ν′ Bisimilarity i
       (x , force (f₁ p)
          , force (f₂ (subst (λ s → Position C s x) eq p))))              ↔⟨ inverse $ Bijection.implicit-Π↔Π ⟩

    (∀ {x} (p : Position C s₁ x) →
     ν′ Bisimilarity i
       (x , force (f₁ p)
          , force (f₂ (subst (λ s → Position C s x) eq p))))              ↔⟨⟩

    (∀ {x} (p : Position C s₁ x) →
     ν′-bisimilar i (f₁ p , f₂ (subst (λ s → Position C s x) eq p)))      □

module Bisimilarity
         {ℓ} {X : Type ℓ} {C : Container X X} {x i}
         (x y : ν C ∞ x)
         where

  -- A "constructor".

  ⟨_,_,_,_⟩ :
    (eq : proj₁ x ≡ proj₁ y) →
    (∀ {o} (p : Container.Position C (proj₁ x) o) →
     ν′-bisimilar i
       ( proj₂ x p
       , proj₂ y (subst (λ s → Container.Position C s o) eq p)
       )) →
    ν-bisimilar i (x , y)
  ⟨_,_,_,_⟩ = curry $ _⇔_.from (ν-bisimilar↔ _ x y)

  -- A "projection".

  split : ν-bisimilar i (x , y) → ⟦ C ⟧₂ (ν′-bisimilar i) (x , y)
  split = ν-bisimilar↔ _ x y

-- Bisimilarity is reflexive.

reflexive-ν :
  ∀ {ℓ} {X : Type ℓ} {C : Container X X} {x} (x : ν C ∞ x) {i} →
  ν-bisimilar i (x , x)
reflexive-ν x =
  Bisimilarity.⟨ x , x , refl
               , (λ { p .force → reflexive-ν (force (proj₂ x p)) })
               ⟩

-- Bisimilarity is symmetric.

symmetric-ν :
  ∀ {ℓ} {X : Type ℓ} {C : Container X X} {x} (x y : ν C ∞ x) {i} →
  ν-bisimilar i (x , y) → ν-bisimilar i (y , x)
symmetric-ν x y bisim with Bisimilarity.split x y bisim
... | refl , bisim′ =
  Bisimilarity.⟨ y , x , refl
               , (λ { p .force →
                      symmetric-ν (force (proj₂ x p))
                                  (force (proj₂ y p))
                                  (force (bisim′ p)) })
               ⟩

-- Bisimilarity is transitive.

transitive-ν :
  ∀ {ℓ} {X : Type ℓ} {C : Container X X} {x} (x y z : ν C ∞ x) {i} →
  ν-bisimilar i (x , y) → ν-bisimilar i (y , z) →
  ν-bisimilar i (x , z)
transitive-ν x y z bisim₁ bisim₂ with Bisimilarity.split x y bisim₁
                                    | Bisimilarity.split y z bisim₂
... | refl , bisim₁′ | refl , bisim₂′ =
  Bisimilarity.⟨ x
               , z
               , refl
               , (λ { p .force →
                      transitive-ν
                        (force (proj₂ x p))
                        (force (proj₂ y p))
                        (force (proj₂ z p))
                        (force (bisim₁′ p))
                        (force (bisim₂′ p)) })
               ⟩

-- Extensionality for ν′ C: bisimilarity implies equality.
--
-- Note that I have not, at the time of writing, determined whether
-- this is a consistent assumption. Uses of this and similar
-- assumptions are tracked using the type system.

ν′-extensionality : ∀ {ℓ} {X : Type ℓ} → Container X X → Type ℓ
ν′-extensionality C =
  ∀ {x} {y z : ν′ C ∞ x} → ν′-bisimilar ∞ (y , z) → y ≡ z

-- The formulation of extensionality given above for ν′ can be used to
-- derive a form of extensionality for ν (in the presence of
-- extensionality for functions).

ν-extensionality :
  ∀ {ℓ} {X : Type ℓ} {C : Container X X} →
  Extensionality ℓ ℓ →
  ν′-extensionality C →
  ∀ {x} {y z : ν C ∞ x} → ν-bisimilar ∞ (y , z) → y ≡ z
ν-extensionality {C = C} ext ν′-ext
                 {y = y@(s , f₁)} {z = z@(.s , f₂)} bisim@(refl , _) =

                                                             $⟨ (λ _ → proj₂ $ Bisimilarity.split y z bisim) ⟩
  (∀ x (p : Position C s x) → ν′-bisimilar ∞ (f₁ p , f₂ p))  ↝⟨ (ν′-ext ∘_) ∘_ ⟩
  (∀ x (p : Position C s x) → f₁ p ≡ f₂ p)                   ↝⟨ implicit-extensionality ext ∘ (apply-ext ext ∘_) ⟩
  (λ {_} → f₁) ≡ f₂                                          ↝⟨ cong (s ,_) ⟩□
  y ≡ z                                                      □

  where
  open Container

------------------------------------------------------------------------
-- More properties related to ν and ν′

-- The greatest fixpoint is a fixpoint in a different sense
-- (assuming two kinds of extensionality and univalence).

ν-fixpoint :
  ∀ {ℓ} →
  Extensionality ℓ (lsuc ℓ) →
  Univalence ℓ →
  {X : Type ℓ} (C : Container X X) →
  ν′-extensionality C →
  ν C ∞ ≡ ⟦ C ⟧ (ν C ∞)
ν-fixpoint ext univ C ν′-ext =
  ν C ∞           ≡⟨⟩
  ⟦ C ⟧ (ν′ C ∞)  ≡⟨ cong ⟦ C ⟧ (apply-ext ext λ _ → ≃⇒≡ univ (Eq.↔⇒≃ ν′↔ν)) ⟩
  ⟦ C ⟧ (ν C ∞)   ∎
  where
  ν′↔ν : ∀ {x} → ν′ C ∞ x ↔ ν C ∞ x
  ν′↔ν = record
    { surjection = record
      { logical-equivalence = record
        { to   = λ x → force x
        ; from = λ x → record { force = x }
        }
      ; right-inverse-of = λ _ → refl
      }
    ; left-inverse-of = λ x →
        ν′-ext (record { force = reflexive-ν (force x) })
    }

-- The unfold function makes a certain diagram commute.

unfold-commute :
  ∀ {ℓ₁ ℓ₂} {X : Type ℓ₁} (C : Container X X) {A : Rel ℓ₂ X}
  (f : A ⊆ ⟦ C ⟧ A) →
  ∀ {i x} (a : A x) →
  ν-bisimilar i
    ( unfold C f a
    , ν-in C (map C (unfold C f) (f a))
    )
unfold-commute C f a =
  Bisimilarity.⟨ unfold C f a
               , ν-in C (map C (unfold C f) (f a))
               , refl
               , (λ { p .force →
                      reflexive-ν (unfold C f (proj₂ (f a) p)) })
               ⟩

-- A uniqueness property for unfold.

unfold-unique :
  ∀ {ℓ₁ ℓ₂} {X : Type ℓ₁} (C : Container X X) {A : Rel ℓ₂ X}
  (f : A ⊆ ⟦ C ⟧ A) (u : A ⊆ ν C ∞) {i} →
  (∀ {x} (a : A x) →
   ν-bisimilar i (u a , ν-in C (map C u (f a)))) →
  ∀ {x} (a : A x) → ν-bisimilar i (u a , unfold C f a)
unfold-unique C f u bisim a
  with Bisimilarity.split (u a) (ν-in C (map C u (f a))) (bisim a)
... | eq , bisim′ =
  Bisimilarity.⟨ u a
               , unfold C f a
               , eq
               , (λ { p .force →
                      let p′ = subst (λ s → Container.Position C s _)
                                     eq p in
                      transitive-ν
                        (force (proj₂ (u a) p))
                        (force (proj₂ (ν-in C (map C u (f a))) p′))
                        (force (proj₂ (unfold C f a) p′))
                        (force (bisim′ p))
                        (unfold-unique C f u bisim _) })
               ⟩

------------------------------------------------------------------------
-- An alternative definition of greatest fixpoints

-- The greatest fixpoint of an indexed "endocontainer" (parametrised
-- by a universe level).

gfp : ∀ {ℓ₁} ℓ₂ {X : Type ℓ₁} → Container X X → Rel (lsuc (ℓ₁ ⊔ ℓ₂)) X
gfp {ℓ₁} ℓ₂ {X} C x = ∃ λ (R : Rel (ℓ₁ ⊔ ℓ₂) X) → R ⊆ ⟦ C ⟧ R × R x

-- The greatest fixpoint is greater than or equal to every
-- sufficiently small post-fixpoint.

gfp-unfold :
  ∀ {ℓ₁ ℓ₂} ℓ₃ {X : Type ℓ₁} {C : Container X X} {A : Rel ℓ₂ X} →
  A ⊆ ⟦ C ⟧ A →
  A ⊆ gfp (ℓ₂ ⊔ ℓ₃) C
gfp-unfold {ℓ₁} ℓ₃ {C = C} {A} f a =
  ↑ (ℓ₁ ⊔ ℓ₃) ∘ A , map C lift ∘ f ∘ lower , lift a

-- The greatest fixpoint is a post-fixpoint.

gfp-out : ∀ {ℓ₁} ℓ₂ {X : Type ℓ₁} {C : Container X X} →
          gfp ℓ₂ C ⊆ ⟦ C ⟧ (gfp ℓ₂ C)
gfp-out ℓ₂ {C = C} (R , R⊆CR , Ri) =
  map C (λ Ri → R , (λ {_} → R⊆CR) , Ri) (R⊆CR Ri)

  -- It is possible to use gfp-unfold ℓ₂ R⊆CR as the second argument
  -- to map above. However, the extra lifting would break the proof
  -- gfp⊆ν∘ν⊆gfp given below.

-- The first definition of greatest fixpoints is contained in the
-- second one.

ν⊆gfp : ∀ {ℓ₁} ℓ₂ {X : Type ℓ₁} {C : Container X X} →
        ν C ∞ ⊆ gfp ℓ₂ C
ν⊆gfp ℓ₂ = gfp-unfold ℓ₂ (ν-out {i = ∞} _)

-- The second definition of greatest fixpoints is contained in the
-- first one.

gfp⊆ν : ∀ {ℓ₁} ℓ₂ {X : Type ℓ₁} {C : Container X X} {i} →
        gfp ℓ₂ C ⊆ ν C i
gfp⊆ν ℓ₂ = unfold _ (gfp-out ℓ₂)

-- Thus the two definitions of greatest fixpoints are pointwise
-- logically equivalent.

gfp⇔ν : ∀ {ℓ₁} ℓ₂ {X : Type ℓ₁} {C : Container X X} {i} →
        gfp ℓ₂ C i ⇔ ν C ∞ i
gfp⇔ν ℓ₂ = record
  { to   = gfp⊆ν ℓ₂
  ; from = ν⊆gfp ℓ₂
  }

-- The function gfp⊆ν is a left inverse of ν⊆gfp (up to pointwise
-- bisimilarity).

gfp⊆ν∘ν⊆gfp :
  ∀ {ℓ₁} ℓ₂ {X : Type ℓ₁} {C : Container X X} {x} (x : ν C ∞ x) {i} →
  ν-bisimilar i (gfp⊆ν ℓ₂ (ν⊆gfp ℓ₂ x) , x)
gfp⊆ν∘ν⊆gfp ℓ₂ {C = C} x =
  _⇔_.from (ν-bisimilar↔ _ (gfp⊆ν ℓ₂ (ν⊆gfp ℓ₂ x)) x)
    ( refl
    , (λ { p .force → gfp⊆ν∘ν⊆gfp ℓ₂ (force (proj₂ x p)) })
    )

-- There is a split surjection from the second definition of greatest
-- fixpoints to the first one (assuming two kinds of extensionality).

gfp↠ν :
  ∀ {ℓ₁} →
  Extensionality ℓ₁ ℓ₁ →
  ∀ ℓ₂ {X : Type ℓ₁} {C : Container X X} →
  ν′-extensionality C →
  ∀ {x} → gfp ℓ₂ C x ↠ ν C ∞ x
gfp↠ν ext ℓ₂ ν′-ext = record
  { logical-equivalence = gfp⇔ν ℓ₂
  ; right-inverse-of    = λ x →
      ν-extensionality ext ν′-ext (gfp⊆ν∘ν⊆gfp ℓ₂ x)
  }

-- The larger versions of gfp are logically equivalent to the smallest
-- one.

larger⇔smallest :
  ∀ {ℓ₁} ℓ₂ {X : Type ℓ₁} {C : Container X X} {x} →
  gfp ℓ₂ C x ⇔ gfp lzero C x
larger⇔smallest ℓ₂ {C = C} {x} =
  gfp ℓ₂ C x     ↝⟨ gfp⇔ν ℓ₂ ⟩
  ν C ∞ x        ↝⟨ inverse $ gfp⇔ν lzero ⟩□
  gfp lzero C x  □

max_stars_repo_name: nad/up-to

max_issues_repo_name: nad/up-to

max_forks_repo_name: nad/up-to


text:
module Utilities.ExistsSyntax where

open import Level using (Level ; _⊔_)
open import Data.Product using (Σ)

variable
  a b : Level
  A : Set a
  B : Set b

∃-syntax : (A : Set a) → (A → Set b) → Set (a ⊔ b)
∃-syntax = Σ

syntax ∃-syntax A (λ x → B) = ∃ x ∶ A • B

max_stars_repo_name: armkeh/agda-computability

max_issues_repo_name: armkeh/agda-computability

max_forks_repo_name: armkeh/agda-computability


text:
------------------------------------------------------------------------
-- An example showing how Container.Tree-sort can be used
------------------------------------------------------------------------

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

open import Equality

module Container.Tree-sort.Example
  {c⁺} (eq : ∀ {a p} → Equality-with-J a p c⁺) where

open Derived-definitions-and-properties eq

open import Prelude using (ℕ; zero; suc; Bool; true; false)

open import Container eq
open import Container.List eq

-- Comparison function for natural numbers.

_≤_ : ℕ → ℕ → Bool
zero  ≤ _     = true
suc _ ≤ zero  = false
suc m ≤ suc n = m ≤ n

open import Container.Tree-sort eq _≤_

-- The sort function seems to return an ordered list.

ordered : sort (3 ∷ 1 ∷ 2 ∷ []) ≡ 1 ∷ 2 ∷ 3 ∷ []
ordered = refl _

-- The sort function definitely returns a list which is bag equivalent
-- to the input. This property can be used to establish bag
-- equivalences between concrete lists.

a-bag-equivalence : 1 ∷ 2 ∷ 3 ∷ [] ≈-bag 3 ∷ 1 ∷ 2 ∷ []
a-bag-equivalence = sort≈ (3 ∷ 1 ∷ 2 ∷ [])

max_stars_repo_name: nad/equality

max_issues_repo_name: nad/equality

max_forks_repo_name: nad/equality


text:
------------------------------------------------------------------------
-- Inversion of (sub)typing in Fω with interval kinds
------------------------------------------------------------------------

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

module FOmegaInt.Typing.Inversion where

open import Data.Product using (_,_; proj₁; proj₂; _×_; map)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Relation.Nullary using (¬_)

open import FOmegaInt.Syntax
open import FOmegaInt.Typing
open import FOmegaInt.Typing.Validity
open import FOmegaInt.Kinding.Declarative.Normalization
open import FOmegaInt.Kinding.Canonical.Equivalence
  using (sound-<:; sound-<∷; complete-<∷; complete-<:-⋯)
import FOmegaInt.Kinding.Canonical.Inversion as CanInv

open Syntax
open TermCtx hiding (map)
open Typing
open Substitution using (_[_]; weaken)
open WfCtxOps using (lookup-tp)
open TypedSubstitution
open TypedNarrowing

------------------------------------------------------------------------
-- Generation/inversion of typing.

infix 4 _⊢Tm-gen_∈_

-- The possible types of a term (i.e. the possible results of
-- generating/inverting _⊢Tp_∈_).
data _⊢Tm-gen_∈_ {n} (Γ : Ctx n) : Term n → Term n → Set where
  ∈-var : ∀ {a b} x → Γ ctx → lookup Γ x ≡ tp a → Γ ⊢ a <: b ∈ * →
          Γ ⊢Tm-gen var x ∈ b
  ∈-∀-i : ∀ {k a b c} → Γ ⊢ k kd → kd k ∷ Γ ⊢Tm a ∈ b → Γ ⊢ Π k b <: c ∈ * →
          Γ ⊢Tm-gen Λ k a ∈ c
  ∈-→-i : ∀ {a b c d} → Γ ⊢Tp a ∈ * → tp a ∷ Γ ⊢Tm b ∈ weaken c →
          Γ ⊢ a ⇒ c <: d ∈ * → Γ ⊢Tm-gen ƛ a b ∈ d
  ∈-∀-e : ∀ {a b k c d} → Γ ⊢Tm a ∈ Π k c → Γ ⊢Tp b ∈ k → Γ ⊢ c [ b ] <: d ∈ * →
          Γ ⊢Tm-gen a ⊡ b ∈ d
  ∈-→-e : ∀ {a b c d e} → Γ ⊢Tm a ∈ c ⇒ d → Γ ⊢Tm b ∈ c → Γ ⊢ d <: e ∈ * →
          Γ ⊢Tm-gen a · b ∈ e

-- Generation/inversion of typing.
Tm∈-gen : ∀ {n} {Γ : Ctx n} {a b} → Γ ⊢Tm a ∈ b → Γ ⊢Tm-gen a ∈ b
Tm∈-gen (∈-var x Γ-ctx Γ[x]≡kd-a) =
  ∈-var x Γ-ctx Γ[x]≡kd-a (<:-refl (Tm∈-valid (∈-var x Γ-ctx Γ[x]≡kd-a)))
Tm∈-gen (∈-∀-i k-kd a∈b) =
  ∈-∀-i k-kd a∈b (<:-refl (Tm∈-valid (∈-∀-i k-kd a∈b)))
Tm∈-gen (∈-→-i a∈* b∈c c∈*) =
  ∈-→-i a∈* b∈c (<:-refl (Tm∈-valid (∈-→-i a∈* b∈c c∈*)))
Tm∈-gen (∈-∀-e a∈∀kc b∈k) =
  ∈-∀-e a∈∀kc b∈k (<:-refl (Tm∈-valid (∈-∀-e a∈∀kc b∈k)))
Tm∈-gen (∈-→-e a∈c⇒d b∈c) =
  ∈-→-e a∈c⇒d b∈c (<:-refl (Tm∈-valid (∈-→-e a∈c⇒d b∈c)))
Tm∈-gen (∈-⇑ a∈b   b<:c) with Tm∈-gen a∈b
Tm∈-gen (∈-⇑ x∈b   c<:d) | ∈-var x Γ-ctx Γ[x]≡kd-a a<:b =
  ∈-var x Γ-ctx Γ[x]≡kd-a (<:-trans a<:b c<:d)
Tm∈-gen (∈-⇑ Λka∈b b<:c) | ∈-∀-i k-kd a∈d ∀kd<:b   =
  ∈-∀-i k-kd a∈d (<:-trans ∀kd<:b b<:c)
Tm∈-gen (∈-⇑ ƛab∈c c<:d) | ∈-→-i a∈* b∈c a⇒c<:d    =
  ∈-→-i a∈* b∈c (<:-trans a⇒c<:d c<:d)
Tm∈-gen (∈-⇑ a·b∈e e<:f) | ∈-∀-e a∈Πcd b∈c d[b]<:e =
  ∈-∀-e a∈Πcd b∈c (<:-trans d[b]<:e e<:f)
Tm∈-gen (∈-⇑ a·b∈e e<:f) | ∈-→-e a∈c⇒d b∈c d<:e    =
  ∈-→-e a∈c⇒d b∈c (<:-trans d<:e e<:f)

------------------------------------------------------------------------
-- Inversion of subtyping (in the empty context).

-- NOTE.  The following two lemmas only hold in the empty context
-- because we can not invert instances of the interval projection
-- rules (<:-⟨| and (<:-|⟩) in arbitrary contexts.  This is because
-- instances of these rules can reflect arbitrary subtyping
-- assumptions into the subtyping relation.  Consider, e.g.
--
--     Γ, X :: ⊤..⊥ ctx    Γ(X) = ⊥..⊤
--     ------------------------------- (∈-var)
--     Γ, X :: ⊤..⊥ ⊢ X :: ⊤..⊥
--     -------------------------- (<:-⟨|, <:-|⟩)
--     Γ, X :: ⊤..⊥ ⊢ ⊤ <: X <: ⊥
--
-- Which allows us to prove that ⊤ <: ⊥ using (<:-trans) under the
-- assumption (X : ⊤..⊥).  On the other hand, it is impossible to give
-- a transitivity-free proof of ⊤ <: ⊥.  In general, it is therefore
-- impossible to invert subtyping statements in non-empty contexts,
-- i.e. one cannot prove lemmas like (<:-→-inv) or (<:-∀-inv) below
-- for arbitrary contexts.

<:-∀-inv : ∀ {k₁ k₂ : Kind Term 0} {a₁ a₂} → [] ⊢ Π k₁ a₁ <: Π k₂ a₂ ∈ * →
           [] ⊢ k₂ <∷ k₁ × kd k₂ ∷ [] ⊢ a₁ <: a₂ ∈ *
<:-∀-inv ∀k₁a₁<:∀k₂a₂∈* =
  let nf-∀k₁a₁<:nf-∀k₂a₂          = complete-<:-⋯ ∀k₁a₁<:∀k₂a₂∈*
      nf-k₂<∷nf-k₁ , nf-a₁<:nf-a₂ = CanInv.<:-∀-inv nf-∀k₁a₁<:nf-∀k₂a₂
      ∀k₁a₁∈* , ∀k₂a₂∈*           = <:-valid ∀k₁a₁<:∀k₂a₂∈*
      k₁≅nf-k₁∈* , a₁≃nf-a₁∈*     = Tp∈-∀-≃-⌞⌟-nf ∀k₁a₁∈*
      k₂≅nf-k₂∈* , a₂≃nf-a₂∈*     = Tp∈-∀-≃-⌞⌟-nf ∀k₂a₂∈*
      k₂<∷nf-k₂∈*                 = ≅⇒<∷ k₂≅nf-k₂∈*
      k₂<∷k₁ = <∷-trans (<∷-trans k₂<∷nf-k₂∈* (sound-<∷ nf-k₂<∷nf-k₁))
                        (≅⇒<∷ (≅-sym k₁≅nf-k₁∈*))
  in k₂<∷k₁ ,
     <:-trans (<:-trans (⇓-<: k₂<∷k₁ (≃⇒<: a₁≃nf-a₁∈*))
                        (⇓-<: k₂<∷nf-k₂∈* (sound-<: nf-a₁<:nf-a₂)))
              (≃⇒<: (≃-sym a₂≃nf-a₂∈*))

<:-→-inv : ∀ {a₁ a₂ b₁ b₂ : Term 0} → [] ⊢ a₁ ⇒ b₁ <: a₂ ⇒ b₂ ∈ * →
           [] ⊢ a₂ <: a₁ ∈ * × [] ⊢ b₁ <: b₂ ∈ *
<:-→-inv a₁⇒b₁<:a₂⇒b₂∈* =
  let nf-a₁⇒b₁<:nf-a₂⇒b₂          = complete-<:-⋯ a₁⇒b₁<:a₂⇒b₂∈*
      nf-a₂<:nf-a₁ , nf-b₁<:nf-b₂ = CanInv.<:-→-inv nf-a₁⇒b₁<:nf-a₂⇒b₂
      a₁⇒b₁∈* , a₂⇒b₂∈*           = <:-valid a₁⇒b₁<:a₂⇒b₂∈*
      a₁≃nf-a₁∈* , b₁≃nf-b₁∈*     = Tp∈-→-≃-⌞⌟-nf a₁⇒b₁∈*
      a₂≃nf-a₂∈* , b₂≃nf-b₂∈*     = Tp∈-→-≃-⌞⌟-nf a₂⇒b₂∈*
  in <:-trans (<:-trans (≃⇒<: a₂≃nf-a₂∈*) (sound-<: nf-a₂<:nf-a₁))
              (≃⇒<: (≃-sym a₁≃nf-a₁∈*)) ,
     <:-trans (<:-trans (≃⇒<: b₁≃nf-b₁∈*) (sound-<: nf-b₁<:nf-b₂))
              (≃⇒<: (≃-sym b₂≃nf-b₂∈*))

-- ⊤ is not a subtype of ⊥.

⊤-≮:-⊥ : ∀ {a : Term 0} → ¬ [] ⊢ ⊤ <: ⊥ ∈ *
⊤-≮:-⊥ ⊤<:⊥ with CanInv.⊤-<:-max (complete-<:-⋯ ⊤<:⊥)
⊤-≮:-⊥ ⊤<:⊥ | ()

-- Arrows are not canonical subtypes of universals and vice-versa.

⇒-≮:-Π : ∀ {a₁ b₁ : Term 0} {k₂ a₂} → ¬ [] ⊢ a₁ ⇒ b₁ <: Π k₂ a₂ ∈ *
⇒-≮:-Π a₁⇒b₁<:∀k₂a₂∈* = CanInv.⇒-≮:-Π (complete-<:-⋯ a₁⇒b₁<:∀k₂a₂∈*)

Π-≮:-⇒ : ∀ {k₁ a₁} {a₂ b₂ : Term 0} → ¬ [] ⊢ Π k₁ a₁ <: a₂ ⇒ b₂ ∈ *
Π-≮:-⇒ ∀k₁a₁<:a₂⇒b₂∈* = CanInv.Π-≮:-⇒ (complete-<:-⋯ ∀k₁a₁<:a₂⇒b₂∈*)

max_stars_repo_name: Blaisorblade/f-omega-int-agda

max_issues_repo_name: Blaisorblade/f-omega-int-agda

max_forks_repo_name: Blaisorblade/f-omega-int-agda


text:
{-# OPTIONS --safe #-}

module Cubical.Data.FinSet.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Structure
open import Cubical.Foundations.Equiv

open import Cubical.HITs.PropositionalTruncation

open import Cubical.Data.Nat
open import Cubical.Data.Fin
open import Cubical.Data.Sigma

private
  variable
    ℓ : Level
    A : Type ℓ

isFinSet : Type ℓ → Type ℓ
isFinSet A = ∃[ n ∈ ℕ ] A ≃ Fin n

-- finite sets are sets
isFinSet→isSet : isFinSet A → isSet A
isFinSet→isSet = rec isPropIsSet (λ (_ , p) → isOfHLevelRespectEquiv 2 (invEquiv p) isSetFin)

isPropIsFinSet : isProp (isFinSet A)
isPropIsFinSet = isPropPropTrunc

-- the type of finite sets

FinSet : (ℓ : Level) → Type (ℓ-suc ℓ)
FinSet ℓ = TypeWithStr _ isFinSet

max_stars_repo_name: FernandoLarrain/cubical


text:
open import Haskell.Prim
open import Agda.Builtin.Nat

data _≤_ : Nat → Nat → Set where
  instance
    zero-≤ : ∀ {n} → zero ≤ n
    suc-≤ : ∀ {m n} → @0 {{m ≤ n}} → suc m ≤ suc n

data Tree {l u : Nat} : Set where
  Leaf  : @0 {{l ≤ u}} → Tree {l} {u}
  Node  : (x : Nat) → Tree {l} {x} → Tree {x} {u} → Tree {l} {u}
{-# COMPILE AGDA2HS Tree #-}


text:
module Serializer.Bool where

open import Data.Bool
open import Data.Fin hiding (_+_)
open import Data.Nat
open import Relation.Binary
open import Relation.Binary.EqReasoning
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; cong ; setoid )
import Relation.Binary.Indexed as I
open import Function.Equality using (_⟶_ ;  _⟨$⟩_ ; Π )
open import Function.LeftInverse hiding (_∘_)
open import Function.Injection
open import Function.Surjection
open import Function.Bijection

open import Serializer

fromBool : Bool -> Fin 2
fromBool true = zero
fromBool false = suc zero

toBool : Fin 2 -> Bool
toBool zero = true
toBool (suc x) = false

bool-cong : Setoid._≈_ (setoid Bool) I.=[ fromBool ]⇒ Setoid._≈_ (setoid (Fin 2))
bool-cong refl = refl

bool-cong-inv : Setoid._≈_ (setoid (Fin 2)) I.=[ toBool ]⇒ Setoid._≈_ (setoid (Bool))
bool-cong-inv refl = refl

from-bool-preserves-eq : setoid Bool ⟶ setoid (Fin 2)
from-bool-preserves-eq = record { _⟨$⟩_ = fromBool ; cong = bool-cong }

from-bool-injective : Injective from-bool-preserves-eq
from-bool-injective {true} {true} refl = refl
from-bool-injective {true} {false} ()
from-bool-injective {false} {true} ()
from-bool-injective {false} {false} refl = refl

bool-preserves-eq-inv : setoid (Fin 2) ⟶ setoid Bool
bool-preserves-eq-inv = record { _⟨$⟩_ = toBool ; cong = bool-cong-inv }

bool-inv : bool-preserves-eq-inv RightInverseOf from-bool-preserves-eq
bool-inv zero = refl
bool-inv (suc zero) = refl
bool-inv (suc (suc ()))

from-bool-surjective : Surjective from-bool-preserves-eq
from-bool-surjective = record { from = bool-preserves-eq-inv ; right-inverse-of = bool-inv   }

bool-bijection : Bijection (setoid Bool) (setoid (Fin 2))
bool-bijection = record { to = from-bool-preserves-eq ; bijective = record { injective =  from-bool-injective ; surjective = from-bool-surjective } }

instance
  serializerBool : Serializer Bool
  serializerBool = record {
    size = 2 ;
    from = fromBool ;
    to = toBool ;
    bijection = bool-bijection }

max_stars_repo_name: mathijsb/generic-in-agda

max_issues_repo_name: mathijsb/generic-in-agda

max_forks_repo_name: mathijsb/generic-in-agda


text:
module Fail.QualifiedRecordProjections where

record Test (a : Set) : Set where
  field
    one : a

{-# COMPILE AGDA2HS Test #-}


text:
{-# OPTIONS --instance-search-depth=10 #-}

module _ where

module _
  {A : Set}
  (B₁ : A → Set)
  (B₂ : A → Set)
  (f : A → A)
  where
  type = ∀ {x : A} → B₁ x → B₂ (f x)
  record Class : Set where field method : type
  method : {{_ : Class}} → type
  method {{I}} = Class.method I

id : ∀ {A : Set} → A → A
id x = x

Ext : {A : Set} (B : A → Set) → A → Set
Ext B x = B x → B x

postulate

  Foo : Set

  instance

    _ : {A : Set}
        {B : A → Set}
        {{_ : Class (Ext B) (Ext B) id}}
        → Class (Ext B) (Ext (λ _ → Foo)) id

module _
  {A : Set}
  (B : A → Set)
  {{_ : Class (Ext B) (Ext B) id}}
  {y}
  (R : B y → Set)
  where

  postulate

    _ : let Point = λ (f : B y → B y) → ∀ x → R (f x) in
        Class Point Point (method (Ext _) (Ext _) id)

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
{-# OPTIONS --safe --warning=error --without-K #-}

open import LogicalFormulae
open import Setoids.Setoids
open import Rings.Definition
open import Rings.Ideals.Definition

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)

module Rings.Ideals.Maximal.Definition {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} {R : Ring S _+_ _*_} {c : _} {pred : A → Set c} (i : Ideal R pred) where

record MaximalIdeal {d : _} : Set (a ⊔ b ⊔ c ⊔ lsuc d) where
  field
    notContained : A
    notContainedIsNotContained : (pred notContained) → False
    isMaximal : {bigger : A → Set d} → Ideal R bigger → ({a : A} → pred a → bigger a) → (Sg A (λ a → bigger a && (pred a → False))) → ({a : A} → bigger a)


text:
module Utilities.VecSplit where

-- Standard libraries imports ----------------------------------------
open import Data.Nat using (ℕ ; _+_)
open import Data.Vec using (Vec ; _++_)

open import Relation.Binary.PropositionalEquality
  using (_≡_)
open import Relation.Binary.HeterogeneousEquality
  using (_≅_)
----------------------------------------------------------------------

record Split {A : Set} {n : ℕ} (xs : Vec A n) : Set where
  field
    {m₁} {m₂} : ℕ
    n≡m₁+m₂ : n ≡ m₁ + m₂
    ys : Vec A m₁
    zs : Vec A m₂
    xs≅ys++zs : xs ≅ ys ++ zs


text:
{-# OPTIONS --allow-unsolved-metas #-}

module x05-842Isomorphism-hc where

import      Relation.Binary.PropositionalEquality as Eq
open        Eq                                    using (_≡_; refl; cong; cong-app; sym; subst) -- added last
open        Eq.≡-Reasoning
open import Data.Nat                              using (ℕ; zero; suc; _+_; _*_; _^_)
open import Data.Nat.Properties                   using (+-comm; +-suc; +-identityʳ) -- added last
------------------------------------------------------------------------------
open import x02-842Induction-hc-2                 hiding (+-suc; +-identityʳ)

------------------------------------------------------------------------------
-- Function composition.

_∘_  : ∀ {A B C : Set} → (B → C) → (A → B) → (A → C)
(g ∘ f)    x = g (f x)

_∘′_ : ∀ {A B C : Set} → (B → C) → (A → B) → (A → C)
g ∘′ f = λ x → g (f x)

------------------------------------------------------------------------------
-- EXTENSIONALITY

postulate
  extensionality : ∀ {A B : Set} {f g : A → B}
    → (∀ (x : A) → f x ≡ g x)
      -----------------------
    →              f   ≡ g

-- def of + that matches on right
_+′_ : ℕ → ℕ → ℕ
m +′ zero  = m
m +′ suc n = suc (m +′ n)

same-app : ∀ (m n : ℕ) → m +′ n ≡ m + n
same-app m  zero         -- (m +′ zero) ≡ m + zero
                         --  m          ≡ m + zero
  rewrite +-identityʳ m  --  m          ≡ m
  = refl
same-app m (suc n) -- (m +′ suc n) ≡ m + suc n
                   -- suc (m +′ n) ≡ m + suc n
  rewrite
    +-suc m n      -- suc (m +′ n) ≡ suc (m + n)
  | same-app m n   -- suc (m +  n) ≡ suc (m + n)
  = refl

-- requires extensionality
+′-same-as-+ : _+′_ ≡ _+_
+′-same-as-+ = extensionality λ m → extensionality λ n → same-app m n

------------------------------------------------------------------------------
-- ISOMORPHISM

infix 0 _≃_
record _≃_ (A B : Set) : Set where
  constructor mk-≃  -- added, not in PLFA
  field
    to      : A → B
    from    : B → A
    from∘to : ∀ (x : A) → from (to x) ≡ x
    to∘from : ∀ (y : B) → to (from y) ≡ y
open _≃_

-- RECORD def equivalent to DATA def and functions:

data _≃′_ (A B : Set): Set where
  mk-≃′ : ∀ (to : A → B) →
          ∀ (from : B → A) →
          ∀ (from∘to : (∀ (x : A) → from (to x) ≡ x)) →
          ∀ (to∘from : (∀ (y : B) → to (from y) ≡ y)) →
          A ≃′ B

to′ : ∀ {A B : Set} → (A ≃′ B) → (A → B)
to′ (mk-≃′ f g g∘f f∘g) = f

from′ : ∀ {A B : Set} → (A ≃′ B) → (B → A)
from′ (mk-≃′ f g g∘f f∘g) = g

from∘to′ : ∀ {A B : Set} → (A≃B : A ≃′ B)
                         → (∀ (x : A)
                         → from′ A≃B (to′ A≃B x) ≡ x)
from∘to′ (mk-≃′ f g g∘f f∘g) = g∘f

to∘from′ : ∀ {A B : Set} → (A≃B : A ≃′ B)
                         → (∀ (y : B)
                         → to′ A≃B (from′ A≃B y) ≡ y)
to∘from′ (mk-≃′ f g g∘f f∘g) = f∘g

-- End of equivalent formulation (records are faster!)

------------------------------------------------------------------------------
-- PROPERTIES OF ISOMORPHISM : AN EQUIVALENCE RELATION (i.e., reflexive, symmetric and transitive)

-- reflexive
≃-refl : ∀ {A : Set}
    -----
  → A ≃ A

-- in empty hole, split on result, get COPATTERNS (not in PLFA)

to      ≃-refl x = x
from    ≃-refl x = x
from∘to ≃-refl x = refl
to∘from ≃-refl x = refl

-- symmetric
≃-sym : ∀ {A B : Set}
  → A ≃ B
    -----
  → B ≃ A

to      (≃-sym A≃B) = from    A≃B
from    (≃-sym A≃B) = to      A≃B
from∘to (≃-sym A≃B) = to∘from A≃B
to∘from (≃-sym A≃B) = from∘to A≃B

-- transitive
≃-trans : ∀ {A B C : Set}
  → A ≃ B
  →     B ≃ C
    -----
  → A ≃     C

to      (≃-trans A≃B B≃C) = to   B≃C ∘ to   A≃B
from    (≃-trans A≃B B≃C) = from A≃B ∘ from B≃C
from∘to (≃-trans A≃B B≃C) x rewrite from∘to B≃C (to   A≃B x) = from∘to A≃B x
to∘from (≃-trans A≃B B≃C) x rewrite to∘from A≃B (from B≃C x) = to∘from B≃C x

-- syntax for isomorphic equational reasoning
module ≃-Reasoning where

  infix  1 ≃-begin_
  infixr 2 _≃⟨_⟩_
  infix  3 _≃-∎

  ≃-begin_ : ∀ {A B : Set}
    → A ≃ B
      -----
    → A ≃ B
  ≃-begin A≃B = A≃B

  _≃⟨_⟩_ : ∀ (A : Set) {B C : Set}
    → A ≃ B
    →     B ≃ C
      -----
    → A ≃     C
  A ≃⟨ A≃B ⟩ B≃C = ≃-trans A≃B B≃C

  _≃-∎ : ∀ (A : Set)
      -----
    → A ≃ A
  A ≃-∎ = ≃-refl

open ≃-Reasoning

------------------------------------------------------------------------------
-- EMBEDDING (weaker than isomorphism)

infix 0 _≲_
record _≲_ (A B : Set) : Set where
  field
    to      : A → B
    from    : B → A
    from∘to : ∀ (x : A) → from (to x) ≡ x
open _≲_

≲-refl : ∀ {A : Set} → A ≲ A
to      ≲-refl x = x
from    ≲-refl x = x
from∘to ≲-refl x = refl

≲-trans : ∀ {A B C : Set} → A ≲ B → B ≲ C → A ≲ C
to      (≲-trans A≲B B≲C) = to   B≲C ∘ to   A≲B
from    (≲-trans A≲B B≲C) = from A≲B ∘ from B≲C
from∘to (≲-trans A≲B B≲C) x rewrite from∘to B≲C (to A≲B x) = from∘to A≲B x

≲-antisym : ∀ {A B : Set}
  → (A≲B : A ≲ B)
  → (B≲A : B ≲ A)
  → (to   A≲B ≡ from B≲A)
  → (from A≲B ≡ to   B≲A)
    -------------------
  → A ≃ B

to      (≲-antisym A≲B B≲A to≡from from≡to)   = to      A≲B
from    (≲-antisym A≲B B≲A to≡from from≡to)   = from    A≲B
from∘to (≲-antisym A≲B B≲A to≡from from≡to) x = from∘to A≲B x
to∘from (≲-antisym A≲B B≲A to≡from from≡to) y
  rewrite from≡to | to≡from                   = from∘to B≲A y

-- equational reasoning for embedding
module ≲-Reasoning where

  infix  1 ≲-begin_
  infixr 2 _≲⟨_⟩_
  infix  3 _≲-∎

  ≲-begin_ : ∀ {A B : Set}
    → A ≲ B
      -----
    → A ≲ B
  ≲-begin A≲B = A≲B

  _≲⟨_⟩_ : ∀ (A : Set) {B C : Set}
    → A ≲ B
    → B ≲ C
      -----
    → A ≲ C
  A ≲⟨ A≲B ⟩ B≲C = ≲-trans A≲B B≲C

  _≲-∎ : ∀ (A : Set)
      -----
    → A ≲ A
  A ≲-∎ = ≲-refl

open ≲-Reasoning

------------------------------------------------------------------------------
-- isomorphism implies embedding

≃-implies-≲ : ∀ {A B : Set}
  → A ≃ B
    -----
  → A ≲ B

to      (≃-implies-≲ a≃b) = to      a≃b
from    (≃-implies-≲ a≃b) = from    a≃b
from∘to (≃-implies-≲ a≃b) = from∘to a≃b

------------------------------------------------------------------------------
-- PROPOSITIONAL EQUIVALENCE (weaker than embedding) - aka IFF
-- an equivalence relation

record _⇔_ (A B : Set) : Set where
  field
    to   : A → B
    from : B → A
open _⇔_ -- added

⇔-refl : ∀ {A : Set}
    -----
  → A ⇔ A

_⇔_.to   ⇔-refl x = x
_⇔_.from ⇔-refl x = x

⇔-sym : ∀ {A B : Set}
  → A ⇔ B
    -----
  → B ⇔ A

_⇔_.to   (⇔-sym A⇔B) = from A⇔B
_⇔_.from (⇔-sym A⇔B) = to   A⇔B

⇔-trans : ∀ {A B C : Set}
  → A ⇔ B
  →     B ⇔ C
    -----
  → A ⇔     C

to   (⇔-trans A⇔B B⇔C) = to   B⇔C ∘ to   A⇔B
from (⇔-trans A⇔B B⇔C) = from A⇔B ∘ from B⇔C

{-
------------------------------------------------------------------------------
-- 842 extended exercise: Canonical bitstrings.
-- Modified and extended from Bin-predicates exercise in PLFA Relations.

cannot prove
              ∀ {n : Bin-ℕ} → tob (fromb n) ≡ n
because of possibility of leading zeroes in Bin-ℕ value (e.g., 'bits x0 x0 x1')

It s true for Bin-ℕ without leading zeroes
-}
-- Predicate that states:
-- value of type One n is evidence that n has a leading one.
data One : Bin-ℕ → Set where
  [bitsx1] :                         One (bits x1)
  _[x0]    : ∀ {b : Bin-ℕ} → One b → One (b x0)
  _[x1]    : ∀ {b : Bin-ℕ} → One b → One (b x1)

-- proof that 'bits x1 x0 x0' has leading one
_ : One (bits x1 x0 x0)
_ = [bitsx1] [x0] [x0]

-- There is no value of type One (bits x0 x0 x1).
-- Can't state and prove yet, because negation not covered until Connectives chapter.

-- Canonical binary representation is either zero or has a leading one.
data Can : Bin-ℕ → Set where
  [zero] :                         Can bits
  [pos]  : ∀ {b : Bin-ℕ} → One b → Can b

_ : Can bits
_ = [zero]

_ : Can (bits x1 x0)
_ = [pos] ([bitsx1] [x0])

-- PLFA Relations Bin-predicates exercise gives three properties of canonicity.
-- First : increment of a canonical number is canonical.
-- Most of the work is done in the following lemma.

-- IncCanOne : increment of a canonical number has a leading one.
one-inc : ∀ {b : Bin-ℕ} → Can b → One (inc b)
one-inc [zero]           =          [bitsx1] -- note: 'n' is bound to 'bits'
one-inc ([pos] [bitsx1]) =          [bitsx1] [x0]
one-inc ([pos] (b [x0])) =                b  [x1]
one-inc ([pos] (b [x1])) = one-inc ([pos] b) [x0]

-- OneInc : 1st canonicity property is now a corollary.
can-inc : ∀ {b : Bin-ℕ} → Can b → Can (inc b)
can-inc cb = [pos] (one-inc cb)

-- CanToB : 2nd canonicity property : converting unary to binary produces a canonical number.
to-can : ∀ (n : ℕ) → Can (tob n)
to-can   zero  = [zero]
to-can (suc n) = can-inc (to-can n)

-- OneDblbX0 : relates binary double to the x0 constructor, for numbers with a leading one.
dblb-x0 : ∀ {b : Bin-ℕ} → One b → dblb b ≡ b x0
dblb-x0 [bitsx1]                     = refl
dblb-x0 (on [x0]) rewrite dblb-x0 on = refl
dblb-x0 (on [x1]) rewrite dblb-x0 on = refl

dblb-x1 : ∀ {b : Bin-ℕ} → One b → inc (dblb b) ≡ b x1
dblb-x1 [bitsx1]  = refl
dblb-x1 (on [x0])           --  inc (dblb (b  x0))    ≡ ((b x0) x1)
                            --      (dblb  b  x1)     ≡ ((b x0) x1)
  rewrite sym (dblb-x0 on)  --      (dblb  b  x1)     ≡ (dblb b x1)
  = refl
dblb-x1 (on [x1])           --  inc (dblb (b  x1))    ≡ ((b x1) x1)
                            -- (inc (dblb  b) x1)     ≡ ((b x1) x1)
  rewrite dblb-x1 on        --           ((b  x1) x1) ≡ ((b x1) x1)
  = refl

-- To prove 3rd property, use lemmas from 842Induction
-- 'one-to∘from' below and some new ones you define.

one-bits-to-nat : ∀ {b : Bin-ℕ} → One b → ℕ
one-bits-to-nat {b} _ = fromb b

one-to∘from : ∀ {b : Bin-ℕ} → One b → tob (fromb b) ≡ b
one-to∘from [bitsx1]  = refl
one-to∘from {b} (on [x0])       --      tob      (fromb (b  x0))  ≡ (b  x0)
                                --      tob  (dbl (fromb b ))     ≡ (b  x0)
  rewrite
    sym (dblb-x0 on)            --      tob  (dbl (fromb b ))     ≡ dblb b
  | to∘dbl (one-bits-to-nat on) --      dblb (tob (fromb b₁))     ≡ dblb b₁
  | one-to∘from on              --      dblb              lhs     ≡ dblb lhs
  = refl
one-to∘from {b} (on [x1])       --      tob      (fromb (b₁ x1))  ≡ (b₁ x1)
                                -- inc (tob (dbl (fromb  b₁)))    ≡ (b₁ x1)
  rewrite
    to∘dbl (one-bits-to-nat on) -- inc (dblb (tob (fromb b₁)))    ≡ (b₁ x1)
  | one-to∘from on              -- inc (dblb lhs)                 ≡ (lhs x1)
  | dblb-x1 on                  --          (lhs x1)              ≡ (lhs x1)
  = refl

-- 3rd canonicity property :
-- converting a canonical number from binary and back to unary produces the same number.
-- CanToFrom
can-to∘from : ∀ {b : Bin-ℕ} → Can b → tob (fromb b) ≡ b
can-to∘from [zero]    = refl
can-to∘from ([pos] b) = one-to∘from b

-- Proofs of positivity are unique.
one-unique : ∀ {b : Bin-ℕ} → (ox oy : One b) → ox ≡ oy
one-unique [bitsx1]  [bitsx1]  = refl
one-unique (ox [x0]) (oy [x0])
  with one-unique ox oy
... | refl = refl
one-unique (ox [x1]) (oy [x1])
  with one-unique ox oy
... | refl = refl

-- Proofs of canonicity are unique.
can-unique : ∀ {b : Bin-ℕ} → (cx cy : Can b) → cx ≡ cy
can-unique [zero]     [zero]     = refl
can-unique ([pos] ox) ([pos] oy)
  with one-unique ox oy
... | refl = refl

------------------------------------------------------------------------------
-- There is NOT an isomorphism between ℕ (unary) and canonical binary representations.
-- Because Can is not a set, but a family of sets, it does not fit into framework for isomorphism.

-- It is possible to roll all the values into one set which is isomorphic to ℕ.
-- A CanR VALUE wraps a Bin-ℕ and proof it has a canonical representation.
data CanR : Set where
  wrap : ∀ (b : Bin-ℕ) → Can b → CanR

-- IsoNCanR : Prove an isomorphism between ℕ and CanR.
iso-ℕ-CanR : ℕ ≃ CanR
to      iso-ℕ-CanR          n  = wrap (tob n) (to-can n) -- -- Goal: CanR; n : ℕ
from    iso-ℕ-CanR (wrap b cb) = fromb b -- Goal: ℕ; cb : Can b, b  : Bin-ℕ
                                         -- Constraints
                                         -- fromb (tob n) = ?0 (b = (tob n)) (cb = (to-can n)) : ℕ
from∘to iso-ℕ-CanR          n  = from∘tob n -- Goal: fromb (tob n) ≡ n; n : ℕ
to∘from iso-ℕ-CanR (wrap b cb)  -- Goal: to iso-ℕ-CanR (from iso-ℕ-CanR (wrap b cb)) ≡ wrap b cb
                                -- Goal: wrap (tob (fromb b)) (to-can (fromb b))     ≡ wrap b cb
                                -- cb : Can b, b  : Bin-ℕ
  with to-can (fromb b) | can-to∘from cb
... |  tcfb             | ctfcb -- Goal: wrap (tob (fromb b)) tcfb ≡ wrap b cb
                                -- ctfcb : tob (fromb b) ≡ b, tcfb  : Can (tob (fromb b))
  rewrite
    ctfcb                       -- Goal: wrap b tcfb ≡ wrap b cb
  | can-unique cb tcfb          -- Goal: wrap b tcfb ≡ wrap b tcfb
  = refl

------------------------------------------------------------------------------
-- BIJECTIVE BINARY NUMBERING -- TODO
-- Isomorphism between ℕ and some binary encoding (without awkward non-canonical values).
-- Via using digits 1 and 2 (instead of 0 and 1) where the multiplier/base is still 2.
-- e.g., <empty>, 1, 2, 11, 12, 21, 22, 111, ...

data Bij-ℕ : Set where
  bits :         Bij-ℕ
  _x1  : Bij-ℕ → Bij-ℕ
  _x2  : Bij-ℕ → Bij-ℕ

--------------------------------------------------
incBij-ℕ : Bij-ℕ → Bij-ℕ
incBij-ℕ   bits  = bits x1
incBij-ℕ (bj x1) = bj x2
incBij-ℕ (bj x2) = (incBij-ℕ bj) x1

_ : incBij-ℕ  bits        ≡ bits       x1
_ = refl
_ : incBij-ℕ (bits    x1) ≡ bits       x2
_ = refl
_ : incBij-ℕ (bits    x2) ≡ bits    x1 x1
_ = refl
_ : incBij-ℕ (bits x1 x1) ≡ bits    x1 x2
_ = refl
_ : incBij-ℕ (bits x1 x2) ≡ bits    x2 x1
_ = refl
_ : incBij-ℕ (bits x2 x1) ≡ bits    x2 x2
_ = refl
_ : incBij-ℕ (bits x2 x2) ≡ bits x1 x1 x1
_ = refl

--------------------------------------------------
toBij-ℕ : ℕ → Bij-ℕ
toBij-ℕ  zero   = bits
toBij-ℕ (suc n) = incBij-ℕ (toBij-ℕ n)

_ : toBij-ℕ  0 ≡ bits
_ = refl
_ : toBij-ℕ  1 ≡ bits          x1
_ = refl
_ : toBij-ℕ  2 ≡ bits          x2
_ = refl
_ : toBij-ℕ  3 ≡ bits       x1 x1
_ = refl
_ : toBij-ℕ  4 ≡ bits       x1 x2
_ = refl
_ : toBij-ℕ  5 ≡ bits       x2 x1
_ = refl
_ : toBij-ℕ  6 ≡ bits       x2 x2
_ = refl
_ : toBij-ℕ  7 ≡ bits    x1 x1 x1
_ = refl
_ : toBij-ℕ  8 ≡ bits    x1 x1 x2
_ = refl
_ : toBij-ℕ  9 ≡ bits    x1 x2 x1
_ = refl
_ : toBij-ℕ 10 ≡ bits    x1 x2 x2
_ = refl
_ : toBij-ℕ 11 ≡ bits    x2 x1 x1
_ = refl
_ : toBij-ℕ 12 ≡ bits    x2 x1 x2
_ = refl
_ : toBij-ℕ 14 ≡ bits    x2 x2 x2
_ = refl
_ : toBij-ℕ 16 ≡ bits x1 x1 x1 x2
_ = refl
_ : toBij-ℕ 18 ≡ bits x1 x1 x2 x2
_ = refl
_ : toBij-ℕ 20 ≡ bits x1 x2 x1 x2
_ = refl
-------------------------
_ : toBij-ℕ  0 ≡ bits
_ = refl
_ : toBij-ℕ  0 ≡ bits
_ = refl
-------------------------
_ : toBij-ℕ  1 ≡ bits          x1
_ = refl
_ : toBij-ℕ  2 ≡ bits          x2
_ = refl
-------------------------
_ : toBij-ℕ  2 ≡ bits          x2
_ = refl
_ : toBij-ℕ  4 ≡ bits       x1 x2
_ = refl
-------------------------
_ : toBij-ℕ  3 ≡ bits       x1 x1
_ = refl
_ : toBij-ℕ  6 ≡ bits       x2 x2
_ = refl
-------------------------
_ : toBij-ℕ  4 ≡ bits       x1 x2
_ = refl
_ : toBij-ℕ  8 ≡ bits    x1 x1 x2
_ = refl
-------------------------
_ : toBij-ℕ  5 ≡ bits       x2 x1
_ = refl
_ : toBij-ℕ 10 ≡ bits    x1 x2 x2
_ = refl
-------------------------
_ : toBij-ℕ  6 ≡ bits       x2 x2
_ = refl
_ : toBij-ℕ 12 ≡ bits    x2 x1 x2
_ = refl
-------------------------
_ : toBij-ℕ  7 ≡ bits    x1 x1 x1
_ = refl
_ : toBij-ℕ 14 ≡ bits    x2 x2 x2
_ = refl
-------------------------
_ : toBij-ℕ  8 ≡ bits    x1 x1 x2
_ = refl
_ : toBij-ℕ 16 ≡ bits x1 x1 x1 x2
_ = refl
-------------------------
_ : toBij-ℕ  9 ≡ bits    x1 x2 x1
_ = refl
_ : toBij-ℕ 18 ≡ bits x1 x1 x2 x2
_ = refl
-------------------------
_ : toBij-ℕ 10 ≡ bits    x1 x2 x2
_ = refl
_ : toBij-ℕ 20 ≡ bits x1 x2 x1 x2
_ = refl
-------------------------

--------------------------------------------------
fromBij-ℕ : Bij-ℕ → ℕ
fromBij-ℕ  bj = fbj bj 0
 where
  fbj : Bij-ℕ → ℕ → ℕ
  fbj bits    _ = zero
  fbj (bj x1) n = (1 * (2 ^ n)) + fbj bj (n + 1)
  fbj (bj x2) n = (2 * (2 ^ n)) + fbj bj (n + 1)

_ : fromBij-ℕ (bits) ≡ 0
_ = refl
_ : fromBij-ℕ (bits          x1)  ≡  1
_ = refl
_ : fromBij-ℕ (bits          x2)  ≡  2
_ = refl
_ : fromBij-ℕ (bits       x1 x1)  ≡  3
_ = refl
_ : fromBij-ℕ (bits       x1 x2)  ≡  4
_ = refl
_ : fromBij-ℕ (bits       x2 x1)  ≡  5
_ = refl
_ : fromBij-ℕ (bits       x2 x2)  ≡  6
_ = refl
_ : fromBij-ℕ (bits    x1 x1 x1)  ≡  7
_ = refl
_ : fromBij-ℕ (bits    x1 x1 x2)  ≡  8
_ = refl
_ : fromBij-ℕ (bits    x1 x2 x1)  ≡  9
_ = refl
_ : fromBij-ℕ (bits    x1 x2 x2)  ≡ 10
_ = refl
_ : fromBij-ℕ (bits x1 x2 x1 x2)  ≡ 20
_ = refl

--------------------------------------------------
doubleBij-ℕ : Bij-ℕ → Bij-ℕ
doubleBij-ℕ  bits   = bits
doubleBij-ℕ (bj x1) = {!!}
doubleBij-ℕ (bj x2) = {!!}

--------------------------------------------------
xxx : ∀ {n : ℕ} → fromBij-ℕ (toBij-ℕ n) ≡ n
xxx {zero}  = refl
xxx {suc n} = {! !}

--------------------------------------------------
-- Prove the isomorphism between ℕ and Bij-ℕ.
-- Largely follows outline of above.

iso-ℕ-Bij-ℕ : ℕ ≃ Bij-ℕ
to      iso-ℕ-Bij-ℕ n   = toBij-ℕ n
from    iso-ℕ-Bij-ℕ bjn = fromBij-ℕ bjn
from∘to iso-ℕ-Bij-ℕ n   = {!!}
to∘from iso-ℕ-Bij-ℕ bjn = {!!}

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


text:
module 010-false-true where

-- In Agda, types are theorems, and instances of types are proofs. The
-- simplest theorem is the theorem which has no proof, and is useful
-- to represent any contradictory situation. We declare False as an
-- algebraic data type without constructors. If "False" has no
-- constructors, then it also has no instances, and thereby perfectly
-- serves our purpose.  Note that what we call here "False" is also
-- sometimes also called bottom and is denoted by ⊥.

data False : Set where

-- The next simplest theorem is the trivial theorem which is always
-- true. We declare it as an algebraic data type "True", with one
-- constructor named "trivial".

data True : Set where
  trivial : True

max_stars_repo_name: mcmtroffaes/agda-proofs

max_issues_repo_name: mcmtroffaes/agda-proofs

max_forks_repo_name: mcmtroffaes/agda-proofs