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

open import lib.Basics
open import lib.types.Bool
open import lib.types.Group
open import lib.types.Nat
open import lib.types.Pi
open import lib.types.Sigma
open import lib.types.Coproduct
open import lib.types.Truncation
open import lib.groups.Homomorphism
open import lib.groups.Isomorphism
open import lib.groups.SubgroupProp
open import lib.groups.Lift
open import lib.groups.Unit

module lib.groups.GroupProduct where

{- binary product -}
×-group-struct : ∀ {i j} {A : Type i} {B : Type j}
  (GS : GroupStructure A) (HS : GroupStructure B)
  → GroupStructure (A × B)
×-group-struct {A = A} {B = B} GS HS = record {M} where
  module G = GroupStructure GS
  module H = GroupStructure HS
  module M where
    ident : A × B
    ident = G.ident , H.ident

    inv : A × B → A × B
    inv (g , h) = G.inv g , H.inv h

    comp : A × B → A × B → A × B
    comp (g₁ , h₁) (g₂ , h₂) = G.comp g₁ g₂ , H.comp h₁ h₂

    abstract
      unit-l : ∀ ab → comp ident ab == ab
      unit-l (g , h) = pair×= (G.unit-l g) (H.unit-l h)

      assoc : ∀ ab₁ ab₂ ab₃ → comp (comp ab₁ ab₂) ab₃ == comp ab₁ (comp ab₂ ab₃)
      assoc (g₁ , h₁) (g₂ , h₂) (g₃ , h₃) =
        pair×= (G.assoc g₁ g₂ g₃) (H.assoc h₁ h₂ h₃)

      inv-l : ∀ ab → comp (inv ab) ab == ident
      inv-l (g , h) = pair×= (G.inv-l g) (H.inv-l h)

infix 80 _×ᴳ_
_×ᴳ_ : ∀ {i j} → Group i → Group j → Group (lmax i j)
_×ᴳ_ (group A A-level A-struct) (group B B-level B-struct) =
  group (A × B) (×-level A-level B-level) (×-group-struct A-struct B-struct)

{- general product -}
Π-group-struct : ∀ {i j} {I : Type i} {A : I → Type j}
  (FS : (i : I) → GroupStructure (A i))
  → GroupStructure (Π I A)
Π-group-struct FS = record {
  ident = ident ∘ FS;
  inv = λ f i → inv (FS i) (f i);
  comp = λ f g i → comp (FS i) (f i) (g i);
  unit-l = λ f → (λ= (λ i → unit-l (FS i) (f i)));
  assoc = λ f g h → (λ= (λ i → assoc (FS i) (f i) (g i) (h i)));
  inv-l = λ f → (λ= (λ i → inv-l (FS i) (f i)))}
  where open GroupStructure

Πᴳ : ∀ {i j} (I : Type i) (F : I → Group j) → Group (lmax i j)
Πᴳ I F = group (Π I (El ∘ F)) (Π-level (λ i → El-level (F i)))
               (Π-group-struct (group-struct ∘ F))
  where open Group

{- functorial behavior of [Πᴳ] -}
Πᴳ-emap-r : ∀ {i j k} (I : Type i) {F : I → Group j} {G : I → Group k}
  → (∀ i → F i ≃ᴳ G i) → Πᴳ I F ≃ᴳ Πᴳ I G
Πᴳ-emap-r I {F} {G} iso = ≃-to-≃ᴳ (Π-emap-r (GroupIso.f-equiv ∘ iso))
  (λ f g → λ= λ i → GroupIso.pres-comp (iso i) (f i) (g i))

{- the product of abelian groups is abelian -}
×ᴳ-is-abelian : ∀ {i j} (G : Group i) (H : Group j)
  → is-abelian G → is-abelian H → is-abelian (G ×ᴳ H)
×ᴳ-is-abelian G H aG aH (g₁ , h₁) (g₂ , h₂) = pair×= (aG g₁ g₂) (aH h₁ h₂)

×ᴳ-abgroup : ∀ {i j} → AbGroup i → AbGroup j → AbGroup (lmax i j)
×ᴳ-abgroup (G , aG) (H , aH) = G ×ᴳ H , ×ᴳ-is-abelian G H aG aH

Πᴳ-is-abelian : ∀ {i j} {I : Type i} {F : I → Group j}
  → (∀ i → is-abelian (F i)) → is-abelian (Πᴳ I F)
Πᴳ-is-abelian aF f₁ f₂ = λ= (λ i → aF i (f₁ i) (f₂ i))

{- defining a homomorphism into a product -}
×ᴳ-fanout : ∀ {i j k} {G : Group i} {H : Group j} {K : Group k}
  → (G →ᴳ H) → (G →ᴳ K) → (G →ᴳ H ×ᴳ K)
×ᴳ-fanout (group-hom h h-comp) (group-hom k k-comp) =
  group-hom
    (λ x → (h x , k x))
    (λ x y → pair×= (h-comp x y) (k-comp x y))

Πᴳ-fanout : ∀ {i j k} {I : Type i} {G : Group j} {F : I → Group k}
  → ((i : I) → G →ᴳ F i) → (G →ᴳ Πᴳ I F)
Πᴳ-fanout h = group-hom
  (λ x i → GroupHom.f (h i) x)
  (λ x y → λ= (λ i → GroupHom.pres-comp (h i) x y))

×ᴳ-fanout-pre∘ : ∀ {i j k l}
  {G : Group i} {H : Group j} {K : Group k} {J : Group l}
  (φ : G →ᴳ H) (ψ : G →ᴳ K) (χ : J →ᴳ G)
  → ×ᴳ-fanout φ ψ ∘ᴳ χ == ×ᴳ-fanout (φ ∘ᴳ χ) (ψ ∘ᴳ χ)
×ᴳ-fanout-pre∘ φ ψ χ = group-hom= idp

{- projection homomorphisms -}
×ᴳ-fst : ∀ {i j} {G : Group i} {H : Group j} → (G ×ᴳ H →ᴳ G)
×ᴳ-fst = group-hom fst (λ _ _ → idp)

×ᴳ-snd : ∀ {i j} {G : Group i} {H : Group j} → (G ×ᴳ H →ᴳ H)
×ᴳ-snd = group-hom snd (λ _ _ → idp)

×ᴳ-snd-is-surj : ∀ {i j} {G : Group i} {H : Group j}
  → is-surjᴳ (×ᴳ-snd {G = G} {H = H})
×ᴳ-snd-is-surj {G = G} h = [ (Group.ident G , h) , idp ]

Πᴳ-proj : ∀ {i j} {I : Type i} {F : I → Group j} (i : I)
  → (Πᴳ I F →ᴳ F i)
Πᴳ-proj i = group-hom (λ f → f i) (λ _ _ → idp)

{- injection homomorphisms -}
module _ {i j} {G : Group i} {H : Group j} where

  ×ᴳ-inl : G →ᴳ G ×ᴳ H
  ×ᴳ-inl = ×ᴳ-fanout (idhom G) cst-hom

  ×ᴳ-inr : H →ᴳ G ×ᴳ H
  ×ᴳ-inr = ×ᴳ-fanout (cst-hom {H = G}) (idhom H)

×ᴳ-diag : ∀ {i} {G : Group i} → (G →ᴳ G ×ᴳ G)
×ᴳ-diag = ×ᴳ-fanout (idhom _) (idhom _)

{- when G is abelian, we can define a map H×K → G as a sum of maps
 - H → G and K → G (that is, the product behaves as a sum)         -}
module _ {i j k} {G : Group i} {H : Group j} {K : Group k}
  (G-abelian : is-abelian G) where

  private
    module G = Group G
    module H = Group H
    module K = Group K

    abstract
      interchange : (g₁ g₂ g₃ g₄ : G.El) →
        G.comp (G.comp g₁ g₂) (G.comp g₃ g₄)
        == G.comp (G.comp g₁ g₃) (G.comp g₂ g₄)
      interchange g₁ g₂ g₃ g₄ =
        (g₁ □ g₂) □ (g₃ □ g₄)
           =⟨ G.assoc g₁ g₂ (g₃ □ g₄) ⟩
         g₁ □ (g₂ □ (g₃ □ g₄))
           =⟨ G-abelian g₃ g₄ |in-ctx (λ w → g₁ □ (g₂ □ w)) ⟩
         g₁ □ (g₂ □ (g₄ □ g₃))
           =⟨ ! (G.assoc g₂ g₄ g₃) |in-ctx (λ w → g₁ □ w) ⟩
         g₁ □ ((g₂ □ g₄) □ g₃)
           =⟨ G-abelian (g₂ □ g₄) g₃ |in-ctx (λ w → g₁ □ w) ⟩
         g₁ □ (g₃ □ (g₂ □ g₄))
           =⟨ ! (G.assoc g₁ g₃ (g₂ □ g₄)) ⟩
         (g₁ □ g₃) □ (g₂ □ g₄) =∎
         where
          infix 80 _□_
          _□_ = G.comp

  ×ᴳ-fanin : (H →ᴳ G) → (K →ᴳ G) → (H ×ᴳ K →ᴳ G)
  ×ᴳ-fanin φ ψ = group-hom (λ {(h , k) → G.comp (φ.f h) (ψ.f k)}) lemma
    where
      module φ = GroupHom φ
      module ψ = GroupHom ψ
      abstract
        lemma : preserves-comp (Group.comp (H ×ᴳ K)) G.comp
                  (λ {(h , k) → G.comp (φ.f h) (ψ.f k)})
        lemma (h₁ , k₁) (h₂ , k₂) =
          G.comp (φ.f (H.comp h₁ h₂)) (ψ.f (K.comp k₁ k₂))
            =⟨ φ.pres-comp h₁ h₂ |in-ctx (λ w → G.comp w (ψ.f (K.comp k₁ k₂))) ⟩
          G.comp (G.comp (φ.f h₁) (φ.f h₂)) (ψ.f (K.comp k₁ k₂))
            =⟨ ψ.pres-comp k₁ k₂
               |in-ctx (λ w → G.comp (G.comp (φ.f h₁) (φ.f h₂)) w)  ⟩
          G.comp (G.comp (φ.f h₁) (φ.f h₂)) (G.comp (ψ.f k₁) (ψ.f k₂))
            =⟨ interchange (φ.f h₁) (φ.f h₂) (ψ.f k₁) (ψ.f k₂) ⟩
          G.comp (G.comp (φ.f h₁) (ψ.f k₁)) (G.comp (φ.f h₂) (ψ.f k₂)) =∎

abstract
  ×ᴳ-fanin-η : ∀ {i j} (G : Group i) (H : Group j)
    (aGH : is-abelian (G ×ᴳ H))
    → idhom (G ×ᴳ H) == ×ᴳ-fanin aGH (×ᴳ-inl {G = G}) (×ᴳ-inr {G = G})
  ×ᴳ-fanin-η G H aGH = group-hom= $ λ= λ {(g , h) →
    ! (pair×= (Group.unit-r G g) (Group.unit-l H h))}

  ×ᴳ-fanin-pre∘ : ∀ {i j k l}
    {G : Group i} {H : Group j} {K : Group k} {L : Group l}
    (aK : is-abelian K) (aL : is-abelian L)
    (φ : K →ᴳ L) (ψ : G →ᴳ K) (χ : H →ᴳ K)
    → ×ᴳ-fanin aL (φ ∘ᴳ ψ) (φ ∘ᴳ χ) == φ ∘ᴳ (×ᴳ-fanin aK ψ χ)
  ×ᴳ-fanin-pre∘ aK aL φ ψ χ = group-hom= $ λ= λ {(g , h) →
    ! (GroupHom.pres-comp φ (GroupHom.f ψ g) (GroupHom.f χ h))}

{- define a homomorphism [G₁ × G₂ → H₁ × H₂] from homomorphisms
 - [G₁ → H₁] and [G₂ → H₂] -}
×ᴳ-fmap : ∀ {i j k l} {G₁ : Group i} {G₂ : Group j}
  {H₁ : Group k} {H₂ : Group l}
  → (G₁ →ᴳ H₁) → (G₂ →ᴳ H₂) → (G₁ ×ᴳ G₂ →ᴳ H₁ ×ᴳ H₂)
×ᴳ-fmap {G₁ = G₁} {G₂} {H₁} {H₂} φ ψ = group-hom (×-fmap φ.f ψ.f) lemma
  where
    module φ = GroupHom φ
    module ψ = GroupHom ψ
    abstract
      lemma : preserves-comp (Group.comp (G₁ ×ᴳ G₂)) (Group.comp (H₁ ×ᴳ H₂))
                (λ {(h₁ , h₂) → (φ.f h₁ , ψ.f h₂)})
      lemma (h₁ , h₂) (h₁' , h₂') = pair×= (φ.pres-comp h₁ h₁') (ψ.pres-comp h₂ h₂')

×ᴳ-emap : ∀ {i j k l} {G₁ : Group i} {G₂ : Group j}
  {H₁ : Group k} {H₂ : Group l}
  → (G₁ ≃ᴳ H₁) → (G₂ ≃ᴳ H₂) → (G₁ ×ᴳ G₂ ≃ᴳ H₁ ×ᴳ H₂)
×ᴳ-emap (φ , φ-is-equiv) (ψ , ψ-is-equiv) =
  ×ᴳ-fmap φ ψ , ×-isemap φ-is-equiv ψ-is-equiv

{- equivalences in Πᴳ -}

Πᴳ-emap-l : ∀ {i j k} {A : Type i} {B : Type j} (F : B → Group k)
            → (e : A ≃ B) → Πᴳ A (F ∘ –> e) ≃ᴳ Πᴳ B F
Πᴳ-emap-l {A = A} {B = B} F e = ≃-to-≃ᴳ (Π-emap-l (Group.El ∘ F) e) lemma
  where abstract lemma = λ f g → λ= λ b → transp-El-pres-comp F (<–-inv-r e b) (f (<– e b)) (g (<– e b))

{- 0ᴳ is a unit for product -}
×ᴳ-unit-l : ∀ {i} (G : Group i) → 0ᴳ ×ᴳ G ≃ᴳ G
×ᴳ-unit-l _ = ×ᴳ-snd {G = 0ᴳ} , is-eq snd (λ g → (unit , g)) (λ _ → idp) (λ _ → idp)

×ᴳ-unit-r : ∀ {i} (G : Group i) → G ×ᴳ 0ᴳ ≃ᴳ G
×ᴳ-unit-r _ = ×ᴳ-fst , is-eq fst (λ g → (g , unit)) (λ _ → idp) (λ _ → idp)

{- A product Πᴳ indexed by Bool is the same as a binary product -}
module _ {i j k} {A : Type i} {B : Type j} (F : A ⊔ B → Group k) where

  Πᴳ₁-⊔-iso-×ᴳ : Πᴳ (A ⊔ B) F ≃ᴳ Πᴳ A (F ∘ inl) ×ᴳ Πᴳ B (F ∘ inr)
  Πᴳ₁-⊔-iso-×ᴳ = ≃-to-≃ᴳ (Π₁-⊔-equiv-× (Group.El ∘ F)) (λ _ _ → idp)

{- Commutativity of ×ᴳ -}
×ᴳ-comm : ∀ {i j} (H : Group i) (K : Group j) → H ×ᴳ K ≃ᴳ K ×ᴳ H
×ᴳ-comm H K =
  group-hom (λ {(h , k) → (k , h)}) (λ _ _ → idp) ,
  is-eq _ (λ {(k , h) → (h , k)}) (λ _ → idp) (λ _ → idp)

{- Associativity of ×ᴳ -}
×ᴳ-assoc : ∀ {i j k} (G : Group i) (H : Group j) (K : Group k)
  → ((G ×ᴳ H) ×ᴳ K) ≃ᴳ (G ×ᴳ (H ×ᴳ K))
×ᴳ-assoc G H K =
  group-hom (λ {((g , h) , k) → (g , (h , k))}) (λ _ _ → idp) ,
  is-eq _ (λ {(g , (h , k)) → ((g , h) , k)}) (λ _ → idp) (λ _ → idp)

