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

open import HoTT
open import cohomology.Theory
open import groups.ExactSequence
open import groups.HomSequence

module cw.cohomology.grid.LongExactSequence {i} (CT : CohomologyTheory i)
  {X Y Z : Ptd i} (n : ℤ) (f : X ⊙→ Y) (g : Y ⊙→ Z) where

open CohomologyTheory CT
open import cohomology.PtdMapSequence CT
open import cw.cohomology.grid.CofiberSplit (fst f) (fst g)
open import cw.cohomology.grid.PtdMap f g

{-
  X --> Y ----> Z
  |     |       |
  v     v       v
  1 -> Y/X --> Z/X
        | this  |
        v   one v
        1 ---> Z/Y
-}

private
  ⊙D-span : ⊙Span
  ⊙D-span = ⊙span Y/X Z Y (⊙cfcod' f) g

  ⊙D : Ptd i
  ⊙D = ⊙Pushout ⊙D-span

  Y/X-to-D : Y/X ⊙→ ⊙D
  Y/X-to-D = B/A-to-D , idp

  open import cohomology.LongExactSequence CT n Y/X-to-D

  ⊙E : Ptd i
  ⊙E = ⊙Cofiber (⊙left ⊙D-span)

  Z/Y-to-E : Z/Y ⊙→ ⊙E
  Z/Y-to-E = C/B-to-E , idp

  Z/X-to-D : Z/X ⊙→ ⊙D
  Z/X-to-D = C/A-to-D , idp

grid-co∂ : C n Y/X →ᴳ C (succ n) Z/Y
grid-co∂ = record {f = CEl-fmap (succ n) Z/Y-to-E ∘ GroupHom.f co∂ ; pres-comp = lemma} where
  abstract lemma = ∘ᴳ-pres-comp (C-fmap (succ n) Z/Y-to-E) co∂

grid-∂-before-Susp : C/B → Susp B/A
grid-∂-before-Susp = extract-glue ∘ C/B-to-E

⊙grid-∂-before-Susp : Z/Y ⊙→ ⊙Susp Y/X
⊙grid-∂-before-Susp = grid-∂-before-Susp , lemma where
  abstract lemma = snd (⊙extract-glue ⊙∘ Z/Y-to-E)

abstract
  grid-co∂-β : GroupHom.f grid-co∂ ∼ CEl-fmap (succ n) ⊙grid-∂-before-Susp ∘ <– (CEl-Susp n Y/X)
  grid-co∂-β x = ∘-CEl-fmap (succ n) Z/Y-to-E ⊙extract-glue _

abstract
  grid-∂-before-Susp-glue-β : ∀ x →
    ap (fst ⊙grid-∂-before-Susp) (glue x) == merid (cfcod x)
  grid-∂-before-Susp-glue-β x =
      ap-∘ extract-glue C/B-to-E (glue x)
    ∙ ap (ap extract-glue) (C/B-to-E-glue-β x)
    ∙ ap-∙' extract-glue (glue (cfcod x)) (ap cfcod (glue x))
    ∙ ap2 _∙'_
        (ExtractGlue.glue-β (cfcod x))
        (∘-ap extract-glue cfcod (glue x) ∙ ap-cst south (glue x))

C-grid-cofiber-seq : HomSequence (C n Z/X) (C (succ n) Y/X)
C-grid-cofiber-seq =
  C n Z/X         →⟨ C-fmap n Y/X-to-Z/X        ⟩ᴳ
  C n Y/X         →⟨ grid-co∂                   ⟩ᴳ
  C (succ n) Z/Y  →⟨ C-fmap (succ n) Z/X-to-Z/Y ⟩ᴳ
  C (succ n) Z/X  →⟨ C-fmap (succ n) Y/X-to-Z/X ⟩ᴳ
  C (succ n) Y/X  ⊣|ᴳ

private
  C-cofiber-seq-to-C-grid-cofiber-seq :
    HomSeqMap C-cofiber-seq C-grid-cofiber-seq
      (C-fmap n Z/X-to-D) (idhom _)
  C-cofiber-seq-to-C-grid-cofiber-seq =
    C-fmap n Z/X-to-D         ↓⟨ comm-sqrᴳ (λ d → ! (C-fmap-idf n _)
                                                ∙ (C-comm-square n B/A-to-C/A-comm-square □$ᴳ d)) ⟩ᴳ
    idhom _                   ↓⟨ comm-sqrᴳ (λ _ → idp) ⟩ᴳ
    C-fmap (succ n) Z/Y-to-E  ↓⟨ C-comm-square (succ n) C/A-to-C/B-comm-square ⟩ᴳ
    C-fmap (succ n) Z/X-to-D  ↓⟨ comm-sqrᴳ (λ d → ! (C-fmap-idf (succ n) _)
                                                ∙ (C-comm-square (succ n) B/A-to-C/A-comm-square □$ᴳ d)) ⟩ᴳ
    idhom _                   ↓|ᴳ

  C-cofiber-seq-equiv-C-grid-cofiber-seq :
    HomSeqEquiv C-cofiber-seq C-grid-cofiber-seq
      (C-fmap n Z/X-to-D) (idhom _)
  C-cofiber-seq-equiv-C-grid-cofiber-seq =
    C-cofiber-seq-to-C-grid-cofiber-seq ,
      CEl-isemap n Z/X-to-D C/A-to-D-is-equiv ,
      idf-is-equiv _ ,
      CEl-isemap (succ n) Z/Y-to-E C/B-to-E-is-equiv ,
      CEl-isemap (succ n) Z/X-to-D C/A-to-D-is-equiv ,
      idf-is-equiv _

abstract
  C-grid-cofiber-seq-is-exact : is-exact-seq C-grid-cofiber-seq
  C-grid-cofiber-seq-is-exact = seq-equiv-preserves-exact
    C-cofiber-seq-equiv-C-grid-cofiber-seq C-cofiber-seq-is-exact

C-grid-cofiber-exact-seq : ExactSequence (C n Z/X) (C (succ n) Y/X)
C-grid-cofiber-exact-seq = C-grid-cofiber-seq , C-grid-cofiber-seq-is-exact

max_stars_repo_name: timjb/HoTT-Agda

max_issues_repo_name: timjb/HoTT-Agda

max_forks_repo_name: timjb/HoTT-Agda


text:
-- Andreas, 2014-11-25, issue reported by Peter Divianski (divipp)

{-# OPTIONS --show-implicit #-}
-- {-# OPTIONS -v tc:10 #-}
-- {-# OPTIONS -v tc.inj:49 #-}
-- {-# OPTIONS -v tc.polarity:49 #-}
-- {-# OPTIONS -v tc.lhs:40 #-}

-- After loading the following Agda code, the last occurrence of 'one' is yellow.

-- Remarks:
-- Probably not an error, but it is against my expectation.
-- The code was obtained by shrinking a more complex one.
-- I guess that the lifting of the local function 'f' happens not as I expect it.
-- The code is quite fragile, the any of following changes fix the problem:
-- - using record ⊤ instead of data Unit
-- - lifting 'f' to be a global function
-- - replacing 'unit' by '_' in the definition of 'f'
-- - giving the implicit argument {v = unit ∷ []} to g

-- Tested with Agda 2.4.2.1 and with the development version of Agda on GitHub (20 Nov 2014)

open import Common.Prelude using (Nat; zero; suc; Unit; unit)

data Vec (A : Set) : Nat → Set where
   []  : Vec A zero
   _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)  -- n is forced

-- Singleton type
data Sg {A : Set} (x : A) : Set where
  sg : Sg x

-- modified length function (counts till 1)
nonNil : ∀ {n} → Vec Unit n → Nat
nonNil []       = zero
nonNil (i ∷ is) = suc (f i) where
  f : Unit → Nat
  f unit = zero

g : ∀ {n} {v : Vec Unit n} → Sg (nonNil v) → Sg v
g sg = sg

one : Sg (suc zero)
one = sg

test : Sg (unit ∷ [])
test = g one    -- `one' is yellow, a meta coming from the forced n

{- Analysis

g :=> Sg (nonNil {_n} _v) -> Sg _v
one :=> Sg (suc zero)
suc zero =?= nonNil {_n} _v
use injectivity
_n := suc _n'
_v := _∷_ {_nv} _i _is
zero =?= f {_nv} {_i} {_is} _i
using injectivity on f creates unsolved, because "forced" meta:

inverting injective function _.f :
({.n : Nat} (i : Unit) (is : Vec Unit .n) → Unit → Nat) for zero
(args = [$ {_32}, $ _33, $ _34, $ _33])
meta patterns [_35, _36, _37]
  perm = x0,x1,x2 -> x0,x1,x2
  tel  = {.n : Nat} (i : Unit) (is : Vec Unit .n)
  ps   = [[]!{VarP ".n"}, []k(VarP "i"), []k(VarP "is"),
          []r(ConP Common.Prelude.Unit.unit(inductive)[] Nothing [])]
inversion
  lhs  = [$ {_35}, $ _36, $ _37, $ unit]
  rhs  = [$ {_32}, $ _33, $ _34, $ _33]
  type = ({.n : Nat} (i : Unit) (is : Vec Unit .n) → Unit → Nat)
  a    = ({.n : Nat} (i : Unit) (is : Vec Unit .n) → Unit → Nat)
  v    = (_.f)
  arg1 = {_35}
  arg2 = {_32}
-- Here, the equality check is skipped as n is "forced", so the
-- assignment _35 := _32 does not happen
  a    = ((i : Unit) (is : Vec Unit _35) → Unit → Nat)
  v    = (_.f {_35})
  arg1 = _36
  arg2 = _33
term _36 := _33
term _36 := _33
solving _36 := _33
  a    = ((is : Vec Unit _35) → Unit → Nat)
  v    = (_.f {_35} _33)
  arg1 = _37
  arg2 = _34
term _37 := _34
term _37 := _34
solving _37 := _34
  a    = (Unit → Nat)
  v    = (_.f {_35} _33 _34)
  arg1 = unit
  arg2 = _33
compareTerm unit == _33 : Unit
term _33 := unit
term _33 := unit
solving _33 := unit
compareTerm zero == (_.f {_32} unit _34 unit) : Nat
-}

-- Should work without unsolved metas.

ext: agda

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
open import Agda.Builtin.Equality

_∋_ : ∀ {a} (A : Set a) → A → A
A ∋ x = x

cong : ∀ {a b} {A : Set a} {B : Set b}
       (f : A → B) {x y} → x ≡ y → f x ≡ f y
cong f refl = refl

record IsRG (Node : Set) (Edge : Set) : Set where
  field
    src : Edge → Node
    tgt : Edge → Node
    rfl : Node → Edge
    eq-src-rfl : ∀{x} → src (rfl x) ≡ x
    eq-tgt-rfl : ∀{x} → tgt (rfl x) ≡ x
open IsRG {{...}} public

module norecord where

  source : ∀{Node Edge : Set} {{i : IsRG Node Edge}} → Edge → Node
  source x = src x

  lemma1 : ∀{Node Edge : Set} {{i : IsRG Node Edge}} → (e : Edge) → (Node ∋ source e) ≡ src e
  lemma1 e = refl

  rfl-src : ∀{Node Edge : Set} {{i : IsRG Node Edge}} → Edge → Edge
  rfl-src {Node} e = rfl (Node ∋ src e)

  lemma2 : ∀{Node Edge : Set} {{i : IsRG Node Edge}} → (n : Node) → rfl-src {Node} (rfl n) ≡ (Edge ∋ rfl n)
  lemma2 {Node}{Edge} n = cong (rfl {Node = Node}) (eq-src-rfl {Edge = Edge})

module yesrecord where

  record RG : Set₁ where
    constructor mkRG
    field
      Node : Set
      Edge : Set
      {{isRG}} : IsRG Node Edge
  open RG public

  source : ∀{rg} → Edge rg → Node rg
  source x = src x

  lemma1 : ∀{rg} → (e : Edge rg) → (Node rg ∋ source {mkRG (Node rg) (Edge rg)} e) ≡ src e
  --causes problems:
  --lemma1 : ∀{rg} → (e : Edge rg) → (Node rg ∋ source {_} e) ≡ src e
  lemma1 e = refl

  rfl-src : ∀{rg} → Edge rg → Edge rg
  rfl-src {rg} e = rfl (Node rg ∋ src e)

  lemma2 : ∀{rg} → (n : Node rg) → rfl-src {rg} (rfl n) ≡ (Edge rg ∋ rfl n)
  lemma2 {rg} n = cong (rfl {Node = Node rg}) (eq-src-rfl {Edge = Edge rg})

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
{- Jesper, 2019-07-05: At first, the fix to #3859 causes the line below to
raise a type error:

  Cannot instantiate the metavariable _6 to solution Set
  (Agda.Primitive.lsuc (Agda.Primitive.lsuc Agda.Primitive.lzero)
  Agda.Primitive.⊔ Agda.Primitive.lsuc a) since it contains the
  variable a which is not in scope of the metavariable or irrelevant
  in the metavariable but relevant in the solution
  when checking that the expression λ (A : Set a) → Set has type
  (A : Set a) → Set₁

Now it is no longer the case. This test case is here to make sure the
error doesn't come back.
-}

F = λ {a} (A : Set a) → Set


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.Ints.DiffInt.Base where

open import Cubical.Foundations.Prelude

open import Cubical.HITs.SetQuotients
open import Cubical.Foundations.Isomorphism

open import Cubical.Data.Sigma
open import Cubical.Data.Nat hiding (+-comm ; +-assoc) renaming (_+_ to _+ℕ_)
open import Cubical.Data.Int

rel : (ℕ × ℕ) → (ℕ × ℕ) → Type₀
rel (a₀ , b₀) (a₁ , b₁) = x ≡ y
  where
    x = a₀ +ℕ b₁
    y = a₁ +ℕ b₀

ℤ = (ℕ × ℕ) / rel

-- Proof of equivalence between Int and DiffInt

private
  -- Prove all the identities for ℕ×ℕ first and use that to build to ℤ

  Int→ℕ×ℕ : Int → (ℕ × ℕ)
  Int→ℕ×ℕ (pos n)    = ( n    , zero  )
  Int→ℕ×ℕ (negsuc n) = ( zero , suc n )

  ℕ×ℕ→Int : (ℕ × ℕ) → Int
  ℕ×ℕ→Int(n , m) = n ℕ- m

  relInt→ℕ×ℕ : ∀ m n → rel (Int→ℕ×ℕ (m ℕ- n)) (m , n)
  relInt→ℕ×ℕ zero zero = refl
  relInt→ℕ×ℕ zero (suc n) = refl
  relInt→ℕ×ℕ (suc m) zero = refl
  relInt→ℕ×ℕ (suc m) (suc n) =
    fst (Int→ℕ×ℕ (m ℕ- n)) +ℕ suc n   ≡⟨ +-suc (fst (Int→ℕ×ℕ (m ℕ- n))) n ⟩
    suc (fst (Int→ℕ×ℕ (m ℕ- n)) +ℕ n) ≡⟨ cong suc (relInt→ℕ×ℕ m n) ⟩
    suc (m +ℕ snd (Int→ℕ×ℕ (m ℕ- n))) ∎

  Int→ℕ×ℕ→Int : ∀ n → ℕ×ℕ→Int (Int→ℕ×ℕ n) ≡ n
  Int→ℕ×ℕ→Int (pos n) = refl
  Int→ℕ×ℕ→Int (negsuc n) = refl

  ℕ×ℕ→Int→ℕ×ℕ : ∀ p → rel (Int→ℕ×ℕ (ℕ×ℕ→Int p)) p
  ℕ×ℕ→Int→ℕ×ℕ (p₀ , p₁) = relInt→ℕ×ℕ p₀ p₁

-- Now build to ℤ using the above

Int→ℤ : Int → ℤ
Int→ℤ n = [ Int→ℕ×ℕ n ]

ℤ→Int : ℤ → Int
ℤ→Int [ z ] = ℕ×ℕ→Int z
ℤ→Int(eq/ a b r i) = lemℤeq a b r i
  where lemℤeq : (a b : (ℕ × ℕ)) → rel a b → ℕ×ℕ→Int(a) ≡ ℕ×ℕ→Int(b)
        lemℤeq (a₀ , a₁) (b₀ , b₁) r = a₀ ℕ- a₁          ≡⟨ pos- a₀ a₁ ⟩
                pos a₀ - pos a₁                          ≡[ i ]⟨ ((pos a₀ - pos a₁) + -Cancel (pos b₁) (~ i)) ⟩
               (pos a₀ - pos a₁) + (pos b₁ - pos b₁)     ≡⟨ +-assoc (pos a₀ + (- pos a₁)) (pos b₁) (- pos b₁) ⟩
              ((pos a₀ - pos a₁) + pos b₁) - pos b₁      ≡[ i ]⟨ +-assoc (pos a₀) (- pos a₁) (pos b₁) (~ i) + (- pos b₁) ⟩
               (pos a₀ + ((- pos a₁) + pos b₁)) - pos b₁ ≡[ i ]⟨ (pos a₀ + +-comm (- pos a₁) (pos b₁) i) - pos b₁ ⟩
               (pos a₀ + (pos b₁ - pos a₁)) - pos b₁     ≡[ i ]⟨ +-assoc (pos a₀) (pos b₁) (- pos a₁) i + (- pos b₁)  ⟩
              ((pos a₀ + pos b₁) - pos a₁) - pos b₁      ≡[ i ]⟨ (pos+ a₀ b₁ (~ i) - pos a₁) - pos b₁ ⟩
               (pos (a₀ +ℕ b₁) - pos a₁) - pos b₁        ≡[ i ]⟨ (pos (r i) - pos a₁) - pos b₁ ⟩
               (pos (b₀ +ℕ a₁) - pos a₁) - pos b₁        ≡[ i ]⟨ (pos+ b₀ a₁ i - pos a₁) - pos b₁ ⟩
              ((pos b₀ + pos a₁) - pos a₁) - pos b₁      ≡[ i ]⟨ +-assoc (pos b₀) (pos a₁) (- pos a₁) (~ i) + (- pos b₁) ⟩
               (pos b₀ + (pos a₁ - pos a₁)) - pos b₁     ≡[ i ]⟨ (pos b₀ + (-Cancel (pos a₁) i)) - pos b₁ ⟩
                pos b₀ - pos b₁                          ≡[ i ]⟨ pos- b₀ b₁ (~ i) ⟩
                b₀ ℕ- b₁                                 ∎
ℤ→Int(squash/ x x₀ p q i j) = isSetInt (ℤ→Int x) (ℤ→Int x₀) (cong ℤ→Int p) (cong ℤ→Int q) i j

Int→ℤ→Int : ∀ z → ℤ→Int (Int→ℤ z) ≡ z
Int→ℤ→Int (pos n)    = refl
Int→ℤ→Int (negsuc n) = refl

ℤ→Int→ℤ : ∀ z → Int→ℤ (ℤ→Int z) ≡ z
ℤ→Int→ℤ = elimProp (λ z → squash/ (Int→ℤ (ℤ→Int z)) z) ℕ×ℕprf
  where ℕ×ℕprf : (a : ℕ × ℕ) → Int→ℤ (ℤ→Int [ a ]) ≡ [ a ]
        ℕ×ℕprf (a , b) = eq/ (Int→ℕ×ℕ (ℕ×ℕ→Int (a , b))) (a , b) (ℕ×ℕ→Int→ℕ×ℕ (a , b))

Int≡DiffInt : Int ≡ ℤ
Int≡DiffInt = isoToPath (iso Int→ℤ ℤ→Int ℤ→Int→ℤ Int→ℤ→Int)

max_stars_repo_name: Edlyr/cubical

max_issues_repo_name: Edlyr/cubical

max_forks_repo_name: Edlyr/cubical


text:
{- Byzantine Fault Tolerant Consensus Verification in Agda, version 0.9.

   Copyright (c) 2021, Oracle and/or its affiliates.
   Licensed under the Universal Permissive License v 1.0 as shown at https://opensource.oracle.com/licenses/upl
-}

open import Level using (0ℓ)
open import Data.String

-- This module defines utility functions to help working on proofs.

module LibraBFT.Base.Util where

  -- These should obviously not be used in any legitimate proof.  They are just for convenience when
  -- we want to avoid importing a module with open holes while working on something else.

  -- This variant allows a comment to be attached conveniently
  obm-dangerous-magic' : ∀ {ℓ} {A : Set ℓ} → String → A
  obm-dangerous-magic' {ℓ} {A} _ = magic
    where postulate magic : A

  obm-dangerous-magic! : ∀ {ℓ} {A : Set ℓ} → A
  obm-dangerous-magic! {ℓ} {A} = obm-dangerous-magic' ""


text:
------------------------------------------------------------------------------
-- Distributive laws on a binary operation: Task B
------------------------------------------------------------------------------

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

module DistributiveLaws.TaskB-I where

open import DistributiveLaws.Base
open import DistributiveLaws.PropertiesI

open import Common.FOL.Relation.Binary.EqReasoning

------------------------------------------------------------------------------
prop₂ : ∀ u x y z →
        (x · y · (z · u)) · ((x · y · (z · u)) · (x · z · (y · u))) ≡
          x · z · (y · u)
prop₂ u x y z =
  xy·zu · (xy·zu · xz·yu)                                         ≡⟨ j₁ ⟩
  xy·zu · (x·zu · y·zu · xz·yu)                                   ≡⟨ j₂ ⟩
  xy·zu · (x·zu · xz·yu · (y·zu · xz·yu))                         ≡⟨ j₃ ⟩
-- Note: The paper proof has a typo in the third proof step:
-- xy·zu · (xz·xu · xz·yu · (z·zu · xz·yu))
  xy·zu · (xz·xu · xz·yu · (y·zu · xz·yu))                        ≡⟨ j₄ ⟩
  xy·zu · (xz · xu·yu · (y·zu · xz·yu))                           ≡⟨ j₅ ⟩
  xy·zu · (xz · xyu · (y·zu · xz·yu))                             ≡⟨ j₆ ⟩
  xy·zu · (xz · xyu · (yz·yu · xz·yu))                            ≡⟨ j₇ ⟩
  xy·zu · (xz · xyu · (yz·xz · yu))                               ≡⟨ j₈ ⟩
  xy·zu · (xz · xyu · (yxz · yu))                                 ≡⟨ j₉ ⟩
  xy·zu · (xz · xyu · (yx·yu · z·yu))                             ≡⟨ j₁₀ ⟩
  xy·zu · (xz · xyu · (y·xu · z·yu))                              ≡⟨ j₁₁ ⟩
  xyz · xyu · (xz · xyu · (y·xu · z·yu))                          ≡⟨ j₁₂ ⟩
  xz·yz · xyu · (xz · xyu · (y·xu · z·yu))                        ≡⟨ j₁₃ ⟩
  xz · xyu · (yz · xyu) · (xz · xyu · (y·xu · z·yu))              ≡⟨ j₁₄ ⟩
  xz · xyu · (yz · xyu · (y·xu · z·yu))                           ≡⟨ j₁₅ ⟩
  xz · xyu · (yz · xu·yu · (y·xu · z·yu))                         ≡⟨ j₁₆ ⟩
  xz · xyu · (y · xu·yu · (z · xu·yu) · (y·xu · z·yu))            ≡⟨ j₁₇ ⟩
  xz · xyu ·
  (y · xu·yu · (y·xu · z·yu) · (z · xu·yu · (y·xu · z·yu)))       ≡⟨ j₁₈ ⟩
  xz · xyu ·
  (y·xu · y·yu · (y·xu · z·yu) · (z · xu·yu · (y·xu · z·yu)))     ≡⟨ j₁₉ ⟩
  xz · xyu · (y·xu · (y·yu · z·yu) · (z · xu·yu · (y·xu · z·yu))) ≡⟨ j₂₀ ⟩
  xz · xyu · (y·xu · yz·yu · (z · xu·yu · (y·xu · z·yu)))         ≡⟨ j₂₁ ⟩
  xz · xyu · (y·xu · y·zu · (z · xu·yu · (y·xu · z·yu)))          ≡⟨ j₂₂ ⟩
  xz · xyu · (y · xu·zu · (z · xu·yu · (y·xu · z·yu)))            ≡⟨ j₂₃ ⟩
  xz · xyu · (y · xu·zu · (z·xu · z·yu · (y·xu · z·yu)))          ≡⟨ j₂₄ ⟩
  (xz · xyu) · (y · xu·zu · (z·xu · y·xu · z·yu))                 ≡⟨ j₂₅ ⟩
  xz · xyu · (y · xu·zu · (zy·xu · z·yu))                         ≡⟨ j₂₆ ⟩
  xz · xyu · (y · xu·zu · (zy·xu · zy·zu))                        ≡⟨ j₂₇ ⟩
  xz · xyu · (y · xu·zu · (zy · xu·zu))                           ≡⟨ j₂₈ ⟩
  xz · xyu · (y·zy · xu·zu)                                       ≡⟨ j₂₉ ⟩
  xz · xyu · (y·zy · xzu)                                         ≡⟨ j₃₀ ⟩
  xz·xy · xzu · (y·zy · xzu)                                      ≡⟨ j₃₁ ⟩
  x·zy · xzu · (y·zy · xzu)                                       ≡⟨ j₃₂ ⟩
  x·zy · y·zy · xzu                                               ≡⟨ j₃₃ ⟩
  xy·zy · xzu                                                     ≡⟨ j₃₄ ⟩
  xzy · xzu                                                       ≡⟨ j₃₅ ⟩
  xz·yu                                                           ∎
  where
  -- Two variables abbreviations

  xz = x · z
  yu = y · u
  yz = y · z
  zy = z · y

  -- Three variables abbreviations

  xyu = x · y · u
  xyz = x · y · z
  xzu = x · z · u
  xzy = x · z · y
  yxz = y · x · z

  x·yu = x · (y · u)
  x·zu = x · (z · u)
  x·zy = x · (z · y)

  y·xu = y · (x · u)
  y·yu = y · (y · u)
  y·zu = y · (z · u)
  y·zy = y · (z · y)

  z·xu = z · (x · u)
  z·yu = z · (y · u)

  -- Four variables abbreviations

  xu·yu = x · u · (y · u)
  xu·zu = x · u · (z · u)

  xy·yz = x · y · (y · z)
  xy·zu = x · y · (z · u)
  xy·zy = x · y · (z · y)

  xz·xu = x · z · (x · u)
  xz·xy = x · z · (x · y)
  xz·yu = x · z · (y · u)
  xz·yz = x · z · (y · z)

  yx·yu = y · x · (y · u)

  yz·xz = y · z · (x · z)
  yz·yu = y · z · (y · u)

  zy·xu = z · y · (x · u)
  zy·zu = z · y · (z · u)

  -- Steps justifications

  j₁ : xy·zu · (xy·zu · xz·yu) ≡
       xy·zu · (x·zu · y·zu · xz·yu)
  j₁ = ·-rightCong (·-leftCong (rightDistributive x y (z · u)))

  j₂ : xy·zu · (x·zu · y·zu · xz·yu) ≡
       xy·zu · (x·zu · xz·yu · (y·zu · xz·yu))
  j₂ = ·-rightCong (rightDistributive x·zu y·zu xz·yu)

  j₃ : xy·zu · (x·zu · xz·yu · (y·zu · xz·yu)) ≡
       xy·zu · (xz·xu · xz·yu · (y·zu · xz·yu))
  j₃ = ·-rightCong (·-leftCong (·-leftCong (leftDistributive x z u)))

  j₄ : xy·zu · (xz·xu · xz·yu · (y·zu · xz·yu)) ≡
       xy·zu · (xz · xu·yu · (y·zu · xz·yu))
  j₄ = ·-rightCong (·-leftCong (sym (leftDistributive (x · z) (x · u) (y · u))))

  j₅ : xy·zu · (xz · xu·yu · (y·zu · xz·yu)) ≡
       xy·zu · (xz · xyu · (y·zu · xz·yu))
  j₅ = ·-rightCong (·-leftCong (·-rightCong (sym (rightDistributive x y u))))

  j₆ : xy·zu · (xz · xyu · (y·zu · xz·yu)) ≡
       xy·zu · (xz · xyu · (yz·yu · xz·yu))
  j₆ = ·-rightCong (·-rightCong (·-leftCong (leftDistributive y z u)))

  j₇ : xy·zu · (xz · xyu · (yz·yu · xz·yu)) ≡
       xy·zu · (xz · xyu · (yz·xz · yu))
  j₇ = ·-rightCong (·-rightCong (sym (rightDistributive (y · z) (x · z) (y · u))))

  j₈ : xy·zu · (xz · xyu · (yz·xz · yu)) ≡
       xy·zu · (xz · xyu · (yxz · yu))
  j₈ = ·-rightCong (·-rightCong (·-leftCong (sym (rightDistributive y x z))))

  j₉ : xy·zu · (xz · xyu · (yxz · yu)) ≡
       xy·zu · (xz · xyu · (yx·yu · z·yu))
  j₉ = ·-rightCong (·-rightCong (rightDistributive (y · x) z yu))

  j₁₀ : xy·zu · (xz · xyu · (yx·yu · z·yu)) ≡
        xy·zu · (xz · xyu · (y·xu · z·yu))
  j₁₀ = ·-rightCong (·-rightCong (·-leftCong (sym (leftDistributive y x u))))

  j₁₁ : xy·zu · (xz · xyu · (y·xu · z·yu)) ≡
        xyz · xyu · (xz · xyu · (y·xu · z·yu))
  j₁₁ = ·-leftCong (leftDistributive (x · y) z u)

  j₁₂ : xyz · xyu · (xz · xyu · (y·xu · z·yu)) ≡
        xz·yz · xyu · (xz · xyu · (y·xu · z·yu))
  j₁₂ = ·-leftCong (·-leftCong (rightDistributive x y z))

  j₁₃ : xz·yz · xyu · (xz · xyu · (y·xu · z·yu)) ≡
        xz · xyu · (yz · xyu) · (xz · xyu · (y·xu · z·yu))
  j₁₃ = ·-leftCong (rightDistributive (x · z) (y · z) xyu)

  j₁₄ : xz · xyu · (yz · xyu) · (xz · xyu · (y·xu · z·yu)) ≡
        xz · xyu · (yz · xyu · (y·xu · z·yu))
  j₁₄ = sym (leftDistributive (xz · xyu) (yz · xyu) (y·xu · z·yu))

  j₁₅ : xz · xyu · (yz · xyu · (y·xu · z·yu)) ≡
        xz · xyu · (yz · xu·yu · (y·xu · z·yu))
  j₁₅ = ·-rightCong (·-leftCong (·-rightCong (rightDistributive x y u)))

  j₁₆ : xz · xyu · (yz · xu·yu · (y·xu · z·yu)) ≡
        xz · xyu · (y · xu·yu · (z · xu·yu) · (y·xu · z·yu))
  j₁₆ = ·-rightCong (·-leftCong (rightDistributive y z xu·yu))

  j₁₇ : xz · xyu · (y · xu·yu · (z · xu·yu) · (y·xu · z·yu)) ≡
        xz · xyu ·
        (y · xu·yu · (y·xu · z·yu) · (z · xu·yu · (y·xu · z·yu)))
  j₁₇ = subst (λ t → xz · xyu · (y · xu·yu · (z · xu·yu) · (y·xu · z·yu)) ≡
                     xz · xyu · t)
              (rightDistributive (y · xu·yu) (z · xu·yu) (y·xu · z·yu))
              refl

  j₁₈ : xz · xyu ·
        (y · xu·yu · (y·xu · z·yu) · (z · xu·yu · (y·xu · z·yu))) ≡
        xz · xyu ·
        (y·xu · y·yu · (y·xu · z·yu) · (z · xu·yu · (y·xu · z·yu)))
  j₁₈ = ·-rightCong (·-leftCong (·-leftCong (leftDistributive y (x · u) (y · u))))

  j₁₉ : xz · xyu ·
        (y·xu · y·yu · (y·xu · z·yu) · (z · xu·yu · (y·xu · z·yu))) ≡
        xz · xyu · (y·xu · (y·yu · z·yu) · (z · xu·yu · (y·xu · z·yu)))
  j₁₉ = subst (λ t → xz · xyu ·
                     (y·xu · y·yu · (y·xu · z·yu) · (z · xu·yu · (y·xu · z·yu)))
                     ≡
                     xz · xyu · (t · (z · xu·yu · (y·xu · z·yu))))
              (sym (leftDistributive y·xu y·yu z·yu))
              refl

  j₂₀ : xz · xyu · (y·xu · (y·yu · z·yu) · (z · xu·yu · (y·xu · z·yu))) ≡
        xz · xyu · (y·xu · yz·yu · (z · xu·yu · (y·xu · z·yu)))
  j₂₀ = ·-rightCong (·-leftCong (·-rightCong (sym (rightDistributive y z (y · u)))))

  j₂₁ : xz · xyu · (y·xu · yz·yu · (z · xu·yu · (y·xu · z·yu))) ≡
        xz · xyu · (y·xu · y·zu · (z · xu·yu · (y·xu · z·yu)))
  j₂₁ = ·-rightCong (·-leftCong (·-rightCong (sym (leftDistributive y z u))))

  j₂₂ : xz · xyu · (y·xu · y·zu · (z · xu·yu · (y·xu · z·yu))) ≡
        xz · xyu · (y · xu·zu · (z · xu·yu · (y·xu · z·yu)))
  j₂₂ = ·-rightCong (·-leftCong (sym (leftDistributive y (x · u) (z · u))))

  j₂₃ : xz · xyu · (y · xu·zu · (z · xu·yu · (y·xu · z·yu))) ≡
        xz · xyu · (y · xu·zu · (z·xu · z·yu · (y·xu · z·yu)))
  j₂₃ = ·-rightCong (·-rightCong (·-leftCong (leftDistributive z (x · u) (y · u))))

  j₂₄ : xz · xyu · (y · xu·zu · (z·xu · z·yu · (y·xu · z·yu))) ≡
        (xz · xyu) · (y · xu·zu · (z·xu · y·xu · z·yu))
  j₂₄ = ·-rightCong (·-rightCong (sym (rightDistributive z·xu y·xu z·yu)))

  j₂₅ : (xz · xyu) · (y · xu·zu · (z·xu · y·xu · z·yu)) ≡
        xz · xyu · (y · xu·zu · (zy·xu · z·yu))
  j₂₅ = ·-rightCong (·-rightCong (·-leftCong (sym (rightDistributive z y (x · u)))))

  j₂₆ : xz · xyu · (y · xu·zu · (zy·xu · z·yu)) ≡
        xz · xyu · (y · xu·zu · (zy·xu · zy·zu))
  j₂₆ = ·-rightCong (·-rightCong (·-rightCong (leftDistributive z y u)))

  j₂₇ : xz · xyu · (y · xu·zu · (zy·xu · zy·zu)) ≡
        xz · xyu · (y · xu·zu · (zy · xu·zu))
  j₂₇ = ·-rightCong (·-rightCong (sym (leftDistributive (z · y) (x · u) (z · u))))

  j₂₈ : xz · xyu · (y · xu·zu · (zy · xu·zu)) ≡
        xz · xyu · (y·zy · xu·zu)
  j₂₈ = ·-rightCong (sym (rightDistributive y zy xu·zu))

  j₂₉ : xz · xyu · (y·zy · xu·zu) ≡
        xz · xyu · (y·zy · xzu)
  j₂₉ = ·-rightCong (·-rightCong (sym (rightDistributive x z u)))

  j₃₀ : xz · xyu · (y·zy · xzu) ≡
        xz·xy · xzu · (y·zy · xzu)
  j₃₀ = ·-leftCong (leftDistributive xz (x · y) u)

  j₃₁ : xz·xy · xzu · (y·zy · xzu) ≡
        x·zy · xzu · (y·zy · xzu)
  j₃₁ = ·-leftCong (·-leftCong (sym (leftDistributive x z y)))

  j₃₂ : x·zy · xzu · (y·zy · xzu) ≡
        x·zy · y·zy · xzu
  j₃₂ = sym (rightDistributive x·zy y·zy xzu)

  j₃₃ : x·zy · y·zy · xzu ≡
        xy·zy · xzu
  j₃₃ = ·-leftCong (sym (rightDistributive x y zy))

  j₃₄ : xy·zy · xzu ≡
        xzy · xzu
  j₃₄ = ·-leftCong (sym (rightDistributive x z y))

  j₃₅ : xzy · xzu ≡
        xz·yu
  j₃₅ = sym (leftDistributive xz y u)

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
-- Andreas, 2019-07-05, during work on issue #3889
-- Test-case for with extracted from the standard library

{-# OPTIONS --cubical-compatible #-}

open import Agda.Primitive
open import Agda.Builtin.Equality
open import Agda.Builtin.List

open import Common.Equality
open import Common.Product

data Any {a}{A : Set a} {p} (P : A → Set p) : List A → Set (a ⊔ p) where
  here  : ∀ {x xs} (px  : P x)      → Any P (x ∷ xs)
  there : ∀ {x xs} (pxs : Any P xs) → Any P (x ∷ xs)

_∈_ : ∀{a}{A : Set a} → A → List A → Set _
x ∈ xs = Any (x ≡_) xs

map : ∀ {a} {A : Set a} {p q} {P : A → Set p} {Q : A → Set q} → (∀{x} → P x → Q x) → ∀{xs} → Any P xs → Any Q xs
map g (here px)   = here (g px)
map g (there pxs) = there (map g pxs)

map₁ : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c} →
       (A → B) → A × C → B × C
map₁ f (x ,  y)= f x , y

map₂ : ∀ {a b c} {A : Set a} {B : A → Set b} {C : A → Set c} →
       (∀ {x} → B x → C x) → Σ A B → Σ A C
map₂ f (x , y) = (x , f y)

find : ∀ {a} {p} {A : Set a} {P : A → Set p} {xs} → Any P xs → Σ _ λ x → x ∈ xs × P x
find (here px)   = (_ , here refl , px)
find (there pxs) = map₂ (map₁ there) (find pxs)

lose : ∀ {a} {p} {A : Set a} {P : A → Set p} {x xs} → x ∈ xs → P x → Any P xs
lose x∈xs px = map (λ eq → subst _ eq px) x∈xs

map∘find : ∀ {a p} {A : Set a} {P : A → Set p} {xs}
           (p : Any P xs) → let p′ = find p in
           {f : ∀{x} → proj₁ p′ ≡ x → P x} →
           f refl ≡ proj₂ (proj₂ p′) →
           map f (proj₁ (proj₂ p′)) ≡ p
map∘find (here  p) hyp = cong here  hyp
map∘find (there p) hyp = cong there (map∘find p hyp)

find∘map : ∀ {a p q} {A : Set a} {P : A → Set p} {Q : A → Set q}
           {xs : List A} (p : Any P xs) (f : ∀{x} → P x → Q x) →
           find (map f p) ≡ map₂ (map₂ f) (find p)
find∘map (here  p) f = refl
find∘map (there p) f rewrite find∘map p f = refl

lose∘find : ∀ {a p} {A : Set a} {P : A → Set p} {xs : List A}
            (p : Any P xs) →
            (let (y , z) = proj₂ (find p)) →
            lose y z ≡ p
lose∘find p = map∘find p refl

postulate
  a b ℓ : Level
  A : Set a
  B : Set b
  P : A → Set ℓ
  Q : B → Set ℓ   -- Level needed

Any-×⁺ : ∀ {xs ys} → Any P xs × Any Q ys →
         Any (λ x → Any (λ y → P x × Q y) ys) xs
Any-×⁺ (p , q) = map (λ p → map (λ q → (p , q)) q) p

Any-×⁻ : ∀ {xs ys} → Any (λ x → Any (λ y → P x × Q y) ys) xs →
         Any P xs × Any Q ys
Any-×⁻ pq with map₂ (map₂ find) (find pq)
... | (x , x∈xs , y , y∈ys , p , q) = (lose x∈xs p , lose y∈ys q)

module _ where
  from∘to : ∀{xs ys} (pq : Any P xs × Any Q ys) → Any-×⁻ (Any-×⁺ pq) ≡ pq
  -- from∘to (p , q) = {!!}
  from∘to (p , q) rewrite
      find∘map p (λ p → map (λ q → (p , q)) q)
    | find∘map q (λ q → proj₂ (proj₂ (find p)) , q)
    | lose∘find p
    | lose∘find q
    = refl


text:
{-# OPTIONS --universe-polymorphism #-}

module Categories.CategorySolver where

open import Level
open import Categories.Category
open import Categories.Functor hiding (equiv) renaming (id to idF; _≡_ to _≡F_; _∘_ to _∘F_; ∘-resp-≡ to ∘F-resp-≡F)
open import Categories.NaturalTransformation hiding (equiv) renaming (id to idT; _≡_ to _≡T_)

{- We need a way to force the universe levels of two categories to be
   the same, to hack together a reified morphism type.  These lift
   operations let us do this in reification. -}

liftCategory : ∀ {o ℓ e o′ ℓ′ e′} (C : Category o ℓ e) → Category (o ⊔ o′) (ℓ ⊔ ℓ′) (e ⊔ e′)
liftCategory {o} {ℓ} {e} {o′} {ℓ′} {e′} C = record {
                                              Obj = Lift {ℓ = o′} (Category.Obj C);
                                              _⇒_ = λ s d → Lift {ℓ = ℓ′} ((lower s) ⇒ (lower d));
                                              _≡_ = λ m₀ m₁ → Lift {ℓ = e′} (lower m₀ ≡ lower m₁);
                                              id = lift id;
                                              _∘_ = λ m₀ m₁ → lift (lower m₀ ∘ lower m₁);
                                              assoc = λ {A} {B} {C₁} {D} {f} {g} {h} → lift C.assoc;
                                              identityˡ = λ {A} {B} {f} → lift C.identityˡ;
                                              identityʳ = λ {A} {B} {f} → lift C.identityʳ;
                                              equiv = record { refl = λ {x} → lift Equiv.refl
                                                             ; sym = λ x → lift (Equiv.sym (lower x))
                                                             ; trans = λ x y → lift (Equiv.trans (lower x) (lower y)) };
                                              ∘-resp-≡ = λ x y → lift (∘-resp-≡ (lower x) (lower y)) }
             where
               module C = Category C
               open C

liftFunctor : ∀ {o₀ ℓ₀ e₀ o′₀ ℓ′₀ e′₀ o₁ ℓ₁ e₁ o′₁ ℓ′₁ e′₁} {C : Category o₀ ℓ₀ e₀} {D : Category o₁ ℓ₁ e₁}
              → Functor C D → Functor (liftCategory {o′ = o′₀} {ℓ′₀} {e′₀} C) (liftCategory {o′ = o′₁} {ℓ′₁} {e′₁} D)
liftFunctor {o₀} {ℓ₀} {e₀} {o′₀} {ℓ′₀} {e′₀} {o₁} {ℓ₁} {e₁} {o′₁} {ℓ′₁} {e′₁} {C} {D} F =
  record {
    F₀ = λ x → lift (F.F₀ (lower x));
    F₁ = λ m → lift (F.F₁ (lower m));
    identity = lift F.identity;
    homomorphism = lift F.homomorphism;
    F-resp-≡ = λ H → lift (F.F-resp-≡ (lower H)) }
  where
    module C = Category C
    module D = Category D
    module ↑C = Category (liftCategory {o′ = o′₀} {ℓ′₀} {e′₀} C)
    module ↑D = Category (liftCategory {o′ = o′₁} {ℓ′₁} {e′₁} D)
    module F = Functor F

mutual
  data ReifiedMorphismHelper {o ℓ e} {C : Category o ℓ e} : Category.Obj C → Category.Obj C → Set (suc (o ⊔ ℓ ⊔ e)) where
    ∥_₁∥₀_ : ∀ {D : Category o ℓ e} → (F : Functor D C) → {s d : Category.Obj D} → (m : ReifiedMorphism {C = D} s d) → ReifiedMorphismHelper (Functor.F₀ F s) (Functor.F₀ F d)

  data ReifiedMorphism {o ℓ e} {C : Category o ℓ e} : Category.Obj C → Category.Obj C → Set (suc (o ⊔ ℓ ⊔ e)) where
    _∥∘∥_ : ∀ {s d d′ : Category.Obj C} → (m2 : ReifiedMorphism {C = C} d d′) → (m1 : ReifiedMorphism {C = C} s d) → ReifiedMorphism s d′
    ∥id∥ : ∀ {x : Category.Obj C} → ReifiedMorphism x x
    ∥_₁∥₁ : ∀ {s d : Category.Obj C} (m : ReifiedMorphismHelper {C = C} s d) → ReifiedMorphism s d
    ∥_∥ : ∀ {s d : Category.Obj C} → (m : Category._⇒_ C s d) → ReifiedMorphism s d

pattern ∥F₁∥m D F s d F₀s F₀d m = ∥_₁∥₁ {F₀s} {F₀d} (∥_₁∥₀_ {D} F {s} {d} m)
pattern ∥_₁∥_ F m = ∥ (∥ F ₁∥₀ m) ₁∥₁

⟱ : ∀ {o ℓ e} → {C : Category o ℓ e} → {s d : Category.Obj C} → ReifiedMorphism {C = C} s d → Category._⇒_ C s d
⟱ {C = C} (∥m₂∥ ∥∘∥ ∥m₁∥) = ⟱ ∥m₂∥ ∘ ⟱ ∥m₁∥
  where open Category C
⟱ {C = C} ∥id∥ = Category.id C
⟱ (∥ F ₁∥ ∥m∥) = Functor.F₁ F (⟱ ∥m∥)
⟱ ∥ m ∥ = m

record ReifiedMorphismOf {o ℓ e} {C : Category o ℓ e} {s d : Category.Obj C} (m : Category._⇒_ C s d) : Set (suc o ⊔ suc ℓ ⊔ suc e) where
  constructor reify
  field
    reified : ReifiedMorphism {C = C} s d
    .reified≡ : Category._≡_ C (⟱ {C = C} reified) m

ReifiedMorphismSimplify : ∀ {o ℓ e} → {C : Category o ℓ e} → {s d : Category.Obj C}
                            → (m : ReifiedMorphism {C = C} s d) → ReifiedMorphismOf {C = C} (⟱ m)
ReifiedMorphismSimplify {C = C} ∥ m ∥ = reify ∥ m ∥ (Category.Equiv.refl C)
ReifiedMorphismSimplify {C = C} ∥id∥  = reify ∥id∥ (Category.Equiv.refl C)
ReifiedMorphismSimplify {C = C} (∥m₀∥ ∥∘∥ ∥m₁∥) = ReifiedMorphismSimplify∥∘∥ {∥m₀∥ = ∥m₀∥} {∥m₁∥} (ReifiedMorphismSimplify ∥m₀∥) (ReifiedMorphismSimplify ∥m₁∥)
  where
    module C = Category C
    open C.HomReasoning

    ReifiedMorphismSimplify∥∘∥ : ∀ {s d d′ : C.Obj} → {∥m₀∥ : ReifiedMorphism {C = C} d d′} → {∥m₁∥ : ReifiedMorphism {C = C} s d}
                                 → ReifiedMorphismOf {C = C} (⟱ ∥m₀∥)
                                 → ReifiedMorphismOf {C = C} (⟱ ∥m₁∥)
                                 → ReifiedMorphismOf {C = C} (⟱ (∥m₀∥ ∥∘∥ ∥m₁∥))
    ReifiedMorphismSimplify∥∘∥ {∥m₀∥ = ∥m₀∥} {∥m₁∥} (reify ∥id∥ id≡m₀) (reify ∥m₁∥′ m₁′≡m₁) =
      reify ∥m₁∥′ (begin
                   ⟱ ∥m₁∥′
                 ↑⟨ C.identityˡ ⟩
                   C.id C.∘ ⟱ ∥m₁∥′
                 ↓⟨ C.∘-resp-≡ id≡m₀ m₁′≡m₁ ⟩
                   ⟱ (∥m₀∥ ∥∘∥ ∥m₁∥)
                 ∎)
    ReifiedMorphismSimplify∥∘∥ {∥m₀∥ = ∥m₀∥} {∥m₁∥} (reify ∥m₀∥′ m₀′≡m₀) (reify ∥id∥ id≡m₁) =
      reify ∥m₀∥′ (begin
                   ⟱ ∥m₀∥′
                 ↑⟨ C.identityʳ ⟩
                   ⟱ ∥m₀∥′ C.∘ C.id
                 ↓⟨ C.∘-resp-≡ m₀′≡m₀ id≡m₁ ⟩
                   ⟱ (∥m₀∥ ∥∘∥ ∥m₁∥)
                 ∎)
    ReifiedMorphismSimplify∥∘∥ {∥m₀∥ = ∥m₀∥} {∥m₁∥} (reify (∥m₀₀∥ ∥∘∥ ∥m₀₁∥) m₀₀∘m₀₁≡m₀) (reify ∥m₁∥′ m₁′≡m₁) =
      reify (∥m₀₀∥ ∥∘∥ (∥m₀₁∥ ∥∘∥ ∥m₁∥′)) (begin
                                     ⟱ (∥m₀₀∥ ∥∘∥ (∥m₀₁∥ ∥∘∥ ∥m₁∥′))
                                   ↑⟨ C.assoc ⟩
                                     (⟱ ∥m₀₀∥ C.∘ ⟱ ∥m₀₁∥) C.∘ ⟱ ∥m₁∥′
                                   ↓⟨ C.∘-resp-≡ m₀₀∘m₀₁≡m₀ m₁′≡m₁ ⟩
                                     ⟱ (∥m₀∥ ∥∘∥ ∥m₁∥)
                                   ∎)
    ReifiedMorphismSimplify∥∘∥ (reify ∥m₀∥′ m₀′≡m₀) (reify ∥m₁∥′ m₁′≡m₁) = reify (∥m₀∥′ ∥∘∥ ∥m₁∥′) (C.∘-resp-≡ m₀′≡m₀ m₁′≡m₁)
ReifiedMorphismSimplify {C = C} (∥F₁∥m D F s d ._ ._ ∥m∥) = ReifiedMorphismSimplifyF₀m {s = s} {d} {∥m∥}
                                                              (ReifiedMorphismSimplify ∥m∥)
  where
    module C = Category C
    module D = Category D
    module F = Functor F
    open C.HomReasoning

    ReifiedMorphismSimplifyF₀m : ∀ {s d : D.Obj} → {∥m∥ : ReifiedMorphism {C = D} s d}
                                   → ReifiedMorphismOf {C = D} (⟱ ∥m∥)
                                   → ReifiedMorphismOf {C = C} (F.F₁ (⟱ ∥m∥))
    ReifiedMorphismSimplifyF₀m {∥m∥ = ∥m∥} (reify ∥id∥ id≡m) =
      reify ∥id∥ (begin
                   C.id
                 ↑⟨ F.identity ⟩
                   F.F₁ D.id
                 ↓⟨ F.F-resp-≡ id≡m ⟩
                   F.F₁ (⟱ ∥m∥)
                 ∎)
    ReifiedMorphismSimplifyF₀m {∥m∥ = ∥m∥} (reify (∥m₀∥ ∥∘∥ ∥m₁∥) m₀∘m₁≡m) =
      reify (∥ F ₁∥ ∥m₀∥ ∥∘∥ ∥ F ₁∥ ∥m₁∥) (begin
                                       F.F₁ (⟱ ∥m₀∥) C.∘ F.F₁ (⟱ ∥m₁∥)
                                     ↑⟨ F.homomorphism ⟩
                                       F.F₁ (⟱ ∥m₀∥ D.∘ ⟱ ∥m₁∥)
                                     ↓⟨ F.F-resp-≡ m₀∘m₁≡m ⟩
                                       F.F₁ (⟱ ∥m∥)
                                     ∎)
    ReifiedMorphismSimplifyF₀m {∥m∥ = ∥m∥} (reify ∥m∥′ m′≡m) = reify (∥ F ₁∥ ∥m∥′) (F.F-resp-≡ m′≡m)

.removeIdentities : ∀ {o ℓ e} {C : Category o ℓ e} {s d : Category.Obj C} {m : Category._⇒_ C s d}
                    → (∥m∥ : ReifiedMorphismOf {C = C} m)
                     → Category._≡_ C (⟱ (ReifiedMorphismOf.reified (ReifiedMorphismSimplify (ReifiedMorphismOf.reified ∥m∥)))) m
removeIdentities {C = C} {m = m} ∥m∥ = begin
                                       ⟱
                                         (ReifiedMorphismOf.reified
                                          (ReifiedMorphismSimplify (ReifiedMorphismOf.reified ∥m∥)))
                                      ↓⟨ ReifiedMorphismOf.reified≡ (ReifiedMorphismSimplify (ReifiedMorphismOf.reified ∥m∥)) ⟩
                                        ⟱ (ReifiedMorphismOf.reified ∥m∥)
                                      ↓⟨ ReifiedMorphismOf.reified≡ ∥m∥ ⟩
                                        m
                                      ∎
  where
    module C = Category C
    open C.HomReasoning

.removeIdentities≡ : ∀ {o ℓ e} {C : Category o ℓ e} {s d : Category.Obj C} {m₀ m₁ : Category._⇒_ C s d}
                     → (∥m₀∥ : ReifiedMorphismOf {C = C} m₀)
                     → (∥m₁∥ : ReifiedMorphismOf {C = C} m₁)
                     → Category._≡_ C (⟱ (ReifiedMorphismOf.reified (ReifiedMorphismSimplify (ReifiedMorphismOf.reified ∥m₀∥))))
                                      (⟱ (ReifiedMorphismOf.reified (ReifiedMorphismSimplify (ReifiedMorphismOf.reified ∥m₁∥))))
                     → Category._≡_ C m₀ m₁
removeIdentities≡ {C = C} {m₀ = m₀} {m₁} ∥m₀∥ ∥m₁∥ m₀≡m₁ =
  begin
    m₀
  ↑⟨ ReifiedMorphismOf.reified≡ ∥m₀∥ ⟩
    ⟱ (ReifiedMorphismOf.reified ∥m₀∥)
  ↑⟨ ReifiedMorphismOf.reified≡
       (ReifiedMorphismSimplify (ReifiedMorphismOf.reified ∥m₀∥)) ⟩
    ⟱
      (ReifiedMorphismOf.reified
       (ReifiedMorphismSimplify (ReifiedMorphismOf.reified ∥m₀∥)))
  ↓⟨ m₀≡m₁ ⟩
    ⟱
      (ReifiedMorphismOf.reified
       (ReifiedMorphismSimplify (ReifiedMorphismOf.reified ∥m₁∥)))
  ↓⟨ ReifiedMorphismOf.reified≡
       (ReifiedMorphismSimplify (ReifiedMorphismOf.reified ∥m₁∥)) ⟩
    ⟱ (ReifiedMorphismOf.reified ∥m₁∥)
  ↓⟨ ReifiedMorphismOf.reified≡ ∥m₁∥ ⟩
    m₁
  ∎
  where
    module C = Category C
    open C.HomReasoning

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
------------------------------------------------------------------------------
-- The FOTC co-inductive lists type
------------------------------------------------------------------------------

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

-- N.B. This module is re-exported by FOTC.Data.Colist.

module FOTC.Data.Colist.Type where

open import FOTC.Base
open import FOTC.Base.List

------------------------------------------------------------------------------
-- The FOTC co-lists type (co-inductive predicate for total list).

-- Functional for the Colist predicate.
-- ColistF : (D → Set) → D → Set
-- ColistF A xs = xs ≡ [] ∨ ∃[ x' ] ∃[ xs' ] xs ≡ x' ∷ xs' ∧ A xs'

-- Colist is the greatest fixed-point of ColistF (by Colist-out and
-- Colist-coind).

postulate
  Colist : D → Set

postulate
-- Colist is a post-fixed point of ColistF, i.e.
--
-- Colist ≤ ColistF Colist.
  Colist-out : ∀ {xs} → Colist xs →
               xs ≡ [] ∨ (∃[ x' ] ∃[ xs' ] xs ≡ x' ∷ xs' ∧ Colist xs')
{-# ATP axiom Colist-out #-}

-- Colist is the greatest post-fixed point of ColistF, i.e.
--
-- ∀ A. A ≤ ColistF A ⇒ A ≤ Colist.
--
-- N.B. This is an axiom schema. Because in the automatic proofs we
-- *must* use an instance, we do not add this postulate as an ATP
-- axiom.
postulate
  Colist-coind :
    (A : D → Set) →
    -- A is post-fixed point of ColistF.
    (∀ {xs} → A xs → xs ≡ [] ∨ (∃[ x' ] ∃[ xs' ] xs ≡ x' ∷ xs' ∧ A xs')) →
    -- Colist is greater than A.
    ∀ {xs} → A xs → Colist xs


text:
module Eq where

infix 4 _≡_

{-
data _≡_ {A : Set} : A → A → Set where
  Refl : {x : A} → x ≡ x
-}

data _≡_ {a} {A : Set a} (x : A) : A → Set a where
  Refl : x ≡ x

{-# BUILTIN EQUALITY _≡_ #-}
{-# BUILTIN REFL Refl #-}

max_stars_repo_name: mjhopkins/PowerOfPi

max_issues_repo_name: mjhopkins/PowerOfPi

max_forks_repo_name: mjhopkins/PowerOfPi


text:
-- {-# OPTIONS -v tc.cc:30 -v tc.cover.splittree:10 #-}
-- 2013-05-03 Andreas, issue raise by Nisse.
module Issue842 where

data D : Set where
  c₁ c₂ : D

F : D → Set₁
F c₁ = Set
F = λ _ → Set

-- While not unthinkable, this is not the intended use of varying arity.
-- Since we are already splitting on the first argument, it should be
-- present on the lhs also in the second clause.

-- This will now give the error:

-- Incomplete pattern matching for F. Missing cases:
--   F c₂

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


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

open import Categories.Category
open import Categories.Category.Monoidal

module Experiment.Categories.Solver.Category.Monoidal
  {o ℓ e} {𝒞 : Category o ℓ e} (M : Monoidal 𝒞) where

open import Level
open import Relation.Binary using (Rel; REL)
open import Data.List

open import Categories.Morphism 𝒞

open Category 𝒞
open Monoidal M

infixr 10 _:⊗₀_ _:⊗₁_

data Sig : Set o where
  ∥_∥   : Obj → Sig
  :unit : Sig
  _:⊗₀_ : Sig → Sig → Sig

private
  variable
    A B C : Obj
    W X Y Z : Sig

data Expr : Rel Sig (o ⊔ ℓ) where
  :id  : Expr X X
  _:∘_ : Expr Y Z → Expr X Y → Expr X Z
  _:⊗₁_ : Expr X Y → Expr Z W → Expr (X :⊗₀ Z) (Y :⊗₀ W)
  :λ⇒ : Expr (:unit :⊗₀ X) X
  :λ⇐ : Expr X (:unit :⊗₀ X)
  :ρ⇒ : Expr (X :⊗₀ :unit) X
  :ρ⇐ : Expr X (X :⊗₀ :unit)
  :α⇒ : Expr ((X :⊗₀ Y) :⊗₀ Z) (X :⊗₀ (Y :⊗₀ Z))
  :α⇐ : Expr (X :⊗₀ (Y :⊗₀ Z)) ((X :⊗₀ Y) :⊗₀ Z)
  -- ∥_∥  : A ⇒ B → Expr ∥ A ∥ ∥ B ∥

NSig : Set o
NSig = List Obj

{-
data NExpr : REL Sig NSig (o ⊔ ℓ) where
  :id : NExpr ∥ A ∥ (A ∷ [])
  :λ⇒ : NExpr (:unit :⊗₀ X) (normaliseSig X)
-}

⟦_⟧Sig : Sig → Obj
⟦ ∥ A ∥   ⟧Sig = A
⟦ :unit   ⟧Sig = unit
⟦ X :⊗₀ Y ⟧Sig = ⟦ X ⟧Sig ⊗₀ ⟦ Y ⟧Sig

⟦_⟧NSig : NSig → Obj
⟦ []    ⟧NSig = unit
⟦ A ∷ X ⟧NSig = A ⊗₀ ⟦ X ⟧NSig

normaliseSig : Sig → NSig
normaliseSig ∥ A ∥     = A ∷ []
normaliseSig :unit     = []
normaliseSig (X :⊗₀ Y) = normaliseSig X ++ normaliseSig Y

private
  λ⇒ = unitorˡ.from
  λ⇐ = unitorˡ.to
  ρ⇒ = unitorʳ.from
  ρ⇐ = unitorʳ.to
  α⇒ = associator.from
  α⇐ = associator.to

⟦_⟧ : Expr X Y → ⟦ X ⟧Sig ⇒ ⟦ Y ⟧Sig
⟦ :id       ⟧ = id
⟦ e₁ :∘ e₂  ⟧ = ⟦ e₁ ⟧ ∘ ⟦ e₂ ⟧
⟦ e₁ :⊗₁ e₂ ⟧ = ⟦ e₁ ⟧ ⊗₁ ⟦ e₂ ⟧
⟦ :λ⇒       ⟧ = λ⇒
⟦ :λ⇐       ⟧ = λ⇐
⟦ :ρ⇒       ⟧ = ρ⇒
⟦ :ρ⇐       ⟧ = ρ⇐
⟦ :α⇒       ⟧ = α⇒
⟦ :α⇐       ⟧ = α⇐

⟦_⟧⁻¹ : Expr X Y → ⟦ Y ⟧Sig ⇒ ⟦ X ⟧Sig
⟦ :id       ⟧⁻¹ = id
⟦ e₁ :∘ e₂  ⟧⁻¹ = ⟦ e₂ ⟧⁻¹ ∘ ⟦ e₁ ⟧⁻¹
⟦ e₁ :⊗₁ e₂ ⟧⁻¹ = ⟦ e₁ ⟧⁻¹ ⊗₁ ⟦ e₂ ⟧⁻¹
⟦ :λ⇒       ⟧⁻¹ = λ⇐
⟦ :λ⇐       ⟧⁻¹ = λ⇒
⟦ :ρ⇒       ⟧⁻¹ = ρ⇐
⟦ :ρ⇐       ⟧⁻¹ = ρ⇒
⟦ :α⇒       ⟧⁻¹ = α⇐
⟦ :α⇐       ⟧⁻¹ = α⇒

⟦_⟧≅ : Expr X Y → ⟦ X ⟧Sig ≅ ⟦ Y ⟧Sig
⟦ :id       ⟧≅ = ≅.refl
⟦ e₁ :∘ e₂  ⟧≅ = ≅.trans ⟦ e₂ ⟧≅ ⟦ e₁ ⟧≅
⟦ e₁ :⊗₁ e₂ ⟧≅ = {!   !}
⟦ :λ⇒       ⟧≅ = {!   !}
⟦ :λ⇐       ⟧≅ = {!   !}
⟦ :ρ⇒       ⟧≅ = {!   !}
⟦ :ρ⇐       ⟧≅ = {!   !}
⟦ :α⇒       ⟧≅ = {!   !}
⟦ :α⇐       ⟧≅ = {!   !}

-- theorem : (e₁ e₂ : Expr S T) → ⟦ e₁ ⟧ ≈ ⟦ e₂ ⟧
-- lemma : Expr S T → ⟦ S ⟧Sig ≅ ⟦ T ⟧Sig
-- lemma : ⟦ normaliseSig S ⟧NSig ≅ ⟦ S ⟧Sig
-- resp : ⟦ S ⟧NSig ≅ ⟦ T ⟧NSig
-- lemma : Expr S T → normaliseSig S ≡ normaliseSig T


text:
{-# OPTIONS --without-K --exact-split --allow-unsolved-metas #-}

module 23-id-pushout where

import 22-descent
open 22-descent public

-- Section 19.1 Characterizing families of maps over pushouts

module hom-Fam-pushout
  { l1 l2 l3 l4 l5 : Level}
  { S : UU l1}
  { A : UU l2}
  { B : UU l3}
  { f : S → A}
  { g : S → B}
  ( P : Fam-pushout l4 f g)
  ( Q : Fam-pushout l5 f g)
  where

  private
    PA = pr1 P
    PB = pr1 (pr2 P)
    PS = pr2 (pr2 P)
    QA = pr1 Q
    QB = pr1 (pr2 Q)
    QS = pr2 (pr2 Q)

  {- Definition 19.1.1 -}

  hom-Fam-pushout :
    UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5)
  hom-Fam-pushout =
    Σ ( (x : A) → (PA x) → (QA x)) (λ hA →
      Σ ( (y : B) → (PB y) → (QB y)) (λ hB →
        ( s : S) →
          ( (hB (g s)) ∘ (map-equiv (PS s))) ~ ((map-equiv (QS s)) ∘ (hA (f s)))))

  {- Remark 19.1.2. We characterize the identity type of hom-Fam-pushout. -}

  htpy-hom-Fam-pushout :
    ( h k : hom-Fam-pushout) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5)
  htpy-hom-Fam-pushout h k =
    Σ ( (x : A) → (pr1 h x) ~ (pr1 k x)) (λ HA →
      Σ ( (y : B) → (pr1 (pr2 h) y) ~ (pr1 (pr2 k) y)) (λ HB →
        ( s : S) →
        ( ((HB (g s)) ·r (map-equiv (PS s))) ∙h (pr2 (pr2 k) s)) ~
        ( (pr2 (pr2 h) s) ∙h ((map-equiv (QS s)) ·l (HA (f s))))))

  reflexive-htpy-hom-Fam-pushout :
    ( h : hom-Fam-pushout) → htpy-hom-Fam-pushout h h
  reflexive-htpy-hom-Fam-pushout h =
    pair
      ( λ x → htpy-refl)
      ( pair
        ( λ y → htpy-refl)
        ( λ s → htpy-inv htpy-right-unit))

  htpy-hom-Fam-pushout-eq :
    ( h k : hom-Fam-pushout) → Id h k → htpy-hom-Fam-pushout h k
  htpy-hom-Fam-pushout-eq h .h refl =
    reflexive-htpy-hom-Fam-pushout h

  is-contr-total-htpy-hom-Fam-pushout :
    ( h : hom-Fam-pushout) →
    is-contr (Σ (hom-Fam-pushout) (htpy-hom-Fam-pushout h))
  is-contr-total-htpy-hom-Fam-pushout h =
    is-contr-total-Eq-structure
      ( λ kA kB-ke (HA : (x : A) → (pr1 h x) ~ (kA x)) →
          Σ ( (y : B) → (pr1 (pr2 h) y) ~ (pr1 kB-ke y)) (λ HB →
            ( s : S) →
              ( ((HB (g s)) ·r (map-equiv (PS s))) ∙h (pr2 kB-ke s)) ~
              ( (pr2 (pr2 h) s) ∙h ((map-equiv (QS s)) ·l (HA (f s))))))
      ( is-contr-total-Eq-Π
        ( λ x τ → (pr1 h x) ~ τ)
        ( λ x → is-contr-total-htpy (pr1 h x))
        ( pr1 h))
      ( pair (pr1 h) (λ x → htpy-refl))
      ( is-contr-total-Eq-structure
        ( λ kB ke (HB : (y : B) → (pr1 (pr2 h) y) ~ kB y) →
          (s : S) →
            ( ((HB (g s)) ·r (map-equiv (PS s))) ∙h (ke s)) ~
            ( (pr2 (pr2 h) s) ∙h ((map-equiv (QS s)) ·l htpy-refl)))
        ( is-contr-total-Eq-Π
          ( λ y τ → (pr1 (pr2 h) y) ~ τ)
          ( λ y → is-contr-total-htpy (pr1 (pr2 h) y))
          ( pr1 (pr2 h)))
        ( pair (pr1 (pr2 h)) (λ y → htpy-refl))
        ( is-contr-total-Eq-Π
          ( λ (s : S) he →
            (he ~ (pr2 (pr2 h) s ∙h (map-equiv (QS s) ·l htpy-refl))))
          ( λ s → is-contr-total-htpy'
            ((pr2 (pr2 h) s) ∙h ((map-equiv (QS s)) ·l htpy-refl)))
          ( λ s →
            ((pr2 (pr2 h) s) ∙h ((map-equiv (QS s)) ·l htpy-refl)))))

  is-equiv-htpy-hom-Fam-pushout-eq :
    ( h k : hom-Fam-pushout) → is-equiv (htpy-hom-Fam-pushout-eq h k)
  is-equiv-htpy-hom-Fam-pushout-eq h =
    fundamental-theorem-id h
      ( reflexive-htpy-hom-Fam-pushout h)
      ( is-contr-total-htpy-hom-Fam-pushout h)
      ( htpy-hom-Fam-pushout-eq h)

  eq-htpy-hom-Fam-pushout :
    ( h k : hom-Fam-pushout) → htpy-hom-Fam-pushout h k → Id h k
  eq-htpy-hom-Fam-pushout h k =
    inv-is-equiv (is-equiv-htpy-hom-Fam-pushout-eq h k)

open hom-Fam-pushout public

{- Definition 19.1.3. Given a cocone structure on X and a family of maps indexed
   by X, we obtain a morphism of descent data. -}

Naturality-fam-maps :
  { l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3}
  ( f : (a : A) → B a → C a) {x x' : A} (p : Id x x') → UU _
Naturality-fam-maps {B = B} {C} f {x} {x'} p =
  (y : B x) → Id (f x' (tr B p y)) (tr C p (f x y))

naturality-fam-maps :
  { l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3}
  ( f : (a : A) → B a → C a) {x x' : A} (p : Id x x') →
  Naturality-fam-maps f p
naturality-fam-maps f refl y = refl

hom-Fam-pushout-map :
  { l1 l2 l3 l4 l5 l6 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
  { f : S → A} {g : S → B} (c : cocone f g X) →
  ( P : X → UU l5) (Q : X → UU l6) → ((x : X) → P x → Q x) →
  hom-Fam-pushout (desc-fam c P) (desc-fam c Q)
hom-Fam-pushout-map {f = f} {g} c P Q h =
  pair
    ( precomp-Π (pr1 c) (λ x → P x → Q x) h)
    ( pair
      ( precomp-Π (pr1 (pr2 c)) (λ x → P x → Q x) h)
      ( λ s → naturality-fam-maps h (pr2 (pr2 c) s)))

{- Theorem 19.1.4. The function hom-Fam-pushout-map is an equivalence. -}

square-path-over-fam-maps :
  { l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3}
  { x x' : A} (p : Id x x') (f : B x → C x) (f' : B x' → C x') →
  Id (tr (λ a → B a → C a) p f) f' →
  ( y : B x) → Id (f' (tr B p y)) (tr C p (f y))
square-path-over-fam-maps refl f f' = htpy-eq ∘ inv

hom-Fam-pushout-dep-cocone :
  { l1 l2 l3 l4 l5 l6 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
  { f : S → A} {g : S → B} (c : cocone f g X) →
  ( P : X → UU l5) (Q : X → UU l6) →
  dep-cocone f g c (λ x → P x → Q x) →
  hom-Fam-pushout (desc-fam c P) (desc-fam c Q)
hom-Fam-pushout-dep-cocone {f = f} {g} c P Q =
  tot (λ hA → tot (λ hB →
    postcomp-Π (λ s →
      square-path-over-fam-maps (pr2 (pr2 c) s) (hA (f s)) (hB (g s)))))

is-equiv-square-path-over-fam-maps :
  { l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3}
  { x x' : A} (p : Id x x') (f : B x → C x) (f' : B x' → C x') →
  is-equiv (square-path-over-fam-maps p f f')
is-equiv-square-path-over-fam-maps refl f f' =
  is-equiv-comp' htpy-eq inv (is-equiv-inv f f') (funext f' f)

is-equiv-hom-Fam-pushout-dep-cocone :
  { l1 l2 l3 l4 l5 l6 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
  { f : S → A} {g : S → B} (c : cocone f g X) →
  ( P : X → UU l5) (Q : X → UU l6) →
  is-equiv (hom-Fam-pushout-dep-cocone c P Q)
is-equiv-hom-Fam-pushout-dep-cocone {f = f} {g} c P Q =
  is-equiv-tot-is-fiberwise-equiv (λ hA →
    is-equiv-tot-is-fiberwise-equiv (λ hB →
      is-equiv-postcomp-Π _
        ( λ s → is-equiv-square-path-over-fam-maps
          ( pr2 (pr2 c) s)
          ( hA (f s))
          ( hB (g s)))))

coherence-naturality-fam-maps :
  { l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} (P : B → UU l3) (Q : B → UU l4) →
  { f f' : A → B} (H : f ~ f') (h : (b : B) → P b → Q b) (a : A) →
  Id ( square-path-over-fam-maps (H a) (h (f a)) (h (f' a)) (apd h (H a)))
     ( naturality-fam-maps h (H a))
coherence-naturality-fam-maps {A = A} {B} P Q {f} {f'} H =
  ind-htpy f
    ( λ f' H →
      ( h : (b : B) → P b → Q b) (a : A) →
      Id ( square-path-over-fam-maps (H a) (h (f a)) (h (f' a)) (apd h (H a)))
         ( naturality-fam-maps h (H a)))
    ( λ h a → refl)
    ( H)

triangle-hom-Fam-pushout-dep-cocone :
  { l1 l2 l3 l4 l5 l6 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
  { f : S → A} {g : S → B} (c : cocone f g X) →
  ( P : X → UU l5) (Q : X → UU l6) →
  ( hom-Fam-pushout-map c P Q) ~
  ( ( hom-Fam-pushout-dep-cocone c P Q) ∘
    ( dep-cocone-map f g c (λ x → P x → Q x)))
triangle-hom-Fam-pushout-dep-cocone {f = f} {g} c P Q h =
  eq-htpy-hom-Fam-pushout
    ( desc-fam c P)
    ( desc-fam c Q)
    ( hom-Fam-pushout-map c P Q h)
    ( hom-Fam-pushout-dep-cocone c P Q
      ( dep-cocone-map f g c (λ x → P x → Q x) h))
    ( pair
      ( λ a → htpy-refl)
      ( pair
        ( λ b → htpy-refl)
        ( λ s →
          ( htpy-eq
            ( coherence-naturality-fam-maps P Q (pr2 (pr2 c)) h s)) ∙h
          ( htpy-inv htpy-right-unit))))

is-equiv-hom-Fam-pushout-map :
  { l1 l2 l3 l4 l5 l6 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
  { f : S → A} {g : S → B} (c : cocone f g X) →
  ( up-X : (l : Level) → universal-property-pushout l f g c)
  ( P : X → UU l5) (Q : X → UU l6) →
  is-equiv (hom-Fam-pushout-map c P Q)
is-equiv-hom-Fam-pushout-map {l5 = l5} {l6} {f = f} {g} c up-X P Q =
  is-equiv-comp
    ( hom-Fam-pushout-map c P Q)
    ( hom-Fam-pushout-dep-cocone c P Q)
    ( dep-cocone-map f g c (λ x → P x → Q x))
    ( triangle-hom-Fam-pushout-dep-cocone c P Q)
    ( dependent-universal-property-universal-property-pushout
      f g c up-X (l5 ⊔ l6) (λ x → P x → Q x))
    ( is-equiv-hom-Fam-pushout-dep-cocone c P Q)

equiv-hom-Fam-pushout-map :
  { l1 l2 l3 l4 l5 l6 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
  { f : S → A} {g : S → B} (c : cocone f g X) →
  ( up-X : (l : Level) → universal-property-pushout l f g c)
  ( P : X → UU l5) (Q : X → UU l6) →
  ( (x : X) → P x → Q x) ≃
  hom-Fam-pushout (desc-fam c P) (desc-fam c Q)
equiv-hom-Fam-pushout-map c up-X P Q =
  pair
    ( hom-Fam-pushout-map c P Q)
    ( is-equiv-hom-Fam-pushout-map c up-X P Q)

{- Definition 19.2.1. Universal families over spans -}

ev-pt-hom-Fam-pushout :
  { l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  { f : S → A} {g : S → B} (P : Fam-pushout l4 f g) (Q : Fam-pushout l5 f g)
  {a : A} → (pr1 P a) → (hom-Fam-pushout P Q) → pr1 Q a
ev-pt-hom-Fam-pushout P Q {a} p h = pr1 h a p

is-universal-Fam-pushout :
  { l1 l2 l3 l4 : Level} (l : Level) {S : UU l1} {A : UU l2} {B : UU l3}
  { f : S → A} {g : S → B} (P : Fam-pushout l4 f g) (a : A) (p : pr1 P a) →
  UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ lsuc l)
is-universal-Fam-pushout l {f = f} {g} P a p =
  ( Q : Fam-pushout l f g) → is-equiv (ev-pt-hom-Fam-pushout P Q p)

{- Lemma 19.2.2. The descent data of the identity type is a universal family. -}

triangle-is-universal-id-Fam-pushout' :
  { l l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
  { f : S → A} {g : S → B} (c : cocone f g X)
  (a : A) ( Q : (x : X) → UU l) →
  ( ev-refl (pr1 c a) {B = λ x p → Q x}) ~
  ( ( ev-pt-hom-Fam-pushout
      ( desc-fam c (Id (pr1 c a)))
      ( desc-fam c Q)
      ( refl)) ∘
    ( hom-Fam-pushout-map c (Id (pr1 c a)) Q))
triangle-is-universal-id-Fam-pushout' c a Q = htpy-refl

is-universal-id-Fam-pushout' :
  { l l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
  { f : S → A} {g : S → B} (c : cocone f g X)
  ( up-X : (l' : Level) → universal-property-pushout l' f g c) (a : A) →
  ( Q : (x : X) → UU l) →
  is-equiv
    ( ev-pt-hom-Fam-pushout
      ( desc-fam c (Id (pr1 c a)))
      ( desc-fam c Q)
      ( refl))
is-universal-id-Fam-pushout' c up-X a Q =
  is-equiv-left-factor
    ( ev-refl (pr1 c a) {B = λ x p → Q x})
    ( ev-pt-hom-Fam-pushout
      ( desc-fam c (Id (pr1 c a)))
      ( desc-fam c Q)
      ( refl))
    ( hom-Fam-pushout-map c (Id (pr1 c a)) Q)
    ( triangle-is-universal-id-Fam-pushout' c a Q)
    ( is-equiv-ev-refl (pr1 c a))
    ( is-equiv-hom-Fam-pushout-map c up-X (Id (pr1 c a)) Q)

is-universal-id-Fam-pushout :
  { l1 l2 l3 l4 : Level} (l : Level)
  { S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
  { f : S → A} {g : S → B} (c : cocone f g X)
  ( up-X : (l' : Level) → universal-property-pushout l' f g c) (a : A) →
  is-universal-Fam-pushout l (desc-fam c (Id (pr1 c a))) a refl
is-universal-id-Fam-pushout l {S = S} {A} {B} {X} {f} {g} c up-X a Q =
  inv-map-equiv
    ( precomp-Π-equiv
      ( equiv-desc-fam c up-X)
      ( λ (Q : Fam-pushout l f g) →
        is-equiv (ev-pt-hom-Fam-pushout
          ( desc-fam c (Id (pr1 c a))) Q refl)))
    ( is-universal-id-Fam-pushout' c up-X a)
    ( Q)

{- We construct the identity morphism and composition, and we show that
   morphisms equipped with two-sided inverses are equivalences. -}

id-hom-Fam-pushout :
  { l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  { f : S → A} {g : S → B} →
  ( P : Fam-pushout l4 f g) → hom-Fam-pushout P P
id-hom-Fam-pushout P =
  pair
    ( λ a → id)
    ( pair
      ( λ b → id)
      ( λ s → htpy-refl))

comp-hom-Fam-pushout :
  { l1 l2 l3 l4 l5 l6 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  { f : S → A} {g : S → B} →
  ( P : Fam-pushout l4 f g) (Q : Fam-pushout l5 f g) (R : Fam-pushout l6 f g) →
  hom-Fam-pushout Q R → hom-Fam-pushout P Q → hom-Fam-pushout P R
comp-hom-Fam-pushout {f = f} {g} P Q R k h =
  pair
    ( λ a → (pr1 k a) ∘ (pr1 h a))
    ( pair
      ( λ b → (pr1 (pr2 k) b) ∘ (pr1 (pr2 h) b))
      ( λ s → coherence-square-comp-horizontal
        ( pr1 h (f s))
        ( pr1 k (f s))
        ( map-equiv (pr2 (pr2 P) s))
        ( map-equiv (pr2 (pr2 Q) s))
        ( map-equiv (pr2 (pr2 R) s))
        ( pr1 (pr2 h) (g s))
        ( pr1 (pr2 k) (g s))
        ( pr2 (pr2 h) s)
        ( pr2 (pr2 k) s)))

has-inverse-hom-Fam-pushout :
  { l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  { f : S → A} {g : S → B} →
  ( P : Fam-pushout l4 f g) (Q : Fam-pushout l5 f g) (h : hom-Fam-pushout P Q) →
  UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5)
has-inverse-hom-Fam-pushout P Q h =
  Σ ( hom-Fam-pushout Q P) (λ k →
    ( htpy-hom-Fam-pushout Q Q
      ( comp-hom-Fam-pushout Q P Q h k)
      ( id-hom-Fam-pushout Q)) ×
    ( htpy-hom-Fam-pushout P P
      ( comp-hom-Fam-pushout P Q P k h)
      ( id-hom-Fam-pushout P)))

is-equiv-hom-Fam-pushout :
  { l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  { f : S → A} {g : S → B} (P : Fam-pushout l4 f g) (Q : Fam-pushout l5 f g) →
  hom-Fam-pushout P Q → UU (l2 ⊔ l3 ⊔ l4 ⊔ l5)
is-equiv-hom-Fam-pushout {A = A} {B} {f} {g} P Q h =
  ((a : A) → is-equiv (pr1 h a)) × ((b : B) → is-equiv (pr1 (pr2 h) b))

is-equiv-has-inverse-hom-Fam-pushout :
  { l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  { f : S → A} {g : S → B} →
  ( P : Fam-pushout l4 f g) (Q : Fam-pushout l5 f g) (h : hom-Fam-pushout P Q) →
  has-inverse-hom-Fam-pushout P Q h → is-equiv-hom-Fam-pushout P Q h
is-equiv-has-inverse-hom-Fam-pushout P Q h has-inv-h =
  pair
    ( λ a →
      is-equiv-has-inverse
        ( pr1 (pr1 has-inv-h) a)
        ( pr1 (pr1 (pr2 has-inv-h)) a)
        ( pr1 (pr2 (pr2 has-inv-h)) a))
    ( λ b →
      is-equiv-has-inverse
        ( pr1 (pr2 (pr1 has-inv-h)) b)
        ( pr1 (pr2 (pr1 (pr2 has-inv-h))) b)
        ( pr1 (pr2 (pr2 (pr2 has-inv-h))) b))

equiv-is-equiv-hom-Fam-pushout :
  { l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  { f : S → A} {g : S → B} (P : Fam-pushout l4 f g) (Q : Fam-pushout l5 f g) →
  ( h : hom-Fam-pushout P Q) →
  is-equiv-hom-Fam-pushout P Q h → equiv-Fam-pushout P Q
equiv-is-equiv-hom-Fam-pushout P Q h is-equiv-h =
  pair
    ( λ a → pair (pr1 h a) (pr1 is-equiv-h a))
    ( pair
      ( λ b → pair (pr1 (pr2 h) b) (pr2 is-equiv-h b))
      ( pr2 (pr2 h)))

{- Theorem 19.1.3. Characterization of identity types of pushouts. -}

hom-identity-is-universal-Fam-pushout :
  { l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l5}
  { f : S → A} {g : S → B} (c : cocone f g X) →
  ( up-X : (l : Level) → universal-property-pushout l f g c) →
  ( P : Fam-pushout l4 f g) (a : A) (p : pr1 P a) →
  is-universal-Fam-pushout l5 P a p →
  Σ ( hom-Fam-pushout P (desc-fam c (Id (pr1 c a))))
    ( λ h → Id (pr1 h a p) refl)
hom-identity-is-universal-Fam-pushout {f = f} {g} c up-X P a p is-univ-P =
  {!!}

is-identity-is-universal-Fam-pushout :
  { l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l5}
  { f : S → A} {g : S → B} (c : cocone f g X) →
  ( up-X : (l : Level) → universal-property-pushout l f g c) →
  ( P : Fam-pushout l4 f g) (a : A) (p : pr1 P a) →
  is-universal-Fam-pushout l5 P a p →
  Σ ( equiv-Fam-pushout P (desc-fam c (Id (pr1 c a))))
    ( λ e → Id (map-equiv (pr1 e a) p) refl)
is-identity-is-universal-Fam-pushout {f = f} {g} c up-X a P p₀ is-eq-P = {!!}

max_stars_repo_name: tmoux/HoTT-Intro

max_issues_repo_name: tmoux/HoTT-Intro

max_forks_repo_name: tmoux/HoTT-Intro


text:
-- In Agda 2.5.3 the error was:

-- μ₂ is not strictly positive, because it occurs
-- in the third argument to ⟦_⟧
-- in the type of the constructor fix
-- in the definition of μ₂.

open import Data.Nat using (ℕ;zero;suc)
open import Data.Fin using (Fin;zero;suc)
open import Data.Vec
open import Data.Empty
open import Data.Product
open import Data.Sum
open import Data.Unit

Σ# : {n : ℕ} -> (Fin n -> Set) -> Set
Σ# {zero} f = ⊥
Σ# {suc zero} f = f zero
Σ# {suc n} f = f zero ⊎ Σ# {n} λ i -> f (suc i)

module Matrices {Ix : Set} {Σ : (Ix -> Set) -> Set} where

  Matrix : Set1
  Matrix = (i j : Ix) -> Set

  _<+>_ : Matrix -> Matrix -> Matrix
  m <+> n = λ i j -> m i j ⊎ n i j
  {-# INLINE _<+>_ #-}

  _<*>_ : Matrix -> Matrix -> Matrix
  m <*> n = λ i j -> Σ λ k -> m i k × n k j
  {-# INLINE _<*>_ #-}

data Poly {Coeffs : Set1} : Set1 where
  0p 1p : Poly
  X : Poly
  _+_ _*_ : (D1 D2 : Poly {Coeffs}) -> Poly {Coeffs}
  K : Coeffs -> Poly

module Dim {n : ℕ} where
  open Matrices {Fin n} {Σ#}

  ⟦_⟧ : Poly {Vec (Vec Set n) n} -> Matrix -> Matrix
  ⟦ 0p ⟧ x i j = ⊥
  ⟦ 1p ⟧ x i j = ⊤
  ⟦ X ⟧ x i j = x i j
  ⟦ D1 + D2 ⟧ x i j = (⟦ D1 ⟧ x <+> ⟦ D2 ⟧ x) i j
  ⟦ D1 * D2 ⟧ x i j = (⟦ D1 ⟧ x <*> ⟦ D2 ⟧ x) i j
  ⟦ K S ⟧ x i j = lookup (lookup S i) j

  ⟪_⟫ : Poly {Set} -> Set → Set
  ⟪ 0p ⟫ x = ⊥
  ⟪ 1p ⟫ x = ⊤
  ⟪ X ⟫ x = x
  ⟪ D1 + D2 ⟫ x = (⟪ D1 ⟫ x ⊎ ⟪ D2 ⟫ x)
  ⟪ D1 * D2 ⟫ x = (⟪ D1 ⟫ x × ⟪ D2 ⟫ x)
  ⟪ K S ⟫ x = S

  data μ₁ (p : Poly) : Set where
    fix : ⟪ p ⟫ (μ₁ p) -> μ₁ p

  data μ₂ (p : Poly) (i j : Fin n) : Set where
    fix : ⟦ p ⟧ (μ₂ p) i j -> μ₂ p i j

max_stars_repo_name: jappeace/agda

max_issues_repo_name: jappeace/agda

max_forks_repo_name: jappeace/agda


text:
{-# OPTIONS --without-K #-}
module hott.level.core where

open import level
open import sum
open import sets.nat.core
open import equality.core
open import equality.groupoid

h : ∀ {i} → ℕ → Set i → Set i
h 0 X = Σ X λ x → (x' : X) → x ≡ x'
h (suc n) X = (x x' : X) →  h n (x ≡ x')

contr : ∀ {i} → Set i → Set i
contr = h 0

prop : ∀ {i} → Set i → Set i
prop X = (x x' : X) → x ≡ x'

h1⇒prop : ∀ {i} {X : Set i} → h 1 X → prop X
h1⇒prop h1 x x' = proj₁ (h1 x x')

prop⇒h1 : ∀ {i} {X : Set i} → prop X → h 1 X
prop⇒h1 {X = X} f x y = p₀ x y , lem x y
  where
    p₀ : (x y : X) → x ≡ y
    p₀ x y = f x y · (f y y)⁻¹

    lem : (x y : X)(p : x ≡ y) → p₀ x y ≡ p
    lem x .x refl = left-inverse (f x x)

contr⇒prop : ∀ {i} {X : Set i} → contr X → prop X
contr⇒prop (x , p) = λ x' x'' → sym (p x') · p x''

h↑ : ∀ {i n}{X : Set i} → h n X → h (suc n) X
h↑ {n = 0} c = prop⇒h1 (contr⇒prop c)
h↑ {n = suc n} hn = λ x x' → h↑ (hn x x')

-- Prop: the set of propositions
HProp : ∀ i → Set (lsuc i)
HProp i = Σ (Set i) (h 1)

-- HSet : sets
HSet : ∀ i → Set (lsuc i)
HSet i = Σ (Set i) (h 2)

-- Types by h-level (shifted by 2)
Type : ∀ i → ℕ → Set (lsuc i)
Type i n = Σ (Set i) (h (suc (suc n)))

_⁻¹_ : ∀ {i k} {X : Set i} {Y : Set k} → (X → Y) → Y → Set (i ⊔ k)
f ⁻¹ y = Σ _ λ x → f x ≡ y

-- singletons are contractible
singl-contr : ∀ {i} {A : Set i} → (x : A) → contr (singleton x)
singl-contr {A = A} x = (x , refl) , λ { (x' , p) → lem x' p }
  where
    lem : (x' : A)(p : x ≡ x') → (x , refl) ≡ (x' , p)
    lem .x refl = refl

singl-contr' : ∀ {i} {A : Set i} → (x : A) → contr (singleton' x)
singl-contr' {A = A} x = (x , refl) , λ { (x' , p) → lem x' p }
  where
    lem : (x' : A)(p : x' ≡ x) → (x , refl) ≡ (x' , p)
    lem .x refl = refl

max_stars_repo_name: HoTT/M-types

max_issues_repo_name: HoTT/M-types

max_forks_repo_name: HoTT/M-types


text:
{-# OPTIONS --allow-unsolved-metas #-}
open import Level
open import Ordinals
module OD {n : Level } (O : Ordinals {n} ) where

open import zf
open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ )
open import  Relation.Binary.PropositionalEquality hiding ( [_] )
open import Data.Nat.Properties
open import Data.Empty
open import Relation.Nullary
open import Relation.Binary  hiding (_⇔_)
open import Relation.Binary.Core hiding (_⇔_)

open import logic
import OrdUtil
open import nat

open Ordinals.Ordinals  O
open Ordinals.IsOrdinals isOrdinal
open Ordinals.IsNext isNext
open OrdUtil O

-- Ordinal Definable Set

record OD : Set (suc n ) where
  field
    def : (x : Ordinal  ) → Set n

open OD

open _∧_
open _∨_
open Bool

record _==_  ( a b :  OD  ) : Set n where
  field
     eq→ : ∀ { x : Ordinal  } → def a x → def b x
     eq← : ∀ { x : Ordinal  } → def b x → def a x

==-refl :  {  x :  OD  } → x == x
==-refl  {x} = record { eq→ = λ x → x ; eq← = λ x → x }

open  _==_

==-trans : { x y z : OD } →  x == y →  y == z →  x ==  z
==-trans x=y y=z  = record { eq→ = λ {m} t → eq→ y=z (eq→ x=y t) ; eq← =  λ {m} t → eq← x=y (eq← y=z t) }

==-sym : { x y  : OD } →  x == y →  y == x
==-sym x=y = record { eq→ = λ {m} t → eq← x=y t ; eq← =  λ {m} t → eq→ x=y t }

⇔→== :  {  x y :  OD  } → ( {z : Ordinal } → (def x z ⇔  def y z)) → x == y
eq→ ( ⇔→==  {x} {y}  eq ) {z} m = proj1 eq m
eq← ( ⇔→==  {x} {y}  eq ) {z} m = proj2 eq m

-- next assumptions are our axiom
--
--  OD is an equation on Ordinals, so it contains Ordinals. If these Ordinals have one-to-one
--  correspondence to the OD then the OD looks like a ZF Set.
--
--  If all ZF Set have supreme upper bound, the solutions of OD have to be bounded, i.e.
--  bbounded ODs are ZF Set. Unbounded ODs are classes.
--
--  In classical Set Theory, HOD is used, as a subset of OD,
--     HOD = { x | TC x ⊆ OD }
--  where TC x is a transitive clusure of x, i.e. Union of all elemnts of all subset of x.
--  This is not possible because we don't have V yet. So we assumes HODs are bounded OD.
--
--  We also assumes HODs are isomorphic to Ordinals, which is ususally proved by Goedel number tricks.
--  There two contraints on the HOD order, one is ∋, the other one is ⊂.
--  ODs have an ovbious maximum, but Ordinals are not, but HOD has no maximum because there is an aribtrary
--  bound on each HOD.
--
--  In classical Set Theory, sup is defined by Uion, since we are working on constructive logic,
--  we need explict assumption on sup.
--
--  ==→o≡ is necessary to prove axiom of extensionality.

-- Ordinals in OD , the maximum
Ords : OD
Ords = record { def = λ x → One }

record HOD : Set (suc n) where
  field
    od : OD
    odmax : Ordinal
    <odmax : {y : Ordinal} → def od y → y o< odmax

open HOD

record ODAxiom : Set (suc n) where
 field
  -- HOD is isomorphic to Ordinal (by means of Goedel number)
  & : HOD  → Ordinal
  * : Ordinal  → HOD
  c<→o<  :  {x y : HOD  }   → def (od y) ( & x ) → & x o< & y
  ⊆→o≤   :  {y z : HOD  }   → ({x : Ordinal} → def (od y) x → def (od z) x ) → & y o< osuc (& z)
  *iso   :  {x : HOD }      → * ( & x ) ≡ x
  &iso   :  {x : Ordinal }  → & ( * x ) ≡ x
  ==→o≡  :  {x y : HOD  }   → (od x == od y) → x ≡ y
  sup-o  :  (A : HOD) → (     ( x : Ordinal ) → def (od A) x →  Ordinal ) →  Ordinal
  sup-o< :  (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x →  Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o<  sup-o A ψ
-- possible order restriction
  ho< : {x : HOD} → & x o< next (odmax x)

postulate  odAxiom : ODAxiom
open ODAxiom odAxiom

-- odmax minimality
--
-- since we have ==→o≡ , so odmax have to be unique. We should have odmaxmin in HOD.
-- We can calculate the minimum using sup but it is tedius.
-- Only Select has non minimum odmax.
-- We have the same problem on 'def' itself, but we leave it.

odmaxmin : Set (suc n)
odmaxmin = (y : HOD) (z : Ordinal) → ((x : Ordinal)→ def (od y) x → x o< z) → odmax y o< osuc z

-- OD ⇔ Ordinal leads a contradiction, so we need bounded HOD
¬OD-order : ( & : OD  → Ordinal ) → ( * : Ordinal  → OD ) → ( { x y : OD  }  → def y ( & x ) → & x o< & y) → ⊥
¬OD-order & * c<→o< = osuc-< <-osuc (c<→o< {Ords} OneObj )

-- Open supreme upper bound leads a contradition, so we use domain restriction on sup
¬open-sup : ( sup-o : (Ordinal →  Ordinal ) → Ordinal) → ((ψ : Ordinal →  Ordinal ) → (x : Ordinal) → ψ x  o<  sup-o ψ ) → ⊥
¬open-sup sup-o sup-o< = o<> <-osuc (sup-o< next-ord (sup-o next-ord)) where
   next-ord : Ordinal → Ordinal
   next-ord x = osuc x

-- Ordinal in OD ( and ZFSet ) Transitive Set
Ord : ( a : Ordinal  ) → HOD
Ord  a = record { od = record { def = λ y → y o< a } ; odmax = a ; <odmax = lemma } where
   lemma :  {x : Ordinal} → x o< a → x o< a
   lemma {x} lt = lt

od∅ : HOD
od∅  = Ord o∅

odef : HOD → Ordinal → Set n
odef A x = def ( od A ) x

_∋_ : ( a x : HOD  ) → Set n
_∋_  a x  = odef a ( & x )

-- _c<_ : ( x a : HOD  ) → Set n
-- x c< a = a ∋ x

d→∋ : ( a : HOD  ) { x : Ordinal} → odef a x → a ∋ (* x)
d→∋ a lt = subst (λ k → odef a k ) (sym &iso) lt

-- odef-subst :  {Z : HOD } {X : Ordinal  }{z : HOD } {x : Ordinal  }→ odef Z X → Z ≡ z  →  X ≡ x  →  odef z x
-- odef-subst df refl refl = df

otrans : {a x y : Ordinal  } → odef (Ord a) x → odef (Ord x) y → odef (Ord a) y
otrans x<a y<x = ordtrans y<x x<a

-- If we have reverse of c<→o<, everything becomes Ordinal
∈→c<→HOD=Ord : ( o<→c< : {x y : Ordinal  } → x o< y → odef (* y) x ) → {x : HOD } →  x ≡ Ord (& x)
∈→c<→HOD=Ord o<→c< {x} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
   lemma1 : {y : Ordinal} → odef x y → odef (Ord (& x)) y
   lemma1 {y} lt = subst ( λ k → k o< & x ) &iso (c<→o< {* y} {x} (d→∋ x lt))
   lemma2 : {y : Ordinal} → odef (Ord (& x)) y → odef x y
   lemma2 {y} lt = subst (λ k → odef k y ) *iso (o<→c< {y} {& x} lt )

-- avoiding lv != Zero error
orefl : { x : HOD  } → { y : Ordinal  } → & x ≡ y → & x ≡ y
orefl refl = refl

==-iso : { x y : HOD  } → od (* (& x)) == od (* (& y))  →  od x == od y
==-iso  {x} {y} eq = record {
      eq→ = λ {z} d →  lemma ( eq→  eq (subst (λ k → odef k z ) (sym *iso) d )) ;
      eq← = λ {z} d →  lemma ( eq←  eq (subst (λ k → odef k z ) (sym *iso) d )) }
        where
           lemma : {x : HOD  } {z : Ordinal } → odef (* (& x)) z → odef x z
           lemma {x} {z} d = subst (λ k → odef k z) (*iso) d

=-iso :  {x y : HOD  } → (od x == od y) ≡ (od (* (& x)) == od y)
=-iso  {_} {y} = cong ( λ k → od k == od y ) (sym *iso)

ord→== : { x y : HOD  } → & x ≡  & y →  od x == od y
ord→==  {x} {y} eq = ==-iso (lemma (& x) (& y) (orefl eq)) where
   lemma : ( ox oy : Ordinal  ) → ox ≡ oy →  od (* ox) == od (* oy)
   lemma ox ox  refl = ==-refl

o≡→== : { x y : Ordinal  } → x ≡  y →  od (* x) == od (* y)
o≡→==  {x} {.x} refl = ==-refl

o∅≡od∅ : * (o∅ ) ≡ od∅
o∅≡od∅  = ==→o≡ lemma where
     lemma0 :  {x : Ordinal} → odef (* o∅) x → odef od∅ x
     lemma0 {x} lt with c<→o< {* x} {* o∅} (subst (λ k → odef (* o∅) k ) (sym &iso) lt)
     ... | t = subst₂ (λ j k → j o< k ) &iso &iso t
     lemma1 :  {x : Ordinal} → odef od∅ x → odef (* o∅) x
     lemma1 {x} lt = ⊥-elim (¬x<0 lt)
     lemma : od (* o∅) == od od∅
     lemma = record { eq→ = lemma0 ; eq← = lemma1 }

ord-od∅ : & (od∅ ) ≡ o∅
ord-od∅  = sym ( subst (λ k → k ≡  & (od∅ ) ) &iso (cong ( λ k → & k ) o∅≡od∅ ) )

≡o∅→=od∅  : {x : HOD} → & x ≡ o∅ → od x == od od∅
≡o∅→=od∅ {x} eq = record { eq→ = λ {y} lt → ⊥-elim ( ¬x<0 {y} (subst₂ (λ j k → j o< k ) &iso eq ( c<→o< {* y} {x} (d→∋ x lt))))
    ; eq← = λ {y} lt → ⊥-elim ( ¬x<0 lt )}

=od∅→≡o∅  : {x : HOD} → od x == od od∅ → & x ≡ o∅
=od∅→≡o∅ {x} eq = trans (cong (λ k → & k ) (==→o≡ {x} {od∅} eq)) ord-od∅

∅0 : record { def = λ x →  Lift n ⊥ } == od od∅
eq→ ∅0 {w} (lift ())
eq← ∅0 {w} lt = lift (¬x<0 lt)

∅< : { x y : HOD  } → odef x (& y ) → ¬ (  od x  == od od∅  )
∅<  {x} {y} d eq with eq→ (==-trans eq (==-sym ∅0) ) d
∅<  {x} {y} d eq | lift ()

∅6 : { x : HOD  }  → ¬ ( x ∋ x )    --  no Russel paradox
∅6  {x} x∋x = o<¬≡ refl ( c<→o<  {x} {x} x∋x )

odef-iso : {A B : HOD } {x y : Ordinal } → x ≡ y  → (odef A y → odef B y)  → odef A x → odef B x
odef-iso refl t = t

is-o∅ : ( x : Ordinal  ) → Dec ( x ≡ o∅  )
is-o∅ x with trio< x o∅
is-o∅ x | tri< a ¬b ¬c = no ¬b
is-o∅ x | tri≈ ¬a b ¬c = yes b
is-o∅ x | tri> ¬a ¬b c = no ¬b

-- the pair
_,_ : HOD  → HOD  → HOD
x , y = record { od = record { def = λ t → (t ≡ & x ) ∨ ( t ≡ & y ) } ; odmax = omax (& x)  (& y) ; <odmax = lemma }  where
    lemma : {t : Ordinal} → (t ≡ & x) ∨ (t ≡ & y) → t o< omax (& x) (& y)
    lemma {t} (case1 refl) = omax-x  _ _
    lemma {t} (case2 refl) = omax-y  _ _

pair<y : {x y : HOD } → y ∋ x  → & (x , x) o< osuc (& y)
pair<y {x} {y} y∋x = ⊆→o≤ lemma where
   lemma : {z : Ordinal} → def (od (x , x)) z → def (od y) z
   lemma (case1 refl) = y∋x
   lemma (case2 refl) = y∋x

-- another possible restriction. We reqest no minimality on odmax, so it may arbitrary larger.
odmax<&  : { x y : HOD } → x ∋ y →  Set n
odmax<& {x} {y} x∋y = odmax x o< & x

in-codomain : (X : HOD  ) → ( ψ : HOD  → HOD  ) → OD
in-codomain  X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( odef X y ∧  ( x ≡ & (ψ (* y )))))  }

_∩_ : ( A B : HOD ) → HOD
A ∩ B = record { od = record { def = λ x → odef A x ∧ odef B x }
        ; odmax = omin (odmax A) (odmax B) ; <odmax = λ y → min1 (<odmax A (proj1 y)) (<odmax B (proj2 y))}

record _⊆_ ( A B : HOD   ) : Set (suc n) where
  field
     incl : { x : HOD } → A ∋ x →  B ∋ x

open _⊆_
infixr  220 _⊆_

-- if we have & (x , x) ≡ osuc (& x),  ⊆→o≤ → c<→o<
⊆→o≤→c<→o< : ({x : HOD} → & (x , x) ≡ osuc (& x) )
   →  ({y z : HOD  }   → ({x : Ordinal} → def (od y) x → def (od z) x ) → & y o< osuc (& z) )
   →   {x y : HOD  }   → def (od y) ( & x ) → & x o< & y
⊆→o≤→c<→o< peq ⊆→o≤ {x} {y} y∋x with trio< (& x) (& y)
⊆→o≤→c<→o< peq ⊆→o≤ {x} {y} y∋x | tri< a ¬b ¬c = a
⊆→o≤→c<→o< peq ⊆→o≤ {x} {y} y∋x | tri≈ ¬a b ¬c = ⊥-elim ( o<¬≡ (peq {x}) (pair<y (subst (λ k → k ∋ x) (sym ( ==→o≡ {x} {y} (ord→== b))) y∋x )))
⊆→o≤→c<→o< peq ⊆→o≤ {x} {y} y∋x | tri> ¬a ¬b c =
  ⊥-elim ( o<> (⊆→o≤ {x , x} {y} y⊆x,x ) lemma1 ) where
    lemma : {z : Ordinal} → (z ≡ & x) ∨ (z ≡ & x) → & x ≡ z
    lemma (case1 refl) = refl
    lemma (case2 refl) = refl
    y⊆x,x : {z : Ordinal} → def (od (x , x)) z → def (od y) z
    y⊆x,x {z} lt = subst (λ k → def (od y) k ) (lemma lt) y∋x
    lemma1 : osuc (& y) o< & (x , x)
    lemma1 = subst (λ k → osuc (& y) o< k ) (sym (peq {x})) (osucc c )

ε-induction : { ψ : HOD  → Set (suc n)}
   → ( {x : HOD } → ({ y : HOD } →  x ∋ y → ψ y ) → ψ x )
   → (x : HOD ) → ψ x
ε-induction {ψ} ind x = subst (λ k → ψ k ) *iso (ε-induction-ord (osuc (& x)) <-osuc )  where
     induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (* oy)) → ψ (* ox)
     induction ox prev = ind  ( λ {y} lt → subst (λ k → ψ k ) *iso (prev (& y) (o<-subst (c<→o< lt) refl &iso )))
     ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (* oy)
     ε-induction-ord ox {oy} lt = TransFinite {λ oy → ψ (* oy)} induction oy

Select : (X : HOD  ) → ((x : HOD  ) → Set n ) → HOD
Select X ψ = record { od = record { def = λ x →  ( odef X x ∧ ψ ( * x )) } ; odmax = odmax X ; <odmax = λ y → <odmax X (proj1 y) }

Replace : HOD  → (HOD  → HOD) → HOD
Replace X ψ = record { od = record { def = λ x → (x o< sup-o X (λ y X∋y → & (ψ (* y)))) ∧ def (in-codomain X ψ) x }
    ; odmax = rmax ; <odmax = rmax<} where
        rmax : Ordinal
        rmax = sup-o X (λ y X∋y → & (ψ (* y)))
        rmax< :  {y : Ordinal} → (y o< rmax) ∧ def (in-codomain X ψ) y → y o< rmax
        rmax< lt = proj1 lt

--
-- If we have LEM, Replace' is equivalent to Replace
--
in-codomain' : (X : HOD  ) → ((x : HOD) → X ∋ x → HOD) → OD
in-codomain'  X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( odef X y ∧  ((lt : odef X y) →  x ≡ & (ψ (* y ) (d→∋ X lt) ))))  }
Replace' : (X : HOD)  → ((x : HOD) → X ∋ x → HOD) → HOD
Replace' X ψ = record { od = record { def = λ x → (x o< sup-o X (λ y X∋y → & (ψ (* y) (d→∋ X X∋y) ))) ∧ def (in-codomain' X ψ) x }
      ; odmax = rmax ; <odmax = rmax< } where
        rmax : Ordinal
        rmax = sup-o X (λ y X∋y → & (ψ (* y) (d→∋ X X∋y)))
        rmax< :  {y : Ordinal} → (y o< rmax) ∧ def (in-codomain' X ψ) y → y o< rmax
        rmax< lt = proj1 lt

Union : HOD  → HOD
Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (* u) x)))  }
    ; odmax = osuc (& U) ; <odmax = umax< } where
        umax< :  {y : Ordinal} → ¬ ((u : Ordinal) → ¬ def (od U) u ∧ def (od (* u)) y) → y o< osuc (& U)
        umax< {y} not = lemma (FExists _ lemma1 not ) where
            lemma0 : {x : Ordinal} → def (od (* x)) y → y o< x
            lemma0 {x} x<y = subst₂ (λ j k → j o< k ) &iso  &iso (c<→o< (d→∋ (* x) x<y ))
            lemma2 : {x : Ordinal} → def (od U) x → x o< & U
            lemma2 {x} x<U = subst (λ k → k o< & U ) &iso (c<→o< (d→∋ U x<U))
            lemma1 : {x : Ordinal} → def (od U) x ∧ def (od (* x)) y → ¬ (& U o< y)
            lemma1 {x} lt u<y = o<> u<y (ordtrans (lemma0 (proj2 lt)) (lemma2 (proj1 lt)) )
            lemma : ¬ ((& U) o< y ) → y o< osuc (& U)
            lemma not with trio< y (& U)
            lemma not | tri< a ¬b ¬c = ordtrans a <-osuc
            lemma not | tri≈ ¬a refl ¬c = <-osuc
            lemma not | tri> ¬a ¬b c = ⊥-elim (not c)
_∈_ : ( A B : HOD  ) → Set n
A ∈ B = B ∋ A

OPwr :  (A :  HOD ) → HOD
OPwr  A = Ord ( sup-o (Ord (osuc (& A))) ( λ x A∋x → & ( A ∩ (* x)) ) )

Power : HOD  → HOD
Power A = Replace (OPwr (Ord (& A))) ( λ x → A ∩ x )
-- ｛_｝ : ZFSet → ZFSet
-- ｛ x ｝ = ( x ,  x )     -- better to use (x , x) directly

union→ :  (X z u : HOD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
union→ X z u xx not = ⊥-elim ( not (& u) ( ⟪ proj1 xx
    , subst ( λ k → odef k (& z)) (sym *iso) (proj2 xx) ⟫ ))
union← :  (X z : HOD) (X∋z : Union X ∋ z) →  ¬  ( (u : HOD ) → ¬ ((X ∋  u) ∧ (u ∋ z )))
union← X z UX∋z =  FExists _ lemma UX∋z where
    lemma : {y : Ordinal} → odef X y ∧ odef (* y) (& z) → ¬ ((u : HOD) → ¬ (X ∋ u) ∧ (u ∋ z))
    lemma {y} xx not = not (* y) ⟪ d→∋ X (proj1 xx) , proj2 xx ⟫

data infinite-d  : ( x : Ordinal  ) → Set n where
    iφ :  infinite-d o∅
    isuc : {x : Ordinal  } →   infinite-d  x  →
            infinite-d  (& ( Union (* x , (* x , * x ) ) ))

-- ω can be diverged in our case, since we have no restriction on the corresponding ordinal of a pair.
-- We simply assumes infinite-d y has a maximum.
--
-- This means that many of OD may not be HODs because of the & mapping divergence.
-- We should have some axioms to prevent this such as & x o< next (odmax x).
--
-- postulate
--     ωmax : Ordinal
--     <ωmax : {y : Ordinal} → infinite-d y → y o< ωmax
--
-- infinite : HOD
-- infinite = record { od = record { def = λ x → infinite-d x } ; odmax = ωmax ; <odmax = <ωmax }

infinite : HOD
infinite = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma }  where
    u : (y : Ordinal ) → HOD
    u y = Union (* y , (* y , * y))
    --   next< : {x y z : Ordinal} → x o< next z  → y o< next x → y o< next z
    lemma8 : {y : Ordinal} → & (* y , * y) o< next (odmax (* y , * y))
    lemma8 = ho<
    ---           (x,y) < next (omax x y) < next (osuc y) = next y
    lemmaa : {x y : HOD} → & x o< & y → & (x , y) o< next (& y)
    lemmaa {x} {y} x<y = subst (λ k → & (x , y) o< k ) (sym nexto≡) (subst (λ k → & (x , y) o< next k ) (sym (omax< _ _ x<y)) ho< )
    lemma81 : {y : Ordinal} → & (* y , * y) o< next (& (* y))
    lemma81 {y} = nexto=n (subst (λ k →  & (* y , * y) o< k ) (cong (λ k → next k) (omxx _)) lemma8)
    lemma9 : {y : Ordinal} → & (* y , (* y , * y)) o< next (& (* y , * y))
    lemma9 = lemmaa (c<→o< (case1 refl))
    lemma71 : {y : Ordinal} → & (* y , (* y , * y)) o< next (& (* y))
    lemma71 = next< lemma81 lemma9
    lemma1 : {y : Ordinal} → & (u y) o< next (osuc (& (* y , (* y , * y))))
    lemma1 = ho<
    --- main recursion
    lemma : {y : Ordinal} → infinite-d y → y o< next o∅
    lemma {o∅} iφ = x<nx
    lemma (isuc {y} x) = next< (lemma x) (next< (subst (λ k → & (* y , (* y , * y)) o< next k) &iso lemma71 ) (nexto=n lemma1))

empty : (x : HOD  ) → ¬  (od∅ ∋ x)
empty x = ¬x<0

_=h=_ : (x y : HOD) → Set n
x =h= y  = od x == od y

pair→ : ( x y t : HOD  ) →  (x , y)  ∋ t  → ( t =h= x ) ∨ ( t =h= y )
pair→ x y t (case1 t≡x ) = case1 (subst₂ (λ j k → j =h= k ) *iso *iso (o≡→== t≡x ))
pair→ x y t (case2 t≡y ) = case2 (subst₂ (λ j k → j =h= k ) *iso *iso (o≡→== t≡y ))

pair← : ( x y t : HOD  ) → ( t =h= x ) ∨ ( t =h= y ) →  (x , y)  ∋ t
pair← x y t (case1 t=h=x) = case1 (cong (λ k → & k ) (==→o≡ t=h=x))
pair← x y t (case2 t=h=y) = case2 (cong (λ k → & k ) (==→o≡ t=h=y))

o<→c< :  {x y : Ordinal } → x o< y → (Ord x) ⊆ (Ord y)
o<→c< lt = record { incl = λ z → ordtrans z lt }

⊆→o< :  {x y : Ordinal } → (Ord x) ⊆ (Ord y) →  x o< osuc y
⊆→o< {x} {y}  lt with trio< x y
⊆→o< {x} {y}  lt | tri< a ¬b ¬c = ordtrans a <-osuc
⊆→o< {x} {y}  lt | tri≈ ¬a b ¬c = subst ( λ k → k o< osuc y) (sym b) <-osuc
⊆→o< {x} {y}  lt | tri> ¬a ¬b c with (incl lt)  (o<-subst c (sym &iso) refl )
... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt &iso refl ))

ψiso :  {ψ : HOD  → Set n} {x y : HOD } → ψ x → x ≡ y   → ψ y
ψiso {ψ} t refl = t
selection : {ψ : HOD → Set n} {X y : HOD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y)
selection {ψ} {X} {y} = ⟪
     ( λ cond → ⟪ proj1 cond , ψiso {ψ} (proj2 cond) (sym *iso)  ⟫ )
  ,  ( λ select → ⟪ proj1 select  , ψiso {ψ} (proj2 select) *iso  ⟫ )
  ⟫

selection-in-domain : {ψ : HOD → Set n} {X y : HOD} → Select X ψ ∋ y → X ∋ y
selection-in-domain {ψ} {X} {y} lt = proj1 ((proj2 (selection {ψ} {X} )) lt)

sup-c< :  (ψ : HOD → HOD) → {X x : HOD} → X ∋ x  → & (ψ x) o< (sup-o X (λ y X∋y → & (ψ (* y))))
sup-c< ψ {X} {x} lt = subst (λ k → & (ψ k) o< _ ) *iso (sup-o< X lt )
replacement← : {ψ : HOD → HOD} (X x : HOD) →  X ∋ x → Replace X ψ ∋ ψ x
replacement← {ψ} X x lt = ⟪ sup-c< ψ {X} {x} lt , lemma ⟫ where
    lemma : def (in-codomain X ψ) (& (ψ x))
    lemma not = ⊥-elim ( not ( & x ) ⟪ lt , cong (λ k → & (ψ k)) (sym *iso)⟫ )
replacement→ : {ψ : HOD → HOD} (X x : HOD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (x =h= ψ y))
replacement→ {ψ} X x lt = contra-position lemma (lemma2 (proj2 lt)) where
    lemma2 :  ¬ ((y : Ordinal) → ¬ odef X y ∧ ((& x) ≡ & (ψ (* y))))
            → ¬ ((y : Ordinal) → ¬ odef X y ∧ (* (& x) =h= ψ (* y)))
    lemma2 not not2  = not ( λ y d →  not2 y ⟪ proj1 d , lemma3 (proj2 d)⟫) where
        lemma3 : {y : Ordinal } → (& x ≡ & (ψ (*  y))) → (* (& x) =h= ψ (* y))
        lemma3 {y} eq = subst (λ k  → * (& x) =h= k ) *iso (o≡→== eq )
    lemma :  ( (y : HOD) → ¬ (x =h= ψ y)) → ( (y : Ordinal) → ¬ odef X y ∧ (* (& x) =h= ψ (* y)) )
    lemma not y not2 = not (* y) (subst (λ k → k =h= ψ (* y)) *iso  ( proj2 not2 ))

---
--- Power Set
---
---    First consider ordinals in HOD
---
--- A ∩ x =  record { def = λ y → odef A y ∧  odef x y }                   subset of A
--
--
∩-≡ :  { a b : HOD  } → ({x : HOD  } → (a ∋ x → b ∋ x)) → a =h= ( b ∩ a )
∩-≡ {a} {b} inc = record {
   eq→ = λ {x} x<a → ⟪ (subst (λ k → odef b k ) &iso (inc (d→∋ a x<a))) , x<a  ⟫ ;
   eq← = λ {x} x<a∩b → proj2 x<a∩b }
--
-- Transitive Set case
-- we have t ∋ x → Ord a ∋ x means t is a subset of Ord a, that is (Ord a) ∩ t =h= t
-- OPwr (Ord a) is a sup of (Ord a) ∩ t, so OPwr (Ord a) ∋ t
-- OPwr  A = Ord ( sup-o ( λ x → & ( A ∩ (* x )) ) )
--
ord-power← : (a : Ordinal ) (t : HOD) → ({x : HOD} → (t ∋ x → (Ord a) ∋ x)) → OPwr (Ord a) ∋ t
ord-power← a t t→A  = subst (λ k → odef (OPwr (Ord a)) k ) (lemma1 lemma-eq) lemma where
    lemma-eq :  ((Ord a) ∩ t) =h= t
    eq→ lemma-eq {z} w = proj2 w
    eq← lemma-eq {z} w = ⟪ subst (λ k → odef (Ord a) k ) &iso ( t→A (d→∋ t w)) , w ⟫
    lemma1 :  {a : Ordinal } { t : HOD }
        → (eq : ((Ord a) ∩ t) =h= t)  → & ((Ord a) ∩ (* (& t))) ≡ & t
    lemma1  {a} {t} eq = subst (λ k → & ((Ord a) ∩ k) ≡ & t ) (sym *iso) (cong (λ k → & k ) (==→o≡ eq ))
    lemma2 : (& t) o< (osuc (& (Ord a)))
    lemma2 = ⊆→o≤  {t} {Ord a} (λ {x} x<t → subst (λ k → def (od (Ord a)) k) &iso (t→A (d→∋ t x<t)))
    lemma :  & ((Ord a) ∩ (* (& t)) ) o< sup-o (Ord (osuc (& (Ord a)))) (λ x lt → & ((Ord a) ∩ (* x)))
    lemma = sup-o< _ lemma2

--
-- Every set in HOD is a subset of Ordinals, so make OPwr (Ord (& A)) first
-- then replace of all elements of the Power set by A ∩ y
--
-- Power A = Replace (OPwr (Ord (& A))) ( λ y → A ∩ y )

-- we have oly double negation form because of the replacement axiom
--
power→ :  ( A t : HOD) → Power A ∋ t → {x : HOD} → t ∋ x → ¬ ¬ (A ∋ x)
power→ A t P∋t {x} t∋x = FExists _ lemma5 lemma4 where
    a = & A
    lemma2 : ¬ ( (y : HOD) → ¬ (t =h=  (A ∩ y)))
    lemma2 = replacement→ {λ x → A ∩ x} (OPwr (Ord (& A))) t P∋t
    lemma3 : (y : HOD) → t =h= ( A ∩ y ) → ¬ ¬ (A ∋ x)
    lemma3 y eq not = not (proj1 (eq→ eq t∋x))
    lemma4 : ¬ ((y : Ordinal) → ¬ (t =h= (A ∩ * y)))
    lemma4 not = lemma2 ( λ y not1 → not (& y) (subst (λ k → t =h= ( A ∩ k )) (sym *iso) not1 ))
    lemma5 : {y : Ordinal} → t =h= (A ∩ * y) →  ¬ ¬  (odef A (& x))
    lemma5 {y} eq not = (lemma3 (* y) eq) not

power← :  (A t : HOD) → ({x : HOD} → (t ∋ x → A ∋ x)) → Power A ∋ t
power← A t t→A = ⟪ lemma1 , lemma2 ⟫ where
    a = & A
    lemma0 : {x : HOD} → t ∋ x → Ord a ∋ x
    lemma0 {x} t∋x = c<→o< (t→A t∋x)
    lemma3 : OPwr (Ord a) ∋ t
    lemma3 = ord-power← a t lemma0
    lemma4 :  (A ∩ * (& t)) ≡ t
    lemma4 = let open ≡-Reasoning in begin
        A ∩ * (& t)
        ≡⟨ cong (λ k → A ∩ k) *iso ⟩
        A ∩ t
        ≡⟨ sym (==→o≡ ( ∩-≡ {t} {A} t→A )) ⟩
        t
        ∎
    sup1 : Ordinal
    sup1 =  sup-o (Ord (osuc (& (Ord (& A))))) (λ x A∋x → & ((Ord (& A)) ∩ (* x)))
    lemma9 : def (od (Ord (Ordinals.osuc O (& (Ord (& A)))))) (& (Ord (& A)))
    lemma9 = <-osuc
    lemmab : & ((Ord (& A)) ∩ (* (& (Ord (& A) )))) o< sup1
    lemmab = sup-o< (Ord (osuc (& (Ord (& A))))) lemma9
    lemmad : Ord (osuc (& A)) ∋ t
    lemmad = ⊆→o≤ (λ {x} lt → subst (λ k → def (od A) k ) &iso (t→A (d→∋ t lt)))
    lemmac : ((Ord (& A)) ∩  (* (& (Ord (& A) )))) =h= Ord (& A)
    lemmac = record { eq→ = lemmaf ; eq← = lemmag } where
        lemmaf : {x : Ordinal} → def (od ((Ord (& A)) ∩  (* (& (Ord (& A)))))) x → def (od (Ord (& A))) x
        lemmaf {x} lt = proj1 lt
        lemmag :  {x : Ordinal} → def (od (Ord (& A))) x → def (od ((Ord (& A)) ∩ (* (& (Ord (& A)))))) x
        lemmag {x} lt = ⟪ lt , subst (λ k → def (od k) x) (sym *iso) lt ⟫
    lemmae : & ((Ord (& A)) ∩ (* (& (Ord (& A))))) ≡ & (Ord (& A))
    lemmae = cong (λ k → & k ) ( ==→o≡ lemmac)
    lemma7 : def (od (OPwr (Ord (& A)))) (& t)
    lemma7 with osuc-≡< lemmad
    lemma7 | case2 lt = ordtrans (c<→o< lt) (subst (λ k → k o< sup1) lemmae lemmab )
    lemma7 | case1 eq with osuc-≡< (⊆→o≤ {* (& t)} {* (& (Ord (& t)))} (λ {x} lt → lemmah lt )) where
        lemmah : {x : Ordinal } → def (od (* (& t))) x → def (od (* (& (Ord (& t))))) x
        lemmah {x} lt = subst (λ k → def (od k) x ) (sym *iso) (subst (λ k → k o< (& t))
            &iso
            (c<→o< (subst₂ (λ j k → def (od j)  k) *iso (sym &iso) lt )))
    lemma7 | case1 eq | case1 eq1 = subst (λ k → k o< sup1) (trans lemmae lemmai) lemmab where
        lemmai : & (Ord (& A)) ≡ & t
        lemmai = let open ≡-Reasoning in begin
                & (Ord (& A))
            ≡⟨ sym (cong (λ k → & (Ord k)) eq) ⟩
                & (Ord (& t))
            ≡⟨ sym &iso ⟩
                & (* (& (Ord (& t))))
            ≡⟨ sym eq1 ⟩
                & (* (& t))
            ≡⟨ &iso ⟩
                & t
            ∎
    lemma7 | case1 eq | case2 lt = ordtrans lemmaj (subst (λ k → k o< sup1) lemmae lemmab ) where
        lemmak : & (* (& (Ord (& t)))) ≡ & (Ord (& A))
        lemmak = let open ≡-Reasoning in begin
                & (* (& (Ord (& t))))
            ≡⟨ &iso ⟩
                & (Ord (& t))
            ≡⟨ cong (λ k → & (Ord k)) eq ⟩
                & (Ord (& A))
            ∎
        lemmaj : & t o< & (Ord (& A))
        lemmaj = subst₂ (λ j k → j o< k ) &iso lemmak lt
    lemma1 : & t o< sup-o (OPwr (Ord (& A))) (λ x lt → & (A ∩ (* x)))
    lemma1 = subst (λ k → & k o< sup-o (OPwr (Ord (& A)))  (λ x lt → & (A ∩ (* x))))
        lemma4 (sup-o< (OPwr (Ord (& A))) lemma7 )
    lemma2 :  def (in-codomain (OPwr (Ord (& A))) (_∩_ A)) (& t)
    lemma2 not = ⊥-elim ( not (& t) ⟪ lemma3 , lemma6 ⟫ ) where
        lemma6 : & t ≡ & (A ∩ * (& t))
        lemma6 = cong ( λ k → & k ) (==→o≡ (subst (λ k → t =h= (A ∩ k)) (sym *iso) ( ∩-≡ {t} {A} t→A  )))

extensionality0 : {A B : HOD } → ((z : HOD) → (A ∋ z) ⇔ (B ∋ z)) → A =h= B
eq→ (extensionality0 {A} {B} eq ) {x} d = odef-iso  {A} {B} (sym &iso) (proj1 (eq (* x))) d
eq← (extensionality0 {A} {B} eq ) {x} d = odef-iso  {B} {A} (sym &iso) (proj2 (eq (* x))) d

extensionality : {A B w : HOD  } → ((z : HOD ) → (A ∋ z) ⇔ (B ∋ z)) → (w ∋ A) ⇔ (w ∋ B)
proj1 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) ( ==→o≡ (extensionality0 {A} {B} eq) ) d
proj2 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) (sym ( ==→o≡ (extensionality0 {A} {B} eq) )) d

infinity∅ : infinite  ∋ od∅
infinity∅ = subst (λ k → odef infinite k ) lemma iφ where
    lemma : o∅ ≡ & od∅
    lemma =  let open ≡-Reasoning in begin
        o∅
        ≡⟨ sym &iso ⟩
        & ( * o∅ )
        ≡⟨ cong ( λ k → & k ) o∅≡od∅ ⟩
        & od∅
        ∎
infinity : (x : HOD) → infinite ∋ x → infinite ∋ Union (x , (x , x ))
infinity x lt = subst (λ k → odef infinite k ) lemma (isuc {& x} lt) where
    lemma :  & (Union (* (& x) , (* (& x) , * (& x))))
        ≡ & (Union (x , (x , x)))
    lemma = cong (λ k → & (Union ( k , ( k , k ) ))) *iso

isZF : IsZF (HOD )  _∋_  _=h=_ od∅ _,_ Union Power Select Replace infinite
isZF = record {
        isEquivalence  = record { refl = ==-refl ; sym = ==-sym; trans = ==-trans }
    ;   pair→  = pair→
    ;   pair←  = pair←
    ;   union→ = union→
    ;   union← = union←
    ;   empty = empty
    ;   power→ = power→
    ;   power← = power←
    ;   extensionality = λ {A} {B} {w} → extensionality {A} {B} {w}
    ;   ε-induction = ε-induction
    ;   infinity∅ = infinity∅
    ;   infinity = infinity
    ;   selection = λ {X} {ψ} {y} → selection {X} {ψ} {y}
    ;   replacement← = replacement←
    ;   replacement→ = λ {ψ} → replacement→ {ψ}
    }

HOD→ZF : ZF
HOD→ZF   = record {
    ZFSet = HOD
    ; _∋_ = _∋_
    ; _≈_ = _=h=_
    ; ∅  = od∅
    ; _,_ = _,_
    ; Union = Union
    ; Power = Power
    ; Select = Select
    ; Replace = Replace
    ; infinite = infinite
    ; isZF = isZF
 }

max_stars_repo_name: shinji-kono/zf-in-agda

max_issues_repo_name: shinji-kono/zf-in-agda

max_forks_repo_name: shinji-kono/zf-in-agda


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

open import HoTT
open import cw.CW
open import homotopy.DisjointlyPointedSet
open import groups.Int
open import cohomology.Theory
open import cohomology.ChainComplex

module cw.cohomology.ReconstructedCochainsIsoCellularCochains {i : ULevel}
  (OT : OrdinaryTheory i) where

  open OrdinaryTheory OT
  open import cw.cohomology.WedgeOfCells OT
  open import cw.cohomology.cellular.ChainComplex as CCC
  open import cw.cohomology.reconstructed.cochain.Complex OT as RCC
  open import cw.cohomology.reconstructed.TipAndAugment OT

  private
    rcc-iso-ccc-nth : ∀ {n} (⊙skel : ⊙Skeleton n) {m} (m≤n : m ≤ n)
      → ⊙has-cells-with-choice 0 ⊙skel i
      →  AbGroup.grp (RCC.cochain-template ⊙skel (inl m≤n))
      ≃ᴳ hom-group (AbGroup.grp (CCC.chain-template (⊙Skeleton.skel ⊙skel) (inl m≤n))) (C2-abgroup 0)
    rcc-iso-ccc-nth ⊙skel {m = O} (inl idp) ac
      =   FreeAbGroup-extend-iso (C2-abgroup 0)
      ∘eᴳ C2×CX₀-diag-β ⊙skel ac
    rcc-iso-ccc-nth ⊙skel {m = S m} (inl idp) ac
      =   FreeAbGroup-extend-iso (C2-abgroup 0)
      ∘eᴳ CXₙ/Xₙ₋₁-diag-β ⊙skel ac
    rcc-iso-ccc-nth ⊙skel {m = O} (inr ltS) ac =
      rcc-iso-ccc-nth (⊙cw-init ⊙skel) (inl idp) (⊙init-has-cells-with-choice ⊙skel ac)
    rcc-iso-ccc-nth ⊙skel {m = S m} (inr ltS) ac =
      rcc-iso-ccc-nth (⊙cw-init ⊙skel) (inl idp) (⊙init-has-cells-with-choice ⊙skel ac)
    rcc-iso-ccc-nth ⊙skel {m = O} (inr (ltSR lt)) ac =
      rcc-iso-ccc-nth (⊙cw-init ⊙skel) (inr lt) (⊙init-has-cells-with-choice ⊙skel ac)
    rcc-iso-ccc-nth ⊙skel {m = S m} (inr (ltSR lt)) ac =
      rcc-iso-ccc-nth (⊙cw-init ⊙skel) (inr lt) (⊙init-has-cells-with-choice ⊙skel ac)

    rcc-iso-ccc-above : ∀ {n} (⊙skel : ⊙Skeleton n) {m} (m≰n : ¬ (m ≤ n))
      →  AbGroup.grp (RCC.cochain-template ⊙skel (inr m≰n))
      ≃ᴳ hom-group (AbGroup.grp (CCC.chain-template (⊙Skeleton.skel ⊙skel) (inr m≰n))) (C2-abgroup 0)
    rcc-iso-ccc-above ⊙skel _
      =   pre∘ᴳ-iso (C2-abgroup 0) lower-iso
      ∘eᴳ trivial-iso-Unit (hom₁-Unit-is-trivial (C2-abgroup 0)) ⁻¹ᴳ
      ∘eᴳ lower-iso

  rcc-iso-ccc-template : ∀ {n} (⊙skel : ⊙Skeleton n) {m : ℕ} (m≤n? : Dec (m ≤ n))
    → ⊙has-cells-with-choice 0 ⊙skel i
    →  AbGroup.grp (RCC.cochain-template ⊙skel m≤n?)
    ≃ᴳ hom-group (AbGroup.grp (CCC.chain-template (⊙Skeleton.skel ⊙skel) m≤n?)) (C2-abgroup 0)
  rcc-iso-ccc-template ⊙skel {m} (inl m≤n) ac = rcc-iso-ccc-nth ⊙skel m≤n ac
  rcc-iso-ccc-template ⊙skel {m} (inr m≰n) _ = rcc-iso-ccc-above ⊙skel m≰n

  rcc-iso-ccc : ∀ {n} (⊙skel : ⊙Skeleton n) (m : ℕ)
    → ⊙has-cells-with-choice 0 ⊙skel i
    →  AbGroup.grp (RCC.cochain-template ⊙skel (≤-dec m n))
    ≃ᴳ hom-group (AbGroup.grp (CCC.chain-template (⊙Skeleton.skel ⊙skel) (≤-dec m n))) (C2-abgroup 0)
  rcc-iso-ccc {n} ⊙skel m = rcc-iso-ccc-template ⊙skel (≤-dec m n)

  rhead-iso-chead : C2 0 ≃ᴳ hom-group (Lift-group {j = i} ℤ-group) (C2-abgroup 0)
  rhead-iso-chead
    =   pre∘ᴳ-iso (C2-abgroup 0) (lower-iso {j = i})
    ∘eᴳ ℤ→ᴳ-iso-idf (C2-abgroup 0) ⁻¹ᴳ


text:
module Squash where

data _==_ {A : Set}(a : A) : A -> Set where
  refl : a == a

data Wrap (A : Set) : Set where
  wrap : A -> Wrap A

data Squash (A : Set) : Set where
  squash : .A -> Squash A

postulate
  A : Set
  a1 a2 : A

irr : squash a1 == squash a2
irr = refl


text:
module Issue2935 where

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

bad : ℕ → ℕ
bad zero = zero
bad suc  = zero


text:
module Impure.LFRef.Syntax where

open import Prelude
open import Data.Vec hiding ([_]; map)
open import Data.List hiding ([_])
open import Data.List.All hiding (lookup)

data Term : (n : ℕ) → Set
data Type : (n : ℕ) → Set

data Term where
  var : ∀ {n} → Fin n → Term n
  loc : ∀ {n} → ℕ → Term n
  unit : ∀ {n} → Term n

  -- constructor application
  con : ∀ {n} → (fn : ℕ) → (ts : List (Term n)) → Term n

infixl 30 _·★_
data Exp : ℕ → Set where
  -- basic lambda expressions
  tm : ∀ {n} → Term n → Exp n

  -- function calls
  _·★_ : ∀ {n} → (fn : ℕ) → (as : List (Term n)) → Exp n

  -- heap manipulation
  ref : ∀ {n} → Exp n → Exp n
  !_ : ∀ {n} → Exp n → Exp n
  _≔_ : ∀ {n} → Exp n → Exp n → Exp n

data SeqExp : ℕ → Set where
  lett : ∀ {n} → (x : Exp n) → (e : SeqExp (suc n)) → SeqExp n
  ret  : ∀ {n} → Exp n → SeqExp n

data Val : Term 0 → Set where
  loc : ∀ {i} → Val (loc i)
  unit : Val unit
  con : ∀ {k ts} → Val (con k ts)

data ExpVal : Exp zero → Set where
  tm : ∀ {t} → Val t → ExpVal (tm t)

data SeqExpVal : SeqExp zero → Set where
  ret-tm : ∀ {t} → Val t → SeqExpVal (ret (tm t))

-- telescoped contexts/arguments
data Tele : (n m : ℕ) → Set where
  ε : ∀ {n} → Tele n 0
  _⟶_ : ∀ {m n} → Type n → Tele (suc n) m → Tele n (suc m)

infixl 20 _[_]
data Type where
  _[_] : ∀ {n} → ℕ → (ts : List (Term n)) → Type n
  Ref : ∀ {n} → (A : Type n) → Type n
  Unit : ∀ {n} → Type n

Store : Set
Store = List (∃ Val)

record ConType : Set where
  field
    m : ℕ
    args : Tele 0 m
    tp   : ℕ
    indices : List (Term m)

record Fun : Set where
  field
    m : ℕ
    args : Tele 0 m
    returntype : Type m
    body : Exp m

record Sig : Set where
  field
    types : List (∃ (Tele 0))
    constructors : List ConType
    funs : List Fun

open import Data.Fin.Substitution

module App {T} (l : Lift T Term) where
  open Lift l

  _tp/_ : ∀ {n n'} → Type n → Sub T n n' → Type n'

  _/_ : ∀ {n n'} → Term n → Sub T n n' → Term n'
  var x / s = lift $ lookup x s
  unit / s = unit
  _/_ {n} {n'} (con c ts) s = con c (map/ ts)
    where
      -- inlined for termination checker..
      map/ : List (Term n) → List (Term n')
      map/ [] = []
      map/ (x ∷ ts₁) = x / s ∷ map/ ts₁
  loc x / s = loc x

  _tele/_ : ∀ {n m n'} → Tele n m → Sub T n n' → Tele n' m
  ε tele/ s = ε
  (x ⟶ t) tele/ s = (x tp/ s) ⟶ (t tele/ (s ↑))

  _tp/_ {n} {n'} (k [ ts ]) s = k [ map/ ts ]
    where
      -- inlined for termination checker..
      map/ : List (Term n) → List (Term n')
      map/ [] = []
      map/ (x ∷ ts₁) = x / s ∷ map/ ts₁
  (Ref A) tp/ s = Ref (A tp/ s)
  Unit tp/ s = Unit

  _exp/_ : ∀ {n n'} → Exp n → Sub T n n' → Exp n'
  tm x exp/ s = tm (x / s)
  _exp/_ {n} {n'} (fn ·★ ts) s = fn ·★ map/ ts
    where
      -- inlined for termination checker..
      map/ : List (Term n) → List (Term n')
      map/ [] = []
      map/ (x ∷ ts₁) = x / s ∷ map/ ts₁
  ref x exp/ s = ref (x exp/ s)
  (! x) exp/ s = ! (x exp/ s)
  (y ≔ x) exp/ s = (y exp/ s) ≔ (x exp/ s)

  _seq/_ : ∀ {n n'} → SeqExp n → Sub T n n' → SeqExp n'
  lett x e seq/ s = lett (x exp/ s) (e seq/ (s ↑))
  ret e seq/ s = ret (e exp/ s)

  open Application (record { _/_ = _/_ }) using (_/✶_)

tmSubst : TermSubst Term
tmSubst = record { var = var; app = App._/_ }

open TermSubst tmSubst hiding (var) public

open App termLift using (_exp/_; _tp/_; _tele/_; _seq/_) public


text:
{-# OPTIONS --type-in-type #-}

Ty% : Set; Ty%
 = (Ty  : Set)
   (ι   : Ty)
   (arr : Ty → Ty → Ty)
 → Ty

ι%   : Ty%; ι% = λ _ ι% _ → ι%
arr% : Ty% → Ty% → Ty%; arr% = λ A B Ty% ι% arr% → arr% (A Ty% ι% arr%) (B Ty% ι% arr%)

Con% : Set;Con%
 = (Con% : Set)
   (nil  : Con%)
   (snoc : Con% → Ty% → Con%)
 → Con%

nil% : Con%;nil%
 = λ Con% nil% snoc → nil%

snoc% : Con% → Ty% → Con%;snoc%
 = λ Γ A Con% nil% snoc% → snoc% (Γ Con% nil% snoc%) A

Var% : Con% → Ty% → Set;Var%
 = λ Γ A →
   (Var% : Con% → Ty% → Set)
   (vz  : (Γ : _)(A : _) → Var% (snoc% Γ A) A)
   (vs  : (Γ : _)(B A : _) → Var% Γ A → Var% (snoc% Γ B) A)
 → Var% Γ A

vz% : ∀{Γ A} → Var% (snoc% Γ A) A;vz%
 = λ Var% vz% vs → vz% _ _

vs% : ∀{Γ B A} → Var% Γ A → Var% (snoc% Γ B) A;vs%
 = λ x Var% vz% vs% → vs% _ _ _ (x Var% vz% vs%)

Tm% : Con% → Ty% → Set;Tm%
 = λ Γ A →
   (Tm%    : Con% → Ty% → Set)
   (var   : (Γ : _) (A : _) → Var% Γ A → Tm% Γ A)
   (lam   : (Γ : _) (A B : _) → Tm% (snoc% Γ A) B → Tm% Γ (arr% A B))
   (app   : (Γ : _) (A B : _) → Tm% Γ (arr% A B) → Tm% Γ A → Tm% Γ B)
 → Tm% Γ A

var% : ∀{Γ A} → Var% Γ A → Tm% Γ A;var%
 = λ x Tm% var% lam app → var% _ _ x

lam% : ∀{Γ A B} → Tm% (snoc% Γ A) B → Tm% Γ (arr% A B);lam%
 = λ t Tm% var% lam% app → lam% _ _ _ (t Tm% var% lam% app)

app% : ∀{Γ A B} → Tm% Γ (arr% A B) → Tm% Γ A → Tm% Γ B;app%
 = λ t u Tm% var% lam% app% →
     app% _ _ _ (t Tm% var% lam% app%) (u Tm% var% lam% app%)

v0% : ∀{Γ A} → Tm% (snoc% Γ A) A;v0%
 = var% vz%

v1% : ∀{Γ A B} → Tm% (snoc% (snoc% Γ A) B) A;v1%
 = var% (vs% vz%)

v2% : ∀{Γ A B C} → Tm% (snoc% (snoc% (snoc% Γ A) B) C) A;v2%
 = var% (vs% (vs% vz%))

v3% : ∀{Γ A B C D} → Tm% (snoc% (snoc% (snoc% (snoc% Γ A) B) C) D) A;v3%
 = var% (vs% (vs% (vs% vz%)))

v4% : ∀{Γ A B C D E} → Tm% (snoc% (snoc% (snoc% (snoc% (snoc% Γ A) B) C) D) E) A;v4%
 = var% (vs% (vs% (vs% (vs% vz%))))

test% : ∀{Γ A} → Tm% Γ (arr% (arr% A A) (arr% A A));test%
  = lam% (lam% (app% v1% (app% v1% (app% v1% (app% v1% (app% v1% (app% v1% v0%)))))))

max_stars_repo_name: int-index/smalltt

max_issues_repo_name: int-index/smalltt

max_forks_repo_name: int-index/smalltt


text:
open import FRP.JS.String using ( String ; _≟_ ; _<_ )
open import FRP.JS.Bool using ( Bool ; true ; false ; _∧_ )
open import FRP.JS.True using ( True )
open import FRP.JS.Maybe using ( Maybe ; just ; nothing )

module FRP.JS.Keys where

infixr 4 _∷_

data IKeys : Set where
  [] : IKeys
  _∷_ : (k : String) → (ks : IKeys) → IKeys

{-# COMPILED_JS IKeys function(x,v) {
  if ((x.array.length) <= (x.offset)) { return v["[]"](); }
  else { return v["_∷_"](x.key(),x.tail()); }
} #-}
{-# COMPILED_JS [] require("agda.keys").iempty #-}
{-# COMPILED_JS _∷_ function(k) { return function(ks) { return ks.cons(k); }; } #-}

head : IKeys → Maybe String
head []       = nothing
head (k ∷ ks) = just k

{-# COMPILED_JS head function(ks) { return require("agda.box").box(ks.key()); } #-}

_<?_ : String → Maybe String → Bool
k <? nothing = true
k <? just l  = k < l

sorted : IKeys → Bool
sorted []       = true
sorted (k ∷ ks) = (k <? head ks) ∧ (sorted ks)

record Keys : Set where
  constructor keys
  field
    ikeys : IKeys
    {ikeys✓} : True (sorted ikeys)

open Keys public

{-# COMPILED_JS Keys function(x,v) { return v.keys(require("agda.keys").iarray(x),null); } #-}
{-# COMPILED_JS keys function(ks) { return function() { return ks.keys(); }; } #-}
{-# COMPILED_JS ikeys function(ks) { return require("agda.keys").iarray(ks); } #-}
{-# COMPILED_JS ikeys✓ function(ks) { return null; } #-}

_∈i_ : String → IKeys → Bool
l ∈i [] = false
l ∈i (k ∷ ks)
 with k ≟ l
... | true  = true
... | false
 with k < l
... | true  = l ∈i ks
... | false = false

_∈_ : String → Keys → Bool
l ∈ keys ks = l ∈i ks

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js