module _ {i} where

  infixl 80 _^ᴳ_
  _^ᴳ_ : Group i → ℕ → Group i
  H ^ᴳ O = Lift-group {j = i} 0ᴳ
  H ^ᴳ (S n) = H ×ᴳ (H ^ᴳ n)

  ^ᴳ-+ : (H : Group i) (m n : ℕ) → H ^ᴳ (m + n) ≃ᴳ (H ^ᴳ m) ×ᴳ (H ^ᴳ n)
  ^ᴳ-+ H O n = ×ᴳ-emap (lift-iso {G = 0ᴳ}) (idiso (H ^ᴳ n)) ∘eᴳ ×ᴳ-unit-l (H ^ᴳ n) ⁻¹ᴳ
  ^ᴳ-+ H (S m) n = ×ᴳ-assoc H (H ^ᴳ m) (H ^ᴳ n) ⁻¹ᴳ ∘eᴳ ×ᴳ-emap (idiso H) (^ᴳ-+ H m n)

module _ where
  Πᴳ-is-trivial : ∀ {i j} (I : Type i) (F : I → Group j)
    → (∀ (i : I) → is-trivialᴳ (F i)) → is-trivialᴳ (Πᴳ I F)
  Πᴳ-is-trivial I F F-is-trivial = λ f → λ= λ i → F-is-trivial i (f i)

module _ {j} {F : Unit → Group j} where
  Πᴳ₁-Unit : Πᴳ Unit F ≃ᴳ F unit
  Πᴳ₁-Unit = ≃-to-≃ᴳ Π₁-Unit (λ _ _ → idp)

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


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

open import library.Basics

open import library.types.Sigma
open import library.types.Bool
open import library.types.Truncation hiding (Trunc)

module Sec8judgmentalBeta where

{-
Recall Definition 3.6:

postulate
  Trunc : Type → Type
  h-tr : (X : Type) → is-prop (Trunc X)
  ∣_∣ : {X : Type} → X → Trunc X
  rec : {X : Type} → {P : Type} → (is-prop P) → (X → P) → Trunc X → P

We now redefine the propositional truncation so that rec has the judgmental β rule.
We use the library implementation (library.types.Truncation).
However, we still only talk about the *propositional* truncation (not the more general n-truncation).

This file is independent of all the previous files of the article.
For the part in Subsection 9.4, we need some statements for for than the lowest universe. Therefore,
we choose to be more careful about universe levels.
-}

Trunc : ∀ {i} → Type i → Type i
Trunc = library.types.Truncation.Trunc ⟨-1⟩

h-tr : ∀ {i} → (X : Type i) → is-prop (Trunc X)
h-tr X = Trunc-level

∣_∣ : ∀ {i} → {X : Type i} → X → Trunc X
∣_∣ = [_]

rec : ∀ {i j} → {X : Type i} → {P : Type j} → (is-prop P) → (X → P) → Trunc X → P
rec = Trunc-rec

ind : ∀ {i j} → {X : Type i} → {P : Trunc X → Type j} → ((z : Trunc X) → is-prop (P z)) → ((x : X) → P ∣ x ∣) → (z : Trunc X) → P z
ind = Trunc-elim

-- Subsection 8.1

-- Theorem 8.1
interval : Type₀
interval = Trunc Bool

i₁ : interval
i₁ = ∣ true ∣

i₂ : interval
i₂ = ∣ false ∣

seg : i₁ == i₂
seg = prop-has-all-paths (h-tr _) _ _

-- We prove that the interval has the "correct" recursion principle:
module interval {i} {Y : Type i} (y₁ y₂ : Y) (p : y₁ == y₂) where

  g : Bool → Σ Y λ y → y₁ == y
  g true = (y₁ , idp)
  g false = (y₂ , p)

  ĝ : interval → Σ Y λ y → y₁ == y
  ĝ = rec (contr-is-prop (pathfrom-is-contr _)) g

  f : interval → Y
  f = fst ∘ ĝ

  f-i₁ : f i₁ == y₁
  f-i₁ = idp

  f-i₂ : f i₂ == y₂
  f-i₂ = idp

  f-seg : ap f seg == p
  f-seg =
    ap f seg                  =⟨ idp ⟩
    ap (fst ∘ ĝ) seg          =⟨ ! (∘-ap _ _ _) ⟩
    (ap fst) (ap ĝ seg)       =⟨ ap (ap fst) (prop-has-all-paths (contr-is-set (pathfrom-is-contr _) _ _) _ _) ⟩
    (ap fst) (pair= p po-aux) =⟨ fst=-β p _ ⟩
    p                         ∎ where
      po-aux : idp == p [ _==_ y₁ ↓ p ]
      po-aux = from-transp (_==_ y₁) p (trans-pathfrom p idp)

-- Everything again outside the module:

interval-rec : ∀ {i} → {Y : Type i} → (y₁ y₂ : Y) → (p : y₁ == y₂) → (interval → Y)
interval-rec  = interval.f

interval-rec-i₁ : ∀ {i} → {Y : Type i} → (y₁ y₂ : Y) → (p : y₁ == y₂) → (interval-rec y₁ y₂ p) i₁ == y₁
interval-rec-i₁ = interval.f-i₁  -- or: λ _ _ _ → idp

interval-rec-i₂ : ∀ {i} →  {Y : Type i} → (y₁ y₂ : Y) → (p : y₁ == y₂) → (interval-rec y₁ y₂ p) i₂ == y₂
interval-rec-i₂ = interval.f-i₂  -- or: λ _ _ _ → idp

interval-rec-seg : ∀ {i} → {Y : Type i} → (y₁ y₂ : Y) → (p : y₁ == y₂) → ap (interval-rec y₁ y₂ p) seg == p
interval-rec-seg = interval.f-seg

-- Subsection 8.2

-- Lemma 8.2 (Shulman) / Corollary 8.3
interval→funext : ∀ {i j} → {X : Type i} → {Y : Type j} → (f g : (X → Y)) → ((x : X) → f x == g x) → f == g
interval→funext {X = X} {Y = Y} f g hom = ap i-x seg where

  x-i : X → interval → Y
  x-i x = interval-rec (f x) (g x) (hom x)

  i-x : interval → X → Y
  i-x i x = x-i x i

-- Thus, function extensionality holds automatically.

open import library.types.Pi

-- Subsection 8.3

-- We use the definitions from Section 5, but we re-define them as our definition of "Trunc" has chanced
factors : ∀ {i j} → {X : Type i} → {Y : Type j} → (f : X → Y) → Type (lmax i j)
factors {X = X} {Y = Y} f = Σ (Trunc X → Y) λ f' → (x : X) → f' ∣ x ∣ == f x

-- Theorem 8.4 - note the line   proof' = λ _ → idp
judgmental-factorr : ∀ {i j} → {X : Type i} → {Y : Type j} → (f : X → Y) → factors f → factors f
judgmental-factorr {X = X} {Y = Y} f (f₂ , proof) = f' , proof' where

  g : X → (z : Trunc X) → Σ Y λ y → y == f₂ z
  g x = λ z → f x , f x     =⟨ ! (proof _) ⟩
                    f₂ ∣ x ∣ =⟨ ap f₂ (prop-has-all-paths (h-tr _) _ _) ⟩
                    f₂ z    ∎

  g-codom-prop : is-prop ((z : Trunc X) → Σ Y λ y → y == f₂ z)
  g-codom-prop = contr-is-prop (Π-level (λ z → pathto-is-contr _))

  ĝ : Trunc X → (z : Trunc X) → Σ Y λ y → y == f₂ z
  ĝ = rec g-codom-prop g

  f' : Trunc X → Y
  f' = λ z → fst (ĝ z z)

  proof' : (x : X) → f' ∣ x ∣ == f x
  proof' = λ _ → idp

-- Theorem 8.5 - we need the induction principle, but with that, it is actually simpler than the previous construction.
-- Still, it is nearly a replication.
factors-dep : ∀ {i j} → {X : Type i} → {Y : Trunc X → Type j} → (f : (x : X) → (Y ∣ x ∣)) → Type (lmax i j)
factors-dep {X = X} {Y = Y} f = Σ ((z : Trunc X) → Y z) λ f₂ → ((x : X) → f x == f₂ ∣ x ∣)

judgmental-factorr-dep : ∀ {i j} → {X : Type i} → {Y : Trunc X → Type j}
  → (f : (x : X) → Y ∣ x ∣) → factors-dep {X = X} {Y = Y} f → factors-dep {X = X} {Y = Y} f
judgmental-factorr-dep {X = X} {Y = Y} f (f₂ , proof) = f' , proof' where

  g : (x : X) → Σ (Y ∣ x ∣) λ y → y == f₂ ∣ x ∣
  g x = f x , proof x

  g-codom-prop : (z : Trunc X) → is-prop (Σ (Y z) λ y → y == f₂ z)
  g-codom-prop z = contr-is-prop (pathto-is-contr _)

  ĝ : (z : Trunc X) →  Σ (Y z) λ y → y == f₂ z
  ĝ = ind g-codom-prop g

  f' : (z : Trunc X) → Y z
  f' = fst ∘ ĝ

  proof' : (x : X) → f' ∣ x ∣ == f x
  proof' x = idp

-- Subsection 8.4

-- The content of this section is partially taken from an earlier formalization by the first-named author;
-- see
--
--       http://homotopytypetheory.org/2013/10/28/
--
-- for a discussion and
--
--       http://red.cs.nott.ac.uk/~ngk/html-trunc-inverse/trunc-inverse.html
--
-- for a formalization (the slightly simpler formalization that is mentioned in the article).

-- Definition 8.6
-- Pointed types
Type• : ∀ {i} → Type (lsucc i)
Type• {i} = Σ (Type i) (idf _)

module _ {i} (X : Type• {i}) where
  base = fst X
  pt   = snd X

  -- We have already used the pathto-types a couple of times.
  -- Let's introduce a name for those that work with pointed types:
  pathto : Type (lsucc i)
  pathto = Σ (Type• {i}) (λ Y → Y == X)

  -- As it is well-known, these type is contractible and thereby propositional:
  pathto-prop : is-prop pathto
  pathto-prop = contr-is-prop (pathto-is-contr X)

-- Definition 8.7
is-transitive : ∀ {i} → Type i → Type (lsucc i)
is-transitive {i} X = (x₁ x₂ : X) → _==_ {A = Type•} (X , x₁) (X , x₂)

-- Example 8.8
module dec-trans {i} (X : Type i) (dec : has-dec-eq X) where

  module _ (x₁ x₂ : X) where

    -- I define a function X → X that switches x and x₀.
    switch : X → X
    switch = λ y → match dec y x₁
                     withl (λ _ → x₂)
                     withr (λ _ → match dec y x₂
                                    withl (λ _ → x₁)
                                    withr (λ _ → y))

    -- Rather tedious to prove, but completely straightforward:
    -- this map is its own inverse.
    switch-selfinverse : (y : X) → switch (switch y) == y
    switch-selfinverse y with dec y x₁
    switch-selfinverse y | inl _ with dec x₂ x₁
    switch-selfinverse y | inl y-x₁  | inl x-x₁ = x-x₁ ∙ ! y-x₁
    switch-selfinverse y | inl _     | inr _ with dec x₂ x₂
    switch-selfinverse y | inl y-x₁  | inr _     | inl _ = ! y-x₁
    switch-selfinverse y | inl _     | inr _     | inr ¬x₂-x₂ = Empty-elim {A = λ _ → x₂ == y} (¬x₂-x₂ idp)
    switch-selfinverse y | inr _ with dec y x₂
    switch-selfinverse y | inr _     | inl _ with dec x₂ x₁
    switch-selfinverse y | inr ¬x₂-x₁ | inl y-x₂  | inl x₂-x₁ = Empty-elim (¬x₂-x₁ (y-x₂ ∙ x₂-x₁))
    switch-selfinverse y | inr _     | inl _     | inr _ with dec x₁ x₁
    switch-selfinverse y | inr _     | inl y-x₂  | inr _ | inl _ = ! y-x₂
    switch-selfinverse y | inr _     | inl _     | inr _ | inr ¬x₁-x₁ = Empty-elim {A = λ _ → _ == y} (¬x₁-x₁ idp)
    switch-selfinverse y | inr _     | inr _ with dec y x₁
    switch-selfinverse y | inr ¬y-x₁ | inr _     | inl y-x₁ = Empty-elim {A = λ _ → x₂ == y} (¬y-x₁ y-x₁)
    switch-selfinverse y | inr _     | inr _     | inr _  with dec y x₂
    switch-selfinverse y | inr _     | inr ¬y-x₂ | inr _ | inl y-x₂ = Empty-elim {A = λ _ → x₁ == y} (¬y-x₂ y-x₂)
    switch-selfinverse y | inr _     | inr _     | inr _ | inr _ = idp

    switch-maps : switch x₂ == x₁
    switch-maps with dec x₂ x₁
    switch-maps | inl x₂-x₁ = x₂-x₁
    switch-maps | inr _ with dec x₂ x₂
    switch-maps | inr _ | inl _ = idp
    switch-maps | inr _ | inr ¬x-x = Empty-elim {A = λ _ → x₂ == x₁} (¬x-x idp)

    -- switch is an equivalence
    switch-eq : X ≃ X
    switch-eq = equiv switch switch
                      switch-selfinverse switch-selfinverse

  -- X is transitive:
  is-trans : is-transitive X
  is-trans x₁ x₂  = pair= (ua X-X) x₁-x₂ where
    X-X : X ≃ X
    X-X = switch-eq x₂ x₁
    x₁-x₂ : PathOver (idf (Type i)) (ua X-X) x₁ x₂
    x₁-x₂ = ↓-idf-ua-in X-X (switch-maps x₂ x₁)

-- Example 8.8 addendum: ℕ is transitive.
open import library.types.Nat

ℕ-trans : is-transitive ℕ
ℕ-trans = dec-trans.is-trans ℕ ℕ-has-dec-eq

-- Example 9.9
-- (Note that this does not need the univalence axiom)

-- preparation
path-trans-aux : ∀ {i} → (X : Type i) → (x₁ x₂ x₃ : X) → (x₂ == x₃)
  → (p₁₂ : x₁ == x₂) → (p₁₃ : x₁ == x₃) → _==_ {A = Type•} (x₁ == x₂ , p₁₂) (x₁ == x₃ , p₁₃)
path-trans-aux X x₁ .x₁ .x₁ p idp idp = idp

-- the lemma
path-trans : ∀ {i} → (X : Type i) → (x₁ x₂ : X) → is-transitive (x₁ == x₂)
path-trans X x₁ x₂ = path-trans-aux X x₁ x₂ x₂ idp

-- In particular, the lemma works for loop spaces.
-- We define them as follows:
Ω : ∀ {i} → Type• {i} → Type• {i}
Ω (X , x) = (x == x , idp)

-- We choose precomposition here - whether the function exponentiation operator is more
-- convenient to use with pre- or postcomposition depends on the concrete case.
infix 10 _^_
_^_ : ∀ {i} {A : Set i} → (A → A) → ℕ → A → A
f ^ 0   = idf _
f ^ S n = f ∘ f ^ n

loop-trans : ∀ {i} → (X : Type• {i}) → (n : ℕ) → is-transitive (fst ((Ω ^ (1 + n)) X))
loop-trans {i} X n = path-trans type point point where

  type : Type i
  type = fst ((Ω ^ n) X)

  point : type
  point = snd ((Ω ^ n) X)

-- Example 8.10 and 8.11
-- (not formalized)

module constr-myst {i} (X : Type i) (x₀ : X) (t : is-transitive X) where

  f : X → Type• {i}
  f x = (X , x)

  f'' : Trunc X → Type• {i}
  f'' _ = (X , x₀)

  f-fact : factors f
  f-fact = f'' , (λ x → t x₀ x)

  f' : Trunc X → Type• {i}
  f' = fst (judgmental-factorr f f-fact)

-- Theorem 9.12
-- the myst function:
  myst : (z : Trunc X) → fst (f' z)
  myst = snd ∘ f'

  check : (x : X) → myst ∣ x ∣ == x
  check x = idp

  myst-∣_∣-is-id : myst ∘ ∣_∣ == idf X
  myst-∣_∣-is-id = λ= λ x → idp

-- Let us do it explicitly for ℕ:
open import library.types.Nat

myst-ℕ = constr-myst.myst ℕ 0 (dec-trans.is-trans ℕ ℕ-has-dec-eq)

myst-∣_∣-is-id : (n : ℕ) → myst-ℕ ∣ n ∣ == n
myst-∣_∣-is-id n = idp

test : myst-ℕ ∣ 17 ∣ == 17
test = idp

ext: agda

max_stars_repo_name: nicolaikraus/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
open import Prelude

module Implicits.Semantics.RewriteContext where

open import Implicits.Syntax
open import Implicits.Substitutions
open import Implicits.Substitutions.Lemmas

open import Data.Vec
open import Data.List.All as All
open import Extensions.Vec

-- rewrite context (relation between implicit and explicit context)
_#_ : ∀ {ν n} (Γ : Ctx ν n) (Δ : ICtx ν) → Set
Γ # Δ = All (λ i → i ∈ Γ) Δ

K# : ∀ {ν n} (K : Ktx ν n) → Set
K# (Γ , Δ) = Γ # Δ

#tvar : ∀ {ν n} {K : Ktx ν n} → K# K → K# (ktx-weaken K)
#tvar All.[] = All.[]
#tvar (px All.∷ K#K) = (∈⋆map px (λ t → t tp/tp TypeLemmas.wk)) All.∷ (#tvar K#K)

#var : ∀ {ν n} {K : Ktx ν n} → (a : Type ν) → K# K → K# (a ∷Γ K)
#var a All.[] = All.[]
#var a (px All.∷ K#K) = there px All.∷ (#var a K#K)

#ivar : ∀ {ν n} {K : Ktx ν n} → (a : Type ν) → K# K → K# (a ∷K K)
#ivar a K#K = here All.∷ (All.map there K#K)


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

module _ where

open import Agda.Primitive using (Level)

variable
 l : Level

postulate
  Σ : {l' : Level}{X : Set} (Y : X → Set l') -> Set
  _,_ : {l' : Level}{X : Set} {Y : X → Set l'} -> (x : X)(y : Y x) -> Σ Y
  is-universal-element : {l' : Level}{X : Set} {A : X → Set l'} -> Σ A → Set

  universality-section : {X : Set} {A : X → Set l}  -> (x : X) (a : A x)
                          → is-universal-element {X = X} (x , a)

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
open import Auto.Core
open import Data.List    using (_∷_; []; length)
open import Data.Nat     using (ℕ; zero; suc)
open import Data.Product using (_,_)
open import Data.Sum     using (inj₁; inj₂)
open import Reflection   using (Term; Name; lam; visible; abs; TC; returnTC; bindTC)

module Auto.Extensible (instHintDB : IsHintDB) where

open IsHintDB     instHintDB public
open PsExtensible instHintDB public
open Auto.Core               public using (dfs; bfs; Exception; throw; searchSpaceExhausted; unsupportedSyntax)

auto : Strategy → ℕ → HintDB → Term → TC Term
auto search depth db type
  with agda2goal×premises type
... | inj₁ msg = returnTC (quoteError msg)
... | inj₂ ((n , g) , args)
  with search (suc depth) (solve g (fromRules args ∙ db))
... | []      = returnTC (quoteError searchSpaceExhausted)
... | (p ∷ _) = bindTC (reify p) (λ rp → returnTC (intros rp))
  where
    intros : Term → Term
    intros = introsAcc (length args)
      where
        introsAcc : ℕ → Term → Term
        introsAcc  zero   t = t
        introsAcc (suc k) t = lam visible (abs "TODO" (introsAcc k t))

infixl 5 _<<_

_<<_ : HintDB → Name → TC HintDB
db << n = bindTC (name2rule n) (λ
  {(inj₁ msg) → returnTC db
  ; (inj₂ (k , r)) → returnTC (db ∙ return r)})
-- db << n with (name2rule n)
-- db << n | inj₁ msg     = db
-- db << n | inj₂ (k , r) = db ∙ return r

max_stars_repo_name: wenkokke/AutoInAgda

max_issues_repo_name: wenkokke/AutoInAgda

max_forks_repo_name: wenkokke/AutoInAgda


text:
module Issue4267.A1 where

record RA1 : Set₁ where
  field
    A : Set

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
module consoleExamples.helloWorld where

open import ConsoleLib

main : ConsoleProg
main = run (WriteString "Hello World")

max_stars_repo_name: agda/ooAgda

max_issues_repo_name: agda/ooAgda

max_forks_repo_name: agda/ooAgda


text:
module Prelude.Smashed where

open import Prelude.Equality
open import Prelude.Unit
open import Prelude.Empty
open import Prelude.Nat.Core
open import Prelude.Function
open import Prelude.Ord

record Smashed {a} (A : Set a) : Set a where
  field
    smashed : ∀ {x y : A} → x ≡ y

open Smashed {{...}} public
{-# DISPLAY Smashed.smashed _ = smashed #-}

instance
  Smash⊤ : Smashed ⊤
  smashed {{Smash⊤}} = refl

  Smash⊥ : Smashed ⊥
  smashed {{Smash⊥}} {}

  Smash≡ : ∀ {a} {A : Set a} {a b : A} → Smashed (a ≡ b)
  smashed {{Smash≡}} {x = refl} {refl} = refl

-- Can't be instance, since this would interfere with the ⊤ and ⊥ instances.
SmashNonZero : ∀ {n : Nat} → Smashed (NonZero n)
SmashNonZero {zero}  = it
SmashNonZero {suc n} = it

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


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

open import Agda.Builtin.Cubical.Path
open import Agda.Primitive

private
  variable
    a   : Level
    A B : Set a

Is-proposition : Set a → Set a
Is-proposition A = (x y : A) → x ≡ y

data ∥_∥ (A : Set a) : Set a where
  ∣_∣        : A → ∥ A ∥
  @0 trivial : Is-proposition ∥ A ∥

rec : @0 Is-proposition B → (A → B) → ∥ A ∥ → B
rec p f ∣ x ∣           = f x
rec p f (trivial x y i) = p (rec p f x) (rec p f y) i

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
{-# OPTIONS --without-K --safe #-}
open import Categories.Category

module Categories.Object.Product.Core {o ℓ e} (𝒞 : Category o ℓ e) where

open import Level
open import Function using (flip; _$_)

open import Categories.Morphism 𝒞
open import Categories.Morphism.Reasoning 𝒞

open Category 𝒞
open HomReasoning

private
  variable
    A B C D X Y Z : Obj
    h i j : A ⇒ B

-- Borrowed from Dan Doel's definition of products
record Product (A B : Obj) : Set (o ⊔ ℓ ⊔ e) where

  infix 10 ⟨_,_⟩

  field
    A×B   : Obj
    π₁    : A×B ⇒ A
    π₂    : A×B ⇒ B
    ⟨_,_⟩ : C ⇒ A → C ⇒ B → C ⇒ A×B

    project₁ : π₁ ∘ ⟨ h , i ⟩ ≈ h
    project₂ : π₂ ∘ ⟨ h , i ⟩ ≈ i
    unique   : π₁ ∘ h ≈ i → π₂ ∘ h ≈ j → ⟨ i , j ⟩ ≈ h

  g-η : ⟨ π₁ ∘ h , π₂ ∘ h ⟩ ≈ h
  g-η = unique refl refl

  η : ⟨ π₁ , π₂ ⟩ ≈ id
  η = unique identityʳ identityʳ

  ⟨⟩-cong₂ : ∀ {f f′ : C ⇒ A} {g g′ : C ⇒ B} → f ≈ f′ → g ≈ g′ → ⟨ f , g ⟩ ≈ ⟨ f′ , g′ ⟩
  ⟨⟩-cong₂ f≡f′ g≡g′ = unique (project₁ ○ ⟺ f≡f′) (project₂ ○ ⟺ g≡g′)

  ∘-distribʳ-⟨⟩ : ∀ {f : C ⇒ A} {g : C ⇒ B} {q : D ⇒ C} → ⟨ f , g ⟩ ∘ q ≈ ⟨ f ∘ q , g ∘ q ⟩
  ∘-distribʳ-⟨⟩ = ⟺ $ unique (pullˡ project₁) (pullˡ project₂)

  unique′ : π₁ ∘ h ≈ π₁ ∘ i → π₂ ∘ h ≈ π₂ ∘ i → h ≈ i
  unique′ eq₁ eq₂ = trans (sym (unique eq₁ eq₂)) g-η

module _ {A B : Obj} where
  open Product {A} {B} renaming (⟨_,_⟩ to _⟨_,_⟩)

  repack : (p₁ p₂ : Product A B) → A×B p₁ ⇒ A×B p₂
  repack p₁ p₂ = p₂ ⟨ π₁ p₁ , π₂ p₁ ⟩

  repack∘ : (p₁ p₂ p₃ : Product A B) → repack p₂ p₃ ∘ repack p₁ p₂ ≈ repack p₁ p₃
  repack∘ p₁ p₂ p₃ = ⟺ $ unique p₃
    (glueTrianglesʳ (project₁ p₃) (project₁ p₂))
    (glueTrianglesʳ (project₂ p₃) (project₂ p₂))

  repack≡id : (p : Product A B) → repack p p ≈ id
  repack≡id = η

  repack-cancel : (p₁ p₂ : Product A B) → repack p₁ p₂ ∘ repack p₂ p₁ ≈ id
  repack-cancel p₁ p₂ = repack∘ p₂ p₁ p₂ ○ repack≡id p₂

up-to-iso : ∀ (p₁ p₂ : Product A B) → Product.A×B p₁ ≅ Product.A×B p₂
up-to-iso p₁ p₂ = record
  { from = repack p₁ p₂
  ; to   = repack p₂ p₁
  ; iso  = record
    { isoˡ = repack-cancel p₂ p₁
    ; isoʳ = repack-cancel p₁ p₂
    }
  }

transport-by-iso : ∀ (p : Product A B) → ∀ {X} → Product.A×B p ≅ X → Product A B
transport-by-iso p {X} p≅X = record
  { A×B = X
  ; π₁ = π₁ ∘ to
  ; π₂ = π₂ ∘ to
  ; ⟨_,_⟩ = λ h₁ h₂ → from ∘ ⟨ h₁ , h₂ ⟩
  ; project₁ = cancelInner isoˡ ○ project₁
  ; project₂ = cancelInner isoˡ ○ project₂
  ; unique = λ {_ i l r} pf₁ pf₂ → begin
    from ∘ ⟨ l , r ⟩                         ≈˘⟨ refl⟩∘⟨ ⟨⟩-cong₂ pf₁ pf₂ ⟩
    from ∘ ⟨ (π₁ ∘ to) ∘ i , (π₂ ∘ to) ∘ i ⟩ ≈⟨ refl⟩∘⟨ unique (⟺ assoc) (⟺ assoc) ⟩
    from ∘ to ∘ i                           ≈⟨ cancelˡ isoʳ ⟩
    i                                        ∎
  }
  where open Product p
        open _≅_ p≅X

Reversible : (p : Product A B) → Product B A
Reversible p = record
  { A×B       = A×B
  ; π₁        = π₂
  ; π₂        = π₁
  ; ⟨_,_⟩     = flip ⟨_,_⟩
  ; project₁  = project₂
  ; project₂  = project₁
  ; unique = flip unique
  }
  where open Product p

Commutative : (p₁ : Product A B) (p₂ : Product B A) → Product.A×B p₁ ≅ Product.A×B p₂
Commutative p₁ p₂ = up-to-iso p₁ (Reversible p₂)

Associable : ∀ (p₁ : Product X Y) (p₂ : Product Y Z) (p₃ : Product X (Product.A×B p₂)) → Product (Product.A×B p₁) Z
Associable p₁ p₂ p₃ = record
  { A×B       = A×B p₃
  ; π₁        = p₁ ⟨ π₁ p₃ , π₁ p₂ ∘ π₂ p₃ ⟩
  ; π₂        = π₂ p₂ ∘ π₂ p₃
  ; ⟨_,_⟩     = λ f g → p₃ ⟨ π₁ p₁ ∘ f , p₂ ⟨ π₂ p₁ ∘ f , g ⟩ ⟩
  ; project₁  = λ {_ f g} → begin
    p₁ ⟨ π₁ p₃ , π₁ p₂ ∘ π₂ p₃ ⟩ ∘ p₃ ⟨ π₁ p₁ ∘ f , p₂ ⟨ π₂ p₁ ∘ f , g ⟩ ⟩ ≈⟨ ∘-distribʳ-⟨⟩ p₁ ⟩
    p₁ ⟨ π₁ p₃ ∘ p₃ ⟨ π₁ p₁ ∘ f , p₂ ⟨ π₂ p₁ ∘ f , g ⟩ ⟩
       , (π₁ p₂ ∘ π₂ p₃) ∘ p₃ ⟨ π₁ p₁ ∘ f , p₂ ⟨ π₂ p₁ ∘ f , g ⟩ ⟩ ⟩       ≈⟨ ⟨⟩-cong₂ p₁ (project₁ p₃) (glueTrianglesˡ (project₁ p₂) (project₂ p₃)) ⟩
    p₁ ⟨ π₁ p₁ ∘ f , π₂ p₁ ∘ f ⟩                                           ≈⟨ g-η p₁ ⟩
    f                                                                      ∎
  ; project₂  = λ {_ f g} → glueTrianglesˡ (project₂ p₂) (project₂ p₃)
  ; unique = λ {_ i f g} pf₁ pf₂ → begin
    p₃ ⟨ π₁ p₁ ∘ f , p₂ ⟨ π₂ p₁ ∘ f , g ⟩ ⟩             ≈⟨ ⟨⟩-cong₂ p₃ (∘-resp-≈ʳ (sym pf₁))
                                                          (⟨⟩-cong₂ p₂ (∘-resp-≈ʳ (sym pf₁)) (sym pf₂)) ⟩
    p₃ ⟨ π₁ p₁ ∘ p₁ ⟨ π₁ p₃ , π₁ p₂ ∘ π₂ p₃ ⟩ ∘ i
       , p₂ ⟨ π₂ p₁ ∘ p₁ ⟨ π₁ p₃ , π₁ p₂ ∘ π₂ p₃ ⟩ ∘ i
            , (π₂ p₂ ∘ π₂ p₃) ∘ i ⟩ ⟩                   ≈⟨ ⟨⟩-cong₂ p₃ (pullˡ (project₁ p₁))
                                                          (⟨⟩-cong₂ p₂ (trans (pullˡ (project₂ p₁)) assoc)
                                                                       assoc) ⟩
    p₃ ⟨ π₁ p₃ ∘ i
       , p₂ ⟨ π₁ p₂ ∘ π₂ p₃ ∘ i , π₂ p₂ ∘ π₂ p₃ ∘ i ⟩ ⟩ ≈⟨ ⟨⟩-cong₂ p₃ refl (g-η p₂) ⟩
    p₃ ⟨ π₁ p₃ ∘ i , π₂ p₃ ∘ i ⟩                        ≈⟨ g-η p₃ ⟩
    i                                                   ∎
  }
  where open Product renaming (⟨_,_⟩ to _⟨_,_⟩)

Associative : ∀ (p₁ : Product X Y) (p₂ : Product Y Z)
                (p₃ : Product X (Product.A×B p₂)) (p₄ : Product (Product.A×B p₁) Z) →
                (Product.A×B p₃) ≅ (Product.A×B p₄)
Associative p₁ p₂ p₃ p₄ = up-to-iso (Associable p₁ p₂ p₃) p₄

Mobile : ∀ {A₁ B₁ A₂ B₂} (p : Product A₁ B₁) → A₁ ≅ A₂ → B₁ ≅ B₂ → Product A₂ B₂
Mobile p A₁≅A₂ B₁≅B₂ = record
  { A×B              = A×B
  ; π₁               = from A₁≅A₂ ∘ π₁
  ; π₂               = from B₁≅B₂ ∘ π₂
  ; ⟨_,_⟩            = λ h k → ⟨ to A₁≅A₂ ∘ h , to B₁≅B₂ ∘ k ⟩
  ; project₁         = begin
    (from A₁≅A₂ ∘ π₁) ∘ ⟨ to A₁≅A₂ ∘ _ , to B₁≅B₂ ∘ _ ⟩ ≈⟨ pullʳ project₁ ⟩
    from A₁≅A₂ ∘ (to A₁≅A₂ ∘ _)                         ≈⟨ cancelˡ (isoʳ A₁≅A₂) ⟩
    _                                                   ∎
  ; project₂         = begin
    (from B₁≅B₂ ∘ π₂) ∘ ⟨ to A₁≅A₂ ∘ _ , to B₁≅B₂ ∘ _ ⟩ ≈⟨ pullʳ project₂ ⟩
    from B₁≅B₂ ∘ (to B₁≅B₂ ∘ _)                         ≈⟨ cancelˡ (isoʳ B₁≅B₂) ⟩
    _                                                   ∎
  ; unique        = λ pfˡ pfʳ → unique (switch-fromtoˡ A₁≅A₂ (⟺ assoc ○ pfˡ))
                                       (switch-fromtoˡ B₁≅B₂ (⟺ assoc ○ pfʳ))
  }
  where open Product p
        open _≅_

max_stars_repo_name: Taneb/agda-categories

max_issues_repo_name: Taneb/agda-categories

max_forks_repo_name: Taneb/agda-categories


text:
module _ where

open import Agda.Builtin.Nat

postulate
  F : Set → Set
  pure : ∀ {A} → A → F A
  -- _<*>_ : ∀ {A B} → F (A → B) → F A → F B

fail : F Nat → F Nat
fail a = (| suc a |)


text:
postulate
  A : Set

f : (B : Set) → B → A
f A a = a

-- Expected error:
-- A !=< A of type Set
-- (because one is a variable and one a defined identifier)
-- when checking that the expression a has type A

max_stars_repo_name: alhassy/agda

max_issues_repo_name: alhassy/agda

max_forks_repo_name: alhassy/agda


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

module FFI.Data.Aeson where

open import Agda.Builtin.Equality using (_≡_)
open import Agda.Builtin.Equality.Rewrite using ()
open import Agda.Builtin.Bool using (Bool)
open import Agda.Builtin.String using (String)

open import FFI.Data.ByteString using (ByteString)
open import FFI.Data.HaskellString using (HaskellString; pack)
open import FFI.Data.Maybe using (Maybe; just; nothing)
open import FFI.Data.Either using (Either; mapL)
open import FFI.Data.Scientific using (Scientific)
open import FFI.Data.Vector using (Vector)

open import Properties.Equality using (_≢_)

{-# FOREIGN GHC import qualified Data.Aeson #-}
{-# FOREIGN GHC import qualified Data.Aeson.Key #-}
{-# FOREIGN GHC import qualified Data.Aeson.KeyMap #-}

postulate
  KeyMap : Set → Set
  Key : Set
  fromString : String → Key
  toString : Key → String
  empty : ∀ {A} → KeyMap A
  singleton : ∀ {A} → Key → A → (KeyMap A)
  insert : ∀ {A} → Key → A → (KeyMap A) → (KeyMap A)
  delete : ∀ {A} → Key → (KeyMap A) → (KeyMap A)
  unionWith : ∀ {A} → (A → A → A) → (KeyMap A) → (KeyMap A) → (KeyMap A)
  lookup : ∀ {A} → Key -> KeyMap A -> Maybe A
{-# POLARITY KeyMap ++ #-}
{-# COMPILE GHC KeyMap = type Data.Aeson.KeyMap.KeyMap #-}
{-# COMPILE GHC Key = type Data.Aeson.Key.Key #-}
{-# COMPILE GHC fromString = Data.Aeson.Key.fromText #-}
{-# COMPILE GHC toString = Data.Aeson.Key.toText #-}
{-# COMPILE GHC empty = \_ -> Data.Aeson.KeyMap.empty #-}
{-# COMPILE GHC singleton = \_ -> Data.Aeson.KeyMap.singleton #-}
{-# COMPILE GHC insert = \_ -> Data.Aeson.KeyMap.insert #-}
{-# COMPILE GHC delete = \_ -> Data.Aeson.KeyMap.delete #-}
{-# COMPILE GHC unionWith = \_ -> Data.Aeson.KeyMap.unionWith #-}
{-# COMPILE GHC lookup = \_ -> Data.Aeson.KeyMap.lookup #-}

postulate lookup-insert : ∀ {A} k v (m : KeyMap A) → (lookup k (insert k v m) ≡ just v)
postulate lookup-empty : ∀ {A} k → (lookup {A} k empty ≡ nothing)
postulate lookup-insert-not : ∀ {A} j k v (m : KeyMap A) → (j ≢ k) → (lookup k m ≡ lookup k (insert j v m))
postulate singleton-insert-empty : ∀ {A} k (v : A) → (singleton k v ≡ insert k v empty)
postulate insert-swap : ∀ {A} j k (v w : A) m → (j ≢ k) → insert j v (insert k w m) ≡ insert k w (insert j v m)
postulate insert-over : ∀ {A} j k (v w : A) m → (j ≡ k) → insert j v (insert k w m) ≡ insert j v m
postulate to-from : ∀ k → toString(fromString k) ≡ k
postulate from-to : ∀ k → fromString(toString k) ≡ k

{-# REWRITE lookup-insert lookup-empty singleton-insert-empty #-}

data Value : Set where
  object : KeyMap Value → Value
  array : Vector Value → Value
  string : String → Value
  number : Scientific → Value
  bool : Bool → Value
  null : Value
{-# COMPILE GHC Value = data Data.Aeson.Value (Data.Aeson.Object|Data.Aeson.Array|Data.Aeson.String|Data.Aeson.Number|Data.Aeson.Bool|Data.Aeson.Null) #-}

Object = KeyMap Value
Array = Vector Value

postulate
  decode : ByteString → Maybe Value
  eitherHDecode : ByteString → Either HaskellString Value
{-# COMPILE GHC decode = Data.Aeson.decodeStrict #-}
{-# COMPILE GHC eitherHDecode = Data.Aeson.eitherDecodeStrict #-}

eitherDecode : ByteString → Either String Value
eitherDecode bytes = mapL pack (eitherHDecode bytes)

max_stars_repo_name: TheGreatSageEqualToHeaven/luau

max_issues_repo_name: TheGreatSageEqualToHeaven/luau

max_forks_repo_name: TheGreatSageEqualToHeaven/luau


text:
import cedille-options
module elaboration-helpers (options : cedille-options.options) where

open import lib
open import monad-instances
open import general-util
open import cedille-types
open import syntax-util
open import ctxt
open import conversion
open import constants
open import to-string options
open import subst
open import rename
open import is-free
open import toplevel-state options {id}
open import spans options {id}
open import datatype-functions
open import templates
open import erase

uncurry' : ∀ {A B C D : Set} → (A → B → C → D) → (A × B × C) → D
uncurry' f (a , b , c) = f a b c

uncurry'' : ∀ {A B C D E : Set} → (A → B → C → D → E) → (A × B × C × D) → E
uncurry'' f (a , b , c , d) = f a b c d

uncurry''' : ∀ {A B C D E F : Set} → (A → B → C → D → E → F) → (A × B × C × D × E) → F
uncurry''' f (a , b , c , d , e) = f a b c d e

ctxt-term-decl' : posinfo → var → type → ctxt → ctxt
ctxt-term-decl' pi x T (mk-ctxt (fn , mn , ps , q) ss is os Δ) =
  mk-ctxt (fn , mn , ps , trie-insert q x (x , [])) ss
    (trie-insert is x (term-decl T , fn , pi)) os Δ

ctxt-type-decl' : posinfo → var → kind → ctxt → ctxt
ctxt-type-decl' pi x k (mk-ctxt (fn , mn , ps , q) ss is os Δ) =
  mk-ctxt (fn , mn , ps , trie-insert q x (x , [])) ss
    (trie-insert is x (type-decl k , fn , pi)) os Δ

ctxt-tk-decl' : posinfo → var → tk → ctxt → ctxt
ctxt-tk-decl' pi x (Tkt T) = ctxt-term-decl' pi x T
ctxt-tk-decl' pi x (Tkk k) = ctxt-type-decl' pi x k

ctxt-param-decl : var → var → tk → ctxt → ctxt
ctxt-param-decl x x' atk Γ @ (mk-ctxt (fn , mn , ps , q) ss is os Δ) =
  let d = case atk of λ {(Tkt T) → term-decl T; (Tkk k) → type-decl k} in
  mk-ctxt
  (fn , mn , ps , trie-insert q x (x , [])) ss
  (trie-insert is x' (d , fn , pi-gen)) os Δ

ctxt-term-def' : var → var → term → type → opacity → ctxt → ctxt
ctxt-term-def' x x' t T op Γ @ (mk-ctxt (fn , mn , ps , q) ss is os Δ) = mk-ctxt
  (fn , mn , ps , qualif-insert-params q (mn # x) x ps) ss
  (trie-insert is x' (term-def (just ps) op (just $ hnf Γ unfold-head t tt) T , fn , x)) os Δ

ctxt-type-def' : var → var → type → kind → opacity → ctxt → ctxt
ctxt-type-def' x x' T k op Γ @ (mk-ctxt (fn , mn , ps , q) ss is os Δ) = mk-ctxt
  (fn , mn , ps , qualif-insert-params q (mn # x) x ps) ss
  (trie-insert is x' (type-def (just ps) op (just $ hnf Γ (unfolding-elab unfold-head) T tt) k , fn , x)) os Δ

ctxt-let-term-def : posinfo → var → term → type → ctxt → ctxt
ctxt-let-term-def pi x t T Γ @ (mk-ctxt (fn , mn , ps , q) ss is os Δ) =
  mk-ctxt (fn , mn , ps , trie-insert q x (x , [])) ss
    (trie-insert is x (term-def nothing OpacTrans (just $ hnf Γ unfold-head t tt) T , fn , pi)) os Δ

ctxt-let-type-def : posinfo → var → type → kind → ctxt → ctxt
ctxt-let-type-def pi x T k Γ @ (mk-ctxt (fn , mn , ps , q) ss is os Δ) =
  mk-ctxt (fn , mn , ps , trie-insert q x (x , [])) ss
    (trie-insert is x (type-def nothing OpacTrans (just $ hnf Γ (unfolding-elab unfold-head) T tt) k , fn , pi)) os Δ
{-
ctxt-μ-out-def : var → term → term → var → ctxt → ctxt
ctxt-μ-out-def x t c y (mk-ctxt mod ss is os Δ) =
  let is' = is --trie-insert is y (term-udef nothing OpacTrans c , "missing" , "missing")
      is'' = trie-insert is' x (term-udef nothing OpacTrans t , y , y) in
  mk-ctxt mod ss is'' os Δ
-}

ctxt-datatype-decl' : var → var → var → args → ctxt → ctxt
ctxt-datatype-decl' X isType/v Type/v as Γ@(mk-ctxt (fn , mn , ps , q) ss is os (Δ , μ' , μ)) =
  mk-ctxt (fn , mn , ps , q) ss is os $ Δ , trie-insert μ' Type/v (X , isType/v , as) , μ
  --mk-ctxt (fn , mn , ps , q) ss (trie-insert is ("/" ^ Type/v) $ rename-def ("/" ^ X) , "missing" , "missing") os $ Δ , trie-insert μ' Type/v (X , isType/v , as) , μ

{-
ctxt-rename-def' : var → var → args → ctxt → ctxt
ctxt-rename-def' x x' as (mk-ctxt (fn , mn , ps , q) ss is os Δ) = mk-ctxt (fn , mn , ps , trie-insert q x (x' , as)) ss (trie-insert is x (rename-def x' , "missing" , "missing")) os Δ
-}

ctxt-kind-def' : var → var → params → kind → ctxt → ctxt
ctxt-kind-def' x x' ps2 k Γ @ (mk-ctxt (fn , mn , ps1 , q) ss is os Δ) = mk-ctxt
  (fn , mn , ps1 , qualif-insert-params q (mn # x) x ps1) ss
  (trie-insert is x' (kind-def (ps1 ++ qualif-params Γ ps2) k' , fn , pi-gen)) os Δ
  where
  k' = hnf Γ (unfolding-elab unfold-head) k tt

{-
ctxt-datatype-def' : var → var → params → kind → kind → ctrs → ctxt → ctxt
ctxt-datatype-def' x x' psᵢ kᵢ k cs Γ@(mk-ctxt (fn , mn , ps , q) ss is os (Δ , μₓ)) = mk-ctxt
  (fn , mn , ps , q') ss
  (trie-insert is x' (type-def (just $ ps ++ psᵢ) OpacTrans nothing k , fn , x)) os
  (trie-insert Δ x' (ps ++ psᵢ , kᵢ , k , cs) , μₓ)
  where
  q' = qualif-insert-params q x x' ps
-}

ctxt-lookup-term-var' : ctxt → var → maybe type
ctxt-lookup-term-var' Γ @ (mk-ctxt (fn , mn , ps , q) ss is os Δ) x =
  env-lookup Γ x ≫=maybe λ where
    (term-decl T , _) → just T
    (term-def ps _ _ T , _ , x') →
      let ps = maybe-else [] id ps in
      just $ abs-expand-type ps T
    _ → nothing

-- TODO: Could there be parameter/argument clashes if the same parameter variable is defined multiple times?
-- TODO: Could variables be parameter-expanded multiple times?
ctxt-lookup-type-var' : ctxt → var → maybe kind
ctxt-lookup-type-var' Γ @ (mk-ctxt (fn , mn , ps , q) ss is os Δ) x =
  env-lookup Γ x ≫=maybe λ where
    (type-decl k , _) → just k
    (type-def ps _ _ k , _ , x') →
      let ps = maybe-else [] id ps in
      just $ abs-expand-kind ps k
    _ → nothing

subst-qualif : ∀ {ed : exprd} → ctxt → renamectxt → ⟦ ed ⟧ → ⟦ ed ⟧
subst-qualif{TERM} Γ ρₓ = subst-renamectxt Γ ρₓ ∘ qualif-term Γ
subst-qualif{TYPE} Γ ρₓ = subst-renamectxt Γ ρₓ ∘ qualif-type Γ
subst-qualif{KIND} Γ ρₓ = subst-renamectxt Γ ρₓ ∘ qualif-kind Γ
subst-qualif Γ ρₓ = id

rename-validify : string → string
rename-validify = 𝕃char-to-string ∘ (h ∘ string-to-𝕃char) where
  validify-char : char → 𝕃 char
  validify-char '/' = [ '-' ]
  validify-char c with
    (c =char 'a')  ||
    (c =char 'z')  ||
    (c =char 'A')  ||
    (c =char 'Z')  ||
    (c =char '\'') ||
    (c =char '-')  ||
    (c =char '_')  ||
    is-digit c     ||
    (('a' <char c) && (c <char 'z')) ||
    (('A' <char c) && (c <char 'Z'))
  ...| tt = [ c ]
  ...| ff = 'Z' :: string-to-𝕃char (ℕ-to-string (toNat c)) ++ [ 'Z' ]
  h : 𝕃 char → 𝕃 char
  h [] = []
  h (c :: cs) = validify-char c ++ h cs

-- Returns a fresh variable name by adding primes and replacing invalid characters
fresh-var' : string → (string → 𝔹) → renamectxt → string
fresh-var' = fresh-var ∘ rename-validify

rename-new_from_for_ : ∀ {X : Set} → var → ctxt → (var → X) → X
rename-new ignored-var from Γ for f = f $ fresh-var' "x" (ctxt-binds-var Γ) empty-renamectxt
rename-new x from Γ for f = f $ fresh-var' x (ctxt-binds-var Γ) empty-renamectxt

rename_from_for_ : ∀ {X : Set} → var → ctxt → (var → X) → X
rename ignored-var from Γ for f = f ignored-var
rename x from Γ for f = f $ fresh-var' x (ctxt-binds-var Γ) empty-renamectxt

fresh-id-term : ctxt → term
fresh-id-term Γ = rename "x" from Γ for λ x → mlam x $ mvar x

get-renaming : renamectxt → var → var → var × renamectxt
get-renaming ρₓ xₒ x = let x' = fresh-var' x (renamectxt-in-range ρₓ) ρₓ in x' , renamectxt-insert ρₓ xₒ x'

rename_-_from_for_ : ∀ {X : Set} → var → var → renamectxt → (var → renamectxt → X) → X
rename xₒ - ignored-var from ρₓ for f = f ignored-var ρₓ
rename xₒ - x from ρₓ for f = uncurry f $ get-renaming ρₓ xₒ x

rename_-_lookup_for_ : ∀ {X : Set} → var → var → renamectxt → (var → renamectxt → X) → X
rename xₒ - x lookup ρₓ for f with renamectxt-lookup ρₓ xₒ
...| nothing = rename xₒ - x from ρₓ for f
...| just x' = f x' ρₓ

qualif-new-var : ctxt → var → var
qualif-new-var Γ x = ctxt-get-current-modname Γ # x

ctxt-datatype-def' : var → var → var → params → kind → kind → ctrs → ctxt → ctxt
ctxt-datatype-def' v Is/v is/v psᵢ kᵢ k cs Γ@(mk-ctxt (fn , mn , ps , q) ss i os (Δ , μ' , μ)) =
  mk-ctxt (fn , mn , ps , q) ss i os
    (trie-insert Δ v (ps ++ psᵢ , kᵢ , k , cs) ,
     trie-insert μ' elab-mu-prev-key (v , is/v , []) ,
     trie-insert μ Is/v v)

mbeta : term → term → term
mrho : term → var → type → term → term
mtpeq : term → term → type
mbeta t t' = Beta pi-gen (SomeTerm t pi-gen) (SomeTerm t' pi-gen)
mrho t x T t' = Rho pi-gen RhoPlain NoNums t (Guide pi-gen x T) t'
mtpeq t1 t2 = TpEq pi-gen t1 t2 pi-gen
{-
subst-args-params : ctxt → args → params → kind → kind
subst-args-params Γ (ArgsCons (TermArg _ t) ys) (ParamsCons (Decl _ _ _ x _ _) ps) k =
  subst-args-params Γ ys ps $ subst Γ t x k
subst-args-params Γ (ArgsCons (TypeArg t) ys) (ParamsCons (Decl _ _ _ x _ _) ps) k =
  subst-args-params Γ ys ps $ subst Γ t x k
subst-args-params Γ ys ps k = k
-}

module reindexing (Γ : ctxt) (isₒ : indices) where

  reindex-fresh-var : renamectxt → trie indices → var → var
  reindex-fresh-var ρₓ is ignored-var = ignored-var
  reindex-fresh-var ρₓ is x =
    fresh-var x (λ x' → ctxt-binds-var Γ x' || trie-contains is x') ρₓ

  rename-indices : renamectxt → trie indices → indices
  rename-indices ρₓ is = foldr {B = renamectxt → indices}
    (λ {(Index x atk) f ρₓ →
       let x' = reindex-fresh-var ρₓ is x in
       Index x' (substh-tk {TERM} Γ ρₓ empty-trie atk) :: f (renamectxt-insert ρₓ x x')})
    (λ ρₓ → []) isₒ ρₓ

  reindex-subst : ∀ {ed} → ⟦ ed ⟧ → ⟦ ed ⟧
  reindex-subst {ed} = substs {ed} {TERM} Γ empty-trie

  reindex-t : Set → Set
  reindex-t X = renamectxt → trie indices → X → X

  {-# TERMINATING #-}
  reindex : ∀ {ed} → reindex-t ⟦ ed ⟧
  reindex-term : reindex-t term
  reindex-type : reindex-t type
  reindex-kind : reindex-t kind
  reindex-tk : reindex-t tk
  reindex-liftingType : reindex-t liftingType
  reindex-optTerm : reindex-t optTerm
  reindex-optType : reindex-t optType
  reindex-optGuide : reindex-t optGuide
  reindex-optClass : reindex-t optClass
  reindex-lterms : reindex-t lterms
  reindex-args : reindex-t args
  reindex-arg : reindex-t arg
  reindex-theta : reindex-t theta
  reindex-vars : reindex-t (maybe vars)
  reindex-defTermOrType : renamectxt → trie indices → defTermOrType → defTermOrType × renamectxt

  reindex{TERM} = reindex-term
  reindex{TYPE} = reindex-type
  reindex{KIND} = reindex-kind
  reindex{TK}   = reindex-tk
  reindex       = λ ρₓ is x → x

  rc-is : renamectxt → indices → renamectxt
  rc-is = foldr λ {(Index x atk) ρₓ → renamectxt-insert ρₓ x x}

  index-var = "indices"
  index-type-var = "Indices"
  is-index-var = isJust ∘ is-pfx index-var
  is-index-type-var = isJust ∘ is-pfx index-type-var

  reindex-term ρₓ is (App t me (Var pi x)) with trie-lookup is x
  ...| nothing = App (reindex-term ρₓ is t) me (reindex-term ρₓ is (Var pi x))
  ...| just is' = indices-to-apps is' $ reindex-term ρₓ is t
  reindex-term ρₓ is (App t me t') =
    App (reindex-term ρₓ is t) me (reindex-term ρₓ is t')
  reindex-term ρₓ is (AppTp t T) =
    AppTp (reindex-term ρₓ is t) (reindex-type ρₓ is T)
  reindex-term ρₓ is (Beta pi ot ot') =
    Beta pi (reindex-optTerm ρₓ is ot) (reindex-optTerm ρₓ is ot')
  reindex-term ρₓ is (Chi pi oT t) =
    Chi pi (reindex-optType ρₓ is oT) (reindex-term ρₓ is t)
  reindex-term ρₓ is (Delta pi oT t) =
    Delta pi (reindex-optType ρₓ is oT) (reindex-term ρₓ is t)
  reindex-term ρₓ is (Epsilon pi lr m t) =
    Epsilon pi lr m (reindex-term ρₓ is t)
  reindex-term ρₓ is (Hole pi) =
    Hole pi
  reindex-term ρₓ is (IotaPair pi t t' g pi') =
    IotaPair pi (reindex-term ρₓ is t) (reindex-term ρₓ is t') (reindex-optGuide ρₓ is g) pi'
  reindex-term ρₓ is (IotaProj t n pi) =
    IotaProj (reindex-term ρₓ is t) n pi
  reindex-term ρₓ is (Lam pi me pi' x oc t) with is-index-var x
  ...| ff = let x' = reindex-fresh-var ρₓ is x in
    Lam pi me pi' x' (reindex-optClass ρₓ is oc) (reindex-term (renamectxt-insert ρₓ x x') is t)
  ...| tt with rename-indices ρₓ is | oc
  ...| isₙ | NoClass = indices-to-lams' isₙ $ reindex-term (rc-is ρₓ isₙ) (trie-insert is x isₙ) t
  ...| isₙ | SomeClass atk = indices-to-lams isₙ $ reindex-term (rc-is ρₓ isₙ) (trie-insert is x isₙ) t
  reindex-term ρₓ is (Let pi fe d t) =
    elim-pair (reindex-defTermOrType ρₓ is d) λ d' ρₓ' → Let pi fe d' (reindex-term ρₓ' is t)
  reindex-term ρₓ is (Open pi o pi' x t) =
    Open pi o pi' x (reindex-term ρₓ is t)
  reindex-term ρₓ is (Parens pi t pi') =
    reindex-term ρₓ is t
  reindex-term ρₓ is (Phi pi t₌ t₁ t₂ pi') =
    Phi pi (reindex-term ρₓ is t₌) (reindex-term ρₓ is t₁) (reindex-term ρₓ is t₂) pi'
  reindex-term ρₓ is (Rho pi op on t og t') =
    Rho pi op on (reindex-term ρₓ is t) (reindex-optGuide ρₓ is og) (reindex-term ρₓ is t')
  reindex-term ρₓ is (Sigma pi t) =
    Sigma pi (reindex-term ρₓ is t)
  reindex-term ρₓ is (Theta pi θ t ts) =
    Theta pi (reindex-theta ρₓ is θ) (reindex-term ρₓ is t) (reindex-lterms ρₓ is ts)
  reindex-term ρₓ is (Var pi x) =
    Var pi $ renamectxt-rep ρₓ x
  reindex-term ρₓ is (Mu pi pi' x t oT pi'' cs pi''') = Var pi-gen "template-mu-not-allowed"
  reindex-term ρₓ is (Mu' pi ot t oT pi' cs pi'') = Var pi-gen "template-mu-not-allowed"

  reindex-type ρₓ is (Abs pi me pi' x atk T) with is-index-var x
  ...| ff = let x' = reindex-fresh-var ρₓ is x in
    Abs pi me pi' x' (reindex-tk ρₓ is atk) (reindex-type (renamectxt-insert ρₓ x x') is T)
  ...| tt = let isₙ = rename-indices ρₓ is in
    indices-to-alls isₙ $ reindex-type (rc-is ρₓ isₙ) (trie-insert is x isₙ) T
  reindex-type ρₓ is (Iota pi pi' x T T') =
    let x' = reindex-fresh-var ρₓ is x in
    Iota pi pi' x' (reindex-type ρₓ is T) (reindex-type (renamectxt-insert ρₓ x x') is T')
  reindex-type ρₓ is (Lft pi pi' x t lT) =
    let x' = reindex-fresh-var ρₓ is x in
    Lft pi pi' x' (reindex-term (renamectxt-insert ρₓ x x') is t) (reindex-liftingType ρₓ is lT)
  reindex-type ρₓ is (NoSpans T pi) =
    NoSpans (reindex-type ρₓ is T) pi
  reindex-type ρₓ is (TpLet pi d T) =
    elim-pair (reindex-defTermOrType ρₓ is d) λ d' ρₓ' → TpLet pi d' (reindex-type ρₓ' is T)
  reindex-type ρₓ is (TpApp T T') =
    TpApp (reindex-type ρₓ is T) (reindex-type ρₓ is T')
  reindex-type ρₓ is (TpAppt T (Var pi x)) with trie-lookup is x
  ...| nothing = TpAppt (reindex-type ρₓ is T) (reindex-term ρₓ is (Var pi x))
  ...| just is' = indices-to-tpapps is' $ reindex-type ρₓ is T
  reindex-type ρₓ is (TpAppt T t) =
    TpAppt (reindex-type ρₓ is T) (reindex-term ρₓ is t)
  reindex-type ρₓ is (TpArrow (TpVar pi x) Erased T) with is-index-type-var x
  ...| ff = TpArrow (reindex-type ρₓ is (TpVar pi x)) Erased (reindex-type ρₓ is T)
  ...| tt = let isₙ = rename-indices ρₓ is in
    indices-to-alls isₙ $ reindex-type (rc-is ρₓ isₙ) is T
  reindex-type ρₓ is (TpArrow T me T') =
    TpArrow (reindex-type ρₓ is T) me (reindex-type ρₓ is T')
  reindex-type ρₓ is (TpEq pi t t' pi') =
    TpEq pi (reindex-term ρₓ is t) (reindex-term ρₓ is t') pi'
  reindex-type ρₓ is (TpHole pi) =
    TpHole pi
  reindex-type ρₓ is (TpLambda pi pi' x atk T) with is-index-var x
  ...| ff = let x' = reindex-fresh-var ρₓ is x in
    TpLambda pi pi' x' (reindex-tk ρₓ is atk) (reindex-type (renamectxt-insert ρₓ x x') is T)
  ...| tt = let isₙ = rename-indices ρₓ is in
    indices-to-tplams isₙ $ reindex-type (rc-is ρₓ isₙ) (trie-insert is x isₙ) T
  reindex-type ρₓ is (TpParens pi T pi') =
    reindex-type ρₓ is T
  reindex-type ρₓ is (TpVar pi x) =
    TpVar pi $ renamectxt-rep ρₓ x

  reindex-kind ρₓ is (KndParens pi k pi') =
    reindex-kind ρₓ is k
  reindex-kind ρₓ is (KndArrow k k') =
    KndArrow (reindex-kind ρₓ is k) (reindex-kind ρₓ is k')
  reindex-kind ρₓ is (KndPi pi pi' x atk k) with is-index-var x
  ...| ff = let x' = reindex-fresh-var ρₓ is x in
    KndPi pi pi' x' (reindex-tk ρₓ is atk) (reindex-kind (renamectxt-insert ρₓ x x') is k)
  ...| tt = let isₙ = rename-indices ρₓ is in
    indices-to-kind isₙ $ reindex-kind (rc-is ρₓ isₙ) (trie-insert is x isₙ) k
  reindex-kind ρₓ is (KndTpArrow (TpVar pi x) k) with is-index-type-var x
  ...| ff = KndTpArrow (reindex-type ρₓ is (TpVar pi x)) (reindex-kind ρₓ is k)
  ...| tt = let isₙ = rename-indices ρₓ is in
    indices-to-kind isₙ $ reindex-kind (rc-is ρₓ isₙ) is k
  reindex-kind ρₓ is (KndTpArrow T k) =
    KndTpArrow (reindex-type ρₓ is T) (reindex-kind ρₓ is k)
  reindex-kind ρₓ is (KndVar pi x as) =
    KndVar pi (renamectxt-rep ρₓ x) (reindex-args ρₓ is as)
  reindex-kind ρₓ is (Star pi) =
    Star pi

  reindex-tk ρₓ is (Tkt T) = Tkt $ reindex-type ρₓ is T
  reindex-tk ρₓ is (Tkk k) = Tkk $ reindex-kind ρₓ is k

  -- Can't reindex large indices in a lifting type (LiftPi requires a type, not a tk),
  -- so for now we will just ignore reindexing lifting types.
  -- Types withing lifting types will still be reindexed, though.
  reindex-liftingType ρₓ is (LiftArrow lT lT') =
    LiftArrow (reindex-liftingType ρₓ is lT) (reindex-liftingType ρₓ is lT')
  reindex-liftingType ρₓ is (LiftParens pi lT pi') =
    reindex-liftingType ρₓ is lT
  reindex-liftingType ρₓ is (LiftPi pi x T lT) =
    let x' = reindex-fresh-var ρₓ is x in
    LiftPi pi x' (reindex-type ρₓ is T) (reindex-liftingType (renamectxt-insert ρₓ x x') is lT)
  reindex-liftingType ρₓ is (LiftStar pi) =
    LiftStar pi
  reindex-liftingType ρₓ is (LiftTpArrow T lT) =
    LiftTpArrow (reindex-type ρₓ is T) (reindex-liftingType ρₓ is lT)

  reindex-optTerm ρₓ is NoTerm = NoTerm
  reindex-optTerm ρₓ is (SomeTerm t pi) = SomeTerm (reindex-term ρₓ is t) pi

  reindex-optType ρₓ is NoType = NoType
  reindex-optType ρₓ is (SomeType T) = SomeType (reindex-type ρₓ is T)

  reindex-optClass ρₓ is NoClass = NoClass
  reindex-optClass ρₓ is (SomeClass atk) = SomeClass (reindex-tk ρₓ is atk)

  reindex-optGuide ρₓ is NoGuide = NoGuide
  reindex-optGuide ρₓ is (Guide pi x T) =
    let x' = reindex-fresh-var ρₓ is x in
    Guide pi x' (reindex-type (renamectxt-insert ρₓ x x') is T)

  reindex-lterms ρₓ is = map λ where
    (Lterm me t) → Lterm me (reindex-term ρₓ is t)

  reindex-theta ρₓ is (AbstractVars xs) = maybe-else Abstract AbstractVars $ reindex-vars ρₓ is $ just xs
  reindex-theta ρₓ is θ = θ

  reindex-vars''' : vars → vars → vars
  reindex-vars''' (VarsNext x xs) xs' = VarsNext x $ reindex-vars''' xs xs'
  reindex-vars''' (VarsStart x) xs = VarsNext x xs
  reindex-vars'' : vars → maybe vars
  reindex-vars'' (VarsNext x (VarsStart x')) = just $ VarsStart x
  reindex-vars'' (VarsNext x xs) = maybe-map (VarsNext x) $ reindex-vars'' xs
  reindex-vars'' (VarsStart x) = nothing
  reindex-vars' : renamectxt → trie indices → var → maybe vars
  reindex-vars' ρₓ is x = maybe-else (just $ VarsStart $ renamectxt-rep ρₓ x)
    (reindex-vars'' ∘ flip foldr (VarsStart "") λ {(Index x atk) → VarsNext x}) (trie-lookup is x)
  reindex-vars ρₓ is (just (VarsStart x)) = reindex-vars' ρₓ is x
  reindex-vars ρₓ is (just (VarsNext x xs)) = maybe-else (reindex-vars ρₓ is $ just xs)
    (λ xs' → maybe-map (reindex-vars''' xs') $ reindex-vars ρₓ is $ just xs) $ reindex-vars' ρₓ is x
  reindex-vars ρₓ is nothing = nothing

  reindex-arg ρₓ is (TermArg me t) = TermArg me (reindex-term ρₓ is t)
  reindex-arg ρₓ is (TypeArg T) = TypeArg (reindex-type ρₓ is T)
  reindex-args ρₓ is = map(reindex-arg ρₓ is)

  reindex-defTermOrType ρₓ is (DefTerm pi x oT t) =
    let x' = reindex-fresh-var ρₓ is x
        oT' = optType-map oT reindex-subst in
    DefTerm elab-hide-key x' (reindex-optType ρₓ is oT') (reindex-term ρₓ is $ reindex-subst t) , renamectxt-insert ρₓ x x'
  reindex-defTermOrType ρₓ is (DefType pi x k T) =
    let x' = reindex-fresh-var ρₓ is x in
    DefType elab-hide-key x' (reindex-kind ρₓ is $ reindex-subst k) (reindex-type ρₓ is $ reindex-subst T) , renamectxt-insert ρₓ x x'

  reindex-cmds : renamectxt → trie indices → cmds → cmds × renamectxt
  reindex-cmds ρₓ is [] = [] , ρₓ
  reindex-cmds ρₓ is ((ImportCmd i) :: cs) =
    elim-pair (reindex-cmds ρₓ is cs) $ _,_ ∘ _::_ (ImportCmd i)
  reindex-cmds ρₓ is ((DefTermOrType op d pi) :: cs) =
    elim-pair (reindex-defTermOrType ρₓ is d) λ d' ρₓ' →
    elim-pair (reindex-cmds ρₓ' is cs) $ _,_ ∘ _::_ (DefTermOrType op d' pi)
  reindex-cmds ρₓ is ((DefKind pi x ps k pi') :: cs) =
    let x' = reindex-fresh-var ρₓ is x in
    elim-pair (reindex-cmds (renamectxt-insert ρₓ x x') is cs) $ _,_ ∘ _::_
      (DefKind pi x' ps (reindex-kind ρₓ is $ reindex-subst k) pi')
  reindex-cmds ρₓ is ((DefDatatype dt pi) :: cs) =
    reindex-cmds ρₓ is cs -- Templates can't use datatypes!

reindex-file : ctxt → indices → start → cmds × renamectxt
reindex-file Γ is (File csᵢ pi' pi'' x ps cs pi''') =
  reindex-cmds empty-renamectxt empty-trie cs
  where open reindexing Γ is

parameterize-file : ctxt → params → cmds → cmds
parameterize-file Γ ps cs = foldr {B = qualif → cmds}
  (λ c cs σ → elim-pair (h c σ) λ c σ → c :: cs σ) (λ _ → []) cs empty-trie
  where
  ps' = ps -- substs-params {ARG} Γ empty-trie ps
  σ+ = λ σ x → qualif-insert-params σ x x ps'

  subst-ps : ∀ {ed} → qualif → ⟦ ed ⟧ → ⟦ ed ⟧
  subst-ps = substs $ add-params-to-ctxt ps' Γ

  h' : defTermOrType → qualif → defTermOrType × qualif
  h' (DefTerm pi x T? t) σ =
    let T?' = case T? of λ where
                (SomeType T) → SomeType $ abs-expand-type ps' $ subst-ps σ T
                NoType → NoType
        t' = params-to-lams ps' $ subst-ps σ t in
    DefTerm pi x T?' t' , σ+ σ x
  h' (DefType pi x k T) σ =
    let k' = abs-expand-kind ps' $ subst-ps σ k
        T' = params-to-tplams ps' $ subst-ps σ T in
    DefType pi x k' T' , σ+ σ x

  h : cmd → qualif → cmd × qualif
  h (ImportCmd i) σ = ImportCmd i , σ
  h (DefTermOrType op d pi) σ = elim-pair (h' d σ) λ d σ → DefTermOrType op d pi , σ
  h (DefKind pi x ps'' k pi') σ = DefKind pi x ps'' k pi' , σ
  h (DefDatatype dt pi) σ = DefDatatype dt pi , σ

open import cedille-syntax

mk-ctr-term : maybeErased → (x X : var) → ctrs → params → term
mk-ctr-term me x X cs ps =
  let t = Mlam X $ ctrs-to-lams' cs $ params-to-apps ps $ mvar x in
  case me of λ where
    Erased → Beta pi-gen NoTerm $ SomeTerm t pi-gen
    NotErased → IotaPair pi-gen (Beta pi-gen NoTerm $ SomeTerm t pi-gen)
                  t NoGuide pi-gen

mk-ctr-type : maybeErased → ctxt → ctr → ctrs → var → type
mk-ctr-type me Γ (Ctr _ x T) cs Tₕ with decompose-ctr-type (ctxt-var-decl Tₕ Γ) T
...| Tₓ , ps , is =
  params-to-alls ps $
  TpAppt (recompose-tpapps is $ mtpvar Tₕ) $
  rename "X" from add-params-to-ctxt ps (ctxt-var-decl Tₕ Γ) for λ X →
  mk-ctr-term me x X cs ps

mk-ctr-fmap-t : Set → Set
mk-ctr-fmap-t X = ctxt → (var × var × var × var × term) → X
{-# TERMINATING #-}
mk-ctr-fmap-η+ : mk-ctr-fmap-t (term → type → term)
mk-ctr-fmap-η- : mk-ctr-fmap-t (term → type → term)
mk-ctr-fmap-η? : mk-ctr-fmap-t (term → type → term) → mk-ctr-fmap-t (term → type → term)
mk-ctr-fmapₖ-η+ : mk-ctr-fmap-t (type → kind → type)
mk-ctr-fmapₖ-η- : mk-ctr-fmap-t (type → kind → type)
mk-ctr-fmapₖ-η? : mk-ctr-fmap-t (type → kind → type) → mk-ctr-fmap-t (type → kind → type)

mk-ctr-fmap-η? f Γ x x' T with is-free-in tt (fst x) T
...| tt = f Γ x x' T
...| ff = x'

mk-ctr-fmapₖ-η? f Γ x x' k with is-free-in tt (fst x) k
...| tt = f Γ x x' k
...| ff = x'

mk-ctr-fmap-η+ Γ x x' T with decompose-ctr-type Γ T
...| Tₕ , ps , _ =
  params-to-lams' ps $
  let Γ' = add-params-to-ctxt ps Γ in
  foldl
    (λ {(Decl _ _ me x'' (Tkt T) _) t → App t me $ mk-ctr-fmap-η? mk-ctr-fmap-η- Γ' x (mvar x'') T;
        (Decl _ _ _ x'' (Tkk k) _) t → AppTp t $ mk-ctr-fmapₖ-η? mk-ctr-fmapₖ-η- Γ' x (mtpvar x'') k})
    x' ps

mk-ctr-fmapₖ-η+ Γ xₒ @ (x , Aₓ , Bₓ , cₓ , castₓ) x' k =
  let is = kind-to-indices Γ (subst Γ (mtpvar Aₓ) x k) in
  indices-to-tplams is $
  let Γ' = add-indices-to-ctxt is Γ in
  foldl
    (λ {(Index x'' (Tkt T)) → flip TpAppt $ mk-ctr-fmap-η?  mk-ctr-fmap-η-  Γ' xₒ (mvar x'') T;
        (Index x'' (Tkk k)) → flip TpApp  $ mk-ctr-fmapₖ-η? mk-ctr-fmapₖ-η- Γ' xₒ (mtpvar x'') k})
    x' $ map (λ {(Index x'' atk) → Index x'' $ subst Γ' (mtpvar x) Aₓ atk}) is

mk-ctr-fmap-η- Γ xₒ @ (x , Aₓ , Bₓ , cₓ , castₓ) x' T with decompose-ctr-type Γ T
...| TpVar _ x'' , ps , as =
  params-to-lams' ps $
  let Γ' = add-params-to-ctxt ps Γ in
    (if ~ x'' =string x then id else mapp
      (recompose-apps (ttys-to-args Erased as) $
        mappe (AppTp (AppTp castₓ (mtpvar Aₓ)) (mtpvar Bₓ)) (mvar cₓ)))
    (foldl (λ {(Decl _ _ me x'' (Tkt T) _) t →
                 App t me $ mk-ctr-fmap-η? mk-ctr-fmap-η+ Γ' xₒ (mvar x'') T;
               (Decl _ _ me x'' (Tkk k) _) t →
                 AppTp t $ mk-ctr-fmapₖ-η? mk-ctr-fmapₖ-η+ Γ' xₒ (mtpvar x'') k}) x' ps)
...| Iota _ _ x'' T₁ T₂ , ps , [] =
  let Γ' = add-params-to-ctxt ps Γ
      tₒ = foldl (λ {
            (Decl _ _ me x'' (Tkt T) _) t →
              App t me $ mk-ctr-fmap-η? mk-ctr-fmap-η+ Γ' xₒ (mvar x'') T;
            (Decl _ _ me x'' (Tkk k) _) t →
              AppTp t $ mk-ctr-fmapₖ-η? mk-ctr-fmapₖ-η+ Γ' xₒ (mtpvar x'') k
          }) x' ps
      t₁ = mk-ctr-fmap-η? mk-ctr-fmap-η- Γ' xₒ (IotaProj tₒ "1" pi-gen) T₁
      t₂ = mk-ctr-fmap-η? mk-ctr-fmap-η- Γ' xₒ (IotaProj tₒ "2" pi-gen)
             (subst Γ (mk-ctr-fmap-η? mk-ctr-fmap-η- Γ' xₒ (mvar x'') T₁) x'' T₂) in
  params-to-lams' ps $ IotaPair pi-gen t₁ t₂ NoGuide pi-gen
...| Tₕ , ps , as = x'

mk-ctr-fmapₖ-η- Γ xₒ @ (x , Aₓ , Bₓ , cₓ , castₓ) x' k with kind-to-indices Γ (subst Γ (mtpvar Bₓ) x k)
...| is =
  indices-to-tplams is $
  let Γ' = add-indices-to-ctxt is Γ in
  foldl (λ {(Index x'' (Tkt T)) → flip TpAppt $ mk-ctr-fmap-η? mk-ctr-fmap-η+ Γ' xₒ (mvar x'') T;
            (Index x'' (Tkk k)) → flip TpApp $ mk-ctr-fmapₖ-η? mk-ctr-fmapₖ-η+ Γ' xₒ (mtpvar x'') k})
    x' $ map (λ {(Index x'' atk) → Index x'' $ subst Γ' (mtpvar x) Bₓ atk}) is

record encoded-datatype-names : Set where
  constructor mk-encoded-datatype-names
  field
    data-functor : var
    data-fmap : var
    data-Mu : var
    data-mu : var
    data-cast : var
    data-functor-ind : var
    cast : var
    fixpoint-type : var
    fixpoint-in : var
    fixpoint-out : var
    fixpoint-ind : var
    fixpoint-lambek : var

elab-mu-t : Set
elab-mu-t = ctxt → ctxt-datatype-info → encoded-datatype-names → var → var ⊎ maybe (term × var × 𝕃 tty) → term → type → cases → maybe (term × ctxt)

record encoded-datatype : Set where
  constructor mk-encoded-datatype
  field
    --data-def : datatype
    --mod-ps : params
    names : encoded-datatype-names
    elab-mu : elab-mu-t
    elab-mu-pure : ctxt → ctxt-datatype-info → maybe var → term → cases → maybe term

  check-mu : ctxt → ctxt-datatype-info → var → var ⊎ maybe (term × var × 𝕃 tty) → term → optType → cases → type → maybe (term × ctxt)
  check-mu Γ d Xₒ x? t oT ms T with d --data-def
  check-mu Γ d Xₒ x? t oT ms T | mk-data-info X mu asₚ asᵢ ps kᵢ k cs fcs -- Data X ps is cs
    with kind-to-indices Γ kᵢ | oT
  check-mu Γ d Xₒ x? t oT ms T | mk-data-info X mu asₚ asᵢ ps kᵢ k cs fcs | is | NoType =
    elab-mu Γ {-(Data X ps is cs)-} d names Xₒ x? t
      (indices-to-tplams is $ TpLambda pi-gen pi-gen ignored-var
        (Tkt $ indices-to-tpapps is $ flip apps-type asₚ $ mtpvar X) T) ms
  check-mu Γ d Xₒ x? t oT ms T | mk-data-info X mu asₚ asᵢ ps kᵢ k cs fcs | is | SomeType Tₘ =
    elab-mu Γ d names Xₒ x? t Tₘ ms

  synth-mu : ctxt → ctxt-datatype-info → var → var ⊎ maybe (term × var × 𝕃 tty) → term → optType → cases → maybe (term × ctxt)
  synth-mu Γ d Xₒ x? t NoType ms = nothing
  synth-mu Γ d Xₒ x? t (SomeType Tₘ) ms = elab-mu Γ d names Xₒ x? t Tₘ ms

record datatype-encoding : Set where
  constructor mk-datatype-encoding
  field
    template : start
    functor : var
    cast : var
    fixpoint-type : var
    fixpoint-in : var
    fixpoint-out : var
    fixpoint-ind : var
    fixpoint-lambek : var
    elab-mu : elab-mu-t
    elab-mu-pure : ctxt → ctxt-datatype-info → encoded-datatype-names → maybe var → term → cases → maybe term

  {-# TERMINATING #-}
  mk-defs : ctxt → datatype → cmds × cmds × encoded-datatype
  mk-defs Γ'' (Data x ps is cs) =
    tcs ,
    (csn OpacTrans functor-cmd $
     csn OpacTrans functor-ind-cmd $
     csn OpacTrans fmap-cmd $
     csn OpacOpaque type-cmd $
     csn OpacOpaque Mu-cmd $
     csn OpacTrans mu-cmd $
     csn OpacTrans cast-cmd $
     foldr (csn OpacTrans ∘ ctr-cmd) [] cs) ,
    record {
      elab-mu = elab-mu;
      elab-mu-pure = λ Γ d → elab-mu-pure Γ d namesₓ;
      --data-def = Data x ps is cs;
      --mod-ps = ctxt-get-current-params Γ;
      names = namesₓ}
    where
    csn : opacity → defTermOrType → cmds → cmds
    csn o d = DefTermOrType o d pi-gen ::_

    k = indices-to-kind is $ Star pi-gen

    Γ' = add-params-to-ctxt ps $ add-ctrs-to-ctxt cs $ ctxt-var-decl x Γ''

    tcs-ρ = reindex-file Γ' is template
    tcs = parameterize-file Γ' (params-set-erased Erased $ {-ctxt-get-current-params Γ'' ++-} ps) $ fst tcs-ρ
    ρₓ = snd tcs-ρ

    data-functorₓ = fresh-var (x ^ "F") (ctxt-binds-var Γ') ρₓ
    data-fmapₓ = fresh-var (x ^ "Fmap") (ctxt-binds-var Γ') ρₓ
    --data-fresh-check = λ f → fresh-var x (λ x → ctxt-binds-var Γ' (f x) || renamectxt-in-field ρₓ (rename-validify $ f x) || renamectxt-in-field ρₓ (f x) || renamectxt-in-field ρₓ (rename-validify $ f x)) ρₓ
    data-Muₓₒ = x -- data-fresh-check data-Is/
    data-muₓₒ = x -- data-fresh-check data-is/
    data-castₓₒ = x -- data-fresh-check data-to/
    data-Muₓ = data-Is/ data-Muₓₒ
    data-muₓ = data-is/ data-muₓₒ
    data-castₓ = data-to/ data-castₓₒ
    data-Muₓᵣ = rename-validify data-Muₓ
    data-muₓᵣ = rename-validify data-muₓ
    data-castₓᵣ = rename-validify data-castₓ
    data-functor-indₓ = fresh-var (x ^ "IndF") (ctxt-binds-var Γ') ρₓ
    functorₓ = renamectxt-rep ρₓ functor
    castₓ = renamectxt-rep ρₓ cast
    fixpoint-typeₓ = renamectxt-rep ρₓ fixpoint-type
    fixpoint-inₓ = renamectxt-rep ρₓ fixpoint-in
    fixpoint-outₓ = renamectxt-rep ρₓ fixpoint-out
    fixpoint-indₓ = renamectxt-rep ρₓ fixpoint-ind
    fixpoint-lambekₓ = renamectxt-rep ρₓ fixpoint-lambek
    Γ = foldr ctxt-var-decl (add-indices-to-ctxt is Γ') (data-functorₓ :: data-fmapₓ :: data-Muₓ :: data-muₓ :: data-castₓ :: data-Muₓᵣ :: data-muₓᵣ :: data-functor-indₓ :: [])
    --Γ = add-indices-to-ctxt is $ ctxt-var-decl data-functorₓ $ ctxt-var-decl data-fmapₓ $ ctxt-var-decl data-Muₓ $ ctxt-var-decl data-muₓ $ ctxt-var-decl data-castₓ $ ctxt-var-decl data-functor-indₓ Γ'
    namesₓ = record {
      data-functor = data-functorₓ;
      data-fmap = data-fmapₓ;
      data-Mu = data-Muₓᵣ;
      data-mu = data-muₓᵣ;
      data-cast = data-castₓᵣ;
      data-functor-ind = data-functor-indₓ;
      cast = castₓ;
      fixpoint-type = fixpoint-typeₓ;
      fixpoint-in = fixpoint-inₓ;
      fixpoint-out = fixpoint-outₓ;
      fixpoint-ind = fixpoint-indₓ;
      fixpoint-lambek = fixpoint-lambekₓ}

    new-var : ∀ {ℓ} {X : Set ℓ} → var → (var → X) → X
    new-var x f = f $ fresh-var x (ctxt-binds-var Γ) ρₓ

    functor-cmd = DefType pi-gen data-functorₓ (params-to-kind ps $ KndArrow k k) $
      params-to-tplams ps $
      TpLambda pi-gen pi-gen x (Tkk $ k) $
      indices-to-tplams is $
      new-var "x" λ xₓ → new-var "X" λ Xₓ →
      Iota pi-gen pi-gen xₓ (mtpeq id-term id-term) $
      Abs pi-gen Erased pi-gen Xₓ
        (Tkk $ indices-to-kind is $ KndTpArrow (mtpeq id-term id-term) star) $
      foldr (λ c → flip TpArrow NotErased $ mk-ctr-type Erased Γ c cs Xₓ)
        (TpAppt (indices-to-tpapps is $ mtpvar Xₓ) (mvar xₓ)) cs

    -- Note: had to set params to erased because args later in mu or mu' could be erased
    functor-ind-cmd = DefTerm pi-gen data-functor-indₓ NoType $
      params-to-lams ps $
      Lam pi-gen Erased pi-gen x (SomeClass $ Tkk k) $
      indices-to-lams is $
      new-var "x" λ xₓ → new-var "y" λ yₓ → new-var "e" λ eₓ → new-var "X" λ Xₓ →
      let T = indices-to-tpapps is $ TpApp (params-to-tpapps ps $ mtpvar data-functorₓ) (mtpvar x) in
      Lam pi-gen NotErased pi-gen xₓ (SomeClass $ Tkt T) $
      Lam pi-gen Erased pi-gen Xₓ
        (SomeClass $ Tkk $ indices-to-kind is $ KndTpArrow T star) $
      flip (foldr λ {c @ (Ctr _ x' _) → Lam pi-gen NotErased pi-gen x' $ SomeClass $
                                        Tkt $ mk-ctr-type NotErased Γ c cs Xₓ}) cs $
      flip mappe (Beta pi-gen NoTerm NoTerm) $
      flip mappe (mvar xₓ) $
      let Γ' = ctxt-var-decl xₓ $ ctxt-var-decl yₓ $ ctxt-var-decl eₓ $ ctxt-var-decl Xₓ Γ in
      flip (foldl λ {(Ctr _ x' T) → flip mapp $
                                  elim-pair (decompose-arrows Γ T) λ ps' Tₕ →
                                  params-to-lams' ps' $
                                  Mlam yₓ $ Mlam eₓ $
                                  params-to-apps ps' $ mvar x'}) cs $
      AppTp (IotaProj (mvar xₓ) "2" pi-gen) $
      indices-to-tplams is $
      TpLambda pi-gen pi-gen xₓ (Tkt $ mtpeq id-term id-term) $
      Abs pi-gen Erased pi-gen yₓ (Tkt T) $
      Abs pi-gen Erased pi-gen eₓ (Tkt $ mtpeq (mvar yₓ) (mvar xₓ)) $
      TpAppt (indices-to-tpapps is $ mtpvar Xₓ) $
      Phi pi-gen (mvar eₓ) (mvar yₓ) (mvar xₓ) pi-gen

    fmap-cmd : defTermOrType
    fmap-cmd with new-var "A" id | new-var "B" id | new-var "c" id
    ...| Aₓ | Bₓ | cₓ = DefTerm pi-gen data-fmapₓ (SomeType $
        params-to-alls ps $
        TpApp (params-to-tpapps ps $ mtpvar functorₓ) $
        params-to-tpapps ps $
        mtpvar data-functorₓ) $
      params-to-lams ps $
      Mlam Aₓ $ Mlam Bₓ $ Mlam cₓ $
      IotaPair pi-gen
        (indices-to-lams is $
         new-var "x" λ xₓ → mlam xₓ $
         IotaPair pi-gen (IotaProj (mvar xₓ) "1" pi-gen)
           (new-var "X" λ Xₓ → Mlam Xₓ $
             ctrs-to-lams' cs $
             foldl
               (flip mapp ∘ eta-expand-ctr)
               (AppTp (IotaProj (mvar xₓ) "2" pi-gen) $ mtpvar Xₓ) cs)
          NoGuide pi-gen)
        (Beta pi-gen NoTerm NoTerm) NoGuide pi-gen
      where
      eta-expand-ctr : ctr → term
      eta-expand-ctr (Ctr _ x' T) =
        mk-ctr-fmap-η+ (ctxt-var-decl Aₓ $ ctxt-var-decl Bₓ $ ctxt-var-decl cₓ Γ)
          (x , Aₓ , Bₓ , cₓ , params-to-apps (params-set-erased Erased ps) (mvar castₓ)) (mvar x') T

    type-cmd = DefType pi-gen x (params-to-kind ps k) $
      params-to-tplams ps $ TpAppt
        (TpApp (params-to-tpapps ps $ mtpvar fixpoint-typeₓ) $
          params-to-tpapps ps $ mtpvar data-functorₓ)
        (params-to-apps ps $ mvar data-fmapₓ)

    mu-proj : var → 𝔹 → type × (term → term)
    mu-proj Xₓ b =
      rename "i" from add-params-to-ctxt ps Γ for λ iₓ →
      let u = if b then id-term else params-to-apps (params-set-erased Erased ps) (mvar fixpoint-outₓ)
          Tₙ = λ T → Iota pi-gen pi-gen iₓ (indices-to-alls is $ TpArrow (indices-to-tpapps is $ mtpvar Xₓ) NotErased $ indices-to-tpapps is T) $ mtpeq (mvar iₓ) u
          T₁ = Tₙ $ params-to-tpapps ps $ mtpvar x
          T₂ = Tₙ $ TpApp (params-to-tpapps ps $ mtpvar data-functorₓ) $ mtpvar Xₓ
          T = if b then T₁ else T₂
          rₓ = if b then "c" else "o"
          t = λ mu → mapp (AppTp mu T) $ mlam "c" $ mlam "o" $ mvar rₓ in
      T , λ mu → Open pi-gen OpacTrans pi-gen data-Muₓ (Phi pi-gen (IotaProj (t mu) "2" pi-gen) (IotaProj (t mu) "1" pi-gen) u pi-gen)

    Mu-cmd = DefType pi-gen data-Muₓ (params-to-kind ps $ KndArrow k star) $
      params-to-tplams ps $
      rename "X" from add-params-to-ctxt ps Γ for λ Xₓ →
      rename "Y" from add-params-to-ctxt ps Γ for λ Yₓ →
      TpLambda pi-gen pi-gen Xₓ (Tkk k) $
      mall Yₓ (Tkk star) $
      flip (flip TpArrow NotErased) (mtpvar Yₓ) $
      TpArrow (fst $ mu-proj Xₓ tt) NotErased $
      TpArrow (fst $ mu-proj Xₓ ff) NotErased $
      mtpvar Yₓ

    mu-cmd = DefTerm pi-gen data-muₓ (SomeType $ params-to-alls (params-set-erased Erased ps) $ TpApp (params-to-tpapps ps $ mtpvar data-Muₓ) $ params-to-tpapps ps $ mtpvar x) $
      params-to-lams (params-set-erased Erased ps) $
      Open pi-gen OpacTrans pi-gen x $
      Open pi-gen OpacTrans pi-gen data-Muₓ $
      rename "Y" from add-params-to-ctxt ps Γ for λ Yₓ →
      rename "f" from add-params-to-ctxt ps Γ for λ fₓ →
      let pair = λ t → IotaPair pi-gen t (Beta pi-gen NoTerm (SomeTerm (erase t) pi-gen)) NoGuide pi-gen in
      Mlam Yₓ $ mlam fₓ $ mapp (mapp (mvar fₓ) $ pair $ indices-to-lams is $ id-term) $ pair $
        mappe (AppTp (params-to-apps (params-set-erased Erased ps) (mvar fixpoint-outₓ)) $ (params-to-tpapps ps $ mtpvar data-functorₓ)) (params-to-apps ps $ mvar data-fmapₓ)

    cast-cmd =
      rename "Y" from add-params-to-ctxt ps Γ for λ Yₓ →
      rename "mu" from add-params-to-ctxt ps Γ for λ muₓ →
      DefTerm pi-gen data-castₓ NoType $
      params-to-lams ps $
      Lam pi-gen Erased pi-gen Yₓ (SomeClass $ Tkk k) $
      Lam pi-gen Erased pi-gen muₓ (SomeClass $ Tkt $
        TpApp (params-to-tpapps ps $ mtpvar data-Muₓ) $ mtpvar Yₓ) $
      snd (mu-proj Yₓ tt) $ mvar muₓ

    ctr-cmd : ctr → defTermOrType
    ctr-cmd (Ctr _ x' T) with subst Γ (params-to-tpapps ps $ mtpvar x) x T
    ...| T' with decompose-ctr-type Γ T'
    ...| Tₕ , ps' , as' = DefTerm pi-gen x' (SomeType $ params-to-alls (ps ++ ps') T') $
      Open pi-gen OpacTrans pi-gen x $
      params-to-lams ps $
      params-to-lams ps' $
      mapp (recompose-apps (ttys-to-args Erased $ drop (length ps) as') $
            mappe (AppTp (params-to-apps (params-set-erased Erased ps) $ mvar fixpoint-inₓ) $
              params-to-tpapps ps $ mtpvar data-functorₓ) $
        params-to-apps ps $ mvar data-fmapₓ) $
      rename "X" from add-params-to-ctxt ps' Γ for λ Xₓ →
      mk-ctr-term NotErased x' Xₓ cs ps'

{- Datatypes -}

ctxt-elab-ctr-def : var → params → type → (ctrs-length ctr-index : ℕ) → ctxt → ctxt
ctxt-elab-ctr-def c ps' t n i Γ@(mk-ctxt mod @ (fn , mn , ps , q) ss is os Δ) = mk-ctxt
  mod ss (trie-insert is ("//" ^ c) (ctr-def [] t n i (unerased-arrows $ abs-expand-type (ps ++ ps') t) , "missing" , "missing")) os Δ

ctxt-elab-ctrs-def : ctxt → params → ctrs → ctxt
ctxt-elab-ctrs-def Γ ps cs = foldr {B = ℕ → ctxt} (λ {(Ctr _ x T) Γ i → ctxt-elab-ctr-def x ps T (length cs) i $ Γ $ suc i}) (λ _ → Γ) cs 0

mendler-elab-mu-pure : ctxt → ctxt-datatype-info → encoded-datatype-names → maybe var → term → cases → maybe term
mendler-elab-mu-pure Γ (mk-data-info X is/X? asₚ asᵢ ps kᵢ k cs fcs) (mk-encoded-datatype-names _ _ _ _ _ _ _ _ fixpoint-inₓ fixpoint-outₓ fixpoint-indₓ fixpoint-lambekₓ) x? t ms =

  let ps-tm = id --λ t → foldr (const $ flip mapp id-term) t $ erase-params ps
      fix-ind = mvar fixpoint-indₓ -- hnf Γ unfold-all (ps-tm $ mvar fixpoint-indₓ) tt
      fix-out = mvar fixpoint-outₓ -- hnf Γ unfold-all (ps-tm $ mvar fixpoint-outₓ) tt
      μ-tm = λ x msf → mapp (mapp fix-ind t) $ mlam x $ rename "x" from ctxt-var-decl x Γ for λ fₓ → mlam fₓ $ msf $ mvar fₓ -- mapp fix-out $ mvar fₓ
      μ'-tm = λ msf → msf $ mapp fix-out t
      set-nth = λ l n a → foldr{B = maybe ℕ → 𝕃 (maybe term)}
        (λ {a' t nothing → a' :: t nothing;
            a' t (just zero) → a :: t nothing;
            a' t (just (suc n)) → a' :: t (just n)})
        (λ _ → []) l (just n) in
  -- Note: removing the implicit arguments below hangs Agda's type-checker!
  foldl{B = 𝕃 (maybe term) → maybe (term → term)}
    (λ c msf l → case_of_{B = maybe (term → term)} c
       λ {(Case _ x cas t) → env-lookup Γ ("//" ^ x) ≫=maybe
         λ {(ctr-def ps? _ n i a , _ , _) →
           msf (set-nth l i (just $ caseArgs-to-lams cas t)); _ → nothing}})
    (-- Note: lambda-expanding this "foldr..." also hangs Agda...?
     foldr (λ t? msf → msf ≫=maybe λ msf → t? ≫=maybe λ t →
              just λ t' → (msf (mapp t' t))) (just λ t → t))
    ms (map (λ _ → nothing) ms) ≫=maybe (just ∘ maybe-else' x? μ'-tm μ-tm)

mendler-elab-mu : elab-mu-t
mendler-elab-mu Γ (mk-data-info X is/X? asₚ asᵢ ps kᵢ k cs fcs)
  (mk-encoded-datatype-names
    data-functorₓ data-fmapₓ data-Muₓ data-muₓ data-castₓ data-functor-indₓ castₓ
    fixpoint-typeₓ fixpoint-inₓ fixpoint-outₓ fixpoint-indₓ fixpoint-lambekₓ)
   Xₒ x? t Tₘ ms =
  let infixl 10 _-is _-ps _`ps _·is _·ps
      _-is = recompose-apps $ ttys-to-args Erased asᵢ
      _`ps = recompose-apps asₚ
      _-ps = recompose-apps $ args-set-erased Erased asₚ
      _·is = recompose-tpapps asᵢ
      _·ps = recompose-tpapps $ args-to-ttys asₚ
      σ = fst (mk-inst ps (asₚ ++ ttys-to-args NotErased asᵢ))
      is = kind-to-indices Γ (substs Γ σ k)
      Γᵢₛ = add-indices-to-ctxt is $ add-params-to-ctxt ps Γ
      is-as : indices → args
      is-as = map λ {(Index x atk) →
        tk-elim atk (λ _ → TermArg Erased $ `vₓ x) (λ _ → TypeArg $ `Vₓ x)}
      is/X? = maybe-map `vₓ_ is/X? maybe-or either-else' x? (λ _ → nothing) (maybe-map fst)
      open? = Open pi-gen OpacTrans pi-gen X
      close? = Open pi-gen OpacOpaque pi-gen X
      ms' = foldr (λ {(Case _ x cas t) σ →
              let Γ' = add-caseArgs-to-ctxt cas Γᵢₛ in
              trie-insert σ x $ caseArgs-to-lams cas $
              rename "y" from Γ' for λ yₓ →
              rename "e" from Γ' for λ eₓ →
              `Λ yₓ ₊ `Λ eₓ ₊ close? (`ρ (`ς `vₓ eₓ) - t)}) empty-trie ms
      fmap = `vₓ data-fmapₓ `ps
      functor = `Vₓ data-functorₓ ·ps
      Xₜₚ = `Vₓ X ·ps
      in-fix = λ is/X? T asᵢ t → either-else' x? (λ x → recompose-apps asᵢ (`vₓ fixpoint-inₓ -ps · functor - fmap) ` (maybe-else' is/X? t λ is/X →
        recompose-apps asᵢ (`vₓ castₓ -ps - (fmap · T · Xₜₚ - (`open data-Muₓ - (is/X ` (`λ "to" ₊ `λ "out" ₊ `vₓ "to"))))) ` t)) (λ e → maybe-else' (is/X? maybe-or maybe-map fst e) t λ is/X → recompose-apps asᵢ (`vₓ castₓ -ps · `Vₓ Xₒ · Xₜₚ - (`open data-Muₓ - (is/X ` (`λ "to" ₊ `λ "out" ₊ `vₓ "to")))) ` t)
      app-lambek = λ is/X? t T asᵢ body → body - (in-fix is/X? T asᵢ t) -
        (recompose-apps asᵢ (`vₓ fixpoint-lambekₓ -ps · functor - fmap) ` (in-fix is/X? T asᵢ t)) in
  rename "x" from Γᵢₛ for λ xₓ →
  rename "y" from Γᵢₛ for λ yₓ →
  rename "y'" from ctxt-var-decl yₓ Γᵢₛ for λ y'ₓ →
  rename "z" from Γᵢₛ for λ zₓ →
  rename "e" from Γᵢₛ for λ eₓ →
  rename "X" from Γᵢₛ for λ Xₓ →
  foldl (λ {(Ctr _ x Tₓ) rec → rec ≫=maybe λ rec → trie-lookup ms' x ≫=maybe λ t →
    just λ tₕ → rec tₕ ` t}) (just λ t → t) cs ≫=maybe λ msf →
  just $ flip (either-else' x?)

    (λ _ → open? (app-lambek is/X? t (`Vₓ Xₒ ·ps) (ttys-to-args Erased asᵢ) (msf
      (let Tₛ = maybe-else' is/X? Xₜₚ λ _ → `Vₓ Xₒ
           fcₜ = maybe-else' is/X? id λ is/X → _`_ $ indices-to-apps is $
             `vₓ castₓ -ps · (functor ·ₜ Tₛ) · (functor ·ₜ Xₜₚ) -
               (fmap · Tₛ · Xₜₚ - (`open data-Muₓ - (is/X ` (`λ "to" ₊ `λ "out" ₊ `vₓ "to"))))
           out = maybe-else' is/X? (`vₓ fixpoint-outₓ -ps · functor - fmap) λ is/X →
             let i = `open data-Muₓ - is/X · (`ι xₓ :ₜ indices-to-alls is (indices-to-tpapps is Tₛ ➔ indices-to-tpapps is (functor ·ₜ Tₛ)) ₊ `[ `vₓ xₓ ≃ `vₓ fixpoint-outₓ ]) ` (`λ "to" ₊ `λ "out" ₊ `vₓ "out") in
             `φ i `₊2 - i `₊1 [ `vₓ fixpoint-outₓ ] in
      (`φ `β - (`vₓ data-functor-indₓ `ps · Tₛ -is ` (out -is ` t)) [ `vₓ fixpoint-outₓ ` erase t ])
        · (indices-to-tplams is $ `λₜ yₓ :ₜ indices-to-tpapps is (functor ·ₜ Tₛ) ₊
           `∀ y'ₓ :ₜ indices-to-tpapps is Xₜₚ ₊ `∀ eₓ :ₜ `[ `vₓ fixpoint-inₓ -ps ` `vₓ yₓ ≃ `vₓ y'ₓ ] ₊
           indices-to-tpapps is Tₘ `ₜ (`φ `vₓ eₓ -
             (indices-to-apps is (`vₓ fixpoint-inₓ -ps · functor - fmap) ` (fcₜ (`vₓ yₓ))) [ `vₓ y'ₓ ]))))) , Γ)

    λ xₒ → rename xₒ from Γᵢₛ for λ x →
    let Rₓₒ = mu-Type/ x
        isRₓₒ = mu-isType/ x in
    rename Rₓₒ from Γᵢₛ for λ Rₓ →
    rename isRₓₒ from Γᵢₛ for λ isRₓ →
    rename "to" from Γᵢₛ for λ toₓ →
    rename "out" from Γᵢₛ for λ outₓ →
    let fcₜ = `vₓ castₓ -ps · (functor ·ₜ `Vₓ Rₓ) · (functor ·ₜ Xₜₚ) - (fmap · `Vₓ Rₓ · Xₜₚ - `vₓ toₓ)
        subst-msf = subst-renamectxt Γᵢₛ (maybe-extract
          (renamectxt-insert* empty-renamectxt (xₒ :: isRₓₒ :: Rₓₒ :: toₓ :: outₓ :: xₓ :: yₓ :: y'ₓ :: []) (x :: isRₓ :: Rₓ :: toₓ :: outₓ :: xₓ :: yₓ :: y'ₓ :: [])) refl) ∘ msf in
    open? (`vₓ fixpoint-indₓ -ps · functor - fmap -is ` t · Tₘ `
      (`Λ Rₓ  ₊ `Λ toₓ ₊ `Λ outₓ ₊ `λ x ₊
       indices-to-lams is (`λ yₓ ₊
       `-[ isRₓ :ₜ `Vₓ data-Muₓ ·ps ·ₜ (`Vₓ Rₓ) `=
           `open data-Muₓ - (`Λ ignored-var ₊ `λ xₓ ₊ `vₓ xₓ ` (`vₓ toₓ) ` (`vₓ outₓ))]-
       (app-lambek (just $ `vₓ isRₓ) (`vₓ yₓ) (`Vₓ Rₓ) (is-as is) $ subst-msf
         ((`φ `β - (indices-to-apps is (`vₓ data-functor-indₓ `ps · (`Vₓ Rₓ)) ` `vₓ yₓ) [ `vₓ yₓ ]) ·
           (indices-to-tplams is $ `λₜ yₓ :ₜ indices-to-tpapps is (functor ·ₜ (`Vₓ Rₓ)) ₊
             `∀ y'ₓ :ₜ indices-to-tpapps is Xₜₚ ₊ `∀ eₓ :ₜ `[ `vₓ fixpoint-inₓ -ps ` `vₓ yₓ ≃ `vₓ y'ₓ ] ₊
             indices-to-tpapps is Tₘ `ₜ (`φ `vₓ eₓ -
               (`vₓ fixpoint-inₓ -ps · functor - fmap ` (indices-to-apps is fcₜ ` (`vₓ yₓ)))
               [ `vₓ y'ₓ ]))))))) , ctxt-datatype-decl' X isRₓ Rₓ asₚ Γ

mendler-encoding : datatype-encoding
mendler-encoding =
  record {
    template = templateMendler;
    functor = "Functor";
    cast = "cast";
    fixpoint-type = "CVFixIndM";
    fixpoint-in = "cvInFixIndM";
    fixpoint-out = "cvOutFixIndM";
    fixpoint-ind = "cvIndFixIndM";
    fixpoint-lambek = "lambek";
    elab-mu = mendler-elab-mu;
    elab-mu-pure = mendler-elab-mu-pure
  }

mendler-simple-encoding : datatype-encoding
mendler-simple-encoding =
  record {
    template = templateMendlerSimple;
    functor = "RecFunctor";
    cast = "cast";
    fixpoint-type = "FixM";
    fixpoint-out = "outFix";
    fixpoint-in = "inFix";
    fixpoint-ind = "IndFixM";
    fixpoint-lambek = "lambek";
    elab-mu = mendler-elab-mu;
    elab-mu-pure = mendler-elab-mu-pure
  }

selected-encoding = case cedille-options.options.datatype-encoding options of λ where
  cedille-options.Mendler → mendler-simple-encoding
  cedille-options.Mendler-old → mendler-encoding

max_stars_repo_name: CarlOlson/cedille

max_issues_repo_name: CarlOlson/cedille

max_forks_repo_name: CarlOlson/cedille


text:
------------------------------------------------------------------------
-- An example: A function that, given a stream, tries to find an
-- element satisfying a predicate
------------------------------------------------------------------------

{-# OPTIONS --cubical --safe #-}

module Search where

open import Equality.Propositional.Cubical
open import Prelude hiding (⊥)

open import Monad equality-with-J
open import Univalence-axiom equality-with-J

open import Partiality-algebra.Monotone
open import Partiality-monad.Inductive
open import Partiality-monad.Inductive.Fixpoints
open import Partiality-monad.Inductive.Monad

-- Streams.

infixr 5 _∷_

record Stream {a} (A : Type a) : Type a where
  coinductive
  constructor _∷_
  field
    head : A
    tail : Stream A

open Stream

-- A direct implementation of the function.

module Direct {a} {A : Type a} (q : A → Bool) where

  Φ : Trans (Stream A) (λ _ → A)
  Φ f xs = if q (head xs) then return (head xs) else f (tail xs)

  Φ-monotone :
    ∀ {f₁ f₂} → (∀ xs → f₁ xs ⊑ f₂ xs) → ∀ xs → Φ f₁ xs ⊑ Φ f₂ xs
  Φ-monotone f₁⊑f₂ xs with q (head xs)
  ... | true  = return (head xs)  ■
  ... | false = f₁⊑f₂ (tail xs)

  Φ-⊑ : Trans-⊑ (Stream A) (λ _ → A)
  Φ-⊑ = record { function = Φ; monotone = Φ-monotone }

  search : Stream A → A ⊥
  search = fix→ Φ-⊑

  search-least :
    ∀ f → (∀ xs → Φ f xs ⊑ f xs) →
    ∀ xs → search xs ⊑ f xs
  search-least = fix→-is-least Φ-⊑

  Φ-ω-continuous :
    (s : ∃ λ (f : ℕ → Stream A → A ⊥) →
           ∀ n xs → f n xs ⊑ f (suc n) xs) →
    Φ (⨆ ∘ at s) ≡ ⨆ ∘ at [ Φ-⊑ $ s ]-inc
  Φ-ω-continuous s = ⟨ext⟩ helper
    where
    helper : ∀ xs → Φ (⨆ ∘ at s) xs ≡ ⨆ (at [ Φ-⊑ $ s ]-inc xs)
    helper xs with q (head xs)
    ... | true  = return (head xs)               ≡⟨ sym ⨆-const ⟩∎
                  ⨆ (constˢ (return (head xs)))  ∎
    ... | false = ⨆ (at s (tail xs))             ∎

  Φ-ω : Trans-ω (Stream A) (λ _ → A)
  Φ-ω = record
    { monotone-function = Φ-⊑
    ; ω-continuous      = Φ-ω-continuous
    }

  search-fixpoint : search ≡ Φ search
  search-fixpoint = fix→-is-fixpoint-combinator Φ-ω

-- An arguably more convenient implementation.

module Indirect {a} {A : Type a} (q : A → Bool) where

  ΦP : Stream A → Partial (Stream A) (λ _ → A) A
  ΦP xs =
    if q (head xs) then
      return (head xs)
    else
      rec (tail xs)

  Φ : Trans (Stream A) (λ _ → A)
  Φ = Trans-⊑.function (transformer ΦP)

  search : Stream A → A ⊥
  search = fixP ΦP

  search-least :
    ∀ f → (∀ xs → Φ f xs ⊑ f xs) →
    ∀ xs → search xs ⊑ f xs
  search-least = fixP-is-least ΦP

  search-fixpoint : search ≡ Φ search
  search-fixpoint = fixP-is-fixpoint-combinator ΦP

max_stars_repo_name: nad/partiality-monad

max_issues_repo_name: nad/partiality-monad

max_forks_repo_name: nad/partiality-monad


text:
{-# OPTIONS --safe --experimental-lossy-unification #-}
module Cubical.ZCohomology.Groups.Coproduct where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.HLevels

open import Cubical.Data.Nat
open import Cubical.Data.Sigma
open import Cubical.Data.Sum as Sum

open import Cubical.Algebra.Group
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.Group.DirProd
open import Cubical.Algebra.Ring
open import Cubical.Algebra.Ring.DirectProd

open import Cubical.HITs.SetTruncation as ST

open import Cubical.ZCohomology.Base
open import Cubical.ZCohomology.GroupStructure

private variable
  ℓ ℓ' : Level

module _
  {X : Type ℓ}
  {Y : Type ℓ'}
  where

  open Iso
  open IsGroupHom
  open GroupStr

  Equiv-Coproduct-CoHom : {n : ℕ} → GroupIso (coHomGr n (X ⊎ Y)) (DirProd (coHomGr n X) (coHomGr n Y))
  Iso.fun (fst Equiv-Coproduct-CoHom)      = ST.rec (isSet× squash₂ squash₂) (λ f → ∣ f ∘ inl ∣₂ , ∣ (f ∘ inr) ∣₂)
  Iso.inv (fst Equiv-Coproduct-CoHom)      = uncurry
                           (ST.rec (λ u v p q i j y → squash₂ (u y) (v y) (λ X → p X y) (λ X → q X y) i j)
                           (λ g → ST.rec squash₂ (λ h → ∣ Sum.rec g h ∣₂)))
  Iso.rightInv (fst Equiv-Coproduct-CoHom) = uncurry
                           (ST.elim (λ x → isProp→isSet λ u v i y → isSet× squash₂ squash₂ _ _ (u y) (v y) i)
                           (λ g → ST.elim (λ _ → isProp→isSet (isSet× squash₂ squash₂ _ _))
                                   (λ h → refl)))
  Iso.leftInv (fst Equiv-Coproduct-CoHom) = ST.elim (λ _ → isProp→isSet (squash₂ _ _))
                          λ f → cong ∣_∣₂ (funExt (Sum.elim (λ x → refl) (λ x → refl)))
  snd Equiv-Coproduct-CoHom =               makeIsGroupHom
                          (ST.elim (λ x → isProp→isSet λ u v i y → isSet× squash₂ squash₂ _ _ (u y) (v y) i)
                          (λ g → ST.elim (λ _ → isProp→isSet (isSet× squash₂ squash₂ _ _))
                          λ h → refl))

max_stars_repo_name: thomas-lamiaux/cubical

max_issues_repo_name: thomas-lamiaux/cubical

max_forks_repo_name: thomas-lamiaux/cubical